feat: add expose_names

Author: leodemoura

src/Init/Grind/Interactive.lean

@@ -172,5 +172,13 @@ macro_rules
 /-- `rename_i x_1 ... x_n` renames the last `n` inaccessible names using the given names. -/
 syntax (name := renameI) "rename_i" (ppSpace colGt binderIdent)+ : grind
 
+/--
+`expose_names` renames all inaccessible variables with accessible names, making them available
+for reference in generated tactics. However, this renaming introduces machine-generated names
+that are not fully under user control. `expose_names` is primarily intended as a preamble for
+generated `grind` tactic scripts.
+-/
+syntax (name := exposeNames) "expose_names" : grind
+
 end Grind
 end Lean.Parser.Tactic

src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean

@@ -20,6 +20,7 @@ import Lean.Meta.Tactic.Grind.Anchor
 import Lean.Meta.Tactic.Grind.Arith.CommRing.PP
 import Lean.Meta.Tactic.Grind.Arith.Linear.PP
 import Lean.Meta.Tactic.Grind.AC.PP
+import Lean.Meta.Tactic.ExposeNames
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.Tactic.RenameInaccessibles
 namespace Lean.Elab.Tactic.Grind
@@ -354,4 +355,10 @@ where
     replaceMainGoal [{ goal with mvarId }]
   | _ => throwUnsupportedSyntax
 
+@[builtin_grind_tactic exposeNames] def evalExposeNames : GrindTactic := fun _ => do
+  let goal ← getMainGoal
+  let mvarId ← goal.mvarId.exposeNames
+  liftGrindM <| resetAnchors
+  replaceMainGoal [{ goal with mvarId }]
+
 end Lean.Elab.Tactic.Grind

tests/lean/run/grind_interactive.lean

@@ -473,4 +473,10 @@ example : (a : Point Nat) → p a → x ≠ y → False := by
     cases #e2a6
     all_goals sorry
 
+example : (a : Point Nat) → p a → x ≠ y → False := by
+  grind =>
+    expose_names
+    cases #6ccb
+    sorry
+
 end Ex1