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.

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.

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

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

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

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

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

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.

• cache : Cache

  Cache of previously simplified expressions to avoid redundant work. Note: Consider moving to SymM.State

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

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
• wellBehavedMethods : Bool

  wellBehavedMethods must not be set to true IF their behavior depends on new hypotheses in the local context. For example, for applying conditional rewrite rules. Reason: it would prevent us from aggressively caching simp results.

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

Equations

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

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

Equations

• Lean.Meta.Sym.Simp.instInhabitedMethods = { default := Lean.Meta.Sym.Simp.instInhabitedMethods.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 theorems, configuration, and initial state

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 theorems 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.getCache : SimpM Cache

Equations

• Lean.Meta.Sym.Simp.getCache = do let __do_lift ← get pure __do_lift.cache

@[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 α

Equations

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

@[reducible, inline]

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

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