We will develop a complete formalization of simply-typed lambda-calculus with constants in Coq, using the Program extension to write dependently-typed programs on inductive families. The development uses a pure de Bruijn encoding and dependently-typed abstract syntax. It includes the theory of lifting and substitution, a denotational semantics given by interpreting terms directly into Coq, and finally a proof of weak normalization for the call-by name strategy.

This paper describes all the technical parts of the development. It is a literate coqdoc script, missing only the proof scripts.

First we define a set of tactics that will be used later.

Rewrite using uniqueness of indentity proofs H = refl_equal X.

Try to abstract a proof of equality, if no proof of the same equality is present in the context.

Apply the tactic tac to proofs of equality appearing as coercion arguments.

Abstract proofs of equalities of coercions.

Factorize proofs, by using proof irrelevance so that two proofs of the same equality in the goal become convertible.

Factorize proofs of equality appearing as coercion arguments.

Clear unused reflexivity proofs.

Clear unused equality proofs.

Everything is done in implicit arguments mode.

Constants

The development is parameterized by module implementing the constants and their typing.

The set of constant types.

The constants themselves.

A typing function for constants.

The implementation.

The functor L implements typing, denotational semantics and normalization of simply-typed lambda-calculus plus constants C.

Abstract syntax

The types are just atoms or the arrow.

A context is either empty or a context and a variable. Contexts are effectively snoc-lists, hence the new inductive.

Appending one context to another, by induction on the second one.

Due to the way append is defined, these two are not convertible.

Associativity of context appending.

Simplification tactic using the previous lemmas.

Variables are encoded as typed de Bruijn indices.

The AST of well-typed terms. Constants get their type from the type_constant function. A rel just embeds a variable. The abstraction constructor lam contains a body typed in an extended environment. Application applies only functions to objects having their domain type.

The really dependent scheme for term. Not used in the development but may be useful.

Tactic to automatically invert contradictory hypotheses.

Use these for solving obligations from now on.

Dealing with coercions and equality.

The next two functions reindex variables and terms in G to a new context G' with respect to an equality between G and G'. These are dynamic coercions in the sense that they can be reduced when applied to a constructed term, contrary to the substitution principle eq_rect.

Like eq_rect, coerce reduces to the identity when G and G' are convertible.

We now define some tactics that help to deal with coercions. They work in multiple passes. First, we abstract any equality proof appearing in the goal as an argument of a coercion, so as not to polute it with irrelevant proof terms. Then we factorize the proofs and normalize the term using proof irrelevance so that two references to the same equality proof are the same. Next we try to simplify the equations using Streicher's axiom K (a proof p of x = x can be substituted by refl_equal x). Finally we try to rewrite the term using the previous lemmas about coerce and refl_equal. This procedure is very effective, most of the coercions can be eliminated this way. We get stuck only when an induction is needed.

Abstract a proof of equality, if none is already present in the context.

Use proof-irrelevance to eliminate remaining non-abstracted proofs.

The two preceding tactics in sequence.

Rewrite coerce_* t (refl_equal _) to t.

Clear the context and term of equality proofs.

Reapeated elimination of eq_rect applications. Abstracting equalities makes it run much faster than an naive implementation.

Combine all the tactics to simplify goals containing coercions.

In fact eq_rect and coerce are always equal, so we can switch between frozen and dynamic coercions at will.

Tactic to change eq_rect applications to coercions. Allows to reduce coercions sometimes.

Lifting and substitution.

We now define lifting and substitution of terms. The specifications of the functions are exactly the lemmas you would expect.

Lifting a variable t in context G ; D by U to get a variable in G :, U ; D. The context D represents the bindings we must avoid to capture.

We prove the defining equations as lemmas.

Lifting a term by a type U is just a fold.

The non recursive version, a.k.a. weakening.

The defining equations for the variable case.

Lifting by a context is lifting by each variable in turn.

Substitution of a variable by a term in context G, under a context D.

The defining equations.

Non-recursive wrapper to substitute the first variable in the context.

Substitution in a term.

Wrapped again.

The defining equations.

Commutation lemmas.

We now relate lifting and substitution to ultimately prove the substitution lemma.

Substituting for a variable just lifted is a no-op.

We first typecheck the statement, which will insert coercions around t to get the right indices. The obligations are automatically resolved using the Heq hypothesis. Note that we separate the equality so that induction can proceed on t of type term G' T while still retaining the equation between G' and G ; D.

Now we prove it, by induction on t. We first rewrite eq_rect to coercions, then simplify the term using simpl_term. This takes care of almost all the plumbing.

The real lemma is then just an instance of the previous one.

We now prove that equality coercion commute with lift to solve some of the later lemmas which involve coercions of lift calls. Idealy this should be either easily derivable or automatically generated by some kind of generic programming.

We have to take care of the opaqueness of these constants all the time, spurious unfoldings can occur otherwise, greatly obfuscating the goal.

We continue on our road to the substitution lemma. Here we prove commutation of lift_var.

Commutation of lifting and substitution, for variables.

Commutation of lifting and substitution, for terms.

The non-recursive case, with no D' context. This time the statement need not contain any coercions.

Finally, we can state the subtitution lemma as usual. The proof uses all the lemmas proven above, including commutation of lift_rec and coerce_term_context.

Non-recursive case, where no coercion is needed anymore.

Interpretation into CIC.

There is a direct embedding of into the Calculus of Constructions, which we build now.

We require interpretations for the constants and their types.

Interpret a type into a coq Set. We need an impredicate Set to work with this definition.

A valuation is a function which associates a term to each variable in a context.

We can extend a valuation by a term.

Now we can interpret terms easily.

The empty valuation.

Interpretation of closed terms.

A proof of weak normalization.

Inspired by , we build a proof of weak-head normalization using a tait-style proof. This is an instance of normalization by evaluation where the semantic domain is given by R, the strong computability predicate.

Beta-reduction and its contextual closure.

Evaluation gives the definition of normal forms, either:

• eval_trans If a term t reduces to s which itself evaluates to r then t evaluates to r. So evaluation is "backward-closed" by reduction.
• eval_lam Lambda expressions are all in normal form.
• eval_cst A constant is a normal form.

R is the glueing model in the sense of Coquand et al. We have a syntactic part v which is the value of the term t and a semantic one given by the function in the arrow case which ensures closure by application. It is trivial for constants. Note that R lives in Set so that we can extract it later.

Extract the "syntactic" part.

Backward-closedness of evaluation extends to computability.

Telescopes.

A substitution is a telescope of terms.

Substitute a term by a telescope.

This predicate ensures R-ness of all the terms in the telescope once they are substituted by previous terms in the telescope. It needs to be in Set as R is in Set.

Inversion of non-empty substitutions.

Substitution has no effect on constants.

Unfolding of telescope substitution on lambdas.

Unfolding of telescope substitution on applications.

Commutation of multiple substitutions is needed to prove that R is substitutive. It is just an application of the substitution lemma proved previously.

We extend subst_lift to contexts using substitution of telescopes and lifting by contexts.

We need to have a dynamic coercion to prove these lemmas.

Extension of the on_coerce_proof tactical.

The rest is just reinstantiation of tactics with the new on_coerce_proof.

We can finaly prove the mult_subst lemma.

Main lemma.

A little lemma on variables is all that is missing before proving our main lemma. We can destruct variables, keeping the equality handy.

We now prove the main lemma, substitutivity of R. Note that we end with a closed term, escaping the problem of variables.

We get weak normalization as a trivial consequence of the previous lemma and R_eval.

Fixpoint neutral G T (t : term G T) {struct t} : Prop := match t with | cst _ => True | rel _ _ => True | lam _ _ _ => False | app _ _ _ _ => True end.

Beta-reduction and its contextual closure.

Evaluation gives the definition of normal forms, either:

• eval_trans If a term t reduces to s which itself evaluates to r then t evaluates to r. So evaluation is "backward-closed" by reduction.
• eval_lam Lambda expressions are all in normal form.
• eval_cst A constant is a normal form.

We need to have a dynamic coercion to prove these lemmas.

Extension of the on_coerce_proof tactical.

The rest is just reinstantiation of tactics with the new on_coerce_proof.

Extract the "syntactic" part.

Backward-closedness of evaluation extends to computability.

All variables are in normal form.

This predicate ensures SN-ness of all the terms in the telescope once they are substituted by previous terms in the telescope. It needs to be in Set as SN is in Set.

Extension of the on_coerce_proof tactical.

The rest is just reinstantiation of tactics with the new on_coerce_proof.

We can finaly prove the mult_subst lemma.

Main lemma.

A little lemma on variables is all that is missing before proving our main lemma. We can destruct variables, keeping the equality handy.

We now prove the main lemma, substitutivity of SN. Note that we end with a closed term, escaping the problem of variables.

We get weak normalization as a trivial consequence of the previous lemma and SN_eval.

Instantiation.

We will now instantiate L with the naturals and booleans. Our constants are naturals or booleans of Coq.

We construct trivial interpretations of the naturals and booleans in Coq.

Wrap interpretation using the previous functions.

An example term.

The identity on naturals.

We can extract the term normalization function from this development.