Documentation

Lean.Meta.Sym.Grind

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.

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

Instances For
    source
    inductive Lean.Meta.Grind.IntrosResult :
    Type
    Instances For
      source
      def Lean.Meta.Grind.Goal.introN (goal : Goal) (num : Nat) :
      Sym.SymM IntrosResult

      Introduces num binders from the goal's target.

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

        Introduces binders with the specified names.

        Instances For
          source
          inductive Lean.Meta.Grind.ApplyResult :
          Type
          Instances For
            source
            def Lean.Meta.Grind.Goal.apply (goal : Goal) (rule : Sym.BackwardRule) :
            Sym.SymM ApplyResult

            Applies a backward rule, returning subgoals on success.

            Instances For
              source
              inductive Lean.Meta.Grind.SimpGoalResult :
              Type
              Instances For
                source
                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.

                Instances For
                  source
                  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.

                  Instances For
                    source
                    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).

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

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

                      Instances For
                        source
                        inductive Lean.Meta.Grind.GrindResult :
                        Type
                        Instances For
                          source
                          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.

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

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

                            Instances For