Documentation

Lean.Meta.Sym.Simp.Have

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
source
def Lean.Meta.Sym.Simp.simpHave (e : Expr) :
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
Instances For
    source
    def Lean.Meta.Sym.Simp.simpHaveAndZetaUnused (e₁ : Expr) :
    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.
    Instances For
      source
      def Lean.Meta.Sym.Simp.simpLet (e : Expr) :
      SimpM Result
      Equations
      Instances For