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.
