Autosubst Tutorial

In this tutorial we will use Autosubst to formalize the simply typed lambda calculus and show substitutivity and type preservation of the reduction relation.

Syntax and the substitution operation

The syntax of the untyped lambda calculus is given by the following grammar. \[ s, t := x \mid s \, t \mid \lambda s \] To generate the substitution operation we need an inductive type corresponding to the terms above with a few annotations.

• There must be exactly one variable constructor which has a single argument of type var. The type var is convertible to nat, which is used to represent de Bruijn indices.
• Subterms with additional bound variables must be of type {bind term} instead of term. The notation {bind T} is convertible to T.

Now we can automatically derive the substitution operations and lemmas. This is done by generating instances for the following typeclasses:

• Ids term provides the generic identity substitution ids for term. It is always equivalent to the variable constructor of term, i.e. to the unique constructor having a single argument of type var. In this example, ids is convertible to Var.
• Rename term provides the renaming operation on term.
• Subst term provides the substitution operation on term and needs a Rename instance in the presence of binders.
• SubstLemmas term contains proofs for the basic lemmas.

Each instance is inferred automatically by using the derive tactic.

At this point we can use the notations:

• s.[sigma] for the application of the substitution sigma to a term s.
• sigma >> tau for the composition of sigma and tau, i.e., the substitution fun x => (sigma x).[tau].

Additionally there is a generic cast ren from renamings (functions of type nat -> nat to substitutions). Let us test the simplification behavior of s.[sigma].

The operator up adapts a substitution when going below a binder. It does not simplify with simpl, but we can use our tactic asimpl to perform the simplification.

Reduction and substitutivity

The single-step reduction relation is defined by the following inference rules \[ \cfrac{}{(\lambda s)\, t \rhd s.[t {\,.:\,} \text{ids}]} \quad \cfrac{s_1 \rhd s_2}{s_1 \, t \rhd s_2 \, t} \quad \cfrac{t_1 \rhd t_2}{s \, t_1 \rhd s \, t_2} \quad \cfrac{s_1 \rhd s_2}{\lambda s_1 \rhd \lambda s_2} \quad \] We write ids for the identity substitution and s .: sigma for the stream-cons operation. Note that substitutions being functions from natural numbers to terms can be seen as streams of terms. Stream-cons satisfies the following equations. Note that s.[t .: ids] replaces 0 in s by t and decreases all other variables by one. So this just expresses the usual definition of beta-reduction. We use the abbreviation s.[t/] for s.[t .: ids]. The definition below is an almost verbatim copy of the inference rules. The one difference is in the beta rule. Instead of using s.[t/] directly, we add an equation to the premise. This makes the constructor applicable even if the reduced term does not syntactically match s1.[t/].

The proof of substitutivity proceeds by induction on the reduction relation. In every case we apply the respective constructor of step. Apart from Step_beta, every case is trivial. For Step_beta, we have to show the equation Since both sides of the equation are simplified to s1.[t.[sigma] .: sigma] using asimpl, this goal can be solved using autosubst.

Type Preservation

We define the syntax for simple types.

For simplicity, the typing relation uses infinite contexts, that is, substitutions Thus we can reuse the primitives and tactics for substitutions.

This lemma is a generalization of the usual weakening lemma and a specialization of ty_subst, which we will prove next.

By generalizing ty_ren to substitutions, we obtain that we preserve typing if we replace variables by terms of the same type.

To show type preservation of the simply typed lambda calculus, we use ty_subst to justify the typing of the result of the beta reduction.