Structural Simplifier for Symbolic Simulation

It is a specialized simplifier designed for symbolic simulation workloads. It addresses performance bottlenecks identified in the standard simp tactic when applied to large terms typical in symbolic execution.

Design Goals

1. Efficient caching via pointer-based keys on maximally shared terms
2. Fast pattern matching using the Pattern infrastructure instead of isDefEq
3. Minimal proof term overhead by using shareCommon and efficient congruence lemma application

Key Performance Problems Addressed

1. Cache Inefficiency (Hash Collisions)

The standard simplifier uses structural equality for cache keys. With large terms, hash collisions cause O(n) comparisons that fail, leading to O(n²) behavior.

Solution: Require maximally shared input terms (shareCommon) and use pointer-based cache keys. Structurally equal terms have equal pointers, making cache lookup O(1).

2. isDefEq in Rewrite Matching

Profiling shows that isDefEq dominates simplification time in many workloads. For each candidate rewrite rule, definitional equality checking with metavariable unification is performed, and sometimes substantial time is spent checking whether the scopes are compatible.

Solution: Use the Pattern infrastructure for syntactic matching:

• No metavariable creation or assignment
• No occurs check (CheckAssignment)
• Direct de Bruijn index comparison

3. inferType in Proof Construction

In the standard simplifier, building Eq.trans and congrArg proofs uses inferType on proof terms, which reconstructs large expressions and destroys sharing. It often causes O(n²) allocation.

Solution:

• Never perform inferType on proof terms when constructing congruence and transitivity proofs.
• Use a pointer-based cache for inferType on terms.

4. funext Proof Explosion

Nested funext applications create O(n²) proof terms due to implicit arguments {f} {g} of size O(n) repeated n times.

Solution: Generate funext_k for k binders at once, stating the implicit arguments only once.

5. Binder Re-entry Cache Invalidation

When a simplification theorem restructures a lambda, re-entering creates a fresh free variable, invalidating all cached results for subterms.

Solution: Reuse free variables across binder re-entry when safe:

• Stack-based approach: reuse when types match on re-entry path
• Instance-aware: track local type class instances separately from hypotheses
• If simplifier doesn't discharge hypotheses from local context, only instances matter

6. Contextual ite Handling

The standard ite_congr theorem adds hypotheses when entering branches, invalidating the cache and causing O(2^n) behavior on conditional trees.

Solution: Non-contextual ite handling for symbolic simulation:

• Only simplify the condition
• If condition reduces to True/False, take the appropriate branch
• Otherwise, keep ite symbolic (let the simulator handle case-splitting)

Architecture

Input Requirements

• Terms must be maximally shared via shareCommon like every other module in Sym.
• Enables pointer-based cache keys throughout

Integration with SymM

SimpM is designed to work within the SymM symbolic simulation framework:

• Uses BackwardRule for control-flow (monadic bind, match, combinators)
• SimpM handles term simplification between control-flow steps
• Avoids entering control-flow binders

structure Lean.Meta.Sym.Simp.Config : Type

Configuration options for the structural simplifier.

• maxSteps : Nat

  Maximum number of steps that can be performed by the simplifier.

• maxDischargeDepth : Nat

  Maximum depth of reentrant simplifier calls through dischargers. Prevents infinite loops when conditional rewrite rules trigger recursive discharge attempts.

@[implicit_reducible]

instance Lean.Meta.Sym.Simp.instInhabitedConfig : Inhabited Config

Equations

• Lean.Meta.Sym.Simp.instInhabitedConfig = { default := Lean.Meta.Sym.Simp.instInhabitedConfig.default }

def Lean.Meta.Sym.Simp.instInhabitedConfig.default : Config

Equations

• Lean.Meta.Sym.Simp.instInhabitedConfig.default = { maxSteps := default, maxDischargeDepth := default }

inductive Lean.Meta.Sym.Simp.Result : Type

The result of simplifying an expression e.

The done flag controls whether simplification should continue after this result:

• done = false (default): Continue with subsequent simplification steps
• done = true: Stop processing, return this result as final

Use cases for done = true

In pre simprocs

Skip simplification of certain subterms entirely:

def skipLambdas : Simproc := fun e =>
  if e.isLambda then return .rfl (done := true)
  else return .rfl

In post simprocs

Perform single-pass normalization without recursive simplification:

def singlePassNormalize : Simproc := fun e =>
  if let some (e', h) ← tryNormalize e then
    return .step e' h (done := true)
  else return .rfl

With done = true, the result e' won't be recursively simplified.

Behavior

The done flag affects:

1. andThen composition: If the first simproc returns done = true, the second simproc is skipped.
2. Recursive simplification: After pre or post returns .step e' h, simp normally recurses on e'. With done = true, recursion is skipped.

The flag is orthogonal to caching: both .rfl and .step results are cached regardless of the done flag, and cached results are always treated as final.

Context-dependent results

The contextDependent flag tracks whether the result depends on the local context (e.g., hypotheses introduced when entering binders). Context-dependent results are stored in a transient cache that is cleared when entering binders, while context-independent results persist across binder entry and across simp invocations.

Propagation rule: when combining sub-results (congruence, transitivity, etc.), contextDependent is the disjunction of all sub-results' flags. This includes .rfl results: if simp returned .rfl (contextDependent := true), it means simp might produce a different result in another local context (e.g., a conditional rewrite could succeed), so all downstream results must be marked context-dependent.

• rfl (done contextDependent : Bool := false) : Result

  No change. If done = true, skip remaining simplification steps for this term.

• step (e' proof : Expr) (done contextDependent : Bool := false) : Result

  Simplified to e' with proof proof : e = e'. If done = true, skip recursive simplification of e'.

@[implicit_reducible]

instance Lean.Meta.Sym.Simp.instInhabitedResult : Inhabited Result

Equations

• Lean.Meta.Sym.Simp.instInhabitedResult = { default := Lean.Meta.Sym.Simp.instInhabitedResult.default }

def Lean.Meta.Sym.Simp.instInhabitedResult.default : Result

Equations

• Lean.Meta.Sym.Simp.instInhabitedResult.default = Lean.Meta.Sym.Simp.Result.rfl default default

def Lean.Meta.Sym.Simp.mkRflResult (done contextDependent : Bool := false) : Result

Pre-computed .rfl results to avoid dynamic memory allocation. Each combination of done and contextDependent maps to a compile-time constant.

Equations

• Lean.Meta.Sym.Simp.mkRflResult = Lean.Meta.Sym.Simp.Result.rfl
• Lean.Meta.Sym.Simp.mkRflResult false true = Lean.Meta.Sym.Simp.Result.rfl false true
• Lean.Meta.Sym.Simp.mkRflResult true = Lean.Meta.Sym.Simp.Result.rfl true
• Lean.Meta.Sym.Simp.mkRflResult true true = Lean.Meta.Sym.Simp.Result.rfl true true

def Lean.Meta.Sym.Simp.mkRflResultCD (contextDependent : Bool) : Result

Like mkRflResult with done := false.

Equations

• Lean.Meta.Sym.Simp.mkRflResultCD contextDependent = if contextDependent = true then Lean.Meta.Sym.Simp.Result.rfl false true else Lean.Meta.Sym.Simp.Result.rfl

@[reducible, inline]

abbrev Lean.Meta.Sym.Simp.Result.isContextDependent : Result → Bool

Returns true if this result depends on the local context (e.g., hypotheses).

Equations

• (Lean.Meta.Sym.Simp.Result.rfl done cd).isContextDependent = cd
• (Lean.Meta.Sym.Simp.Result.step e' proof done cd).isContextDependent = cd

def Lean.Meta.Sym.Simp.Result.withContextDependent : Result → Result

Marks a result as context-dependent.

Equations

• (Lean.Meta.Sym.Simp.Result.rfl done cd).withContextDependent = Lean.Meta.Sym.Simp.Result.rfl done true
• (Lean.Meta.Sym.Simp.Result.step e' proof done cd).withContextDependent = Lean.Meta.Sym.Simp.Result.step e' proof done true

def Lean.Meta.Sym.Simp.MethodsRef : Type

Equations

• Lean.Meta.Sym.Simp.MethodsRef = Lean.Meta.Sym.Simp.MethodsRefPointed✝.type

instance Lean.Meta.Sym.Simp.instNonemptyMethodsRef : Nonempty MethodsRef

structure Lean.Meta.Sym.Simp.Context : Type

Read-only context for the simplifier.

• config : Config

  Simplifier configuration options.

• initialLCtxSize : Nat

  Size of the local context when simplification started. Used to determine which free variables were introduced during simplification.

• dischargeDepth : Nat

@[reducible, inline]

abbrev Lean.Meta.Sym.Simp.Cache : Type

Cache mapping expressions (by pointer equality) to their simplified results.

Equations

• Lean.Meta.Sym.Simp.Cache = Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Sym.Simp.Result

structure Lean.Meta.Sym.Simp.State : Type

Mutable state for the simplifier.

• numSteps : Nat

  Number of steps performed so far.

• persistentCache : Cache

  Cache for context-independent results. Survives across binder entry and across simp invocations within a sym => block.

• transientCache : Cache

  Cache for context-dependent results. Cleared when entering binders (where new hypotheses may change the result).

• funext : PHashMap ExprPtr Expr

  Cache for generated funext theorems

@[reducible, inline]

abbrev Lean.Meta.Sym.Simp.SimpM (α : Type) : Type

Monad for the structural simplifier, layered on top of SymM.

Equations

• Lean.Meta.Sym.Simp.SimpM = ReaderT Lean.Meta.Sym.Simp.MethodsRef (ReaderT Lean.Meta.Sym.Simp.Context (StateRefT' IO.RealWorld Lean.Meta.Sym.Simp.State Lean.Meta.Sym.SymM))

@[implicit_reducible]

instance Lean.Meta.Sym.Simp.instInhabitedSimpM {α : Type} : Inhabited (SimpM α)

Equations

• Lean.Meta.Sym.Simp.instInhabitedSimpM = { default := Lean.throwError (Lean.toMessageData "<default>") }

@[reducible, inline]

abbrev Lean.Meta.Sym.Simp.Simproc : Type

Equations

• Lean.Meta.Sym.Simp.Simproc = (Lean.Expr → Lean.Meta.Sym.Simp.SimpM Lean.Meta.Sym.Simp.Result)

structure Lean.Meta.Sym.Simp.Methods : Type

• pre : Simproc
• post : Simproc

@[implicit_reducible]

instance Lean.Meta.Sym.Simp.instInhabitedMethods : Inhabited Methods

Equations

• Lean.Meta.Sym.Simp.instInhabitedMethods = { default := Lean.Meta.Sym.Simp.instInhabitedMethods.default }

def Lean.Meta.Sym.Simp.instInhabitedMethods.default : Methods

Equations

• Lean.Meta.Sym.Simp.instInhabitedMethods.default = { pre := default, post := default }

unsafe def Lean.Meta.Sym.Simp.Methods.toMethodsRefImpl (m : Methods) : MethodsRef

Equations

• m.toMethodsRefImpl = unsafeCast m

@[implemented_by Lean.Meta.Sym.Simp.Methods.toMethodsRefImpl]

opaque Lean.Meta.Sym.Simp.Methods.toMethodsRef (m : Methods) : MethodsRef

@[reducible, inline]

unsafe abbrev Lean.Meta.Sym.Simp.MethodsRef.toMethodsImpl (m : MethodsRef) : Methods

Equations

• m.toMethodsImpl = unsafeCast m

@[implemented_by Lean.Meta.Sym.Simp.MethodsRef.toMethodsImpl]

opaque Lean.Meta.Sym.Simp.MethodsRef.toMethods (m : MethodsRef) : Methods

def Lean.Meta.Sym.Simp.getMethods : SimpM Methods

Equations

• Lean.Meta.Sym.Simp.getMethods = do let __do_lift ← read pure __do_lift.toMethods

def Lean.Meta.Sym.Simp.SimpM.run {α : Type} (x : SimpM α) (methods : Methods := { }) (config : Config := { }) (s : State := { }) : SymM (α × State)

Runs a SimpM computation with the given methods, configuration, and state. The transientCache is always reset (context-dependent results don't survive across invocations). The persistentCache and funext cache are preserved from s.

Equations

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

def Lean.Meta.Sym.Simp.SimpM.run' {α : Type} (x : SimpM α) (methods : Methods := { }) (config : Config := { }) : SymM α

Runs a SimpM computation with the given methods and configuration.

Equations

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

@[extern lean_sym_simp]

opaque Lean.Meta.Sym.Simp.simp : Simproc

def Lean.Meta.Sym.Simp.getConfig : SimpM Config

Equations

• Lean.Meta.Sym.Simp.getConfig = do let __do_lift ← readThe Lean.Meta.Sym.Simp.Context pure __do_lift.config

@[reducible, inline]

abbrev Lean.Meta.Sym.Simp.pre : Simproc

Equations

• Lean.Meta.Sym.Simp.pre e = do let __do_lift ← Lean.Meta.Sym.Simp.getMethods __do_lift.pre e

@[reducible, inline]

abbrev Lean.Meta.Sym.Simp.post : Simproc

Equations

• Lean.Meta.Sym.Simp.post e = do let __do_lift ← Lean.Meta.Sym.Simp.getMethods __do_lift.post e

@[reducible, inline]

abbrev Lean.Meta.Sym.Simp.withoutModifyingCache {α : Type} (k : SimpM α) : SimpM α

Saves and restores both caches and funext. Used by dischargers.

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Sym.Simp.withFreshTransientCache {α : Type} (k : SimpM α) : SimpM α

Saves and restores the transient cache and funext, leaving the persistent cache untouched. Used when entering binders.

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Sym.simp (e : Expr) (methods : Simp.Methods := { }) (config : Simp.Config := { }) : SymM Simp.Result

Equations

• Lean.Meta.Sym.simp e methods config = (Lean.Meta.Sym.Simp.simp e).run' methods config