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

Equations

• Lean.Meta.Grind.TGrindStep = Lean.TSyntax `Lean.Parser.Tactic.Grind.grindStep

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

Equations

• (Lean.Meta.Grind.ActionResult.closed seq).toMessageData = Lean.toMessageData "closed " ++ Lean.toMessageData seq
• (Lean.Meta.Grind.ActionResult.stuck goals).toMessageData = Lean.toMessageData "stuck " ++ Lean.toMessageData (List.map (fun (x : Lean.Meta.Grind.Goal) => x.mvarId) goals)

instance Lean.Meta.Grind.instToMessageDataActionResult : ToMessageData ActionResult

Equations

• Lean.Meta.Grind.instToMessageDataActionResult = { toMessageData := Lean.Meta.Grind.ActionResult.toMessageData }

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

Equations

• Lean.Meta.Grind.Action.skip goal x✝ kp = kp goal

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

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

Equations

• Lean.Meta.Grind.Action.done goal kna x✝ = if goal.inconsistent = true then pure (Lean.Meta.Grind.ActionResult.closed []) else kna goal

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.

Equations

• x.andThen y goal kna kp = x goal kna fun (goal' : Lean.Meta.Grind.Goal) => y goal' kp kp

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

Equations

• Lean.Meta.Grind.Action.instAndThen = { andThen := fun (x : Lean.Meta.Grind.Action) (y : Unit → Lean.Meta.Grind.Action) => x.andThen (y ()) }

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

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

Equations

• x.orElse y goal kna kp = x goal (fun (goal : Lean.Meta.Grind.Goal) => y goal kna kp) kp

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

Equations

• Lean.Meta.Grind.Action.instOrElse = { orElse := fun (x : Lean.Meta.Grind.Action) (y : Unit → Lean.Meta.Grind.Action) => x.orElse (y ()) }

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

Repeats x up to n times while it remains applicable.

Equations

• One or more equations did not get rendered due to their size.

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

loop reference implementation without tryCatchRuntimeEx for proving sanity checking lemmas.

Equations

• Lean.Meta.Grind.Action.loopRef 0 x goal x✝ kp = kp goal
• Lean.Meta.Grind.Action.loopRef n_2.succ x goal x✝ kp = x goal kp fun (goal' : Lean.Meta.Grind.Goal) => Lean.Meta.Grind.Action.loopRef n_2 x goal' kp kp

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

Runs action a on the given goal.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• x.skipIfNA goal x✝ kp = x goal kp kp

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

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

Equations

• Lean.Meta.Grind.Action.mkGrindStep t = Lean.mkNode `Lean.Parser.Tactic.Grind.grindStep #[t.raw, Lean.mkNullNode]

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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ₙ

Equations

• One or more equations did not get rendered due to their size.

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ₙ]

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.Action.concatTactic r mk = do let __do_lift ← Lean.Meta.Grind.getConfig if __do_lift.trace = true then pure r else pure r

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

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.Action.checkSeqAt s? goal seq = pure 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

Equations

• One or more equations did not get rendered due to their size.

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

Helper action for satellite solvers that use CheckResult.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

Some sanity check properties.

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