feat: basic case-split for grind (#6559)

This PR adds a basic case-splitting strategy for the `grind` tactic. We
still need to add support for user customization.

src/Init/Grind/Lemmas.lean

@@ -25,6 +25,9 @@ theorem and_eq_of_eq_false_right {a b : Prop} (h : b = False) : (a ∧ b) = Fals
 theorem eq_true_of_and_eq_true_left {a b : Prop} (h : (a ∧ b) = True) : a = True := by simp_all
 theorem eq_true_of_and_eq_true_right {a b : Prop} (h : (a ∧ b) = True) : b = True := by simp_all
 
+theorem or_of_and_eq_false {a b : Prop} (h : (a ∧ b) = False) : (¬a ∨ ¬b) := by
+  by_cases a <;> by_cases b <;> simp_all
+
 /-! Or -/
 
 theorem or_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a ∨ b) = True := by simp [h]

src/Init/Grind/Tactics.lean

@@ -24,14 +24,9 @@ The configuration for `grind`.
 Passed to `grind` using, for example, the `grind (config := { eager := true })` syntax.
 -/
 structure Config where
-  /-- When `eager` is true (default: `false`), `grind` eagerly splits `if-then-else` and `match` expressions during internalization. -/
-  eager : Bool := false
-  /-- Maximum number of branches (i.e., case-splits) in the proof search tree. -/
-  splits : Nat := 100
-  /--
-  Maximum number of E-matching (aka heuristic theorem instantiation)
-  in a proof search tree branch.
-  -/
+  /-- Maximum number of case-splits in a proof search branch. It does not include splits performed during normalization. -/
+  splits : Nat := 5
+  /-- Maximum number of E-matching (aka heuristic theorem instantiation) rounds before each case split. -/
   ematch : Nat := 5
   /--
   Maximum term generation.

src/Lean/Meta/Tactic/Grind.lean

@@ -39,6 +39,9 @@ builtin_initialize registerTraceClass `grind.ematch.instance
 builtin_initialize registerTraceClass `grind.ematch.instance.assignment
 builtin_initialize registerTraceClass `grind.issues
 builtin_initialize registerTraceClass `grind.simp
+builtin_initialize registerTraceClass `grind.split
+builtin_initialize registerTraceClass `grind.split.candidate
+builtin_initialize registerTraceClass `grind.split.resolved
 
 /-! Trace options for `grind` developers -/
 builtin_initialize registerTraceClass `grind.debug

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

@@ -0,0 +1,71 @@
+/-
+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.Types
+
+namespace Lean.Meta.Grind
+
+/-!
+Combinators for manipulating `GrindTactic`s.
+TODO: a proper tactic language for `grind`.
+-/
+
+def GrindTactic := Goal → GrindM (Option (List Goal))
+
+def GrindTactic.try (x : GrindTactic) : GrindTactic := fun g => do
+  let some gs ← x g | return some [g]
+  return some gs
+
+def applyToAll (x : GrindTactic)  (goals : List Goal) : GrindM (List Goal) := do
+  go goals []
+where
+  go (goals : List Goal) (acc : List Goal) : GrindM (List Goal) := do
+    match goals with
+    | [] => return acc.reverse
+    | goal :: goals => match (← x goal) with
+      | none => go goals (goal :: acc)
+      | some goals' => go goals (goals' ++ acc)
+
+partial def GrindTactic.andThen (x y : GrindTactic) : GrindTactic := fun goal => do
+  let some goals ← x goal | return none
+  applyToAll y goals
+
+instance : AndThen GrindTactic where
+  andThen a b := GrindTactic.andThen a (b ())
+
+partial def GrindTactic.iterate (x : GrindTactic) : GrindTactic := fun goal => do
+  go [goal] []
+where
+  go (todo : List Goal) (result : List Goal) : GrindM (List Goal) := do
+    match todo with
+    | [] => return result
+    | goal :: todo =>
+      if let some goalsNew ← x goal then
+        go (goalsNew ++ todo) result
+      else
+        go todo (goal :: result)
+
+partial def GrindTactic.orElse (x y : GrindTactic) : GrindTactic := fun goal => do
+  let some goals ← x goal | y goal
+  return goals
+
+instance : OrElse GrindTactic where
+  orElse a b := GrindTactic.andThen a (b ())
+
+def toGrindTactic (f : GoalM Unit) : GrindTactic := fun goal => do
+  let goal ← GoalM.run' goal f
+  if goal.inconsistent then
+    return some []
+  else
+    return some [goal]
+
+def GrindTactic' := Goal → GrindM (List Goal)
+
+def GrindTactic'.toGrindTactic (x : GrindTactic') : GrindTactic := fun goal => do
+  let goals ← x goal
+  return some goals
+
+end Lean.Meta.Grind

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

@@ -51,6 +51,8 @@ structure Context where
   useMT : Bool := true
   /-- `EMatchTheorem` being processed. -/
   thm   : EMatchTheorem := default
+  /-- Initial application used to start E-matching -/
+  initApp : Expr := default
   deriving Inhabited
 
 /-- State for the E-matching monad -/
@@ -64,6 +66,9 @@ abbrev M := ReaderT Context $ StateRefT State GoalM
 def M.run' (x : M α) : GoalM α :=
   x {} |>.run' {}
 
+@[inline] private abbrev withInitApp (e : Expr) (x : M α) : M α :=
+  withReader (fun ctx => { ctx with initApp := e }) x
+
 /--
 Assigns `bidx := e` in `c`. If `bidx` is already assigned in `c`, we check whether
 `e` and `c.assignment[bidx]` are in the same equivalence class.
@@ -213,6 +218,8 @@ private def addNewInstance (origin : Origin) (proof : Expr) (generation : Nat) :
     check proof
   let mut prop ← inferType proof
   if Match.isMatchEqnTheorem (← getEnv) origin.key then
+    -- `initApp` is a match-application that we don't need to split at anymore.
+    markCaseSplitAsResolved (← read).initApp
     prop ← annotateMatchEqnType prop
   trace[grind.ematch.instance] "{← origin.pp}: {prop}"
   addTheoremInstance proof prop (generation+1)
@@ -288,9 +295,10 @@ private def main (p : Expr) (cnstrs : List Cnstr) : M Unit := do
     let n ← getENode app
     if (n.heqProofs || n.isCongrRoot) &&
        (!useMT || n.mt == gmt) then
-      if let some c ← matchArgs? { cnstrs, assignment, gen := n.generation } p app |>.run then
-        modify fun s => { s with choiceStack := [c] }
-        processChoices
+      withInitApp app do
+        if let some c ← matchArgs? { cnstrs, assignment, gen := n.generation } p app |>.run then
+          modify fun s => { s with choiceStack := [c] }
+          processChoices
 
 def ematchTheorem (thm : EMatchTheorem) : M Unit := do
   if (← checkMaxInstancesExceeded) then return ()
@@ -341,14 +349,14 @@ def ematch : GoalM Unit := do
     }
 
 /-- Performs one round of E-matching, and assert new instances. -/
-def ematchAndAssert? (goal : Goal) : GrindM (Option (List Goal)) := do
+def ematchAndAssert : GrindTactic := fun goal => do
   let numInstances := goal.numInstances
   let goal ← GoalM.run' goal ematch
   if goal.numInstances == numInstances then
     return none
   assertAll goal
 
-def ematchStar (goal : Goal) : GrindM (List Goal) := do
-  iterate goal ematchAndAssert?
+def ematchStar : GrindTactic :=
+  ematchAndAssert.iterate
 
 end Lean.Meta.Grind

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

@@ -31,6 +31,10 @@ def addCongrTable (e : Expr) : GoalM Unit := do
   else
     modify fun s => { s with congrTable := s.congrTable.insert { e } }
 
+/--
+Given an application `e` of the form `f a_1 ... a_n`,
+adds entry `f ↦ e` to `appMap`. Recall that `appMap` is a multi-map.
+-/
 private def updateAppMap (e : Expr) : GoalM Unit := do
   let key := e.toHeadIndex
   modify fun s => { s with
@@ -40,6 +44,34 @@ private def updateAppMap (e : Expr) : GoalM Unit := do
       s.appMap.insert key [e]
   }
 
+/-- Inserts `e` into the list of case-split candidates. -/
+private def addSplitCandidate (e : Expr) : GoalM Unit := do
+  trace[grind.split.candidate] "{e}"
+  modify fun s => { s with splitCadidates := e :: s.splitCadidates }
+
+-- TODO: add attribute to make this extensible
+private def forbiddenSplitTypes := [``Eq, ``HEq, ``True, ``False]
+
+/-- Inserts `e` into the list of case-split candidates if applicable. -/
+private def checkAndaddSplitCandidate (e : Expr) : GoalM Unit := do
+  unless e.isApp do return ()
+  if e.isIte || e.isDIte then
+    addSplitCandidate e
+  else if (← isMatcherApp e) then
+    if let .reduced _ ← reduceMatcher? e then
+      -- When instantiating `match`-equations, we add `match`-applications that can be reduced,
+      -- and consequently don't need to be splitted.
+      return ()
+    else
+      addSplitCandidate e
+  else
+    let .const declName _  := e.getAppFn | return ()
+    if forbiddenSplitTypes.contains declName then return ()
+    -- We should have a mechanism for letting users to select types to case-split.
+    -- Right now, we just consider inductive predicates that are not in the forbidden list
+    if (← isInductivePredicate declName) then
+      addSplitCandidate e
+
 mutual
 /-- Internalizes the nested ground terms in the given pattern. -/
 private partial def internalizePattern (pattern : Expr) (generation : Nat) : GoalM Expr := do
@@ -116,6 +148,7 @@ partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do
       -- We do not want to internalize the components of a literal value.
       mkENode e generation
     else e.withApp fun f args => do
+      checkAndaddSplitCandidate e
       addMatchEqns f generation
       if f.isConstOf ``Lean.Grind.nestedProof && args.size == 2 then
         -- We only internalize the proposition. We can skip the proof because of

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

@@ -11,6 +11,7 @@ import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Cases
 import Lean.Meta.Tactic.Grind.Injection
 import Lean.Meta.Tactic.Grind.Core
+import Lean.Meta.Tactic.Grind.Combinators
 
 namespace Lean.Meta.Grind
 
@@ -88,7 +89,7 @@ private def applyInjection? (goal : Goal) (fvarId : FVarId) : MetaM (Option Goal
     return none
 
 /-- Introduce new hypotheses (and apply `by_contra`) until goal is of the form `... ⊢ False` -/
-partial def intros (goal : Goal) (generation : Nat) : GrindM (List Goal) := do
+partial def intros  (generation : Nat) : GrindTactic' := fun goal => do
   let rec go (goal : Goal) : StateRefT (Array Goal) GrindM Unit := do
     if goal.inconsistent then
       return ()
@@ -116,11 +117,11 @@ partial def intros (goal : Goal) (generation : Nat) : GrindM (List Goal) := do
   return goals.toList
 
 /-- Asserts a new fact `prop` with proof `proof` to the given `goal`. -/
-def assertAt (goal : Goal) (proof : Expr) (prop : Expr) (generation : Nat) : GrindM (List Goal) := do
+def assertAt (proof : Expr) (prop : Expr) (generation : Nat) : GrindTactic' := fun goal => do
   if (← isCasesCandidate prop) then
     let mvarId ← goal.mvarId.assert (← mkFreshUserName `h) prop proof
     let goal := { goal with mvarId }
-    intros goal generation
+    intros generation goal
   else
     let goal ← GoalM.run' goal do
       let r ← simp prop
@@ -130,25 +131,13 @@ def assertAt (goal : Goal) (proof : Expr) (prop : Expr) (generation : Nat) : Gri
     if goal.inconsistent then return [] else return [goal]
 
 /-- Asserts next fact in the `goal` fact queue. -/
-def assertNext? (goal : Goal) : GrindM (Option (List Goal)) := do
+def assertNext : GrindTactic := fun goal => do
   let some (fact, newFacts) := goal.newFacts.dequeue?
     | return none
-  assertAt { goal with newFacts } fact.proof fact.prop fact.generation
-
-partial def iterate (goal : Goal) (f : Goal → GrindM (Option (List Goal))) : GrindM (List Goal) := do
-  go [goal] []
-where
-  go (todo : List Goal) (result : List Goal) : GrindM (List Goal) := do
-    match todo with
-    | [] => return result
-    | goal :: todo =>
-      if let some goalsNew ← f goal then
-        go (goalsNew ++ todo) result
-      else
-        go todo (goal :: result)
+  assertAt fact.proof fact.prop fact.generation { goal with newFacts }
 
 /-- Asserts all facts in the `goal` fact queue. -/
-partial def assertAll (goal : Goal) : GrindM (List Goal) := do
-  iterate goal assertNext?
+partial def assertAll : GrindTactic :=
+  assertNext.iterate
 
 end Lean.Meta.Grind

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

@@ -14,6 +14,7 @@ import Lean.Meta.Tactic.Grind.Util
 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.SimpUtil
 
 namespace Lean.Meta.Grind
@@ -68,7 +69,7 @@ def all (goals : List Goal) (f : Goal → GrindM (List Goal)) : GrindM (List Goa
 
 /-- A very simple strategy -/
 private def simple (goals : List Goal) : GrindM (List Goal) := do
-  all goals ematchStar
+  applyToAll (ematchStar >> (splitNext >> ematchStar).iterate) goals
 
 def main (mvarId : MVarId) (config : Grind.Config) (mainDeclName : Name) (fallback : Fallback) : MetaM (List MVarId) := do
   let go : GrindM (List MVarId) := do