feat: exact? +try? uses try? as a discharger

This PR adds a `+try?` option to `exact?` and `apply?` tactics,
similar to the existing `+grind` option.

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

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

Co-Authored-By: Claude <[email protected]>

Author: kim-em

src/Init/Tactics.lean

@@ -1697,6 +1697,9 @@ 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`
@@ -1707,6 +1710,7 @@ used by `exact?` when closing the goal.  This is most useful if there are multip
 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?" optConfig (" using " (colGt ident),+)? : tactic
 
@@ -1718,6 +1722,7 @@ The optional `using` clause provides identifiers in the local context that must
 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?" optConfig (" using " (colGt term),+)? : tactic
 

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

@@ -38,7 +38,7 @@ def exact? (ref : Syntax) (config : Parser.Tactic.LibrarySearchConfig)
   goal.withContext do
     let required := (← (required.getD #[]).mapM getFVarId).toList.map .fvar
     let tactic := fun goals =>
-      solveByElim required (exfalso := false) goals (maxDepth := 6) (grind := config.grind)
+      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

src/Lean/Meta/Tactic/LibrarySearch.lean

@@ -11,6 +11,8 @@ 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
 
@@ -62,22 +64,54 @@ def grindDischarger (mvarId : MVarId) : MetaM (Option (List MVarId)) := do
   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) (grind : Bool := false) := do
+    (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 as a fallback discharger (tried after intro/constructor fail)
-  let cfg := if grind then cfg.withDischarge grindDischarger else cfg
+  -- 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/library_search_grind.lean

@@ -46,3 +46,49 @@ info: Try this:
 #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?