Many people interested in interactive theorem-proving want to prove theorems about programming languages. That domain also provides a good setting for demonstrating how to apply the ideas from the earlier parts of this book. This part introduces some techniques for encoding the syntax and semantics of programming languages, along with some example proofs designed to be as practical as possible, rather than to illustrate basic Coq technique.

To prove anything about a language, we must first formalize the language's syntax. We have a broad design space to choose from, and it makes sense to start with the simplest options, so-called first-order syntax encodings that do not use dependent types. These encodings are first-order because they do not use Coq function types in a critical way. In this chapter, we consider the most popular first-order encodings, using each to prove a basic type soundness theorem.

Concrete Binding

The most obvious encoding of the syntax of programming languages follows usual context-free grammars literally. We represent variables as strings and include a variable in our AST definition wherever a variable appears in the informal grammar. Concrete binding turns out to involve a surprisingly large amount of menial bookkeeping, especially when we encode higher-order languages with nested binder scopes. This section's example should give a flavor of what is required.

We need our variable type and its decidable equality operation.

We will formalize basic simply-typed lambda calculus. The syntax of expressions and types follows what we would write in a context-free grammar.

It is useful to define a syntax extension that lets us write function types in more standard notation.

Now we turn to a typing judgment. We will need to define it in terms of typing contexts, which we represent as lists of pairs of variables and types.

The definitions of our judgments will be prettier if we write them using mixfix syntax. To define a judgment for looking up the type of a variable in a context, we first reserve a notation for the judgment. Reserved notations enable mutually-recursive definition of a judgment and its notation; in this sense, the reservation is like a forward declaration in C.

Now we define the judgment itself, for variable typing, using a where clause to associate a notation definition.

The same technique applies to defining the main typing judgment. We use an at next level clause to cause the argument e of the notation to be parsed at a low enough precedence level.

It is useful to know that variable lookup results are unchanged by adding extra bindings to the end of a context.

The same property extends to the full typing judgment.

Much of the inconvenience of first-order encodings comes from the need to treat capture-avoiding substitution explicitly. We must start by defining a substitution function.

We are substituting expression e1 for every free occurrence of x. Note that this definition is specialized to the case where e1 is closed; substitution is substantially more complicated otherwise, potentially involving explicit alpha-variation. Luckily, our example of type safety for a call-by-value semantics only requires this restricted variety of substitution.

We can prove a few theorems about substitution in well-typed terms, where we assume that e1 is closed and has type xt.

It is helpful to establish a notation asserting the freshness of a particular variable in a context.

To prove type preservation, we will need lemmas proving consequences of variable lookup proofs.

Another set of lemmas allows us to remove provably unused variables from the ends of typing contexts.

Disjointness facts may be extended to larger contexts when the appropriate obligations are met.

Finally, we arrive at the main theorem about substitution: it preserves typing.

We wrap the last theorem into an easier-to-apply form specialized to closed expressions.

A notation for substitution will make the operational semantics easier to read.

To define a call-by-value small-step semantics, we rely on a standard judgment characterizing which expressions are values.

Now the step relation is easy to define.

The progress theorem says that any well-typed expression that is not a value can take a step. To deal with limitations of the induction tactic, we put most of the proof in a lemma whose statement uses the usual trick of introducing extra equality hypotheses.

A similar pattern works for the preservation theorem, which says that any step of execution preserves an expression's type.

This was a relatively simple example, giving only a taste of the proof burden associated with concrete syntax. We were helped by the fact that, with call-by-value semantics, we only need to reason about substitution in closed expressions. There was also no need to alpha-vary an expression.

De Bruijn Indices

De Bruijn indices are much more popular than concrete syntax. This technique provides a canonical representation of syntax, where any two alpha-equivalent expressions have syntactically equal encodings, removing the need for explicit reasoning about alpha conversion. Variables are represented as natural numbers, where variable n denotes a reference to the nth closest enclosing binder. Because variable references in effect point to binders, there is no need to label binders, such as function abstraction, with variables.

The definition of typing proceeds much the same as in the last section. Since variables are numbers, contexts can be simple lists of types. This makes it possible to write the lookup judgment without mentioning inequality of variables.

In the hasType case for function abstraction, there is no need to choose a variable name. We simply push the function domain type onto the context G.

We prove roughly the same weakening theorems as before.

Substitution is easier to define than with concrete syntax. While our old definition needed to use two comparisons for equality of variables, the de Bruijn substitution only needs one comparison.

We prove similar theorems about inversion of variable lookup.

The next lemma is included solely to guide eauto, which will not apply computational equivalences automatically.

Finally, we are ready for the main theorem about substitution and typing.

We define the operational semantics much as before.

Since we have added the right hints, the progress and preservation theorem statements and proofs are exactly the same as in the concrete encoding example.

Locally Nameless Syntax

The most popular Coq syntax encoding today is the locally nameless style, which has been around for a while but was popularized recently by Aydemir et al., following a methodology summarized in their paper "Engineering Formal Metatheory." A specialized tutorial by that group explains the approach, based on a library. In this section, we will build up all of the necessary ingredients from scratch.

The one-sentence summary of locally nameless encoding is that we represent free variables as concrete syntax does, and we represent bound variables with de Bruijn indices. Many proofs involve reasoning about terms transplanted into different free variable contexts; concrete encoding of free variables means that, to perform such a transplanting, we need no fix-up operation to adjust de Bruijn indices. At the same time, use of de Bruijn indices for local variables gives us canonical representations of expressions, with respect to the usual convention of alpha-equivalence. This makes many operations, including substitution of open terms in open terms, easier to implement.

The "Engineering Formal Metatheory" methodology involves a number of subtle design decisions, which we will describe as they appear in the latest version of our running example.

Note the different constructors for free vs. bound variables, and note that the lack of a variable annotation on Abs nodes is inherited from the de Bruijn convention.

As typing only depends on types of free variables, our contexts borrow their form from the concrete binding example.

The first unusual operation we need is opening, where we replace a particular bound variable with a particular free variable. Whenever we "go under a binder," in the typing judgment or elsewhere, we choose a new free variable to replace the old bound variable of the binder. Opening implements the replacement of one by the other. It is like a specialized version of the substitution function we used for pure de Bruijn terms. We implement opening with both the richly-typed natural number equality test eq_nat_dec that we have discussed previously and with another standard library function le_lt_dec, which is an analogous richly-typed test for <=.

We will also need to reason about an expression's set of free variables. To keep things simple, we represent sets as lists that may contain duplicates. Note how much easier this operation is to implement than over pure de Bruijn terms, since we do not need to maintain a separate numeric argument that keeps track of how deeply we have descended into the input expression.

It will be useful to have a well-formedness judgment for our terms. This notion is called local closure. An expression may be declared to be closed, up to a particular maximum de Bruijn index.

Now we are ready to define the typing judgment.

Compared to the previous versions, only the TAbs rule is surprising. The rule uses co-finite quantiifcation. That is, the premise of the rule quantifies over all x values that are not members of a finite set L. A proof may choose any value of L when applying TAbs. An alternate, more intuitive version of the rule would fix L to be freeVars e'. It turns out that the greater flexibility of the rule above simplifies many proofs significantly. This typing judgment may be proved equivalent to the more intuitive version, though we will not carry out the proof here.

Specifially, what our version of TAbs says is that, to prove that Abs e' has a function type, we must prove that any opening of e' with a variable not in L has the proper type. For each x choice, we extend the context G in the usual way.

We prove a standard weakening theorem for typing, adopting a more general form than in the previous sections.

We define a simple extension of crush to apply in many of the lemmas that follow.

Two basic properties of local closure will be useful later.

To prove some further properties, we need the ability to choose a variable that is disjoint from a particular finite set. We implement a specific choice function fresh; its details do not matter, as all we need is the final theorem about it, freshOk. Concretely, to choose a variable disjoint from set L, we sum the lengths of the variable names in L and choose a new variable name that is one longer than that sum. This variable can be the string x"", followed by a number of primes equal to the sum.

A few lemmas suffice to establish the correctness theorem freshOk for fresh.

Now we can prove that well-typedness implies local closure. fresh will be used for us automatically by eauto in the Abs case, driven by the presence of freshOk as a hint.

An important consequence of local closure is that certain openings are idempotent.

We are now almost ready to get down to the details of substitution. First, we prove six lemmas related to treating lists as sets.

Now we can define our simplest substitution function yet, thanks to the fact that we only subsitute for free variables, which are distinguished syntactically from bound variables.

It comes in handy to define disjointness of a variable and a context differently than in previous examples. We use the standard list function map, as well as the function fst for projecting the first element of a pair. We write fst@ _ _ rather than just fst to ask that fst's implicit arguments be instantiated with inferred values.

Some basic properties of variable lookup will be needed on the road to our usual theorem connecting substitution and typing.

We need to know that substitution and opening commute under appropriate circumstances.

We state a corollary of the last result which will work more smoothly with eauto.

Another lemma establishes the validity of weakening variable lookup judgments with fresh variables.

Finally, it is useful to state a version of the TAbs rule specialized to the choice of L that is useful in our main substitution proof.

Now we can prove the main inductive lemma in a manner similar to what worked for concrete binding.

The main theorem about substitution of closed expressions follows easily.

We can define the operational semantics in almost the same way as in previous examples.

The only interesting change is that the Beta rule requires identifying a fresh variable x to use in opening the abstraction body. We could have avoided this by implementing a more general open that allows substituting expressions for variables, not just variables for variables, but it simplifies the proofs to have just one general substitution function.

Now we are ready to prove progress and preservation. The same proof script from the last examples suffices to prove progress, though significantly different lemmas are applied for us by eauto.

To establish preservation, it is useful to formalize a principle of sound alpha-variation. In particular, when we open an expression with a particular variable and then immediately substitute for the same variable, we can replace that variable with any other that is not free in the body of the opened expression.

Again it is useful to state a direct corollary which is easier to apply in proof search.

Now the previous sections' preservation proof scripts finish the job.