Grind Goal API for Symbolic Simulation

This module provides an API for building symbolic simulation engines and verification condition generators on top of grind. It wraps Sym operations to work with grind's Goal type, enabling users to carry grind state through symbolic execution while using lightweight Sym operations for the main loop.

Typical usage pattern

let goal ← mkGoal mvarId
let .goal xs goal ← goal.introN 2 | failure
let .goal goal ← goal.simp methods | failure
let goal ← goal.internalizeAll
-- ... symbolic execution loop using goal.apply ...
let .closed ← goal.grind | failure

Design

Operations like introN, apply, and simp run in SymM for performance. internalize and grind run in GrindM to access the E-graph.

def Lean.Meta.Grind.mkGoal (mvarId : MVarId) : GrindM Goal

Creates a Goal from an MVarId, applying Sym preprocessing. Preprocessing ensures the goal is compatible with Sym operations.

Equations

• Lean.Meta.Grind.mkGoal mvarId = do let mvarId ← liftM (Lean.Meta.Sym.preprocessMVar mvarId) Lean.Meta.Grind.mkGoalCore mvarId

inductive Lean.Meta.Grind.IntrosResult : Type

• failed : IntrosResult
• goal (newDecls : Array FVarId) (goal : Goal) : IntrosResult

def Lean.Meta.Grind.Goal.introN (goal : Goal) (num : Nat) : Sym.SymM IntrosResult

Introduces num binders from the goal's target.

Equations

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

def Lean.Meta.Grind.Goal.intros (goal : Goal) (names : Array Name) : Sym.SymM IntrosResult

Introduces binders with the specified names.

Equations

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

inductive Lean.Meta.Grind.ApplyResult : Type

• failed : ApplyResult
• goals (subgoals : List Goal) : ApplyResult

def Lean.Meta.Grind.Goal.apply (goal : Goal) (rule : Sym.BackwardRule) : Sym.SymM ApplyResult

Applies a backward rule, returning subgoals on success.

Equations

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

inductive Lean.Meta.Grind.SimpGoalResult : Type

• noProgress : SimpGoalResult
• closed : SimpGoalResult
• goal (goal : Goal) : SimpGoalResult

def Lean.Meta.Grind.Goal.simp (goal : Goal) (methods : Sym.Simp.Methods := { }) (config : Sym.Simp.Config := { }) : Sym.SymM SimpGoalResult

Simplifies the goal using the given methods.

Equations

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

def Lean.Meta.Grind.Goal.simpIgnoringNoProgress (goal : Goal) (methods : Sym.Simp.Methods := { }) (config : Sym.Simp.Config := { }) : Sym.SymM SimpGoalResult

Like simp, but returns the original goal unchanged when no progress is made.

Equations

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

def Lean.Meta.Grind.Goal.internalize (goal : Goal) (num : Nat) : GrindM Goal

Internalizes the next num hypotheses from the local context into the grind state (e.g., its E-graph).

Equations

• goal.internalize num = Lean.Meta.Grind.processHypotheses goal (some num)

def Lean.Meta.Grind.Goal.internalizeAll (goal : Goal) : GrindM Goal

Internalizes all (un-internalized) hypotheses from the local context into the grind state.

Equations

• goal.internalizeAll = Lean.Meta.Grind.processHypotheses goal

inductive Lean.Meta.Grind.GrindResult : Type

• failed (goal : Goal) : GrindResult
• closed : GrindResult

def Lean.Meta.Grind.Goal.grind (goal : Goal) : GrindM GrindResult

Attempts to close the goal using grind. Returns .closed on success, or .failed with the first subgoal that failed to be closed.

Equations

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

def Lean.Meta.Grind.Goal.assumption (goal : Goal) : MetaM Bool

Closes the goal if its target matches a hypothesis. Returns true on success.

Equations

• goal.assumption = goal.mvarId.assumptionCore