This module implements efficient pattern matching and unification module for the symbolic simulation framework (Sym). The design prioritizes performance by using a two-phase approach:

Phase 1 (Syntactic Matching)

• Patterns use de Bruijn indices for expression variables and renamed level params (_uvar.0, _uvar.1, ...) for universe variables
• Matching is purely structural after reducible definitions are unfolded during preprocessing
• Universe levels treat max and imax as uninterpreted functions (no AC reasoning)
• Binders and term metavariables are deferred to Phase 2

Phase 2 (Pending Constraints)

• Handles binders (Miller patterns) and metavariable unification
• Converts remaining de Bruijn variables to metavariables
• Falls back to structural isDefEqS when necessary.
• It still uses the standard isDefEq for instances.

Key design decisions:

• Preprocessing unfolds reducible definitions and performs beta/zeta reduction
• Kernel projections are expected to be folded as projection applications before matching
• Assignment conflicts are deferred to pending rather than invoking isDefEq inline
• instantiateRevS ensures maximal sharing of result expressions

structure Lean.Meta.Sym.Pattern : Type

• levelParams : List Name
• varTypes : Array Expr
• varInfos? : Option ProofInstInfo

  If some argsInfo, argsInfo stores whether the pattern variables are instances/proofs. It is none if no pattern variables are instance/proof.

• pattern : Expr
• fnInfos : AssocList Name ProofInstInfo
• checkTypeMask? : Option (Array Bool)

  If checkTypeMask? = some mask, then we must check the type of pattern variable i if mask[i] is true. Moreover mask.size == varTypes.size. See mkCheckTypeMask

def Lean.Meta.Sym.instInhabitedPattern.default : Pattern

Equations

• Lean.Meta.Sym.instInhabitedPattern.default = { levelParams := default, varTypes := default, varInfos? := default, pattern := default, fnInfos := default, checkTypeMask? := default }

@[implicit_reducible]

instance Lean.Meta.Sym.instInhabitedPattern : Inhabited Pattern

Equations

• Lean.Meta.Sym.instInhabitedPattern = { default := Lean.Meta.Sym.instInhabitedPattern.default }

def Lean.Meta.Sym.mkPatternFromDecl (declName : Name) (num? : Option Nat := none) : MetaM Pattern

Creates a Pattern from the type of a theorem.

The pattern is constructed by stripping leading universal quantifiers from the theorem's type. Each quantified variable becomes a pattern variable, with its type recorded in varTypes and whether it is a type class instance recorded in isInstance. The remaining type after stripping quantifiers becomes the pattern expression.

Universe level parameters are replaced with fresh unification variables (prefixed with _uvar).

If num? is some n, at most n leading quantifiers are stripped. If num? is none, all leading quantifiers are stripped.

Equations

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

def Lean.Meta.Sym.mkPatternFromExpr (e : Expr) (levelParams : List Name := []) (num? : Option Nat := none) : MetaM Pattern

Equations

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

@[inline]

def Lean.Meta.Sym.mkPatternFromDeclWithKey {α : Type} (declName : Name) (selectKey : Expr → MetaM (Expr × α)) : MetaM (Pattern × α)

Creates a Pattern from a theorem, using the supplied selection function to extract the key from the theorem's result type.

This function is used to implement mkEqPatternFromDecl. Like mkPatternFromDecl, this strips all leading universal quantifiers, recording variable types and instance status. However, instead of using the entire resulting type as the pattern, it uses the selection function to extract the key.

For a theorem ∀ x₁ ... xₙ, type, returns a pattern matching the first component of selectKey type with n pattern variables.

Equations

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

@[inline]

def Lean.Meta.Sym.mkPatternFromExprWithKey {α : Type} (e : Expr) (levelParams : List Name := []) (selectKey : Expr → MetaM (Expr × α)) : MetaM (Pattern × α)

Like mkPatternFromDeclWithKey, but for a complex proof expression instead of the declaration of a theorem.

Equations

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

def Lean.Meta.Sym.mkEqPatternFromDecl (declName : Name) : MetaM (Pattern × Expr)

Creates a Pattern from an equational theorem, using the left-hand side of the equation. It also returns the right-hand side of the equation

Like mkPatternFromDecl, this strips all leading universal quantifiers, recording variable types and instance status. However, instead of using the entire resulting type as the pattern, it extracts just the LHS of the equation.

For a theorem ∀ x₁ ... xₙ, lhs = rhs, returns a pattern matching lhs with n pattern variables. Throws an error if the theorem's conclusion is not an equality.

Equations

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

def Lean.Meta.Sym.isDefEqS (t s : Expr) (unify zetaDelta : Bool := true) (mvarsNew mvarsToCheckType : Array MVarId := #[]) : SymM Bool

A lightweight structural definitional equality for the symbolic simulation framework. Unlike the full isDefEq, it avoids expensive operations while still supporting Miller pattern unification.

Equations

• Lean.Meta.Sym.isDefEqS t s unify zetaDelta mvarsNew mvarsToCheckType = Lean.Meta.Sym.DefEqM.run✝ unify zetaDelta mvarsNew mvarsToCheckType (Lean.Meta.Sym.isDefEqMain✝ t s)

structure Lean.Meta.Sym.MatchUnifyResult : Type

• us : List Level
• args : Array Expr

def Lean.Meta.Sym.Pattern.match? (p : Pattern) (e : Expr) (zetaDelta : Bool := true) : SymM (Option MatchUnifyResult)

Attempts to match expression e against pattern p using purely syntactic matching.

Returns some result if matching succeeds, where result contains:

• us: Level assignments for the pattern's universe variables
• args: Expression assignments for the pattern's bound variables

Matching fails if:

• The term contains metavariables (use unify? instead)
• Structural mismatch after reducible unfolding

Instance arguments are deferred for later synthesis. Proof arguments are skipped via proof irrelevance.

Equations

• p.match? e zetaDelta = Lean.Meta.Sym.main✝ p e false zetaDelta

def Lean.Meta.Sym.Pattern.unify? (p : Pattern) (e : Expr) (zetaDelta : Bool := true) : SymM (Option MatchUnifyResult)

Attempts to unify expression e against pattern p, allowing metavariables in e.

Returns some result if unification succeeds, where result contains:

• us: Level assignments for the pattern's universe variables
• args: Expression assignments for the pattern's bound variables

Unlike match?, this handles terms containing metavariables by deferring constraints to Phase 2 unification. Use this when matching against goal expressions that may contain unsolved metavariables.

Instance arguments are deferred for later synthesis. Proof arguments are skipped via proof irrelevance.

Equations

• p.unify? e zetaDelta = Lean.Meta.Sym.main✝ p e true zetaDelta