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

@@ -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
 

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

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

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