[POPLmark] A "locally nameless" solution in Coq

[Xavier Leroy]

Dear all,

The interesting discussions at ICFP and Merlin two weeks ago finally
motivated me to clean up and put online my (partial) solution to the
POPLmark challenge:

      http://cristal.inria.fr/~xleroy/POPLmark/locally-nameless/

This solution covers only part 1a of the challenge (algorithmic
subtyping, no record types).  It is written in Coq, and uses a
"locally nameless" representation for binders: variables bound within
terms are represented by de Bruijn indices, but variables free in
terms are represented by names.  I was inspired by Randy Pollack's
talk, "Reasoning About Languages with Binding":

  http://homepages.inf.ed.ac.uk/rap/export/bindingChallenge_slides.pdf

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.

Enjoy,

- Xavier Leroy