feat: grind interactive mode basic tactics (#10677)

This PR implements the basic tactics for the new `grind` interactive
mode. While many additional `grind` tactics will be added later, the
foundational framework is already operational. The following `grind`
tactics are currently implemented: `skip`, `done`, `finish`, `lia`, and
`ring`.
This PR also removes the notion of `grind` fallback procedure since it
is subsumed by the new framework. Examples:
```lean
example (x y : Nat) : x ≥ y + 1 → x > 0 := by
  grind => skip; lia; done

open Lean Grind

example [CommRing α] (a b c : α)
  : a + b + c = 3 →
    a^2 + b^2 + c^2 = 5 →
    a^3 + b^3 + c^3 = 7 →
    a^4 + b^4 + c^4 = 9 := by
  grind => ring
```

src/Init/Grind/Interactive.lean

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Init.Tactics
-public meta import Init.Meta
 public section
 namespace Lean.Parser.Tactic.Grind
 
@@ -18,12 +17,19 @@ syntax grindSeq1Indented := sepBy1IndentSemicolon(grind)
 syntax grindSeqBracketed := "{" withoutPosition(sepByIndentSemicolon(grind)) "}"
 syntax grindSeq := grindSeqBracketed <|> grindSeq1Indented
 
+/-- `(grindSeq)` runs the `grindSeq` in sequence on the current list of targets.
+This is pure grouping with no added effects. -/
+syntax (name := paren) "(" withoutPosition(grindSeq) ")" : grind
+
 /-- `skip` does nothing. -/
 syntax (name := skip) "skip" : grind
 /-- `lia` linear integer arithmetic. -/
 syntax (name := lia) "lia" : grind
 /-- `ring` (commutative) rings and fields. -/
 syntax (name := ring) "ring" : grind
+/-- `done` succeeds iff there are no remaining goals. -/
+syntax (name := done) "done" : grind
+
 /-- `finish` tries to close the current goal using `grind`'s default strategy -/
 syntax (name := finish) "finish" : grind
 
@@ -32,7 +38,4 @@ syntax (name := «have») "have" letDecl : grind
 /-- Executes the given tactic block to close the current goal. -/
 syntax (name := nestedTacticCore) "tactic" " => " tacticSeq : grind
 
-/-- `grind` interactive mode -/
-syntax (name := grind) "grind" " => " grindSeq : tactic
-
 end Lean.Parser.Tactic.Grind

src/Init/Grind/Tactics.lean

@@ -5,10 +5,10 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Init.Grind.Attr
 public import Init.Core
+public import Init.Grind.Attr
+public import Init.Grind.Interactive
 public section
-
 namespace Lean.Grind
 /--
 The configuration for `grind`.
@@ -219,6 +219,8 @@ when selecting patterns.
 syntax grindLemmaMin := ppGroup("!" (Attr.grindMod ppSpace)? ident)
 syntax grindParam    := grindErase <|> grindLemma <|> grindLemmaMin
 
+open Parser.Tactic.Grind
+
 /--
 `grind` is a tactic inspired by modern SMT solvers. **Picture a virtual whiteboard**:
 every time grind discovers a new equality, inequality, or logical fact,
@@ -489,7 +491,7 @@ example (as : Array α) (lo hi i j : Nat) :
 syntax (name := grind)
   "grind" optConfig (&" only")?
   (" [" withoutPosition(grindParam,*) "]")?
-  (&" on_failure " term)? : tactic
+  (" => " grindSeq)? : tactic
 
 /--
 `grind?` takes the same arguments as `grind`, but reports an equivalent call to `grind only`
@@ -499,7 +501,7 @@ theorems in a local invocation.
 syntax (name := grindTrace)
   "grind?" optConfig (&" only")?
   (" [" withoutPosition(grindParam,*) "]")?
-  (&" on_failure " term)? : tactic
+  : tactic
 
 /--
 `cutsat` solves linear integer arithmetic goals.

src/Init/Notation.lean

@@ -6,13 +6,10 @@ Authors: Leonardo de Moura, Mario Carneiro
 Notation for operators defined at Prelude.lean
 -/
 module
-
 prelude
 public import Init.Coe
-
 public section
 set_option linter.missingDocs true -- keep it documented
-
 namespace Lean
 
 /--

src/Init/Tactics.lean

@@ -4,13 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
 module
-
 prelude
 public import Init.Notation
-
 public section
 set_option linter.missingDocs true -- keep it documented
-
 namespace Lean.Parser.Tactic
 
 /--

src/Lean/Elab/Tactic/Grind.lean

@@ -7,3 +7,4 @@ module
 prelude
 public import Lean.Elab.Tactic.Grind.Main
 public import Lean.Elab.Tactic.Grind.Basic
+public import Lean.Elab.Tactic.Grind.BuiltinTactic

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

@@ -8,18 +8,21 @@ prelude
 public import Lean.Elab.Term
 public import Lean.Elab.Tactic.Basic
 public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Tactic.Grind.Main
+public import Lean.Meta.Tactic.Grind.SearchM
+import Lean.Meta.Tactic.Grind.Intro
 public section
 namespace Lean.Elab.Tactic.Grind
 open Meta
 
 structure Context extends Tactic.Context where
-  ctx    : Grind.Context
+  ctx    : Meta.Grind.Context
   methods: Grind.Methods
 
 open Meta.Grind (Goal)
 
 structure State where
-  state : Grind.State
+  state : Meta.Grind.State
   goals : List Goal
 
 structure SavedState where
@@ -173,6 +176,44 @@ instance : MonadBacktrack SavedState GrindTacticM where
   saveState := Grind.saveState
   restoreState b := b.restore
 
+/--
+Runs `x` with only the first unsolved goal as the goal.
+Fails if there are no goal to be solved.
+-/
+def focus (k : GrindTacticM α) : GrindTacticM α := do
+  let mvarId :: mvarIds ← getUnsolvedGoals
+    | throwNoGoalsToBeSolved
+  setGoals [mvarId]
+  let a ← k
+  let mvarIds' ← getUnsolvedGoals
+  setGoals (mvarIds' ++ mvarIds)
+  pure a
+
+/--
+Runs `tactic` with only the first unsolved goal as the goal, and expects it leave no goals.
+Fails if there are no goal to be solved.
+-/
+def focusAndDone (tactic : GrindTacticM α) : GrindTacticM α :=
+  focus do
+    let a ← tactic
+    done
+    pure a
+
+/-- Close the main goal using the given tactic. If it fails, log the error and `admit` -/
+def closeUsingOrAdmit (tac : GrindTacticM Unit) : GrindTacticM Unit := do
+  /- Important: we must define `closeUsingOrAdmit` before we define
+     the instance `MonadExcept` for `GrindTacticM` since it backtracks the state including error messages. -/
+  let goal :: goals ← getUnsolvedGoals | throwNoGoalsToBeSolved
+  tryCatchRuntimeEx
+    (focusAndDone tac)
+    fun ex => do
+      if (← read).recover then
+        logException ex
+        admitGoal goal.mvarId
+        setGoals goals
+      else
+        throw ex
+
 /--
 Non-backtracking `try`/`catch`.
 -/
@@ -270,4 +311,48 @@ def tryTactic (tac : GrindTacticM α) : GrindTacticM Bool := do
   catch _ =>
     pure false
 
+open Grind
+
+def liftGrindM (k : GrindM α) : GrindTacticM α := do
+  let ctx ← read
+  let s ← get
+  let (a, state) ← liftMetaM <| k ctx.methods.toMethodsRef ctx.ctx |>.run s.state
+  modify fun s => { s with state }
+  return a
+
+def replaceMainGoal (goals : List Goal) : GrindTacticM Unit := do
+  let goals := goals.filter fun goal => !goal.inconsistent
+  let (_ :: goals') ← getGoals | throwNoGoalsToBeSolved
+  modify fun s => { s with goals := goals ++ goals' }
+
+def liftGoalM (k : GoalM α) : GrindTacticM α := do
+  let goal ← getMainGoal
+  let (a, goal) ← liftGrindM <| k.run goal
+  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 GrindTacticM.runAtGoal (mvarId : MVarId) (params : Params) (k : GrindTacticM α) : TacticM (α × State) := do
+  let (methods, ctx, state) ← liftMetaM <| GrindM.runAtGoal mvarId params fun goal => do
+    let methods ← getMethods
+    let ctx ← readThe Meta.Grind.Context
+    let state ← get
+    -- **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
+      getGoal
+    let goals := if goal.inconsistent then [] else [goal]
+    pure (methods, ctx, { state, goals })
+  let tctx ← read
+  k { tctx with methods, ctx } |>.run state
+
 end Lean.Elab.Tactic.Grind

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

@@ -0,0 +1,60 @@
+/-
+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.Elab.Tactic.Grind.Basic
+import Init.Grind.Interactive
+import Lean.Meta.Tactic.Grind.Solve
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Search
+import Lean.Meta.Tactic.Grind.Arith.CommRing.EqCnstr
+namespace Lean.Elab.Tactic.Grind
+
+def evalSepTactics (stx : Syntax) : GrindTacticM Unit := do
+  for arg in stx.getArgs, i in *...stx.getArgs.size do
+    if i % 2 == 0 then
+      evalGrindTactic arg
+    else
+      saveTacticInfoForToken arg
+
+@[builtin_grind_tactic grindSeq1Indented]
+def evalGrindSeq1Indented : GrindTactic := fun stx =>
+  evalSepTactics stx[0]
+
+@[builtin_grind_tactic grindSeqBracketed]
+def evalGrindSeqBracketed : GrindTactic := fun stx => do
+  let initInfo ← mkInitialTacticInfo stx[0]
+  withRef stx[2] <| closeUsingOrAdmit do
+    -- save state before/after entering focus on `{`
+    withInfoContext (pure ()) initInfo
+    evalSepTactics stx[1]
+
+@[builtin_grind_tactic grindSeq]
+def evalGrindSeq : GrindTactic := fun stx =>
+  evalGrindTactic stx[0]
+
+@[builtin_grind_tactic Parser.Tactic.Grind.«done»] def evalDone : GrindTactic := fun _ =>
+  done
+
+@[builtin_grind_tactic skip] def evalSkip : GrindTactic := fun _ =>
+  return ()
+
+@[builtin_grind_tactic paren] def evalParen : GrindTactic := fun stx =>
+  evalGrindTactic stx[1]
+
+open Meta Grind
+
+@[builtin_grind_tactic finish] def evalFinish : GrindTactic := fun _ => do
+  let goal ← getMainGoal
+  let goal? ← liftGrindM <| solve goal
+  replaceMainGoal goal?.toList
+
+@[builtin_grind_tactic lia] def evalLIA : GrindTactic := fun _ => do
+  liftGoalM <| discard <| Arith.Cutsat.check
+
+@[builtin_grind_tactic ring] def evalRing : GrindTactic := fun _ => do
+  liftGoalM <| discard <| Arith.CommRing.check
+
+end Lean.Elab.Tactic.Grind

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

@@ -12,6 +12,7 @@ public import Lean.Elab.Command
 public import Lean.Elab.Tactic.Basic
 public import Lean.Elab.Tactic.Config
 import Lean.Meta.Tactic.Grind.SimpUtil
+import Lean.Elab.Tactic.Grind.Basic
 import Lean.Elab.MutualDef
 meta import Lean.Meta.Tactic.Grind.Parser
 public section
@@ -215,58 +216,53 @@ def grind
     (mvarId : MVarId) (config : Grind.Config)
     (only : Bool)
     (ps   :  TSyntaxArray ``Parser.Tactic.grindParam)
-    (fallback : Grind.Fallback) : TacticM Grind.Trace := do
+    (seq? : Option (TSyntax `Lean.Parser.Tactic.Grind.grindSeq))
+    : TacticM Grind.Trace := do
+  if debug.terminalTacticsAsSorry.get (← getOptions) then
+    mvarId.admit
+    return {}
   mvarId.withContext do
     let params ← mkGrindParams config only ps
     let type ← mvarId.getType
     let mvar' ← mkFreshExprSyntheticOpaqueMVar type
-    let result ← Grind.main mvar'.mvarId! params fallback
-    if result.hasFailed then
-      throwError "`grind` failed\n{← result.toMessageData}"
-    trace[grind.debug.proof] "{← instantiateMVars mvar'}"
-    -- `grind` proofs are often big, if `abstractProof` is true, we create an auxiliary theorem.
-    let e ← if !config.abstractProof then
-      instantiateMVarsProfiling mvar'
-    else if (← isProp type) then
-      mkAuxTheorem type (← instantiateMVarsProfiling mvar') (zetaDelta := true)
+    let finalize (result : Grind.Result) : TacticM Grind.Trace := do
+      if result.hasFailed then
+        throwError "`grind` failed\n{← result.toMessageData}"
+      trace[grind.debug.proof] "{← instantiateMVars mvar'}"
+      -- `grind` proofs are often big, if `abstractProof` is true, we create an auxiliary theorem.
+      let e ← if !config.abstractProof then
+        instantiateMVarsProfiling mvar'
+      else if (← isProp type) then
+        mkAuxTheorem type (← instantiateMVarsProfiling mvar') (zetaDelta := true)
+      else
+        let auxName ← Term.mkAuxName `grind
+        mkAuxDefinition auxName type (← instantiateMVarsProfiling mvar') (zetaDelta := true)
+      mvarId.assign e
+      return result.trace
+    if let some seq := seq? then
+      let (result, _) ← Grind.GrindTacticM.runAtGoal mvar'.mvarId! params do
+        Grind.evalGrindTactic seq
+        -- **Note**: We are returning only the first goal that could not be solved.
+        let goal? := if let goal :: _ := (← get).goals then some goal else none
+        Grind.liftGrindM <| Grind.mkResult params goal?
+      finalize result
     else
-      let auxName ← Term.mkAuxName `grind
-      mkAuxDefinition auxName type (← instantiateMVarsProfiling mvar') (zetaDelta := true)
-    mvarId.assign e
-    return result.trace
-
-private def elabFallback (fallback? : Option Term) : TermElabM (Grind.GoalM Unit) := do
-  let some fallback := fallback? | return (pure ())
-  let type := mkApp (mkConst ``Grind.GoalM) (mkConst ``Unit)
-  let value ← withLCtx {} {} do Term.elabTermAndSynthesize fallback type
-  let auxDeclName ← if let .const declName _ := value then
-    pure declName
-  else
-    let auxDeclName ← Term.mkAuxName `_grind_fallback
-    let decl := Declaration.defnDecl {
-      name := auxDeclName
-      levelParams := []
-      type, value, hints := .opaque, safety := .safe
-    }
-    modifyEnv (addMeta · auxDeclName)
-    addAndCompile decl
-    pure auxDeclName
-  unsafe evalConst (Grind.GoalM Unit) auxDeclName
+      let result ← Grind.main mvar'.mvarId! params
+      finalize result
 
 def evalGrindCore
     (ref : Syntax)
     (config : Grind.Config)
     (only : Option Syntax)
-    (params : Option (Syntax.TSepArray `Lean.Parser.Tactic.grindParam ","))
-    (fallback? : Option Term)
+    (params? : Option (Syntax.TSepArray `Lean.Parser.Tactic.grindParam ","))
+    (seq? : Option (TSyntax `Lean.Parser.Tactic.Grind.grindSeq))
     : TacticM Grind.Trace := do
-  let fallback ← elabFallback fallback?
   let only := only.isSome
-  let params := if let some params := params then params.getElems else #[]
+  let params := if let some params := params? then params.getElems else #[]
   if Grind.grind.warning.get (← getOptions) then
     logWarningAt ref "The `grind` tactic is new and its behavior may change in the future. This project has used `set_option grind.warning true` to discourage its use."
   withMainContext do
-    let result ← grind (← getMainGoal) config only params fallback
+    let result ← grind (← getMainGoal) config only params seq?
     replaceMainGoal []
     return result
 
@@ -291,7 +287,6 @@ def getGrindParams (stx : TSyntax `tactic) : Array Syntax :=
 
 def mkGrindOnly
     (config : TSyntax ``Lean.Parser.Tactic.optConfig)
-    (fallback? : Option Term)
     (trace : Grind.Trace)
     : MetaM (TSyntax `tactic) := do
   let mut params := #[]
@@ -340,26 +335,23 @@ def mkGrindOnly
       let decl : Ident := mkIdent (← unresolveNameGlobalAvoidingLocals declName)
       let param ← `(Parser.Tactic.grindParam| cases $decl)
       params := params.push param
-  let result ← if let some fallback := fallback? then
-    `(tactic| grind $config:optConfig only on_failure $fallback)
-  else
-    `(tactic| grind $config:optConfig only)
+  let result ← `(tactic| grind $config:optConfig only)
   return setGrindParams result params
 
 @[builtin_tactic Lean.Parser.Tactic.grind] def evalGrind : Tactic := fun stx => do
   match stx with
-  | `(tactic| grind $config:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? $[on_failure $fallback?]?) =>
+  | `(tactic| grind $config:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? $[=> $seq:grindSeq]?) =>
     let config ← elabGrindConfig config
-    discard <| evalGrindCore stx config only params fallback?
+    discard <| evalGrindCore stx config only params seq
   | _ => throwUnsupportedSyntax
 
 @[builtin_tactic Lean.Parser.Tactic.grindTrace] def evalGrindTrace : Tactic := fun stx => do
   match stx with
-  | `(tactic| grind?%$tk $configStx:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? $[on_failure $fallback?]?) =>
+  | `(tactic| grind?%$tk $configStx:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]?) =>
     let config ← elabGrindConfig configStx
     let config := { config with trace := true }
-    let trace ← evalGrindCore stx config only params fallback?
-    let stx ← mkGrindOnly configStx fallback? trace
+    let trace ← evalGrindCore stx config only params none
+    let stx ← mkGrindOnly configStx trace
     Tactic.TryThis.addSuggestion tk stx (origSpan? := ← getRef)
   | _ => throwUnsupportedSyntax
 

src/Lean/Elab/Tactic/Try.lean

@@ -203,8 +203,8 @@ private def evalSuggestAtomic (tac : TSyntax `tactic) : TacticM (TSyntax `tactic
 
 private def grindTraceToGrind (tac : TSyntax `tactic) : TacticM (TSyntax `tactic) := do
   match tac with
-  | `(tactic| grind? $config:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? $[on_failure $fallback?]?) =>
-    `(tactic| grind $config:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? $[on_failure $fallback?]?)
+  | `(tactic| grind? $config:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]?) =>
+    `(tactic| grind $config:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]?)
   | _ => throwUnsupportedSyntax
 
 private def simpTraceToSimp (tac : TSyntax `tactic) : TacticM (TSyntax `tactic) := do
@@ -384,14 +384,14 @@ where
 
 private def evalSuggestGrindTrace : TryTactic := fun tac => do
   match tac with
-  | `(tactic| grind? $configStx:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? $[on_failure $fallback?]?) =>
+  | `(tactic| grind? $configStx:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]?) =>
     let config ← elabGrindConfig configStx
     let config := { config with trace := (← read).config.only, verbose := false }
     let tac ← grindTraceToGrind tac
-    let trace ← evalGrindCore tac config only params fallback?
+    let trace ← evalGrindCore tac config only params none
     trace[try.debug] "`grind` succeeded"
     if (← read).config.only then
-      let tac' ← mkGrindOnly configStx fallback? trace
+      let tac' ← mkGrindOnly configStx trace
       mkTrySuggestions #[tac, tac']
     else
       return tac

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

@@ -48,10 +48,9 @@ def mkParams (config : Grind.Config) : MetaM Params := do
   let symPrios ← getGlobalSymbolPriorities
   return { config, norm, normProcs, symPrios }
 
-def mkMethods (fallback : Fallback) : CoreM Methods := do
+def mkMethods : CoreM Methods := do
   let builtinPropagators ← builtinPropagatorsRef.get
   return {
-    fallback
     propagateUp := fun e => do
       propagateForallPropUp e
       propagateReflCmp e
@@ -79,7 +78,7 @@ private def discharge? (e : Expr) : SimpM (Option Expr) := do
   else
     return none
 
-def GrindM.run (x : GrindM α) (params : Params) (fallback : Fallback) : MetaM α := do
+def GrindM.run (x : GrindM α) (params : Params) : MetaM α := do
   let (falseExpr, scState)  := shareCommonAlpha (mkConst ``False) {}
   let (trueExpr, scState)   := shareCommonAlpha (mkConst ``True) scState
   let (bfalseExpr, scState) := shareCommonAlpha (mkConst ``Bool.false) scState
@@ -92,7 +91,7 @@ def GrindM.run (x : GrindM α) (params : Params) (fallback : Fallback) : MetaM
   let simp := params.norm
   let config := params.config
   let symPrios := params.symPrios
-  x (← mkMethods fallback).toMethodsRef { config, simpMethods, simp, trueExpr, falseExpr, natZExpr, btrueExpr, bfalseExpr, ordEqExpr, intExpr, symPrios }
+  x (← mkMethods).toMethodsRef { config, simpMethods, simp, trueExpr, falseExpr, natZExpr, btrueExpr, bfalseExpr, ordEqExpr, intExpr, symPrios }
     |>.run' { scState }
 
 private def mkCleanState (mvarId : MVarId) (params : Params) : MetaM Clean.State := mvarId.withContext do
@@ -207,26 +206,28 @@ private def initCore (mvarId : MVarId) (params : Params) : GrindM Goal := do
   appendTagSuffix mvarId `grind
   mkGoal mvarId params
 
-def main (mvarId : MVarId) (params : Params) (fallback : Fallback) : MetaM Result := do profileitM Exception "grind" (← getOptions) do
-  if debug.terminalTacticsAsSorry.get (← getOptions) then
-    mvarId.admit
-    return {
-        failure? := none, issues := [], config := params.config, trace := {}, counters := {}, simp := {}, splitDiags := {}
-    }
-  let go : GrindM Result := withReducible do
-    let goal       ← initCore mvarId params
-    let failure?   ← solve goal
-    let issues     := (← get).issues
-    let trace      := (← get).trace
-    let counters   := (← get).counters
-    let splitDiags := (← get).splitDiags
-    let simp       := { (← get).simp with }
-    if failure?.isNone then
-      -- If there are no failures and diagnostics are enabled, we still report the performance counters.
-      if (← isDiagnosticsEnabled) then
-        if let some msg ← mkGlobalDiag counters simp splitDiags then
-          logInfo msg
-    return { failure?, issues, config := params.config, trace, counters, simp, splitDiags }
-  go.run params fallback
+def mkResult (params : Params) (failure? : Option Goal) : GrindM Result := do
+  let issues     := (← get).issues
+  let trace      := (← get).trace
+  let counters   := (← get).counters
+  let splitDiags := (← get).splitDiags
+  let simp       := { (← get).simp with }
+  if failure?.isNone then
+    -- If there are no failures and diagnostics are enabled, we still report the performance counters.
+    if (← isDiagnosticsEnabled) then
+      if let some msg ← mkGlobalDiag counters simp splitDiags then
+        logInfo msg
+  return { failure?, issues, config := params.config, trace, counters, simp, splitDiags }
+
+def GrindM.runAtGoal (mvarId : MVarId) (params : Params) (k : Goal → GrindM α) : MetaM α := do
+  let go : GrindM α := withReducible do
+    let goal ← initCore mvarId params
+    k goal
+  go.run params
+
+def main (mvarId : MVarId) (params : Params) : MetaM Result := do profileitM Exception "grind" (← getOptions) do
+  GrindM.runAtGoal mvarId params fun goal => do
+    let failure? ← solve goal
+    mkResult params failure?
 
 end Lean.Meta.Grind

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

@@ -124,7 +124,7 @@ private def closeLastPending (falseProof : Expr) : SearchM Unit := do
     resetChoiceStack
 
 /--
-Auxliary function for implementing `nextGoal`.
+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`,

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

@@ -13,16 +13,6 @@ import Lean.Meta.Tactic.Grind.Lookahead
 import Lean.Meta.Tactic.Grind.Intro
 public section
 namespace Lean.Meta.Grind
-def tryFallback : GoalM Bool := do
-  (← getMethods).fallback
-  if (← isInconsistent)  then
-    return true
-  if (← (← get).mvarId.isAssigned) then
-    -- User-provided fallback may not have properly set `inconsistent` flag.
-    modify fun s => { s with inconsistent := true }
-    return true
-  return false
-
 /--
 Try to solve/close the given goal.
 Returns `some goal` if this subgoal failed to be closed,
@@ -50,7 +40,7 @@ where
         else
           break
       if (← assertAll <||> Solvers.check <||> ematch <||> lookahead <||> splitNext
-           <||> Solvers.mbtc <||> tryFallback) then
+           <||> Solvers.mbtc) then
         continue
       return some (← getGoal) -- failed
     return none -- solved

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

@@ -276,6 +276,9 @@ def getIntExpr : GrindM Expr := do
 def cheapCasesOnly : GrindM Bool :=
   return (← readThe Context).cheapCases
 
+def withCheapCasesOnly (k : GrindM α) : GrindM α :=
+  withTheReader Grind.Context (fun ctx => { ctx with cheapCases := true }) k
+
 def reportMVarInternalization : GrindM Bool :=
   return (← readThe Context).reportMVarIssue
 
@@ -1288,12 +1291,10 @@ def forEachEqcRoot (f : ENode → GoalM Unit) : GoalM Unit := do
       f n
 
 abbrev Propagator := Expr → GoalM Unit
-abbrev Fallback := GoalM Unit
 
 structure Methods where
   propagateUp   : Propagator := fun _ => return ()
   propagateDown : Propagator := fun _ => return ()
-  fallback      : Fallback := pure ()
   deriving Inhabited
 
 def Methods.toMethodsRef (m : Methods) : MethodsRef :=
@@ -1311,10 +1312,6 @@ def propagateUp (e : Expr) : GoalM Unit := do
 def propagateDown (e : Expr) : GoalM Unit := do
   (← getMethods).propagateDown e
 
-def applyFallback : GoalM Unit := do
-  let fallback : GoalM Unit := (← getMethods).fallback
-  fallback
-
 def Goal.getGeneration (goal : Goal) (e : Expr) : Nat :=
   if let some n := goal.getENode? e then
     n.generation

tests/lean/run/grind_canon_insts.lean

@@ -1,5 +1,6 @@
 module
 public meta import Lean.Meta.Tactic.Grind
+#exit -- TODO: reenable after we add support for running code in interactive mode
 public section
 set_option grind.debug true
 

tests/lean/run/grind_canon_types.lean

@@ -1,5 +1,6 @@
 module
 meta import Lean.Meta.Tactic.Grind
+#exit -- TODO: reenable after we add support for running code in interactive mode
 
 def g (s : Type) := s
 def f (a : α) := a

tests/lean/run/grind_congr.lean

@@ -1,5 +1,7 @@
 module
 meta import Lean
+#exit
+
 def f (a : Nat) := a + a + a
 def g (a : Nat) := a + a
 

tests/lean/run/grind_diseq_api.lean

@@ -1,81 +0,0 @@
-module
-meta import Lean
-
-opaque a : Nat
-opaque b : Nat
-
--- Prints the equivalence class containing a `f` application
-open Lean Meta Grind in
-meta def fallback : Fallback := do
-  let a ← shareCommon <| mkConst ``a
-  let b ← shareCommon <| mkConst ``b
-  let some h ← mkDiseqProof? a b |
-    throwError "terms are not diseq"
-  check h
-  trace[Meta.debug] "{h} : {← inferType h}"
-  assert! (← isDiseq a b)
-  assert! (← isDiseq b a)
-  let some h' ← mkDiseqProof? b a |
-    throwError "terms are not diseq"
-  let h' ← mkAppM ``Ne.symm #[h']
-  assert! (← isDefEq h h')
-  (← get).mvarId.admit
-
-set_option trace.Meta.debug true
-
-/--
-trace: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h_2 (Lean.Grind.ne_of_ne_of_eq_left h (Ne.symm h_1)) : a ≠ b
--/
-#guard_msgs (trace) in
-example (x y : Nat) : a = x → y ≠ x → b = y → False := by
-  grind on_failure fallback
-
-/--
-trace: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h_2 (Lean.Grind.ne_of_ne_of_eq_left h h_1) : a ≠ b
--/
-#guard_msgs (trace) in
-example (x y : Nat) : a = x → x ≠ y → b = y → False := by
-  grind on_failure fallback
-
-/--
-trace: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h_3 (Lean.Grind.ne_of_ne_of_eq_left (Eq.trans h (Eq.symm h_1)) h_2) : a ≠ b
--/
-#guard_msgs (trace) in
-example (x y z : Nat) : a = x → z = x → z ≠ y → b = y → False := by
-  grind on_failure fallback
-
-/-- trace: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_left h (Ne.symm h_1) : a ≠ b -/
-#guard_msgs (trace) in
-example (x : Nat) : a = x → b ≠ x → False := by
-  grind on_failure fallback
-
-/-- trace: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_left h h_1 : a ≠ b -/
-#guard_msgs (trace) in
-example (x : Nat) : a = x → x ≠ b → False := by
-  grind on_failure fallback
-
-
-/-- trace: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h h_1 : a ≠ b -/
-#guard_msgs (trace) in
-example (x : Nat) : b = x → a ≠ x → False := by
-  grind on_failure fallback
-
-/-- trace: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h (Ne.symm h_1) : a ≠ b -/
-#guard_msgs (trace) in
-example (x : Nat) : b = x → x ≠ a → False := by
-  grind on_failure fallback
-
-/-- trace: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_left h (Ne.symm h_1) : a ≠ b -/
-#guard_msgs (trace) in
-example (x : Nat) : a = x → b ≠ x → False := by
-  grind on_failure fallback
-
-/-- trace: [Meta.debug] h : ¬a = b -/
-#guard_msgs (trace) in
-example : a ≠ b → False := by
-  grind on_failure fallback
-
-/-- trace: [Meta.debug] Ne.symm h : a ≠ b -/
-#guard_msgs (trace) in
-example : b ≠ a → False := by
-  grind on_failure fallback

tests/lean/run/grind_interactive.lean

@@ -0,0 +1,48 @@
+/--
+error: `grind` failed
+case grind
+α : Type u
+op : α → α → α
+inst : Std.Associative op
+a b c d : α
+h : d = op b c
+h_1 : ¬op a d = op (op a b) c
+⊢ False
+[grind] Goal diagnostics
+  [facts] Asserted facts
+    [prop] Std.Associative op
+    [prop] d = op b c
+    [prop] ¬op a d = op (op a b) c
+  [eqc] True propositions
+    [prop] Std.Associative op
+  [eqc] False propositions
+    [prop] op a d = op (op a b) c
+  [eqc] Equivalence classes
+    [eqc] {d, op b c}
+  [assoc] Operator `op`
+    [diseqs] Disequalities
+      [_] op a d ≠ op a (op b c)
+-/
+#guard_msgs in
+example {α : Type u} (op : α → α → α) [Std.Associative op] (a b c d : α)
+    : d = op b c → op a d = op (op a b) c := by
+  grind => skip
+
+example {α : Type u} (op : α → α → α) [Std.Associative op] (a b c d : α)
+    : d = op b c → op a d = op (op a b) c := by
+  grind => finish
+
+example (x y : Nat) : x ≥ y + 1 → x > 0 := by
+  grind => lia
+
+example (x y : Nat) : x ≥ y + 1 → x > 0 := by
+  grind => skip; lia; done
+
+open Lean Grind
+
+example [CommRing α] (a b c : α)
+  : a + b + c = 3 →
+    a^2 + b^2 + c^2 = 5 →
+    a^3 + b^3 + c^3 = 7 →
+    a^4 + b^4 + c^4 = 9 := by
+  grind => ring

tests/lean/run/grind_many_eqs.lean

@@ -1,5 +1,5 @@
 module
-meta import Lean.Meta.Tactic.Grind
+set_option warn.sorry false
 
 def f (a : Nat) := a + a + a
 def g (a : Nat) := a + a
@@ -8,24 +8,13 @@ def h (n : Nat) : Prop :=
   | 0   => f 0 = f 1
   | n+1 => f (n+1) = f n ∧ g (2*n + 1) = g (2*n) ∧ h n
 
--- Prints the equivalence class containing a `f` application
-open Lean Meta Grind in
-meta def fallback (n : Nat) : Fallback := do
-  let f0 ← Grind.shareCommon (mkApp (mkConst ``f) (mkNatLit 0))
-  -- The `f 0` equivalence class contains `n+1` elements
-  assert! (← getEqc f0).length == n + 1
-  forEachENode fun node => do
-    if node.self.isApp && node.self.isAppOf ``g then
-      -- Any equivalence class containing a `g`-application contains 2 elements
-      assert! (← getEqc (← getRoot node.self)).length == 2
-  (← get).mvarId.admit
-
-set_option grind.debug true in
 example : h 5 → False := by
   simp [h]
-  grind on_failure fallback 5
+  -- TODO: use `grind => print_eqc; sorry` to display equivalence classes containing `f`-applications
+  sorry
 
 set_option maxRecDepth 2048
 example : h 100 → False := by
   simp [h]
-  grind on_failure fallback 100
+  -- TODO: use `grind => print_eqc; sorry` to display equivalence classes containing `f`-applications
+  sorry

tests/lean/run/grind_nested_proofs.lean

@@ -1,5 +1,6 @@
 module
 meta import Lean.Meta.Tactic.Grind
+#exit -- TODO: reenable after we add support for running code in interactive mode
 
 def f (α : Type) [Add α] (a : α) := a + a + a
 

tests/lean/run/grind_norm_levels.lean

@@ -1,19 +1,27 @@
 module
-meta import Lean.Meta.Tactic.Grind
-
 def g {α : Sort u} (a : α) := a
 
-open Lean Meta Grind in
-meta def fallback : Fallback := do
-  let nodes ← filterENodes fun e => return e.self.isApp && e.self.isAppOf ``g
-  trace[Meta.debug] "{nodes.toList.map (·.self)}"
-  (← get).mvarId.admit
-
--- `grind` final state must contain only two `g`-applications
-set_option trace.Meta.debug true in
 /--
-trace: [Meta.debug] [g (a, b), g (g (a, b))]
+error: `grind` failed
+case grind
+β : Type v
+α : Type u
+a c : α
+b d : β
+h : g (a, b) = (c, d)
+h_1 : g (g (a, b)) = (c, d)
+⊢ False
+[grind] Goal diagnostics
+  [facts] Asserted facts
+    [prop] g (a, b) = (c, d)
+    [prop] g (g (a, b)) = (c, d)
+  [eqc] Equivalence classes
+    [eqc] {c, (g (g (a, b))).fst, (g (a, b)).fst}
+      [eqc] {(c, d).fst}
+    [eqc] {d, (g (g (a, b))).snd, (g (a, b)).snd}
+      [eqc] {(c, d).snd}
+    [eqc] {g (g (a, b)), g (a, b), (c, d), ((g (g (a, b))).fst, (g (g (a, b))).snd), ((g (a, b)).fst, (g (a, b)).snd)}
 -/
-#guard_msgs (trace) in
+#guard_msgs in
 example {β : Type v} {α : Type u} (a c : α) (b d : β) : g.{max u v + 1} (a, b) = (c, d) → g (g.{max (u+1) (v+1)} (a, b)) = (c, d) → False := by
-  grind on_failure fallback
+  grind

tests/lean/run/grind_pp_attr.lean

@@ -10,7 +10,6 @@ def test (stx : Syntax) : CommandElabM Unit := do
   let st := fmt.pretty
   dbg_trace st
 
-
 /--
 info: @[grind =]
 example :=
@@ -74,8 +73,3 @@ example :=
 -/
 #guard_msgs in
 run_cmd test (← `(@[grind ← gen] example := 0))
-
-set_option hygiene false in
-/-- info: example := by grind [a] on_failure 3 -/
-#guard_msgs in
-run_cmd test (← `(example := by grind [a] on_failure 3))

tests/lean/run/grind_propagate_connectives.lean

@@ -1,100 +0,0 @@
-module
-meta import Lean.Meta.Tactic.Grind
-
-set_option trace.Meta.debug true
-
-open Lean Meta Grind in
-private meta def fallback : Fallback := do
-  let trueExprs := (← filterENodes fun e => return e.self.isFVar && (← isEqTrue e.self)).toList.map (·.self)
-  let falseExprs := (← filterENodes fun e => return e.self.isFVar && (← isEqFalse e.self)).toList.map (·.self)
-  trace[Meta.debug] "true:  {trueExprs}"
-  trace[Meta.debug] "false: {falseExprs}"
-  forEachEqcRoot fun n => do
-    unless (← isProp n.self) || (← isType n.self) || n.size == 1 do
-      let eqc ← getEqc n.self
-      trace[Meta.debug] eqc
-  (← get).mvarId.admit
-
-set_option grind.debug true
-set_option grind.debug.proofs true
-
-/--
-trace: [Meta.debug] true:  [q, w]
-[Meta.debug] false: [p, r]
--/
-#guard_msgs (trace) in
-example : (p ∨ (q ∧ ¬r ∧ w)) → ¬p → False := by
-  grind on_failure fallback
-
-
-/--
-trace: [Meta.debug] true:  [r]
-[Meta.debug] false: [p, q]
--/
-#guard_msgs (trace) in
-example : (p ∨ q ∨ r) → (p ∨ ¬q) → ¬p → False := by
-  grind on_failure fallback
-
-
-/--
-trace: [Meta.debug] true:  [r]
-[Meta.debug] false: [p₁, q]
--/
-#guard_msgs (trace) in
-example : ((p₁ ∧ p₂) ∨ q ∨ r) → (p₁ ∨ ¬q) → p₁ = False → False := by
-  grind on_failure fallback
-
-/--
-trace: [Meta.debug] true:  [r]
-[Meta.debug] false: [p₂, q]
--/
-#guard_msgs (trace) in
-example : ((p₁ ∧ p₂) ∨ q ∨ r) → ((p₂ ∧ p₁) ∨ ¬q) → p₂ = False → False := by
-  grind on_failure fallback
-
-/--
-trace: [Meta.debug] true:  [q, r]
-[Meta.debug] false: [p]
--/
-#guard_msgs (trace) in
-example (p q r : Prop) : p ∨ (q ↔ r) → p = False → q → False := by
-  grind on_failure fallback
-
-/--
-trace: [Meta.debug] true:  [r]
-[Meta.debug] false: [p, s]
--/
-#guard_msgs (trace) in
-example (p q r : Prop) : p ∨ ¬(s ∨ (p ↔ r)) → p = False → False := by
-  grind on_failure fallback
-
-/--
-trace: [Meta.debug] true:  [p]
-[Meta.debug] false: []
-[Meta.debug] [b, a]
--/
-#guard_msgs (trace) in
-example (p : Prop) (a : Vector Nat 5) (b : Vector Nat 6) : (p → a ≍ b) → p → False := by
-  grind on_failure fallback
-
-/--
-trace: [Meta.debug] true:  [p, q]
-[Meta.debug] false: [r]
--/
-#guard_msgs (trace) in
-example (p q r : Prop) : p ∨ (q ↔ r) → q → ¬r → False := by
-  grind on_failure fallback
-
-/--
-trace: [Meta.debug] hello world
-[Meta.debug] true:  [p, q]
-[Meta.debug] false: [r]
--/
-#guard_msgs (trace) in
-example (p q r : Prop) : p ∨ (q ↔ r) → ¬r → q → False := by
-  grind on_failure do
-    trace[Meta.debug] "hello world"
-    fallback
-
-example (a b : Nat) : (a = b) = (b = a) := by
-  grind

tests/lean/run/sharecommon_mpz.lean

@@ -3,7 +3,7 @@ import Lean
 open Lean Meta Tactic Grind
 
 def runGrind (x : GrindM α) : MetaM α := do
-  GrindM.run x (← mkParams {}) (pure ())
+  GrindM.run x (← mkParams {})
 
 @[noinline] def mkA (x : Nat) := x + 1