[POPLmark] A "locally nameless" solution in Coq

[Benjamin Pierce]

Hi Xavier,

Very pretty! I'm particularly grateful for the extensive  
documentation and elegant typesetting.  Even as a non-Coq-expert, I  
was able to read it straight through (trusting you and Coq on the  
details of the proofs :-), and it gave me a much better appreciation  
than I'd had before of some of the fine points of the McKinna-Pollack  
approach to binding.

One question about the boilerplate: Do you have a sense of how  
difficult it would be to generate (at least most of) these lemmas  
automatically?  A few months' hacking, or >=1 PhD?  (Of course, if it  
was *easy* you'd have done it already... :-)

Regards,

     - Benjamin


On Oct 10, 2005, at 12:47 PM, Xavier Leroy wrote:

> 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
> _______________________________________________
> Poplmark mailing list
> Poplmark at lists.seas.upenn.edu
> http://lists.seas.upenn.edu/mailman/listinfo/poplmark
>