Xavier Leroy's solution

- Author: Xavier Leroy.
- Parts addressed: 1a, 2a and 3.
- Proof assistant / theorem prover used: Coq.
- Encoding technique: Locally nameless.
- Files: available from the author's page.

Xavier Leroy's solution

- Author: Xavier Leroy.
- Parts addressed: 1a, 2a and 3.
- Proof assistant / theorem prover used: Coq.
- Encoding technique: Locally nameless.
- Files: available from the author's page.

Commentary

A technical report describes the solution. The following remarks are copied from a message from Leroy to the POPLmark mailing list.

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.