From b01ca8ee237a1b3c299384e73ad79d424e216a84 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Wed, 5 Feb 2025 21:44:25 -0800
Subject: [PATCH] feat: use `expose_names` in `try?` (#6967)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR ensures `try?` can suggest tactics that need to reference
inaccessible local names.
Example:
```lean
/--
info: Try these:
• · expose_names; induction as, bs_1 using app.induct <;> grind [= app]
• · expose_names; induction as, bs_1 using app.induct <;> grind only [app]
-/
#guard_msgs (info) in
example : app (app as bs) cs = app as (app bs cs) := by
  have bs := 20 -- shadows `bs` in the target
  try?
```
---
 src/Lean/Elab/Tactic/Try.lean  | 13 ++++++++++---
 tests/lean/run/try_trace1.lean | 22 ++++++++++++++++++++++
 2 files changed, 32 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Try.lean b/src/Lean/Elab/Tactic/Try.lean
index c2c0a9f5730b..35a806948cca 100644
--- a/src/Lean/Elab/Tactic/Try.lean
+++ b/src/Lean/Elab/Tactic/Try.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Try
 import Init.Grind.Tactics
+import Lean.Meta.Tactic.ExposeNames
 import Lean.Meta.Tactic.Try
 import Lean.Meta.Tactic.TryThis
 import Lean.Elab.Tactic.Config
@@ -382,15 +383,21 @@ private def allAccessible (majors : Array FVarId) : MetaM Bool :=
 open Try.Collector in
 private def mkFunIndStx (c : FunIndCandidate) (cont : TSyntax `tactic) : MetaM (TSyntax `tactic) := do
   if (← allAccessible c.majors) then
+    go
+  else withNewMCtxDepth do
+    -- Create a helper goal to apply
+    let mvarId := (← mkFreshExprMVar (mkConst ``True)).mvarId!
+    let mvarId ← mvarId.exposeNames
+    mvarId.withContext do
+      `(tactic| (expose_names; $(← go):tactic))
+where
+  go : MetaM (TSyntax `tactic) := do
     let mut terms := #[]
     for major in c.majors do
       let localDecl ← major.getDecl
       terms := terms.push (← `($(mkIdent localDecl.userName):term))
     let indFn ← toIdent c.funIndDeclName
     `(tactic| induction $terms,* using $indFn <;> $cont)
-  else
-    -- TODO: use `expose_names`
-    throwError "`induction` failed, majors contain inaccessible vars"
 
 private def mkAllFunIndStx (info : Try.Info) (cont : TSyntax `tactic) : MetaM (TSyntax `tactic) := do
   let tacs ← info.funIndCandidates.toArray.mapM (mkFunIndStx · cont)
diff --git a/tests/lean/run/try_trace1.lean b/tests/lean/run/try_trace1.lean
index 745345c19c5a..09d84f225327 100644
--- a/tests/lean/run/try_trace1.lean
+++ b/tests/lean/run/try_trace1.lean
@@ -75,3 +75,25 @@ info: Try these:
 #guard_msgs (info) in
 example : app (app as bs) cs = app as (app bs cs) := by
   try?
+
+/--
+info: Try these:
+• · expose_names; induction as, bs_1 using app.induct <;> grind [= app]
+• · expose_names; induction as, bs_1 using app.induct <;> grind only [app]
+-/
+#guard_msgs (info) in
+example : app (app as bs) cs = app as (app bs cs) := by
+  have bs := 20 -- shadow variable in the goal
+  try?
+
+/--
+info: Try these:
+• · expose_names; induction as, bs using app.induct <;> grind [= app]
+• · expose_names; induction as, bs using app.induct <;> grind only [app]
+-/
+#guard_msgs (info) in
+example : app (app as bs) cs = app as (app bs cs) := by
+  revert as bs cs
+  intro _ _ _
+  -- `as`, `bs`, and `cs` now have inaccessible names.
+  try?