Have-Telescope Simplification for Sym.simp

This module implements efficient simplification of have-telescopes (sequences of non-dependent let bindings) in the symbolic simplifier. The key insight is to transform telescopes into a "parallel" beta-application form, simplify the arguments independently, and then convert back to have form.

The Problem

Consider a have-telescope:

have x₁ := v₁
have x₂ := v₂[x₁]
...
have xₙ := vₙ[x₁, ..., xₙ₋₁]
b[x₁, ..., xₙ]

Naively generating proofs using have_congr leads to quadratic kernel type-checking time. The issue is that when the kernel type-checks congruence proofs, it creates fresh free variables for each binder, destroying sharing and generating O(n²) terms.

The Solution: Virtual Parallelization

We transform the sequential have telescope into a parallel beta-application:

(fun x₁ x₂' ... xₙ' => b[x₁, x₂' x₁, ..., xₙ' (xₙ₋₁' ...)]) v₁ (fun x₁ => v₂[x₁]) ... (fun ... xₙ₋₁ => vₙ[..., xₙ₋₁])

Each xᵢ' is now a function that takes its dependencies as arguments. This form:

1. Is definitionally equal to the original (so conversion is free)
2. Enables independent simplification of each argument
3. Produces proofs that type-check in linear time using the existing efficient simplification procedure for lambdas.

Algorithm Overview

1. toBetaApp: Transform have-telescope → parallel beta-application

   • Track dependency graph: which have depends on which previous haves
   • Convert each value vᵢ[x₁, ..., xₖ] to (fun y₁ ... yₖ => vᵢ[y₁, ..., yₖ])
   • Build the body with appropriate applications

2. simpBetaApp: Simplify the beta-application using congruence lemmas

   • Simplify function and each argument independently
   • Generate proof using congr, congrArg, congrFun'
   • This procedure is optimized for functions taking many arguments.

3. toHave: Convert simplified beta-application → have-telescope

   • Reconstruct the have bindings from the lambda structure
   • Apply each argument to recover original variable references

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

Result of converting a have-telescope to a parallel beta-application.

Given:

have x₁ := v₁; have x₂ := v₂[x₁]; ...; have xₙ := vₙ[...]; b[x₁, ..., xₙ]

We produce:

(fun x₁ x₂' ... xₙ' => b'[...]) v₁ (fun deps => v₂[deps]) ... (fun deps => vₙ[deps])

where each xᵢ' has type deps_type → Tᵢ and b' contains applications xᵢ' (deps).

• α : Expr

  Type of the input have-expression.

• u : Level

  The universe level of α.

• e : Expr

  The beta-application form: (fun x₁ ... xₙ' => b') v₁ ... (fun deps => vₙ).

• h : Expr

  Proof that the original expression equals e (by reflexivity + hints, since definitionally equal).

• varDeps : Array (Array Nat)

  Dependency information for each have. varDeps[i] contains the indices of previous haves that vᵢ depends on. Used by toHave to reconstruct the telescope.

• fType : Expr

  The function type: T₁ → (deps₁ → T₂) → ... → (depsₙ₋₁ → Tₙ) → β. Used to compute universe levels for congruence lemmas.

def Lean.Meta.Sym.Simp.instInhabitedToBetaAppResult.default : ToBetaAppResult

Equations

• Lean.Meta.Sym.Simp.instInhabitedToBetaAppResult.default = { α := default, u := default, e := default, h := default, varDeps := default, fType := default }

@[implicit_reducible]

instance Lean.Meta.Sym.Simp.instInhabitedToBetaAppResult : Inhabited ToBetaAppResult

Equations

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

def Lean.Meta.Sym.Simp.toBetaApp (haveExpr : Expr) : SymM ToBetaAppResult

Transform a have-telescope into a parallel beta-application.

Input: have x₁ := v₁; ...; have xₙ := vₙ; b

Output: A ToBetaAppResult containing the equivalent beta-application.

Transformation Details

For each have xᵢ := vᵢ where vᵢ depends on xᵢ₁, ..., xᵢₖ (aka depsₖ)

• The argument becomes fun depsₖ => vᵢ[depsₖ]
• The type becomes Dᵢ₁ → ... → Dᵢₖ → Tᵢ where Dᵢⱼ is the type of xᵢⱼ
• In the body, xᵢ is replaced by xᵢ' sᵢ₁ ... sᵢₖ where sᵢⱼ is the replacement for xᵢⱼ

The proof is rfl since the transformation is definitionally equal.

Equations

• Lean.Meta.Sym.Simp.toBetaApp haveExpr = Lean.Meta.Sym.Simp.toBetaApp.go✝ haveExpr haveExpr #[] #[] #[] #[] #[] #[] ∅

def Lean.Meta.Sym.Simp.simpHave (e : Expr) (simpBody : Simproc) : SimpM Result

Simplify a have-telescope.

This is the main entry point for have-telescope simplification in Sym.simp. See module documentation for the algorithm overview.

Equations

• Lean.Meta.Sym.Simp.simpHave e simpBody = do let __do_lift ← Lean.Meta.Sym.Simp.simpHaveCore✝ e simpBody pure (Lean.Meta.Sym.Simp.SimpHaveResult.result✝ __do_lift)

def Lean.Meta.Sym.Simp.simpHaveAndZetaUnused (e₁ : Expr) (simpBody : Simproc) : SimpM Result

Simplify a have-telescope and eliminate unused bindings.

This combines simplification with dead variable elimination in a single pass, avoiding quadratic behavior from multiple passes.

Equations

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

def Lean.Meta.Sym.Simp.simpLet' (simpBody : Simproc) (e : Expr) : SimpM Result

Equations

• Lean.Meta.Sym.Simp.simpLet' simpBody e = if (!e.letNondep!) = true then pure Lean.Meta.Sym.Simp.Result.rfl else Lean.Meta.Sym.Simp.simpHaveAndZetaUnused e simpBody

def Lean.Meta.Sym.Simp.simpLet : Simproc

Equations

• Lean.Meta.Sym.Simp.simpLet = Lean.Meta.Sym.Simp.simpLet' Lean.Meta.Sym.Simp.simpLambda