From 5eca093a89bc7dcd09e54b0a9c71bb3472d66709 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Fri, 7 Feb 2025 14:43:30 -0800
Subject: [PATCH] feat: `exact?` in `try?` (#6995)

This PR implements support for `exact?` in the `try?` tactic.
---
 src/Lean/Elab/Tactic/Try.lean          | 111 ++++++++++++++++++++-----
 tests/lean/run/grind_eval_suggest.lean |   4 +-
 tests/lean/run/grind_try_exact.lean    |  35 ++++++++
 3 files changed, 125 insertions(+), 25 deletions(-)
 create mode 100644 tests/lean/run/grind_try_exact.lean

diff --git a/src/Lean/Elab/Tactic/Try.lean b/src/Lean/Elab/Tactic/Try.lean
index e1fd1c87fe..abc348fb56 100644
--- a/src/Lean/Elab/Tactic/Try.lean
+++ b/src/Lean/Elab/Tactic/Try.lean
@@ -11,6 +11,7 @@ import Lean.Meta.Tactic.Try
 import Lean.Meta.Tactic.TryThis
 import Lean.Elab.Tactic.Config
 import Lean.Elab.Tactic.SimpTrace
+import Lean.Elab.Tactic.LibrarySearch
 import Lean.Elab.Tactic.Grind
 
 namespace Lean.Elab.Tactic
@@ -28,6 +29,59 @@ namespace Try
 combinatiors such as `first`, `attempt_all`, `<;>`, `;`, and `try`.
 -/
 
+/-- Returns `true` if `fvarId` has an accessible name. -/
+private def isAccessible (fvarId : FVarId) : MetaM Bool := do
+  let localDecl ← fvarId.getDecl
+  if localDecl.userName.hasMacroScopes then
+    return false
+  else
+    -- Check whether variable has been shadowed
+    let some localDecl' := (← getLCtx).findFromUserName? localDecl.userName
+      | return false
+    return localDecl'.fvarId == localDecl.fvarId
+
+/-- Returns `true` if all free variables occurring in `e` are accessible. -/
+private def isExprAccessible (e : Expr) : MetaM Bool := do
+  let (_, s) ← e.collectFVars |>.run {}
+  s.fvarIds.allM isAccessible
+
+/-- Creates a temporary local context where all names are exposed, and executes `k`-/
+private def withExposedNames (k : MetaM α) : MetaM α := do
+  withNewMCtxDepth do
+    -- Create a helper goal to apply
+    let mvarId := (← mkFreshExprMVar (mkConst ``True)).mvarId!
+    let mvarId ← mvarId.exposeNames
+    mvarId.withContext do k
+
+/-- Executes `tac` in the saved state. This function is used to validate a tactic before suggesting it. -/
+def checkTactic (savedState : SavedState) (tac : TSyntax `tactic) : TacticM Unit := do
+  let currState ← saveState
+  savedState.restore
+  try
+    evalTactic tac
+  finally
+    currState.restore
+
+def evalSuggestExact : TacticM (TSyntax `tactic) := do
+  let savedState ← saveState
+  let mvarId :: mvarIds ← getGoals
+    | throwError "no goals"
+  mvarId.withContext do
+    let tactic := fun exfalso => LibrarySearch.solveByElim [] (exfalso := exfalso) (maxDepth := 6)
+    let allowFailure := fun _ => return false
+    let .none ← LibrarySearch.librarySearch mvarId tactic allowFailure
+      | throwError "`exact?` failed"
+    let proof := (← instantiateMVars (mkMVar mvarId)).headBeta
+    let tac ← if (← isExprAccessible proof) then
+      let stx ← PrettyPrinter.delab proof
+      `(tactic| exact $stx)
+    else withExposedNames do
+      let stx ← PrettyPrinter.delab proof
+      `(tactic| (expose_names; exact $stx))
+    checkTactic savedState tac
+    setGoals mvarIds
+    return tac
+
 /-- Returns the suggestions represented by `tac`.  -/
 private def getSuggestionOfTactic (tac : TSyntax `tactic) : Array (TSyntax `tactic) :=
   match tac with
@@ -53,6 +107,29 @@ private def filterSkipDone (tacs : Array (TSyntax `tactic)) : Array (TSyntax `ta
     | `(tactic| done) | `(tactic| skip) => false
     | _ => true
 
+private def getTacSeqElems? (tseq : TSyntax ``Parser.Tactic.tacticSeq) : Option (Array (TSyntax `tactic)) :=
+  match tseq with
+  | `(tacticSeq| { $t;* }) => some t.getElems
+  | `(tacticSeq| $t;*) => some t.getElems
+  | _ => none
+
+private def isCDotTac (tac : TSyntax `tactic) : Bool :=
+  match tac with
+  | `(tactic| · $_:tacticSeq) => true
+  | _ => false
+
+private def appendSeq (tacs : Array (TSyntax `tactic)) (tac : TSyntax `tactic) : Array (TSyntax `tactic) := Id.run do
+  match tac with
+  | `(tactic| ($tseq:tacticSeq)) =>
+    if let some tacs' := getTacSeqElems? tseq then
+      return tacs ++ tacs'
+  | `(tactic| · $tseq:tacticSeq) =>
+    if let some tacs' := getTacSeqElems? tseq then
+      if !tacs'.any isCDotTac then
+        return tacs ++ tacs'
+  | _ => pure ()
+  return tacs.push tac
+
 private def mkSeq (tacs : Array (TSyntax `tactic)) (terminal : Bool) : CoreM (TSyntax `tactic) := do
   let tacs := filterSkipDone tacs
   if tacs.size = 0 then
@@ -354,9 +431,9 @@ private def evalSuggestSeq (tacs : Array (TSyntax `tactic)) : M (TSyntax `tactic
   if (← read).terminal then
     let mut result := #[]
     for i in [:tacs.size - 1] do
-      result := result.push (← withNonTerminal <| evalSuggest tacs[i]!)
+      result := appendSeq result (← withNonTerminal <| evalSuggest tacs[i]!)
     let suggestions ← getSuggestionOfTactic (← evalSuggest tacs.back!) |>.mapM fun tac =>
-      mkSeq (result.push tac) (terminal := true)
+      mkSeq (appendSeq result tac) (terminal := true)
     mkTrySuggestions suggestions
   else
     mkSeq (← tacs.mapM evalSuggest) (terminal := false)
@@ -373,6 +450,8 @@ private def evalSuggestTacticSeq (s : TSyntax ``Parser.Tactic.tacticSeq) : M (TS
 
 /-- `evalSuggest` for `first` tactic. -/
 private partial def evalSuggestFirst (tacs : Array (TSyntax ``Parser.Tactic.tacticSeq)) : M (TSyntax `tactic) := do
+  if tacs.size == 0 then
+    throwError "`first` expects at least one argument"
   go 0
 where
   go (i : Nat) : M (TSyntax `tactic) := do
@@ -414,6 +493,7 @@ where
 -- `evalSuggest` implementation
 @[export lean_eval_suggest_tactic]
 private partial def evalSuggestImpl (tac : TSyntax `tactic) : M (TSyntax `tactic) := do
+  trace[try.debug] "{tac}"
   match tac with
   | `(tactic| $tac1 <;> $tac2) => evalSuggestChain tac1 tac2
   | `(tactic| first $[| $tacs]*) => evalSuggestFirst tacs
@@ -429,6 +509,8 @@ private partial def evalSuggestImpl (tac : TSyntax `tactic) : M (TSyntax `tactic
         evalSuggestGrindTrace tac
       else if k == ``Parser.Tactic.simpTrace then
         evalSuggestSimpTrace tac
+      else if k == ``Parser.Tactic.exact? then
+        evalSuggestExact
       else
         evalSuggestAtomic tac
       if (← read).terminal then
@@ -515,27 +597,12 @@ private def mkSimpleTacStx : CoreM (TSyntax `tactic) :=
 
 /-! Function induction generators -/
 
-private def allAccessible (majors : Array FVarId) : MetaM Bool :=
-  majors.allM fun major => do
-    let localDecl ← major.getDecl
-    if localDecl.userName.hasMacroScopes then
-      return false
-    else
-      -- Check whether variable has been shadowed
-      let some localDecl' := (← getLCtx).findFromUserName? localDecl.userName
-        | return false
-      return localDecl'.fvarId == localDecl.fvarId
-
 open Try.Collector in
 private def mkFunIndStx (c : FunIndCandidate) (cont : TSyntax `tactic) : MetaM (TSyntax `tactic) := do
-  if (← allAccessible c.majors) then
+  if (← c.majors.allM isAccessible) 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))
+  else withExposedNames do
+    `(tactic| (expose_names; $(← go):tactic))
 where
   go : MetaM (TSyntax `tactic) := do
     let mut terms := #[]
@@ -558,11 +625,11 @@ private def mkTryEvalSuggestStx (info : Try.Info) : MetaM (TSyntax `tactic) := d
   let grind ← mkGrindStx info
   let atomic ← `(tactic| attempt_all | $simple:tactic | $simp:tactic | $grind:tactic | simp_all)
   let funInds ← mkAllFunIndStx info atomic
-  `(tactic| first | $atomic:tactic | $funInds:tactic)
+  let extra ← `(tactic| (intros; first | $simple:tactic | $simp:tactic | exact?))
+  `(tactic| first | $atomic:tactic | $funInds:tactic | $extra:tactic)
 
 -- TODO: vanilla `induction`.
 -- TODO: make it extensible.
--- TODO: librarySearch integration.
 -- TODO: premise selection.
 
 @[builtin_tactic Lean.Parser.Tactic.tryTrace] def evalTryTrace : Tactic := fun stx => do
diff --git a/tests/lean/run/grind_eval_suggest.lean b/tests/lean/run/grind_eval_suggest.lean
index 0d0e48ab02..dced961fbc 100644
--- a/tests/lean/run/grind_eval_suggest.lean
+++ b/tests/lean/run/grind_eval_suggest.lean
@@ -83,9 +83,7 @@ example : False := by
 set_option hygiene false in
 macro "simple_tac2" : tactic => `(tactic| eval_suggest (intros; (simp only [Nat.zero_add]; simp only [Nat.one_mul]); simp [*]))
 
-/--
-info: Try this: · intros; (simp only [Nat.zero_add]; simp only [Nat.one_mul]); simp [*]
--/
+/-- info: Try this: · intros; simp only [Nat.zero_add]; simp only [Nat.one_mul]; simp [*] -/
 #guard_msgs (info) in
 example : x = 0 → 0 + 1*x = 0 := by
   simple_tac2
diff --git a/tests/lean/run/grind_try_exact.lean b/tests/lean/run/grind_try_exact.lean
new file mode 100644
index 0000000000..099a17700c
--- /dev/null
+++ b/tests/lean/run/grind_try_exact.lean
@@ -0,0 +1,35 @@
+opaque P : Nat → Prop
+opaque Q : Nat → Prop
+
+theorem Pall : Q x → P x := sorry
+
+/-- info: Try this: exact Pall h -/
+#guard_msgs (info) in
+example (h : Q x) (_ : x > 0) : P x := by
+  try?
+
+/-- info: Try this: · intros; expose_names; exact Pall h -/
+#guard_msgs (info) in
+example: Q x → True → P x := by
+  try?
+
+/-- info: Try this: · intros; expose_names; exact Pall h_1 -/
+#guard_msgs (info) in
+example: True → Q x → True → P x := by
+  try?
+
+theorem Qall {x y : Nat} : Q x := sorry
+
+/--
+error: tactic 'try?' failed, consider using `grind` manually, or `try? +missing` for partial proofs containing `sorry`
+x : Nat
+⊢ Q x
+-/
+#guard_msgs (error) in
+example : Q x := by
+  try? -- should fail, we cannot elaborate `exact Qall`
+
+/-- info: Try this: · expose_names; exact Pall h -/
+#guard_msgs (info) in
+example (_ : Q x) (_ : x > 0) : P x := by
+  try?