feat: exact? +grind and exact? +try? discharger options (#11469)

kim-em · claude · web-flow · commit 226a90f1ebbb · 2025-12-02T06:31:56.000Z
This PR adds `+grind` and `+try?` options to `exact?` and `apply?`
tactics.

## `+grind` option

When `+grind` is enabled, `grind` is used as a fallback discharger for
subgoals that `solve_by_elim` cannot close. The proof is wrapped in
`Grind.Marker` so suggestions display `(by grind)` instead of the
complex grind proof term.

Example:
```lean
axiom foo (x : Nat) : x &lt; 37 → 5 &lt; x → x.log2 &lt; 6

/--
info: Try this:
  [apply] exact foo x (by grind) (by grind)
-/
#guard_msgs in
example (x : Nat) (h₁ : x &lt; 30) (h₂ : 8 &lt; x) : x.log2 &lt; 6 := by
  exact? +grind
```

## `+try?` option

When `+try?` is enabled, `try?` is used as a fallback discharger for
subgoals. This is useful when subgoals require induction or other
strategies that `try?` can find but `solve_by_elim` and `grind` cannot.

Example:
```lean
inductive MyList (α : Type _) where
  | nil : MyList α
  | cons : α → MyList α → MyList α

axiom MyListProp : MyList α → Prop
@[grind .] axiom mylist_nil : MyListProp (MyList.nil : MyList α)
@[grind .] axiom mylist_cons : ∀ (x : α) (xs : MyList α), MyListProp xs → MyListProp (MyList.cons x xs)

axiom qux (xs : MyList α) (p : MyListProp xs) : MyListProp2 xs

/--
info: Try this:
  [apply] exact qux xs (by try?)
-/
example (xs : MyList α) : MyListProp2 xs := by
  exact? +try?
```

🤖 Prepared with Claude Code

---------

Co-authored-by: Claude &lt;noreply@anthropic.com&gt;
diff --git a/src/Init/Grind/Util.lean b/src/Init/Grind/Util.lean
@@ -122,4 +122,15 @@ See comment at `alreadyNorm`
 theorem em (p : Prop) : alreadyNorm p ∨ alreadyNorm (¬ p) :=
   Classical.em p
 
+/--
+Marker for grind-solved subproofs in `exact? +grind` suggestions.
+When `exact?` uses grind as a discharger, it wraps the proof in this marker
+so that the unexpander can replace it with `(by grind)` in the suggestion.
+-/
+@[inline] def Marker {α : Sort u} (a : α) : α := a
+
+@[app_unexpander Marker]
+meta def markerUnexpander : PrettyPrinter.Unexpander := fun _ => do
+  `(by grind)
+
 end Lean.Grind
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
@@ -1690,24 +1690,41 @@ a lemma from the list until it gets stuck.
 syntax (name := applyRules) "apply_rules" optConfig (&" only")? (args)? (using_)? : tactic
 end SolveByElim
 
+/--
+Configuration for the `exact?` and `apply?` tactics.
+-/
+structure LibrarySearchConfig where
+  /-- If true, use `grind` as a discharger for subgoals that cannot be closed
+  by `solve_by_elim` alone. -/
+  grind : Bool := false
+  /-- If true, use `try?` as a discharger for subgoals that cannot be closed
+  by `solve_by_elim` alone. -/
+  try? : Bool := false
+
 /--
 Searches environment for definitions or theorems that can solve the goal using `exact`
 with conditions resolved by `solve_by_elim`.
 
 The optional `using` clause provides identifiers in the local context that must be
 used by `exact?` when closing the goal.  This is most useful if there are multiple
 ways to resolve the goal, and one wants to guide which lemma is used.
+
+Use `+grind` to enable `grind` as a fallback discharger for subgoals.
+Use `+try?` to enable `try?` as a fallback discharger for subgoals.
 -/
-syntax (name := exact?) "exact?" (" using " (colGt ident),+)? : tactic
+syntax (name := exact?) "exact?" optConfig (" using " (colGt ident),+)? : tactic
 
 /--
 Searches environment for definitions or theorems that can refine the goal using `apply`
 with conditions resolved when possible with `solve_by_elim`.
 
 The optional `using` clause provides identifiers in the local context that must be
 used when closing the goal.
+
+Use `+grind` to enable `grind` as a fallback discharger for subgoals.
+Use `+try?` to enable `try?` as a fallback discharger for subgoals.
 -/
-syntax (name := apply?) "apply?" (" using " (colGt term),+)? : tactic
+syntax (name := apply?) "apply?" optConfig (" using " (colGt term),+)? : tactic
 
 /--
 Syntax for excluding some names, e.g. `[-my_lemma, -my_theorem]`.
diff --git a/src/Init/Try.lean b/src/Init/Try.lean
@@ -82,3 +82,18 @@ macro "∎" : tactic => `(tactic| try?)
 /-- `∎` (typed as `\qed`) is a macro that expands to `by try? (wrapWithBy := true)` in term mode.
     The `wrapWithBy` config option causes suggestions to be prefixed with `by`. -/
 macro "∎" : term => `(by try? (wrapWithBy := true))
+
+namespace Lean.Try
+
+/--
+Marker for try?-solved subproofs in `exact? +try?` suggestions.
+When `exact?` uses try? as a discharger, it wraps the proof in this marker
+so that the unexpander can replace it with `(by try?)` in the suggestion.
+-/
+@[inline] def Marker {α : Sort u} (a : α) : α := a
+
+@[app_unexpander Marker]
+meta def markerUnexpander : PrettyPrinter.Unexpander := fun _ => do
+  `(by try?)
+
+end Lean.Try
diff --git a/src/Lean/Elab/Tactic/LibrarySearch.lean b/src/Lean/Elab/Tactic/LibrarySearch.lean
@@ -9,6 +9,7 @@ prelude
 public import Lean.Meta.Tactic.LibrarySearch
 public import Lean.Meta.Tactic.TryThis
 public import Lean.Elab.Tactic.ElabTerm
+public import Lean.Elab.Tactic.Config
 
 public section
 
@@ -17,22 +18,27 @@ namespace Lean.Elab.LibrarySearch
 open Lean Meta LibrarySearch
 open Elab Tactic Term TryThis
 
+declare_config_elab elabLibrarySearchConfig Parser.Tactic.LibrarySearchConfig
+
 /--
 Implementation of the `exact?` tactic.
 
 * `ref` contains the input syntax and is used for locations in error reporting.
+* `config` contains configuration options (e.g., `grind` for using grind as a discharger).
 * `required` contains an optional list of terms that should be used in closing the goal.
 * `requireClose` indicates if the goal must be closed.
   It is `true` for `exact?` and `false` for `apply?`.
 -/
-def exact? (ref : Syntax) (required : Option (Array (TSyntax `term))) (requireClose : Bool) :
+def exact? (ref : Syntax) (config : Parser.Tactic.LibrarySearchConfig)
+    (required : Option (Array (TSyntax `term))) (requireClose : Bool) :
     TacticM Unit := do
   let mvar ← getMainGoal
   let initialState ← saveState
   let (_, goal) ← (← getMainGoal).intros
   goal.withContext do
     let required := (← (required.getD #[]).mapM getFVarId).toList.map .fvar
-    let tactic := fun goals => solveByElim required (exfalso := false) goals (maxDepth := 6)
+    let tactic := fun goals =>
+      solveByElim required (exfalso := false) goals (maxDepth := 6) (grind := config.grind) (try? := config.try?)
     let allowFailure := fun g => do
       let g ← g.withContext (instantiateMVars (.mvar g))
       return required.all fun e => e.occurs g
@@ -55,16 +61,18 @@ def exact? (ref : Syntax) (required : Option (Array (TSyntax `term))) (requireCl
 
 @[builtin_tactic Lean.Parser.Tactic.exact?]
 def evalExact : Tactic := fun stx => do
-  let `(tactic| exact? $[using $[$required],*]?) := stx
+  let `(tactic| exact? $cfg:optConfig $[using $[$required],*]?) := stx
         | throwUnsupportedSyntax
-  exact? (← getRef) required true
+  let config ← elabLibrarySearchConfig cfg
+  exact? (← getRef) config required true
 
 
 @[builtin_tactic Lean.Parser.Tactic.apply?]
 def evalApply : Tactic := fun stx => do
-  let `(tactic| apply? $[using $[$required],*]?) := stx
+  let `(tactic| apply? $cfg:optConfig $[using $[$required],*]?) := stx
         | throwUnsupportedSyntax
-  exact? (← getRef) required false
+  let config ← elabLibrarySearchConfig cfg
+  exact? (← getRef) config required false
 
 @[builtin_term_elab Lean.Parser.Syntax.exact?]
 def elabExact?Term : TermElab := fun stx expectedType? => do
diff --git a/src/Lean/Meta/Tactic/LibrarySearch.lean b/src/Lean/Meta/Tactic/LibrarySearch.lean
@@ -8,7 +8,11 @@ module
 prelude
 public import Lean.Meta.LazyDiscrTree
 public import Lean.Meta.Tactic.SolveByElim
+public import Lean.Meta.Tactic.Grind.Main
 public import Lean.Util.Heartbeats
+import Init.Grind.Util
+import Init.Try
+import Lean.Elab.Tactic.Basic
 
 public section
 
@@ -36,16 +40,78 @@ builtin_initialize registerTraceClass `Tactic.librarySearch.lemmas
 
 open SolveByElim
 
+/--
+A discharger that tries `grind` on the goal.
+The proof is wrapped in `Grind.Marker` so that suggestions display `(by grind)`
+instead of the complex grind proof term.
+Returns `some []` if grind succeeds, `none` otherwise (leaving the goal as a subgoal).
+-/
+def grindDischarger (mvarId : MVarId) : MetaM (Option (List MVarId)) := do
+  try
+    -- Apply the marker wrapper, creating a subgoal for grind to solve
+    let type ← mvarId.getType
+    let u ← getLevel type
+    let markerExpr := mkApp (.const ``Lean.Grind.Marker [u]) type
+    let [subgoal] ← mvarId.apply markerExpr
+      | return none
+    -- Solve the subgoal with grind
+    let params ← Grind.mkParams {}
+    let result ← Grind.main subgoal params
+    if result.hasFailed then
+      return none
+    else
+      return some []
+  catch _ =>
+    return none
+
+/--
+A discharger that tries `try?` on the goal.
+The proof is wrapped in `Try.Marker` so that suggestions display `(by try?)`
+instead of the complex proof term.
+Returns `some []` if try? succeeds, `none` otherwise (leaving the goal as a subgoal).
+-/
+def tryDischarger (mvarId : MVarId) : MetaM (Option (List MVarId)) := do
+  try
+    -- Apply the marker wrapper, creating a subgoal for try? to solve
+    let type ← mvarId.getType
+    let u ← getLevel type
+    let markerExpr := mkApp (.const ``Lean.Try.Marker [u]) type
+    let [subgoal] ← mvarId.apply markerExpr
+      | return none
+    -- Run try? via TacticM to solve the subgoal
+    -- We suppress the "Try this" messages since we're using try? as a discharger
+    let tacStx ← `(tactic| try?)
+    let remainingGoals ← Elab.Term.TermElabM.run' <| Elab.Tactic.run subgoal do
+      -- Suppress info messages from try?
+      let initialLog ← Core.getMessageLog
+      Elab.Tactic.evalTactic tacStx
+      Core.setMessageLog initialLog
+    if remainingGoals.isEmpty then
+      return some []
+    else
+      return none
+  catch _ =>
+    return none
+
 /--
 Wrapper for calling `Lean.Meta.SolveByElim.solveByElim with
 appropriate arguments for library search.
+
+If `grind` is true, `grind` will be used as a fallback discharger for subgoals
+that cannot be closed by other means.
+If `try?` is true, `try?` will be used as a fallback discharger (via grind internally).
 -/
-def solveByElim (required : List Expr) (exfalso : Bool) (goals : List MVarId) (maxDepth : Nat) := do
+def solveByElim (required : List Expr) (exfalso : Bool) (goals : List MVarId)
+    (maxDepth : Nat) (grind : Bool := false) (try? : Bool := false) := do
   let cfg : SolveByElimConfig :=
     { maxDepth, exfalso := exfalso, symm := true, commitIndependentGoals := true,
       transparency := ← getTransparency,
       -- `constructor` has been observed to significantly slow down `exact?` in Mathlib.
       constructor := false }
+  -- Add grind or try? as a fallback discharger (tried after intro/constructor fail)
+  let cfg := if try? then cfg.withDischarge tryDischarger
+             else if grind then cfg.withDischarge grindDischarger
+             else cfg
   let ⟨lemmas, ctx⟩ ← SolveByElim.mkAssumptionSet false false [] [] #[]
   let cfg := if !required.isEmpty then cfg.requireUsingAll required else cfg
   SolveByElim.solveByElim cfg lemmas ctx goals
diff --git a/tests/lean/run/info_trees.lean b/tests/lean/run/info_trees.lean
@@ -3,57 +3,59 @@
 -- it is fine to simply remove the `#guard_msgs` and expected output.
 
 /--
-info: • [Command] @ ⟨77, 0⟩-⟨77, 40⟩ @ Lean.Elab.Command.elabDeclaration
-  • [Term] Nat : Type @ ⟨77, 15⟩-⟨77, 18⟩ @ Lean.Elab.Term.elabIdent
-    • [Completion-Id] Nat : some Sort.{?_uniq.1} @ ⟨77, 15⟩-⟨77, 18⟩
-    • [Term] Nat : Type @ ⟨77, 15⟩-⟨77, 18⟩
-  • [Term] n (isBinder := true) : Nat @ ⟨77, 11⟩-⟨77, 12⟩
-  • [Term] 0 ≤ n : Prop @ ⟨77, 22⟩-⟨77, 27⟩ @ «_aux_Init_Notation___macroRules_term_≤__2»
+info: • [Command] @ ⟨79, 0⟩-⟨79, 40⟩ @ Lean.Elab.Command.elabDeclaration
+  • [Term] Nat : Type @ ⟨79, 15⟩-⟨79, 18⟩ @ Lean.Elab.Term.elabIdent
+    • [Completion-Id] Nat : some Sort.{?_uniq.1} @ ⟨79, 15⟩-⟨79, 18⟩
+    • [Term] Nat : Type @ ⟨79, 15⟩-⟨79, 18⟩
+  • [Term] n (isBinder := true) : Nat @ ⟨79, 11⟩-⟨79, 12⟩
+  • [Term] 0 ≤ n : Prop @ ⟨79, 22⟩-⟨79, 27⟩ @ «_aux_Init_Notation___macroRules_term_≤__2»
     • [MacroExpansion]
       0 ≤ n
       ===>
       binrel% LE.le✝ 0 n
-      • [Term] 0 ≤ n : Prop @ ⟨77, 22⟩†-⟨77, 27⟩† @ Lean.Elab.Term.Op.elabBinRel
-        • [Term] 0 ≤ n : Prop @ ⟨77, 22⟩†-⟨77, 27⟩†
-          • [Completion-Id] LE.le✝ : none @ ⟨77, 22⟩†-⟨77, 27⟩†
-          • [Term] 0 : Nat @ ⟨77, 22⟩-⟨77, 23⟩ @ Lean.Elab.Term.elabNumLit
-          • [Term] n : Nat @ ⟨77, 26⟩-⟨77, 27⟩ @ Lean.Elab.Term.elabIdent
-            • [Completion-Id] n : none @ ⟨77, 26⟩-⟨77, 27⟩
-            • [Term] n : Nat @ ⟨77, 26⟩-⟨77, 27⟩
+      • [Term] 0 ≤ n : Prop @ ⟨79, 22⟩†-⟨79, 27⟩† @ Lean.Elab.Term.Op.elabBinRel
+        • [Term] 0 ≤ n : Prop @ ⟨79, 22⟩†-⟨79, 27⟩†
+          • [Completion-Id] LE.le✝ : none @ ⟨79, 22⟩†-⟨79, 27⟩†
+          • [Term] 0 : Nat @ ⟨79, 22⟩-⟨79, 23⟩ @ Lean.Elab.Term.elabNumLit
+          • [Term] n : Nat @ ⟨79, 26⟩-⟨79, 27⟩ @ Lean.Elab.Term.elabIdent
+            • [Completion-Id] n : none @ ⟨79, 26⟩-⟨79, 27⟩
+            • [Term] n : Nat @ ⟨79, 26⟩-⟨79, 27⟩
   • [CustomInfo(Lean.Elab.Term.AsyncBodyInfo)]
-    • [Term] n (isBinder := true) : Nat @ ⟨77, 11⟩-⟨77, 12⟩
+    • [Term] n (isBinder := true) : Nat @ ⟨79, 11⟩-⟨79, 12⟩
     • [CustomInfo(Lean.Elab.Term.BodyInfo)]
-      • [Tactic] @ ⟨77, 31⟩-⟨77, 40⟩
-        (Term.byTactic "by" (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])])))
+      • [Tactic] @ ⟨79, 31⟩-⟨79, 40⟩
+        (Term.byTactic
+         "by"
+         (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" (Tactic.optConfig []) [])])))
         before ⏎
         n : Nat
         ⊢ 0 ≤ n
         after no goals
-        • [Tactic] @ ⟨77, 31⟩-⟨77, 33⟩
+        • [Tactic] @ ⟨79, 31⟩-⟨79, 33⟩
           "by"
           before ⏎
           n : Nat
           ⊢ 0 ≤ n
           after no goals
-          • [Tactic] @ ⟨77, 34⟩-⟨77, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq
-            (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])]))
+          • [Tactic] @ ⟨79, 34⟩-⟨79, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq
+            (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" (Tactic.optConfig []) [])]))
             before ⏎
             n : Nat
             ⊢ 0 ≤ n
             after no goals
-            • [Tactic] @ ⟨77, 34⟩-⟨77, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq1Indented
-              (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])])
+            • [Tactic] @ ⟨79, 34⟩-⟨79, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq1Indented
+              (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" (Tactic.optConfig []) [])])
               before ⏎
               n : Nat
               ⊢ 0 ≤ n
               after no goals
-              • [Tactic] @ ⟨77, 34⟩-⟨77, 40⟩ @ Lean.Elab.LibrarySearch.evalExact
-                (Tactic.exact? "exact?" [])
+              • [Tactic] @ ⟨79, 34⟩-⟨79, 40⟩ @ Lean.Elab.LibrarySearch.evalExact
+                (Tactic.exact? "exact?" (Tactic.optConfig []) [])
                 before ⏎
                 n : Nat
                 ⊢ 0 ≤ n
                 after no goals
-                • [Tactic] @ ⟨77, 34⟩†-⟨77, 40⟩† @ Lean.Elab.Tactic.evalExact
+                • [Tactic] @ ⟨79, 34⟩†-⟨79, 40⟩† @ Lean.Elab.Tactic.evalExact
                   (Tactic.exact "exact" (Term.app `Nat.zero_le [`n]))
                   before ⏎
                   n : Nat
@@ -66,8 +68,8 @@ info: • [Command] @ ⟨77, 0⟩-⟨77, 40⟩ @ Lean.Elab.Command.elabDeclarati
                       • [Completion-Id] n : some Nat @ ⟨1, 5⟩†-⟨1, 5⟩†
                       • [Term] n : Nat @ ⟨1, 5⟩†-⟨1, 5⟩†
                 • [CustomInfo(Lean.Meta.Tactic.TryThis.TryThisInfo)]
-    • [Term] t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨77, 8⟩-⟨77, 9⟩
-    • [Term] t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨77, 8⟩-⟨77, 9⟩
+    • [Term] t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨79, 8⟩-⟨79, 9⟩
+    • [Term] t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨79, 8⟩-⟨79, 9⟩
 ---
 info: Try this:
   [apply] exact Nat.zero_le n
diff --git a/tests/lean/run/library_search_grind.lean b/tests/lean/run/library_search_grind.lean
diff --git a/tests/lean/run/prelude-injectivity.lean b/tests/lean/run/prelude-injectivity.lean
