refactor: remove old grindSearchM framework (#11226)

This PR finally removes the old `grind` framework `SearchM`. It has been
replaced with the new `Action` framework.

src/Lean/Elab/Tactic/Grind/Basic.lean

@@ -7,7 +7,6 @@ module
 prelude
 public import Lean.Elab.Tactic.Basic
 public import Lean.Meta.Tactic.Grind.Main
-public import Lean.Meta.Tactic.Grind.SearchM
 import Lean.CoreM
 import Lean.Meta.Tactic.Grind.Intro
 import Lean.Meta.Tactic.Grind.PP
@@ -301,15 +300,6 @@ def liftGoalM (k : GoalM α) : GrindTacticM α := do
   replaceMainGoal [goal]
   return a
 
-def liftSearchM (k : SearchM α) : GrindTacticM α := do
-  let goal ← getMainGoal
-  let (a, state) ← liftGrindM <| SearchM.run goal k
-  unless state.choiceStack.isEmpty do
-    -- **TODO**: Convert pending goals into new subgoals.
-    throwError "`grind` internal error, `SearchM` action has pending choices, this is not supported yet."
-  replaceMainGoal [state.goal]
-  return a
-
 def liftAction (a : Action) : GrindTacticM Unit := do
   let goal ← getMainGoal
   let ka := fun _ => throwError "tactic is not applicable"
@@ -382,17 +372,22 @@ def mkEvalTactic (params : Params) : TacticM (Goal → TSyntax `grind → GrindM
 
 def GrindTacticM.runAtGoal (mvarId : MVarId) (params : Params) (k : GrindTacticM α) : TacticM (α × State) := do
   let evalTactic ← mkEvalTactic params
-  let (methods, ctx, state) ← liftMetaM <| GrindM.runAtGoal mvarId params (evalTactic? := some evalTactic) fun goal => do
-    let methods ← getMethods
-    -- **Note**: We use `withCheapCasesOnly` to ensure multiple goals are not created.
-    -- We will add support for this case in the future.
-    let (goal, _) ← withCheapCasesOnly <| SearchM.run goal do
-      intros 0; discard <| assertAll
-      getGoal
-    let goals := if goal.inconsistent then [] else [goal]
-    let ctx ← readThe Meta.Grind.Context
-    let state ← get
-    pure (methods, ctx, { state, goals })
+  /-
+  **Note**: We don't want to close branches using `sorry` after applying `intros + assertAll`.
+  Reconsider the option `useSorry`.
+  -/
+  let params' := { params with config.useSorry := false }
+  let (methods, ctx, state) ← liftMetaM <| GrindM.runAtGoal mvarId params' (evalTactic? := some evalTactic) fun goal => do
+      let a : Action := Action.intros 0 >> Action.assertAll
+      let goals ← match (← a.run goal) with
+        | .closed _ => pure []
+        | .stuck gs => pure gs
+      let methods ← getMethods
+      let ctx ← readThe Meta.Grind.Context
+      /- Restore original config -/
+      let ctx := { ctx with config := params.config }
+      let state ← get
+      pure (methods, ctx, { state, goals })
   let tctx ← read
   k { tctx with methods, ctx, params } |>.run state
 

src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean

@@ -135,16 +135,13 @@ def logTheoremAnchor (proof : Expr) : TermElabM Unit := do
   Term.addTermInfo' stx proof
 
 def ematchThms (only : Bool) (thms : Array EMatchTheorem) : GrindTacticM Unit := do
+  -- **TODO**: add `instantiate` action that takes `thms`
   let progress ← liftGoalM do
     let thms ← thms.mapM (preprocessTheorem · 0)
     if only then ematchOnly thms else ematch thms
   unless progress do
     throwError "`instantiate` tactic failed to instantiate new facts, use `show_patterns` to see active theorems and their patterns."
-  let goal ← getMainGoal
-  let (goal, _) ← liftGrindM <| withCheapCasesOnly <| SearchM.run goal do
-    discard <| assertAll
-    getGoal
-  replaceMainGoal [goal]
+  liftAction Action.assertAll
 
 @[builtin_grind_tactic instantiate] def evalInstantiate : GrindTactic := fun stx => withMainContext do
   let `(grind| instantiate $[ only%$only ]? $[ approx ]? $[ [ $[$thmRefs?:thm],* ] ]?) := stx | throwUnsupportedSyntax
@@ -268,30 +265,28 @@ def logAnchor (c : SplitInfo) : TermElabM Unit := do
     -/
     Term.addTermInfo' stx e (isDisplayableTerm := True)
 
+def split? (c : SplitInfo) : Action := fun goal kna kp => do
+  let (.ready numCases isRec _, goal) ← GoalM.run goal (checkSplitStatus c)
+    | throwError "`cases` tactic failed, case-split is not ready{indentExpr c.getExpr}"
+  let gen := goal.getGeneration c.getExpr
+  let genNew := if numCases > 1 || isRec then gen+1 else gen
+  let a : Action :=
+    Action.splitCore c numCases isRec (stopAtFirstFailure := false) (compress := false) >> Action.intros genNew >> Action.assertAll
+  a goal kna kp
+
 @[builtin_grind_tactic cases] def evalCases : GrindTactic := fun stx => do
   let `(grind| cases #$anchor:hexnum) := stx | throwUnsupportedSyntax
   let anchorRef ← elabAnchorRef anchor
   let goal ← getMainGoal
   let candidates := goal.split.candidates
-  let (c, goals, genNew) ← liftSearchM do
+  let c ← liftGrindM <| goal.withContext do
     for c in candidates do
       let anchor ← c.getAnchor
       if anchorRef.matches anchor then
-        let some result ← split? c
-          | throwError "`cases` tactic failed, case-split is not ready{indentExpr c.getExpr}"
-        return (c, result)
+        return c
     throwError "`cases` tactic failed, invalid anchor"
   goal.withContext <| withRef anchor <| logAnchor c
-  let goals ← goals.filterMapM fun goal => do
-    let goal := { goal with ematch.num := 0 }
-    let (goal, _) ← liftGrindM <| SearchM.run goal do
-      intros genNew; discard <| assertAll
-      getGoal
-    if goal.inconsistent then
-      return none
-    else
-      return some goal
-  replaceMainGoal goals
+  liftAction <| split? c
 
 def mkCasesSuggestions (candidates : Array SplitCandidateWithAnchor) (numDigits : Nat) : MetaM (Array Tactic.TryThis.Suggestion) := do
   candidates.mapM fun { anchor, e, .. } => do

src/Lean/Elab/Tactic/Grind/Have.lean

@@ -39,10 +39,8 @@ where
   let goal ← getMainGoal
   let mvarId ← goal.mvarId.assert n t v
   let goal := { goal with mvarId }
-  let (goal, _) ← liftGrindM <| withCheapCasesOnly <| SearchM.run goal do
-    intros 0
-    getGoal
   replaceMainGoal [goal]
+  liftAction <| Action.intros 0
 
 @[builtin_grind_tactic Parser.Tactic.Grind.haveSilent] def evalHaveSilent : GrindTactic := fun stx => withMainContext do
   let `(grind| have $[$id?:ident]? : $prop:term) := stx | throwUnsupportedSyntax
@@ -61,9 +59,7 @@ where
   let v ← instantiateMVars mvar
   let mvarId ← goal.mvarId.assert id prop v
   let goal := { goal with mvarId }
-  let (goal, _) ← liftGrindM <| withCheapCasesOnly <| SearchM.run goal do
-    intros 0
-    getGoal
   setGoals (goal :: goals)
+  liftAction <| Action.intros 0
 
 end Lean.Elab.Tactic.Grind

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

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Init.Grind.Lemmas
-public import Lean.Meta.Tactic.Grind.SearchM
 public import Lean.Meta.Tactic.Grind.Action
 import Lean.Meta.Tactic.Apply
 import Lean.Meta.Tactic.Grind.Simp
@@ -300,114 +299,4 @@ def assertAll : Action :=
 
 end Action
 
-/-!
-**------------------------------------------**
-**------------------------------------------**
-**TODO** Delete rest of the file
-**------------------------------------------**
-**------------------------------------------**
--/
-
-private def applyCases? (fvarId : FVarId) (generation : Nat) : SearchM Bool := withCurrGoalContext do
-  /-
-  Remark: we used to use `whnfD`. This was a mistake, we don't want to unfold user-defined abstractions.
-  Example: `a ∣ b` is defined as `∃ x, b = a * x`
-  -/
-  let type ← whnf (← fvarId.getType)
-  if isEagerCasesCandidate (← getGoal) type then
-    if (← cheapCasesOnly) then
-      unless (← isCheapInductive type) do
-        return false
-    if let .const declName _ := type.getAppFn then
-      saveCases declName
-    let goal ← getGoal
-    let mvarId ← goal.mkAuxMVar
-    let mvarIds ← cases mvarId (mkFVar fvarId)
-    let goals := mvarIds.map fun mvarId => { goal with mvarId }
-    mkChoice (mkMVar mvarId) goals generation
-    return true
-  return false
-
-/--
-Introduce new hypotheses (and apply `by_contra`) until goal is of the form `... ⊢ False`
-or is inconsistent.
--/
-def intros (generation : Nat) : SearchM Unit := withCurrGoalContext do
-  repeat
-    if (← isInconsistent) then
-      return ()
-    match (← introNext (← getGoal) generation) with
-    | .done goal =>
-      let goal ← exfalsoIfNotProp goal
-      if let some mvarId ← goal.mvarId.byContra? then
-        setGoal { goal with mvarId }
-      else
-        setGoal goal
-        return ()
-    | .newDepHyp goal =>
-      setGoal goal
-    | .newLocal fvarId goal =>
-      setGoal goal
-      discard <| applyCases? fvarId generation
-    | .newHyp fvarId goal =>
-      if let some goal ← applyInjection? goal fvarId then
-        setGoal goal
-      else
-        setGoal goal
-        if (← applyCases? fvarId generation) then
-          pure ()
-        else
-          addHypothesis fvarId generation
-
-/--
-Similar to `intros`, but returns `true` if new hypotheses have been added,
-and `false` otherwise.
--/
-def intros' (generation : Nat) : SearchM Bool := do
-  let target ← (← getGoal).mvarId.getType
-  if target.isFalse then return false
-  intros generation
-  return true
-
-/-- Asserts a new fact `prop` with proof `proof` to the given `goal`. -/
-private def assertAt (proof : Expr) (prop : Expr) (generation : Nat) : SearchM Unit := do
-  if isEagerCasesCandidate (← getGoal) prop then
-    let goal ← getGoal
-    let mvarId ← goal.mvarId.assert (← mkFreshUserName `h) prop proof
-    setGoal { goal with mvarId }
-    intros generation
-  else withCurrGoalContext do
-    let r ← preprocess prop
-    let prop' := r.expr
-    let proof' := mkApp4 (mkConst ``Eq.mp [levelZero]) prop r.expr (← r.getProof) proof
-    add prop' proof' generation
-
-/--
-Asserts next fact in the `goal` fact queue.
-Returns `true` if the queue was not empty and `false` otherwise.
--/
-def assertNext : SearchM Bool := do
-  if (← isInconsistent) then return false
-  let goal ← getGoal
-  let some (fact, newRawFacts) := goal.newRawFacts.dequeue?
-    | return false
-  setGoal { goal with newRawFacts }
-  withSplitSource fact.splitSource do
-    -- Remark: we should probably add `withGeneration`
-    assertAt fact.proof fact.prop fact.generation
-    return true
-
-/--
-Asserts all facts in the `goal` fact queue.
-Returns `true` if the queue was not empty and `false` otherwise.
--/
-def assertAll : SearchM Bool := do
-  let mut progress := false
-  repeat
-    if (← assertNext) then
-      progress := true
-    else
-      return progress
-  unreachable!
-
 end Lean.Meta.Grind

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

@@ -14,18 +14,24 @@ import Lean.Meta.Tactic.Grind.EMatchAction
 public section
 namespace Lean.Meta.Grind
 
-private partial def solve (generation : Nat) : SearchM Bool := withIncRecDepth do
-  unless (← get).choiceStack.isEmpty do
-    return false -- `splitNext` should have been configured to not create choice points
-  if (← getGoal).inconsistent then
-    return true
-  if (← intros' generation <||> assertAll <||> Solvers.check <||> splitNext <||> ematch) then
-    solve generation
-  else
-    return false
+/-
+This code is not used anymore.
+TODO: Decide whether we should delete it or not.
+-/
 
--- **TODO**: use `_action` instead of `solve`
-private def tryLookahead (e : Expr) (_action : Action) : GoalM Bool :=
+private abbrev maxIterations := 10000 -- **TODO**: Add option
+
+private def solve (goal : Goal) (generation : Nat) : GrindM (Option Goal) := do
+  let solvers ← Solvers.mkAction
+  let step : Action := solvers <|> Action.splitNext <|> Action.instantiate
+  let a := Action.intros generation >> Action.assertAll >> step.loop maxIterations
+  match (← a.run goal) with
+  | .closed _ => return none
+  | .stuck gs =>
+    let goal :: _ := gs | return some goal
+    return some goal
+
+private def tryLookahead (e : Expr) : GoalM Bool :=
   withTheReader Grind.Context
     (fun ctx => { ctx with config.qlia := true, cheapCases := true }) do
   -- TODO: if `e` is an arithmetic expression, we can avoid creating an auxiliary goal.
@@ -39,8 +45,7 @@ private def tryLookahead (e : Expr) (_action : Action) : GoalM Bool :=
     let mvar ← mkFreshExprSyntheticOpaqueMVar target tag
     let goalAux := { goal with mvarId := mvar.mvarId!, newFacts := {} }
     let gen ← getGeneration e
-    let (ok, _) ← (solve gen).run goalAux
-    if ok then
+    if (← solve goalAux gen).isNone then
       return some (← instantiateMVars mvar)
     else
       return none
@@ -52,13 +57,6 @@ private def tryLookahead (e : Expr) (_action : Action) : GoalM Bool :=
   else
     return false
 
-public abbrev maxIterations := 1000 -- **TODO**: Add option
-
-private def mkLookaheadAction : IO Action := do
-  let solvers ← Solvers.mkAction
-  let step : Action := Action.done <|> solvers <|> Action.splitNext <|> Action.instantiate
-  return step.loop maxIterations
-
 def lookahead : GoalM Bool := do
   unless (← getConfig).lookahead do
     return false
@@ -67,7 +65,6 @@ def lookahead : GoalM Bool := do
   let mut postponed := []
   let mut progress := false
   let infos := (← get).split.lookaheads
-  let action ← mkLookaheadAction
   modify fun s => { s with split.lookaheads := [] }
   for info in infos do
     if (← isInconsistent) then
@@ -77,7 +74,7 @@ def lookahead : GoalM Bool := do
     | .ready _ _ true
     | .notReady => postponed := info :: postponed
     | .ready _ _ false =>
-      if (← tryLookahead info.getExpr action) then
+      if (← tryLookahead info.getExpr) then
         progress := true
       else
         postponed := info :: postponed

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

@@ -1,216 +0,0 @@
-/-
-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
--/
-module
-prelude
-public import Lean.Meta.Tactic.Grind.Types
-import Lean.Util.ForEachExpr
-public section
-namespace Lean.Meta.Grind
-/--
-A `choice` (aka backtracking) point in the search tree.
--/
-structure Choice where
-  info?       : Option SplitInfo
-  /--
-  Goal where the case-split was performed.
-  Invariant: `goalPending.mvarId` is not assigned.
-  -/
-  goalPending : Goal
-  /--
-  Expression to be assigned to `goalPending.mvarId` if it is not possible to perform
-  non-chronological backtracking.
-  `proof` is often a `casesOn` application containing meta-variables.
-  -/
-  proof      : Expr
-  /--
-  Subgoals that still need to be processed.
-  -/
-  todo       : List Goal
-  generation : Nat
-  deriving Inhabited
-
-structure SearchM.State where
-  goal        : Goal
-  choiceStack : List Choice := []
-
-abbrev SearchM := StateRefT SearchM.State GrindM
-
-def getGoal : SearchM Goal :=
-  return (← get).goal
-
-def setGoal (goal : Goal) : SearchM Unit :=
-  modify fun s => { s with goal }
-
-abbrev withCurrGoalContext (x : SearchM α) : SearchM α := do
-  (← getGoal).mvarId.withContext x
-
-abbrev liftGoalM (x : GoalM α) : SearchM α := do
-  let (a, goal) ← withCurrGoalContext do x.runCore (← get).goal
-  modify fun s => { s with goal }
-  return a
-
-instance : MonadLift GoalM SearchM where
-  monadLift := liftGoalM
-
-@[inline] def SearchM.run (goal : Goal) (x : SearchM α) : GrindM (α × SearchM.State) :=
-  goal.mvarId.withContext do StateRefT'.run x { goal }
-
-/--
-Given a proof containing meta-variables corresponding to the given subgoals,
-create a choice point.
-- If there are no choice points, we just close the current goal using `proof`.
-- If there is only one subgoal `s`, we close the current goal using `proof`, and
-update current goal using `s`.
-- If there are more than one `s :: ss`, we create a choice point using the current
-goal as the pending goal, and update the current goal with `s`.
--/
-def mkChoice (proof : Expr) (subgoals : List Goal) (generation : Nat) (info? : Option SplitInfo := none) : SearchM Unit := do
-  assert! !(← isInconsistent)
-  match subgoals with
-  | [] =>
-    (← getGoal).mvarId.assign proof
-    modify fun s => { s with goal.inconsistent := true }
-  | [subgoal] =>
-    (← getGoal).mvarId.assign proof
-    setGoal subgoal
-  | subgoal :: subgoals =>
-    let goalPending ← getGoal
-    modify fun s => { s with
-      goal := subgoal
-      choiceStack := { info?, goalPending, proof, generation, todo := subgoals } :: s.choiceStack
-    }
-
-/--
-Returns the maximum free variable id occurring in `e`
--/
-private def findMaxFVarIdx? (e : Expr) : MetaM (Option Nat) := do
-  let go (e : Expr) : StateT (Option Nat) MetaM Bool := do
-    unless e.hasFVar do return false
-    let .fvar fvarId := e | return true
-    let localDecl ← fvarId.getDecl
-    modify fun
-      | none => some localDecl.index
-      | some index => some (max index localDecl.index)
-    return false
-  let (_, s?) ← e.forEach' go |>.run none
-  return s?
-
-private def resetChoiceStack : SearchM Unit :=
-  modify fun s => { s with choiceStack := [] }
-
-/--
-Use `falseProof` to close the last pending goal in the choice stack,
-and reset it.
-We use this function when `falseProof` does not have free variables.
--/
-private def closeLastPending (falseProof : Expr) : SearchM Unit := do
-  let choices := (← get).choiceStack
-  if h : choices.isEmpty then
-    return
-  else
-    let last := choices.getLast (ne_of_apply_ne List.isEmpty h) |>.goalPending
-    last.mvarId.assignFalseProof falseProof
-    resetChoiceStack
-
-/--
-Auxiliary function for implementing `nextGoal`.
-It is similar to `nextGoal`, but uses chronological backtracking.
-We use it when we cannot extract a proof of `False` from proof used to close the current goal.
-Returns `some gen` if a new goal was found for a choice point with generation `gen`,
-and returns `none` otherwise.
--/
-private def nextChronoGoal? : SearchM (Option Nat) := do
-  let mut choices := (← get).choiceStack
-  repeat
-    match choices with
-    | [] => return none
-    | choice :: choices' =>
-      match choice.todo with
-      | [] =>
-        -- Choice point has been fully resolved.
-        -- Go to next one.
-        choice.goalPending.mvarId.assign choice.proof
-        choices := choices'
-      | goal :: todo =>
-        let choice := { choice with todo }
-        modify fun s => { s with
-          goal
-          choiceStack := choice :: choices'
-        }
-        return some choice.generation
-  unreachable!
-
-private def isTargetFalse (mvarId : MVarId) : MetaM Bool := do
-  return (← mvarId.getType).isFalse
-
-private def getFalseProof? (mvarId : MVarId) : MetaM (Option Expr) := mvarId.withContext do
-  let proof ← instantiateMVars (mkMVar mvarId)
-  if (← isTargetFalse mvarId) then
-    return some proof
-  else if proof.isAppOfArity ``False.elim 2 || proof.isAppOfArity ``False.casesOn 2 then
-    return some proof.appArg!
-  else
-    return none
-
-/--
-Select the next goal to be processed from the `choiceStack`.
-This function assumes the current goal has been closed (i.e., `inconsistent` is `true`)
-Returns `some gen` if a new goal was found for a choice point with generation `gen`,
-and returns `none` otherwise.
--/
-def nextGoal? : SearchM (Option Nat) := do
-  let mut choices := (← get).choiceStack
-  if choices.isEmpty then
-    return none -- done
-  let goal := (← get).goal
-  assert! goal.inconsistent
-  let some falseProof ← getFalseProof? goal.mvarId
-    | nextChronoGoal?
-  let mut falseProof := falseProof
-  let some max ← goal.mvarId.withContext <| findMaxFVarIdx? falseProof
-    | closeLastPending falseProof; return none
-  let mut maxFVarIdx := max
-  repeat
-    let choice :: choices' := choices
-      | resetChoiceStack; return none
-    let mvarDecl ← choice.goalPending.mvarId.getDecl
-    let numIndices := mvarDecl.lctx.numIndices
-    if maxFVarIdx < numIndices then
-      -- `falseProof` can close `choice.goalPending` since all its free-variables are in scope.
-      choice.goalPending.mvarId.assignFalseProof falseProof
-      -- keep looking at next choice point
-      -- Remark: we may be able to find other choice points using falseProof.
-      choices := choices'
-    else match choice.todo with
-      | [] =>
-        -- All subgoals have been solved. We can finally assign `choice.proof` to `goalPending.mvarId`.
-        let proof ← instantiateMVars choice.proof
-        choice.goalPending.mvarId.assign proof
-        if (← isTargetFalse choice.goalPending.mvarId) then
-          -- `proof` is a proof of `False`, we can continue using non-chronological backtracking
-          falseProof := proof
-          let some max ← choice.goalPending.mvarId.withContext <| findMaxFVarIdx? falseProof
-            | closeLastPending falseProof; return none
-          maxFVarIdx := max
-          choices := choices'
-        else
-          -- `proof` is not a proof of `False`. Thus, we switch to chronological backtracking.
-          -- This case can only happen if we are using eager case-splitting with types with
-          -- more than one constructor.
-          modify fun s => { s with choiceStack := choices' }
-          return (← nextChronoGoal?)
-      | goal :: todo =>
-        -- Found `next` goal to be processed.
-        -- Update the current choice point, and current goal.
-        let choice := { choice with todo }
-        modify fun s => { s with
-          goal
-          choiceStack := choice :: choices'
-        }
-        return some choice.generation
-  unreachable!
-
-end Lean.Meta.Grind

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

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.SearchM
 public import Lean.Meta.Tactic.Grind.Action
 public import Lean.Meta.Tactic.Grind.Anchor
 import Lean.Meta.Tactic.Grind.Intro
@@ -491,62 +490,4 @@ def splitNext (stopAtFirstFailure := true) (compress := true) : Action := fun go
 
 end Action
 
-/-!
-**------------------------------------------**
-**------------------------------------------**
-**TODO** Delete rest of the file
-**------------------------------------------**
-**------------------------------------------**
--/
-
-/--
-Performs a case-split using `c`.
-Remarks:
-- `mvarId` is not necessarily `(← getGoal).mvarId`, `splitNext` creates an auxiliary meta-variable
-  to be able to implement non-chronological backtracking.
-- `numCases` and `isRec` are computed using `checkSplitStatus`.
--/
-private def splitCore (mvarId : MVarId) (c : SplitInfo) (numCases : Nat) (isRec : Bool) : SearchM (List Goal × Nat) := do
-  let cExpr := c.getExpr
-  let gen ← getGeneration cExpr
-  let genNew := if numCases > 1 || isRec then gen+1 else gen
-  saveSplitDiagInfo cExpr genNew numCases c.source
-  markCaseSplitAsResolved cExpr
-  trace_goal[grind.split] "{cExpr}, generation: {gen}"
-  let mvarIds ← if let .imp e h _ := c then
-    casesWithTrace mvarId (mkGrindEM (e.forallDomain h))
-  else if (← isMatcherApp cExpr) then
-    casesMatch mvarId cExpr
-  else
-    casesWithTrace mvarId (← mkCasesMajor cExpr)
-  let goal ← getGoal
-  let numSubgoals := mvarIds.length
-  let goals := mvarIds.mapIdx fun i mvarId => { goal with
-    mvarId
-    split.trace := { expr := cExpr, i, num := numSubgoals, source := c.source } :: goal.split.trace
-  }
-  return (goals, genNew)
-
-/--
-Selects a case-split from the list of candidates, and adds new choice point
-(aka backtracking point). Returns true if successful.
--/
-def splitNext : SearchM Bool := withCurrGoalContext do
-  let .some info numCases isRec _ ← selectNextSplit?
-    | return false
-  let mvarId ← (← getGoal).mkAuxMVar
-  let (goals, genNew) ← splitCore mvarId info numCases isRec
-  mkChoice (mkMVar mvarId) goals genNew (info? := some info)
-  intros genNew
-  return true
-
-/--
-Tries to perform a case-split using `c`. Returns `none` if `c` has already been resolved or
-is not ready.
--/
-def split? (c : SplitInfo) : SearchM (Option (List Goal × Nat)) := do
-  let .ready numCases isRec _ ← checkSplitStatus c | return none
-  let mvarId := (← getGoal).mvarId
-  return some (← splitCore mvarId c numCases isRec)
-
 end Lean.Meta.Grind