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.

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.

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

Introduces binders with the specified names.

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.

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.

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.

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).

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

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

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.

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

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