Arthur Charguéraud's locally nameless solution

• Author: Arthur Charguéraud.
• Parts addressed: 1a + lemma A.10 and type safety for STLC.
• Proof assistant / theorem prover used: Coq.
• Encoding technique: Locally nameless.
• Files: available from the author's page.

Commentary

This locally nameless formalization is the result towards which I have converged at the end of an internship focused on the POPLMark Challenge. The work took place from March to July 2006 at the University of Pennsylvania, with Benjamin Pierce and Stephanie Weirich as advisors.

This solution benefits from two nice properties:

• The proofs of the main results are short and simple to follow through: the arguments are mostly the same as in a paper proof.
• The machinery involved is rather intuitive (in the sense that it does not require the ingenuity needed with pure de-Bruijn indices), and in the same time it is not too heavy (this is probably not true of a representation fully relying on names).

Main aspects of the solution:

• It is based on a locally nameless representation. As usual with this representation, there are two substitutions involved: one for indices and another one for names.
• Environments are built as lists of bindings, but then used as sets of bindings. This makes the proofs simpler because we can "forget" about the ordering of the environment. We use this not only to capture weakening, but also to capture substitution in environment. A nice side-effect is that the narrowing lemma becomes an instance of the "preservation of subtyping through type substitution" lemma.
• In SA-all rule, the name introduced is not quantified as "exists X # E", nor as "forall X # E", but as "forall X not_in L", where L is an arbitrary list of names (note that L is introduced by the constructor SA-all, and is not a parameter of the relation). The interest of this quantification is that there is no need for a formal proof of equivariance: this SA-all rule works everywhere. (Remark: equivariance is still needed to show the adequacy of the universal quantification with respect to the existential one).
• All the subtyping rules have premises enforcing the well-formation of the arguments. Tanks to a special notation for this, it does not look too bad. The advantage is that symmetry are preserved, and it seems to simplify the proofs.
• Proofs by inductions on the size of types are replaced by proofs on the derivation of the well-formation relation, which are closer to the notion of "induction on the structure of a type".

About the implementation:

• At first sight, the source file is quite long (580 lines). This is because there are a good numbers of definitions, and many lemmas. But then the total amount of proof is quite small. More precisely, Coqwc reports some 300 lines of specifications and some 150 lines of proofs
• There are around 40 lemmas, but most of them have less than 3 lines of proofs. Only 6 lemmas have more than 4 lines of proof, and together the lines of proofs of those 6 lemma add up to about 50 lines.
• Proof-search tactics are used extensively; as a result, only the key arguments appear in the proofs.
• Very few tactics specialized for this development are introduced. Thus the proofs are easy to follow and one does not need to learn the syntax of the tactic language to use the code.

Possible improvements in the solution:

• For some reason, the proof-search tactic sometimes fail to solve some goals while we could expect it to do so. This is why some cases labelled "Case SA-arrow" have to be done by hand.
• Proofs of some lemmas dealing with well-formation could probably be simplified, or at least beautified.