This module provides functions for "closing" open terms and creating auxiliary definitions. Here, we say a term is "open" if it contains free/meta-variables.

The "closure" is performed by lambda abstracting the free/meta-variables. Recall that in dependent type theory lambda abstracting a let-variable may produce type incorrect terms. For example, given the context

(n : Nat := 20)
(x : Vector α n)
(y : Vector α 20)

the term x = y is correct. However, its closure using lambda abstractions is not.

fun (n : Nat) (x : Vector α n) (y : Vector α 20) => x = y

A previous version of this module would address this issue by always use let-expressions to abstract let-vars. In the example above, it would produce

let n : Nat := 20; fun (x : Vector α n) (y : Vector α 20) => x = y

This approach produces correct result, but produces unsatisfactory results when we want to create auxiliary definitions. For example, consider the context

(x : Nat)
(y : Nat := fact x)

and the term h (g y), now suppose we want to create an auxiliary definition for y. The previous version of this module would compute the auxiliary definition

def aux := fun (x : Nat) => let y : Nat := fact x; h (g y)

and would return the term aux x as a substitute for h (g y). This is correct, but we will re-evaluate fact x whenever we use aux. In this module, we produce

def aux := fun (y : Nat) => h (g y)

Note that in this particular case, it is safe to lambda abstract the let-varible y. This module uses the following approach to decide whether it is safe or not to lambda abstract a let-variable.

1. We enable zeta-expansion tracking in MetaM. That is, whenever we perform type checking if a let-variable needs to zeta expanded, we store it in the set zetaFVarIds. We say a let-variable is zeta expanded when we replace it with its value.
2. We use the MetaM type checker check to type check the expression we want to close, and the type of the binders.
3. If a let-variable is not in zetaFVarIds, we lambda abstract it.

Remark: We still use let-expressions for let-variables in zetaFVarIds, but we move the let inside the lambdas. The idea is to make sure the auxiliary definition does not have an interleaving of lambda and let expressions. Thus, if the let-variable occurs in the type of one of the lambdas, we simply zeta-expand it there. As a final example consider the context

(x_1 : Nat)
(x_2 : Nat)
(x_3 : Nat)
(x   : Nat := fact (10 + x_1 + x_2 + x_3))
(ty  : Type := Nat → Nat)
(f   : ty := fun x => x)
(n   : Nat := 20)
(z   : f 10)

and we use this module to compute an auxiliary definition for the term

(let y  : { v : Nat // v = n } := ⟨20, rfl⟩; y.1 + n + f x, z + 10)

we obtain

def aux (x : Nat) (f : Nat → Nat) (z : Nat) : Nat×Nat :=
let n : Nat := 20;
(let y : {v // v=n} := {val := 20, property := ex._proof_1}; y.val+n+f x, z+10)

BTW, this module also provides the zeta : Bool flag. When set to true, it expands all let-variables occurring in the target expression.

structure Lean.Meta.Closure.ToProcessElement : Type

• fvarId : Lean.FVarId
• newFVarId : Lean.FVarId

instance Lean.Meta.Closure.instInhabitedToProcessElement : Inhabited Lean.Meta.Closure.ToProcessElement

Equations

• Lean.Meta.Closure.instInhabitedToProcessElement = { default := { fvarId := default, newFVarId := default } }

structure Lean.Meta.Closure.Context : Type

• zeta : Bool

structure Lean.Meta.Closure.State : Type

• visitedLevel : Lean.LevelMap Lean.Level
• visitedExpr : Lean.ExprStructMap Lean.Expr
• levelParams : Array Lake.Name
• nextLevelIdx : Nat
• levelArgs : Array Lean.Level
• newLocalDecls : Array Lean.LocalDecl
• newLocalDeclsForMVars : Array Lean.LocalDecl
• newLetDecls : Array Lean.LocalDecl
• nextExprIdx : Nat
• exprMVarArgs : Array Lean.Expr
• exprFVarArgs : Array Lean.Expr
• toProcess : Array Lean.Meta.Closure.ToProcessElement

@[inline, reducible]

abbrev Lean.Meta.Closure.ClosureM (α : Type) : Type

Equations

• Lean.Meta.Closure.ClosureM = ReaderT Lean.Meta.Closure.Context (StateRefT' IO.RealWorld Lean.Meta.Closure.State Lean.MetaM)

@[inline]

def Lean.Meta.Closure.visitLevel (f : Lean.Level → Lean.Meta.Closure.ClosureM Lean.Level) (u : Lean.Level) : Lean.Meta.Closure.ClosureM Lean.Level

Equations

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

@[inline]

def Lean.Meta.Closure.visitExpr (f : Lean.Expr → Lean.Meta.Closure.ClosureM Lean.Expr) (e : Lean.Expr) : Lean.Meta.Closure.ClosureM Lean.Expr

Equations

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

def Lean.Meta.Closure.mkNewLevelParam (u : Lean.Level) : Lean.Meta.Closure.ClosureM Lean.Level

Equations

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

partial def Lean.Meta.Closure.collectLevelAux : Lean.Level → Lean.Meta.Closure.ClosureM Lean.Level

def Lean.Meta.Closure.collectLevel (u : Lean.Level) : Lean.Meta.Closure.ClosureM Lean.Level

Equations

• Lean.Meta.Closure.collectLevel u = Lean.Meta.Closure.visitLevel Lean.Meta.Closure.collectLevelAux u

def Lean.Meta.Closure.preprocess (e : Lean.Expr) : Lean.Meta.Closure.ClosureM Lean.Expr

Equations

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

def Lean.Meta.Closure.mkNextUserName : Lean.Meta.Closure.ClosureM Lake.Name

Remark: This method does not guarantee unique user names. The correctness of the procedure does not rely on unique user names. Recall that the pretty printer takes care of unintended collisions.

Equations

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

def Lean.Meta.Closure.pushToProcess (elem : Lean.Meta.Closure.ToProcessElement) : Lean.Meta.Closure.ClosureM Unit

Equations

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

partial def Lean.Meta.Closure.collectExprAux (e : Lean.Expr) : Lean.Meta.Closure.ClosureM Lean.Expr

def Lean.Meta.Closure.collectExpr (e : Lean.Expr) : Lean.Meta.Closure.ClosureM Lean.Expr

Equations

• Lean.Meta.Closure.collectExpr e = do let e ← Lean.Meta.Closure.preprocess e Lean.Meta.Closure.visitExpr Lean.Meta.Closure.collectExprAux e

partial def Lean.Meta.Closure.pickNextToProcessAux (lctx : Lean.LocalContext) (i : Nat) (toProcess : Array Lean.Meta.Closure.ToProcessElement) (elem : Lean.Meta.Closure.ToProcessElement) : Lean.Meta.Closure.ToProcessElement × Array Lean.Meta.Closure.ToProcessElement

def Lean.Meta.Closure.pickNextToProcess? : Lean.Meta.Closure.ClosureM (Option Lean.Meta.Closure.ToProcessElement)

Equations

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

def Lean.Meta.Closure.pushFVarArg (e : Lean.Expr) : Lean.Meta.Closure.ClosureM Unit

Equations

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

def Lean.Meta.Closure.pushLocalDecl (newFVarId : Lean.FVarId) (userName : Lake.Name) (type : Lean.Expr) (bi : optParam Lean.BinderInfo Lean.BinderInfo.default) : Lean.Meta.Closure.ClosureM Unit

Equations

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

partial def Lean.Meta.Closure.process : Lean.Meta.Closure.ClosureM Unit

@[inline]

def Lean.Meta.Closure.mkBinding (isLambda : Bool) (decls : Array Lean.LocalDecl) (b : Lean.Expr) : Lean.Expr

Equations

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

def Lean.Meta.Closure.mkLambda (decls : Array Lean.LocalDecl) (b : Lean.Expr) : Lean.Expr

Equations

• Lean.Meta.Closure.mkLambda decls b = Lean.Meta.Closure.mkBinding true decls b

def Lean.Meta.Closure.mkForall (decls : Array Lean.LocalDecl) (b : Lean.Expr) : Lean.Expr

Equations

• Lean.Meta.Closure.mkForall decls b = Lean.Meta.Closure.mkBinding false decls b

structure Lean.Meta.Closure.MkValueTypeClosureResult : Type

• levelParams : Array Lake.Name
• type : Lean.Expr
• value : Lean.Expr
• levelArgs : Array Lean.Level
• exprArgs : Array Lean.Expr

def Lean.Meta.Closure.mkValueTypeClosureAux (type : Lean.Expr) (value : Lean.Expr) : Lean.Meta.Closure.ClosureM (Lean.Expr × Lean.Expr)

Equations

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

def Lean.Meta.Closure.mkValueTypeClosure (type : Lean.Expr) (value : Lean.Expr) (zeta : Bool) : Lean.MetaM Lean.Meta.Closure.MkValueTypeClosureResult

Equations

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

def Lean.Meta.mkAuxDefinition (name : Lake.Name) (type : Lean.Expr) (value : Lean.Expr) (zeta : optParam Bool false) (compile : optParam Bool true) : Lean.MetaM Lean.Expr

Create an auxiliary definition with the given name, type and value. The parameters type and value may contain free and meta variables. A "closure" is computed, and a term of the form name.{u_1 ... u_n} t_1 ... t_m is returned where u_is are universe parameters and metavariables type and value depend on, and t_js are free and meta variables type and value depend on.

Equations

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

def Lean.Meta.mkAuxDefinitionFor (name : Lake.Name) (value : Lean.Expr) (zeta : optParam Bool false) : Lean.MetaM Lean.Expr

Similar to mkAuxDefinition, but infers the type of value.

Equations

• Lean.Meta.mkAuxDefinitionFor name value zeta = do let type ← Lean.Meta.inferType value let type : Lean.Expr := Lean.Expr.headBeta type Lean.Meta.mkAuxDefinition name type value zeta true

def Lean.Meta.mkAuxTheorem (name : Lake.Name) (type : Lean.Expr) (value : Lean.Expr) (zeta : optParam Bool false) : Lean.MetaM Lean.Expr

Create an auxiliary theorem with the given name, type and value. It is similar to mkAuxDefinition.

Equations

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

def Lean.Meta.mkAuxTheoremFor (name : Lake.Name) (value : Lean.Expr) (zeta : optParam Bool false) : Lean.MetaM Lean.Expr

Similar to mkAuxTheorem, but infers the type of value.

Equations

• Lean.Meta.mkAuxTheoremFor name value zeta = do let type ← Lean.Meta.inferType value let type : Lean.Expr := Lean.Expr.headBeta type Lean.Meta.mkAuxTheorem name type value zeta