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.

Instances For
    Instances For
      Instances For
        @[inline, reducible]
        Instances For

          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.

          Instances For
            Instances For
              Instances For

                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.

                Instances For

                  Similar to mkAuxDefinition, but infers the type of value.

                  Instances For

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

                    Instances For

                      Similar to mkAuxTheorem, but infers the type of value.

                      Instances For