feat: improve grind search procedure (#6657)

This PR improves the `grind` search procedure, and adds the new
configuration option: `failures`.

src/Init/Grind/Tactics.lean

@@ -45,6 +45,8 @@ structure Config where
   If `splitIndPred` is `true`, `grind` performs case-splitting on inductive predicates.
   Otherwise, it performs case-splitting only on types marked with `[grind_split]` attribute. -/
   splitIndPred : Bool := true
+  /-- By default, `grind` halts as soon as it encounters a sub-goal where no further progress can be made. -/
+  failures : Nat := 1
   deriving Inhabited, BEq
 
 end Lean.Grind

src/Lean/Meta/Tactic/Grind/EMatch.lean

@@ -370,7 +370,4 @@ def ematchAndAssert : GrindTactic := fun goal => do
     return none
   assertAll goal
 
-def ematchStar : GrindTactic :=
-  ematchAndAssert.iterate
-
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Main.lean

@@ -15,6 +15,7 @@ import Lean.Meta.Tactic.Grind.Inv
 import Lean.Meta.Tactic.Grind.Intro
 import Lean.Meta.Tactic.Grind.EMatch
 import Lean.Meta.Tactic.Grind.Split
+import Lean.Meta.Tactic.Grind.Solve
 import Lean.Meta.Tactic.Grind.SimpUtil
 
 namespace Lean.Meta.Grind
@@ -68,17 +69,10 @@ private def initCore (mvarId : MVarId) : GrindM (List Goal) := do
   goals.forM (·.checkInvariants (expensive := true))
   return goals.filter fun goal => !goal.inconsistent
 
-def all (goals : List Goal) (f : Goal → GrindM (List Goal)) : GrindM (List Goal) := do
-  goals.foldlM (init := []) fun acc goal => return acc ++ (← f goal)
-
-/-- A very simple strategy -/
-private def simple (goals : List Goal) : GrindM (List Goal) := do
-  applyToAll (assertAll >> ematchStar >> (splitNext >> assertAll >> ematchStar).iterate) goals
-
 def main (mvarId : MVarId) (config : Grind.Config) (mainDeclName : Name) (fallback : Fallback) : MetaM (List Goal) := do
   let go : GrindM (List Goal) := do
     let goals ← initCore mvarId
-    let goals ← simple goals
+    let goals ← solve goals
     let goals ← goals.filterMapM fun goal => do
       if goal.inconsistent then return none
       let goal ← GoalM.run' goal fallback

src/Lean/Meta/Tactic/Grind/Solve.lean

@@ -0,0 +1,92 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Combinators
+import Lean.Meta.Tactic.Grind.Split
+import Lean.Meta.Tactic.Grind.EMatch
+
+namespace Lean.Meta.Grind
+
+namespace Solve
+
+structure State where
+  todo     : List Goal
+  failures : List Goal := []
+  stop     : Bool := false
+
+private abbrev M := StateRefT State GrindM
+
+def getNext? : M (Option Goal) := do
+  let goal::todo := (← get).todo | return none
+  modify fun s => { s with todo }
+  return some goal
+
+def pushGoal (goal : Goal) : M Unit :=
+  modify fun s => { s with todo := goal :: s.todo }
+
+def pushGoals (goals : List Goal) : M Unit :=
+  modify fun s => { s with todo := goals ++ s.todo }
+
+def pushFailure (goal : Goal) : M Unit := do
+  modify fun s => { s with failures := goal :: s.failures }
+  if (← get).failures.length ≥ (← getConfig).failures then
+    modify fun s => { s with stop := true }
+
+@[inline] def stepGuard (x : Goal → M Bool) (goal : Goal) : M Bool := do
+  try
+    x goal
+  catch ex =>
+    if ex.isMaxHeartbeat || ex.isMaxRecDepth then
+      let goal ← goal.reportIssue ex.toMessageData
+      pushFailure goal
+      return true
+    else
+      throw ex
+
+def applyTac (x : GrindTactic) (goal : Goal) : M Bool := do
+  let go (goal : Goal) : M Bool := do
+    let some goals ← x goal | return false
+    pushGoals goals
+    return true
+  stepGuard go goal
+
+def tryAssertNext : Goal → M Bool := applyTac assertNext
+
+def tryEmatch : Goal → M Bool := applyTac ematchAndAssert
+
+def trySplit : Goal → M Bool := applyTac splitNext
+
+def maxNumFailuresReached : M Bool := do
+  return (← get).failures.length ≥ (← getConfig).failures
+
+partial def main : M Unit := do
+  repeat do
+    if (← get).stop then
+      return ()
+    let some goal ← getNext? |
+      return ()
+    if goal.inconsistent then
+      continue
+    if (← tryAssertNext goal) then
+      continue
+    if (← tryEmatch goal) then
+      continue
+    if (← trySplit goal) then
+      continue
+    pushFailure goal
+
+end Solve
+
+/--
+Try to solve/close the given goals, and returns the ones that could not be solved.
+-/
+def solve (goals : List Goal) : GrindM (List Goal) := do
+  let (_, s) ← Solve.main.run { todo := goals }
+  let todo ← s.todo.mapM fun goal => do
+    goal.reportIssue m!"this goal was not fully processed due to previous failures, threshold: `(failures := {(← getConfig).failures})`"
+  return s.failures.reverse ++ todo
+
+end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -416,14 +416,19 @@ def updateLastTag : GoalM Unit := do
       trace[grind] "working on goal `{currTag}`"
       modifyThe Grind.State fun s => { s with lastTag := currTag }
 
-def reportIssue (msg : MessageData) : GoalM Unit := do
+def Goal.reportIssue (goal : Goal) (msg : MessageData) : MetaM Goal := do
   let msg ← addMessageContext msg
-  modify fun s => { s with issues := .trace { cls := `issue } msg #[] :: s.issues }
+  let goal := { goal with issues := .trace { cls := `issue } msg #[] :: goal.issues }
   /-
   We also add a trace message because we may want to know when
   an issue happened relative to other trace messages.
   -/
   trace[grind.issues] msg
+  return goal
+
+def reportIssue (msg : MessageData) : GoalM Unit := do
+  let goal ← (← get).reportIssue msg
+  set goal
 
 /--
 Macro similar to `trace[...]`, but it includes the trace message `trace[grind] "working on <current goal>"`

tests/lean/run/grind_pre.lean

@@ -198,6 +198,8 @@ h : p
   [eqc] False propositions
     [prop] ¬p
     [prop] ¬r
+  [issues] Issues
+    [issue] this goal was not fully processed due to previous failures, threshold: `(failures := 1)`
 -/
 #guard_msgs (error) in
 example (a : α) (p q r : Prop) : (h₁ : HEq p a) → (h₂ : HEq q a) → (h₃ : p = r) → False := by