feat: exact? +grind uses grind as a discharger

Author: kim-em

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,24 +1690,36 @@ 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
+
 /--
 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.
 -/
-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.
 -/
-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/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)
     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,9 @@ 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
 
 public section
 
@@ -36,16 +38,46 @@ 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
+
 /--
 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.
 -/
-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) := 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
   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

@@ -0,0 +1,48 @@
+/-!
+# 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