From d464b13569ffd6a2a8cb7e00bbba56e5ab344ac7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 11 Nov 2025 19:26:18 -0800
Subject: [PATCH] feat: add `cases_next` to `grind` tactic mode (#11148)

This PR addst the `cases_next` tactic to the `grind` interactive mode.
---
 src/Init/Grind/Interactive.lean               |  5 +++
 src/Lean/Elab/Tactic/Grind/Basic.lean         |  8 ++++
 src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean | 11 ++++--
 tests/lean/run/grind_finish_trace.lean        | 37 +++++++++++++++++++
 4 files changed, 57 insertions(+), 4 deletions(-)

diff --git a/src/Init/Grind/Interactive.lean b/src/Init/Grind/Interactive.lean
index b9ed34d4e3..ba32dee067 100644
--- a/src/Init/Grind/Interactive.lean
+++ b/src/Init/Grind/Interactive.lean
@@ -123,6 +123,11 @@ available in the `grind` state.
 -/
 syntax (name := casesTrace) "cases?" grindFilter : grind
 
+/--
+Performs the next case-split. The case-split is selected using the same heuristic used by `finish`.
+-/
+syntax (name := casesNext) "cases_next" : grind
+
 /-- `done` succeeds iff there are no remaining goals. -/
 syntax (name := done) "done" : grind
 
diff --git a/src/Lean/Elab/Tactic/Grind/Basic.lean b/src/Lean/Elab/Tactic/Grind/Basic.lean
index e3be546f84..2e60d556b6 100644
--- a/src/Lean/Elab/Tactic/Grind/Basic.lean
+++ b/src/Lean/Elab/Tactic/Grind/Basic.lean
@@ -310,6 +310,14 @@ def liftSearchM (k : SearchM α) : GrindTacticM α := do
   replaceMainGoal [state.goal]
   return a
 
+def liftAction (a : Action) : GrindTacticM Unit := do
+  let goal ← getMainGoal
+  let ka := fun _ => throwError "tactic is not applicable"
+  let kp := fun goal => return .stuck [goal]
+  match (← liftGrindM <| a goal ka kp) with
+  | .closed _ => replaceMainGoal []
+  | .stuck gs => replaceMainGoal gs
+
 def done : GrindTacticM Unit := do
   pruneSolvedGoals
   let goals ← getGoals
diff --git a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
index 8880ea7e99..44b9bff8c0 100644
--- a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
@@ -106,15 +106,15 @@ If the goal is not inconsistent and progress has been made,
 -/
 def evalCheck (tacticName : Name) (k : GoalM Bool)
     (pp? : Goal → MetaM (Option MessageData)) : GrindTacticM Unit := do
+  let recover := (← read).recover
   liftGoalM do
     let progress ← k
     unless progress do
       throwError "`{tacticName}` failed"
     processNewFacts
-    unless (← Grind.getConfig).verbose do
-      return ()
-    if (← get).inconsistent then
-      return ()
+    unless (← Grind.getConfig).verbose do return ()
+    unless recover do return ()
+    if (← get).inconsistent then return ()
     let some msg ← pp? (← get) | return ()
     logInfo msg
 
@@ -311,6 +311,9 @@ def mkCasesSuggestions (candidates : Array SplitCandidateWithAnchor) (numDigits
   Tactic.TryThis.addSuggestions stx suggestions
   return ()
 
+@[builtin_grind_tactic casesNext] def evalCasesNext : GrindTactic := fun _ => do
+  liftAction (Action.splitNext (stopAtFirstFailure := false))
+
 @[builtin_grind_tactic Parser.Tactic.Grind.focus] def evalFocus : GrindTactic := fun stx => do
   let mkInfo ← mkInitialTacticInfo stx[0]
   focus do
diff --git a/tests/lean/run/grind_finish_trace.lean b/tests/lean/run/grind_finish_trace.lean
index f2073a81a0..bb11ff1ae2 100644
--- a/tests/lean/run/grind_finish_trace.lean
+++ b/tests/lean/run/grind_finish_trace.lean
@@ -30,6 +30,43 @@ example (p : Nat → Prop) (x y z w : Int) :
     (z = 1 ∨ z = 0) → x + y ≤ 6 := by
   grind => finish?
 
+/-- error: tactic is not applicable -/
+#guard_msgs in
+example (a b c : Int) : a + b ≤ 2 → b = c → 2*b - c + a ≤ 3 := by
+  grind => cases_next
+
+example (p : Nat → Prop) (x y z w : Int) :
+    (x = 1 ∨ x = 2) →
+    (w = 1 ∨ w = 4) →
+    (y = 1 ∨ (∃ x : Nat, y = 3 - x ∧ p x)) →
+    (z = 1 ∨ z = 0) → x + y ≤ 6 := by
+  grind =>
+    cases_next <;> cases_next <;> cases_next <;> cases_next <;> lia
+
+example (p : Nat → Prop) (x y z w : Int) :
+    (x = 1 ∨ x = 2) →
+    (w = 1 ∨ w = 4) →
+    (y = 1 ∨ (∃ x : Nat, y = 3 - x ∧ p x)) →
+    (z = 1 ∨ z = 0) → x + y ≤ 6 := by
+  grind =>
+    repeat (first (lia) (cases_next))
+
+example (p : Nat → Prop) (x y z w : Int) :
+    (x = 1 ∨ x = 2) →
+    (w = 1 ∨ w = 4) →
+    (y = 1 ∨ (∃ x : Nat, y = 3 - x ∧ p x)) →
+    (z = 1 ∨ z = 0) → x + y ≤ 6 := by
+  grind =>
+    repeat (first (cases_next) (lia))
+
+example (p : Nat → Prop) (x y z w : Int) :
+    (x = 1 ∨ x = 2) →
+    (w = 1 ∨ w = 4) →
+    (y = 1 ∨ (∃ x : Nat, y = 3 - x ∧ p x)) →
+    (z = 1 ∨ z = 0) → x + y ≤ 6 := by
+  grind =>
+    repeat (first (ring) (cases_next) (lia))
+
 /--
 info: Try these:
   [apply] cases #5c4b <;> cases #896f <;> ac