Action

Action is the control interface for grind’s search steps. It is defined in Continuation-Passing Style (CPS):

abbrev Action :=
  Goal → (kna : Goal → GrindM ActionResult) → (kp : Goal → GrindM ActionResult) → GrindM ActionResult

An Action receives: the current Goal, a continuation kna to run when the action is not applicable, and a continuation kp to run when it makes progress.

It returns an ActionResult:

• .closed seq: the goal was fully solved, and seq is the sequence of tactics that, if replayed, closes the goal.

• .stuck gs: search ran and got stuck at goals gs. Remark: actions such as splitNext can decide whether they stop at the first failure or not.

Why CPS?

Two core requirements motivated CPS:

• Non-chronological backtracking (NCB) for branching steps like splitNext. A branching action must be able to run the full continuation on each subgoal and decide—based on the entire downstream proof whether the case split is actually needed or not. CPS gives the action visibility and control over kp.

• Tactic script generation. Some leaves (e.g. ematch) should log only the facts/instantiations actually used by the final proof. Running the continuation first and then post-processing what happened lets an action commit exactly the steps that mattered.

Contract (what every Action must guarantee)

• Return exactly once. An action may call kp zero or more times internally (e.g. once per branch), but it must eventually return a single ActionResult.

• .stuck g and .closed seq reflect the final choice the action made after any internal calls to kp. Combinators reason only about this final result.

• When an action is not applicable, it must invoke kna and perform no observable effects.

Why Action is not a Monad

Although it looks like “a computation that can call a continuation”, Action is a control operator, not a lawful monad:

• Multi-shot continuations. splitNext legitimately calls kp multiple times (once per subgoal). Standard bind assumes a linear continuation. Duplicating the continuation breaks associativity (agreed?)

• Future inspection. Many actions decide what to keep/commit after seeing the entire result of kp (e.g., the generated proof term). That is delimited control (callCC/handlers) rather than plain monadic sequencing. It seems overkill to use callCC here.

@[reducible, inline]

abbrev Lean.Meta.Grind.TGrindStep : Type

def Lean.Meta.Grind.ActionResult.toMessageData : ActionResult → MessageData

instance Lean.Meta.Grind.instToMessageDataActionResult : ToMessageData ActionResult

def Lean.Meta.Grind.Action.skip : Action

def Lean.Meta.Grind.Action.done : Action

If the goal is already inconsistent, returns .closed []. Otherwise, executes then not applicable continuation.

def Lean.Meta.Grind.Action.andThen (x y : Action) : Action

x >> y, executes x and then y

• If x is not applicable, then x >> y is not applicable.
• If y is not applicable, it behaves like a skip.

instance Lean.Meta.Grind.Action.instAndThen : AndThen Action

def Lean.Meta.Grind.Action.orElse (x y : Action) : Action

Choice: tries x, if not applicable, tries y.

instance Lean.Meta.Grind.Action.instOrElse : OrElse Action

def Lean.Meta.Grind.Action.loop (n : Nat) (x : Action) : Action

Repeats x up to n times while it remains applicable.

def Lean.Meta.Grind.Action.loopRef (n : Nat) (x : Action) : Action

loop reference implementation without tryCatchRuntimeEx for proving sanity checking lemmas.

def Lean.Meta.Grind.Action.run (goal : Goal) (a : Action) : GrindM ActionResult

Runs action a on the given goal.

def Lean.Meta.Grind.Action.skipIfNA (x : Action) : Action

Executes x, but behaves like a skip if it is not applicable.

def Lean.Meta.Grind.Action.mkGrindStep (t : TGrind) : TGrindStep

TSyntax `grind => TSyntax `Lean.Parser.Tactic.Grind.grindStep

def Lean.Meta.Grind.Action.TGrindStep.getTactic : TGrindStep → TGrind

def Lean.Meta.Grind.Action.mkGrindSeq (s : List TGrind) : TSyntax `Lean.Parser.Tactic.Grind.grindSeq

def Lean.Meta.Grind.Action.mkGrindNext (s : List TGrind) : CoreM TGrind

Given [t₁, ..., tₙ], returns

· t₁
  ...
  tₙ

If the list is empty, it returns · done.

def Lean.Meta.Grind.Action.group : Action

If tracing is enabled and continuation produced .closed [t₁, ..., tₙ], returns the singleton sequence [t] where t is

· t₁
  ...
  tₙ

def Lean.Meta.Grind.Action.ungroup : Action

If tracing is enabled and continuation produced .closed [(next => t₁; ...; tₙ)] or its variant using · returns .close [t₁, ... tₙ]

def Lean.Meta.Grind.Action.concatTactic (r : ActionResult) (mk : GrindM TGrind) : GrindM ActionResult

Appends a new tactic syntax to a successful result. Used by leaf actions to record the tactic that produced progress. If (← getConfig).trace is false, it just returns r.

def Lean.Meta.Grind.Action.closeWith (mk : GrindM TGrind) : GrindM ActionResult

Returns .closed [← mk] if tracing is enabled, and .closed [] otherwise.

def Lean.Meta.Grind.Action.terminalAction (check : GoalM Bool) (mkTac : GrindM TGrind) : Action

A terminal action which closes the goal or not. This kind of action may make progress, but we only include mkTac into the resulting tactic sequence if it closed the goal.

def Lean.Meta.Grind.Action.saveStateIfTracing : GrindM (Option SavedState)

def Lean.Meta.Grind.Action.checkSeqAt (s? : Option SavedState) (goal : Goal) (seq : List TGrind) : GrindM Bool

Returns true if the tactic sequence seq closes goal starting at saved state s?. If s? is none just returns true.

def Lean.Meta.Grind.Action.checkTactic (warnOnly : Bool) : Action

Helper action that checks whether the resulting tactic script produced by its continuation can close the original goal. If warnOnly = true, just generates a warning message instead of an error

def Lean.Meta.Grind.Action.solverAction (check : GoalM CheckResult) (mkTac : GrindM TGrind) : Action

Helper action for satellite solvers that use CheckResult.

def Lean.Meta.Grind.Action.mbtc : Action

Some sanity check properties.

theorem Lean.Meta.Grind.Action.loop_skipIfNA {n : Nat} (a : Action) : (loopRef n a).skipIfNA = loopRef n a