Jérôme Vouillon's solution

• Authors: Jérôme Vouillon
• Parts addressed: 1 and 2.
• Proof assistant / theorem prover used: Coq.
• Encoding technique: de Bruijn indices.
• Files: [tar.gz]

Commentary

This solution offers an excellent baseline against which to measure others: the representation technique (pure deBruijn) is one of the simplest and most concrete imaginable, and some of the development is correspondingly concerned with low-level details of index manipulation, etc. However, by appropriate choices of tactics and and low-level lemmas, these low-level details are largely kept from polluting the main definitions or theorems, which closely follow the paper presentation.