test: update #guard_msgs for exact? syntax change

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>

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

src/Init/Tactics.lean

@@ -1690,6 +1690,17 @@ 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`.
@@ -1697,8 +1708,11 @@ 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`
@@ -1706,8 +1720,11 @@ 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]`.

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

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

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

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

tests/lean/run/library_search_grind.lean

@@ -0,0 +1,94 @@
+/-!
+# Tests for `exact? +grind` and `apply? +grind`
+
+These tests verify that the `+grind` option is accepted syntactically and
+enables `grind` as a fallback discharger for subgoals.
+-/
+
+/--
+info: Try this:
+  [apply] exact List.ne_nil_of_length_pos h
+-/
+#guard_msgs in
+example (l : List Nat) (h : 0 < l.length) : l ≠ [] := by exact?
+
+/--
+info: Try this:
+  [apply] exact List.ne_nil_of_length_pos (h trivial)
+-/
+#guard_msgs in
+example (l : List Nat) (h : True → 0 < l.length) : l ≠ [] := by exact?
+
+example (l : List Nat) (h : 1 < l.length) : l ≠ [] := by exact List.ne_nil_of_length_pos (by grind)
+
+/--
+info: Try this:
+  [apply] exact List.ne_nil_of_length_pos (by grind)
+-/
+#guard_msgs in
+example (l : List Nat) (h : 1 < l.length) : l ≠ [] := by
+  exact? +grind
+
+/--
+info: Try this:
+  [apply] exact List.ne_nil_of_length_pos (by grind)
+-/
+#guard_msgs in
+example {P : Prop} (l : List Nat) (p : P) (h : P → 1 < l.length) : l ≠ [] := by
+  exact? +grind
+
+axiom foo (x : Nat) : x < 37 → 5 < x → x.log2 < 6
+
+/--
+info: Try this:
+  [apply] exact foo x (by grind) (by grind)
+-/
+#guard_msgs in
+example (x : Nat) (h₁ : x < 30) (h₂ : 8 < x) : x.log2 < 6 := by
+  exact? +grind
+
+
+inductive MyList (α : Type _) where
+  | nil : MyList α
+  | cons : α → MyList α → MyList α
+
+axiom MyListProp : MyList α → Prop
+axiom MyListProp2 : MyList α → Prop
+
+@[grind .] axiom mylist_nil : MyListProp (MyList.nil : MyList α)
+@[grind .] axiom mylist_cons : ∀ (x : α) (xs : MyList α), MyListProp xs → MyListProp (MyList.cons x xs)
+
+/--
+info: Try these:
+  [apply] (induction xs) <;> grind
+  [apply] (induction xs) <;> grind only [mylist_nil, mylist_cons]
+  [apply] ·
+    induction xs
+    · grind => instantiate only [mylist_nil]
+    · grind => instantiate only [mylist_cons]
+-/
+#guard_msgs in
+example (xs : MyList α) : MyListProp xs := by
+  try?
+
+axiom qux (xs : MyList α) (p : MyListProp xs) : MyListProp2 xs
+
+/--
+info: Try these:
+  [apply] (induction xs) <;> grind
+  [apply] (induction xs) <;> grind only [mylist_nil, mylist_cons]
+  [apply] ·
+    induction xs
+    · grind => instantiate only [mylist_nil]
+    · grind => instantiate only [mylist_cons]
+-/
+#guard_msgs in
+example (xs : MyList α) : MyListProp2 xs := by
+  exact qux xs (by try?)
+
+/--
+info: Try this:
+  [apply] exact qux xs (by try?)
+-/
+example (xs : MyList α) : MyListProp2 xs := by
+  exact? +try?

tests/lean/run/prelude-injectivity.lean

@@ -21,6 +21,7 @@ gen_injective_theorems% Syntax.SepArray
 gen_injective_theorems% Syntax.TSepArray
 gen_injective_theorems% Try.Config
 gen_injective_theorems% Parser.Tactic.DecideConfig
+gen_injective_theorems% Parser.Tactic.LibrarySearchConfig
 -/
 #guard_msgs in
 run_meta