Submission by Xavier Leroy

[edit] General information and files

Files for this submission:

Directly from the author's page.
Mirrored copies at UPenn (copied on 30 December 2005): commentary.pdf, part1a.v, extralibrary.v.

(The following remarks are copied from a message from Leroy to the POPLmark mailing list. See also the links above.)

Some good things about this representation:

Alpha-equivalence is term equality, which makes life much simpler in Coq.
The statements (and even the proofs) of the main theorems are quite close to what one would write on paper.
Despite not being completely nominal, it still illustrates some of the key aspects of fully nominal approaches, especially the "forall/exists" equivalence for the choice of fresh variables.

Some bad things about this representation:

There is a lot of boilerplate involved before getting to the meat of the proof: two substitution functions (of names and of de Bruijn variables), computation and properties of free names, swaps, commutation of swaps with many definitions, the "forall/exists" theorems, etc. Consequently, the development is larger than a pure de Bruijn solution.
Extending this approach to part 2 of the challenge exceeds my fortitude: two sorts of names, six substitution functions, even more swaps, commutation theorems all over the place, ... Enough is enough :-)

One good thing about my solution:

It is heavily commented, then typeset using the coqdoc tool. Message to my fellow solution submitters: you, too, can write good English; don't be shy.

One bad thing about my solution:

My Coq proof scripts do not have the conciseness and elegance of Jérôme Vouillon's. Sorry, I've been using Coq for only 6 years...

Final thoughts:

If the purpose is just to solve the challenge and be done with it, I would rather go for pure de Bruijn.
However, this could change if some of the nominal boilerplate was built into the logic or at least into the prover.
The exercise has some educational value, to me at least.

A Technical Report that describes the full solution, including parts 1a, 2a and 3.