Support for representing HaveTelescopes and simplifying them. We use this module to implement both Sym.simp and Meta.simp using the MonadSimp adapter.

structure Lean.Meta.HaveInfo : Type

Information about a single have in a have telescope. Created by getHaveTelescopeInfo.

• typeBackDeps : Std.HashSet Nat

  Previous haves that the type of this have depends on, as indices into HaveTelescopeInfo.haveInfo. Used in computeFixedUsed to compute used haves.

• valueBackDeps : Std.HashSet Nat

  Previous haves that the value of this have depends on, as indices into HaveTelescopeInfo.haveInfo. Used in computeFixedUsed to compute used haves.

• decl : LocalDecl

  The local decl for the have, so that the local context can be re-entered have-by-have. N.B. This stores the fvarid for the have as well as cached versions of the value and type instantiated with the fvars from the telescope.

• level : Level

  The level of the type for this have, cached.

def Lean.Meta.instInhabitedHaveInfo.default : HaveInfo

Equations

• Lean.Meta.instInhabitedHaveInfo.default = { typeBackDeps := default, valueBackDeps := default, decl := default, level := default }

instance Lean.Meta.instInhabitedHaveInfo : Inhabited HaveInfo

Equations

• Lean.Meta.instInhabitedHaveInfo = { default := Lean.Meta.instInhabitedHaveInfo.default }

structure Lean.Meta.HaveTelescopeInfo : Type

Information about a have telescope. Created by getHaveTelescopeInfo and used in simpHaveTelescope.

The data is used to avoid applying Expr.abstract more than once on any given subexpression when constructing terms and proofs during simplification. Abstraction is linear in the size t of a term, and so in a depth-n telescope it is O(nt), quadratic in n, since n ≤ t. For example, given have x₁ := v₁; ...; have xₙ := vₙ; b and h : b = b', we need to construct

have_body_congr (fun x₁ => ... have_body_congr (fun xₙ => h)))

We apply Expr.abstract to h once and then build the term, rather than using mkLambdaFVars #[fvarᵢ] pfᵢ at each step.

As an additional optimization, we save the fvar-instantiated terms calculated by getHaveTelescopeInfo so that we don't have to compute them again. This is only saving a constant factor.

It is also used for computing used haves in computeFixedUsed. In have x₁ := v; have x₂ := x₁; ⋯; have xₙ := xₙ₋₁; b, if xₙ is unused in b, then all the haves are unused. Without a global computation of used haves, the proof term would be quadratic in the number of haves (with n iterations of simp). Knowing which haves are transitively unused lets the proof term be linear in size.

• haveInfo : Array HaveInfo

  Information about each have in the telescope.

• bodyDeps : Std.HashSet Nat

  The set of haves that the body depends on, as indices into haveInfo. Used in computeFixedUsed to compute used haves.

• bodyTypeDeps : Std.HashSet Nat

  The set of haves that the type of the body depends on, as indices into haveInfo. This is the set of fixed haves.

• body : Expr

  A cached version of the telescope body, instantiated with fvars from each HaveInfo.decl.

• bodyType : Expr

  A cached version of the telescope body's type, instantiated with fvars from each HaveInfo.decl.

• level : Level

  The universe level for the have expression, cached.

instance Lean.Meta.instInhabitedHaveTelescopeInfo : Inhabited HaveTelescopeInfo

Equations

• Lean.Meta.instInhabitedHaveTelescopeInfo = { default := Lean.Meta.instInhabitedHaveTelescopeInfo.default }

def Lean.Meta.instInhabitedHaveTelescopeInfo.default : HaveTelescopeInfo

Equations

• Lean.Meta.instInhabitedHaveTelescopeInfo.default = { haveInfo := default, bodyDeps := default, bodyTypeDeps := default, body := default, bodyType := default, level := default }

def Lean.Meta.getHaveTelescopeInfo (e : Expr) : MetaM HaveTelescopeInfo

Efficiently collect dependency information for a have telescope. This is part of a scheme to avoid quadratic overhead from the locally nameless discipline (see HaveTelescopeInfo and simpHaveTelescope).

The expression e must not have loose bvars.

Equations

• Lean.Meta.getHaveTelescopeInfo e = do let __do_lift ← Lean.getLCtx Lean.Meta.getHaveTelescopeInfo.collect✝ e 0 { } __do_lift #[]

def Lean.Meta.HaveTelescopeInfo.computeFixedUsed (info : HaveTelescopeInfo) (keepUnused : Bool) : MetaM (Array Bool × Array Bool)

Computes which haves in the telescope are fixed and which are unused. The length of the unused array may be less than the number of haves: use unused.getD i true.

Equations

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

inductive Lean.Meta.ZetaUnusedMode : Type

Configuration for specifying how unused let-declarations are eliminated.

• no : ZetaUnusedMode

  Do not eliminate unused let-declarations.

• singlePass : ZetaUnusedMode

  Simplify and eliminate unused let-declarations in a single pass.

• twoPasses : ZetaUnusedMode

  Simplify and then eliminate unused let-declarations.

def Lean.Meta.zetaUnused (e : Expr) : MetaM Expr

Remove unused-let declarations.

Equations

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

def Lean.Meta.simpHaveTelescope {m : Type → Type} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] [MonadSimp m] (e : Expr) (zetaUnusedMode : ZetaUnusedMode := ZetaUnusedMode.twoPasses) : m MonadSimp.Result

Routine for simplifying have telescopes. Used by simpLet. This is optimized to be able to handle deep have telescopes while avoiding quadratic complexity arising from the locally nameless expression representations.

Overview

Consider a have telescope:

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

We say xᵢ is fixed if it appears in the type of b. If xᵢ is fixed, then it can only be rewritten using definitional equalities. Otherwise, we can freely rewrite the value using a propositional equality vᵢ = vᵢ'. The body b can always be freely rewritten using a propositional equality b = b'. (All the mentioned equalities must be type correct with respect to the obvious local contexts.)

If xᵢ neither appears in b nor any Tⱼ nor any vⱼ, then its have is unused. Unused haves can be eliminated, which we do if cfg.zetaUnused is true. We clear haves from the end, to be able to transitively clear chains of unused haves. This is why we honor zetaUnused here even though reduceStep is also responsible for it; reduceStep can only eliminate unused haves at the start of a telescope. Eliminating all transitively unused haves at once like this also avoids quadratic complexity.

If debug.simp.check.have is enabled then we typecheck the resulting expression and proof.

Proof generation

There are two main complications with generating proofs.

1. We work almost exclusively with expressions with loose bound variables, to avoid overhead from instantiating and abstracting free variables, which can lead to complexity quadratic in the telescope length. (See HaveTelescopeInfo.)
2. We want to avoid triggering zeta reductions in the kernel.

Regarding this second point, the issue is that we cannot organize the proof using congruence theorems in the obvious way. For example, given

theorem have_congr {α : Sort u} {β : Sort v} {a a' : α} {f f' : α → β}
    (h₁ : a = a') (h₂ : ∀ x, f x = f' x) :
    (have x := a; f x) = (have x := a'; f' x)

the kernel sees that the type of have_congr (fun x => b) (fun x => b') h₁ h₂ is (have x := a; (fun x => b) x) = (have x := a'; (fun x => b') x), since when instantiating values it does not beta reduce at the same time. Hence, when is_def_eq is applied to the LHS and have x := a; b for example, it will do whnf_core to both sides.

Instead, we use the form (fun x => b) a = (fun x => b') a' in the proofs, which we can reliably match up without triggering beta reductions in the kernel. The zeta/beta reductions are then limited to the type hint for the entire telescope, when we convert this back into have form. In the base case, we include an optimization to avoid unnecessary zeta/beta reductions, by detecting a simpHaveTelescope proofs and removing the type hint.