[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Adam Chlipala]

Daniel C. Wang wrote:

> I guess, I should have specified that you're theory of expressions 
> should support a notion of "alpha-equality" and capture avoiding 
> substitution. I think, your Coq solution fails in that case.

The idea was that you check capture avoidance et al. with side 
conditions.  I've updated my solution to include definitions of these:
    http://www.cs.berkeley.edu/~adamc/lamheight/

The end result is a 'legalSubst' predicate that only allows 
capture-avoiding substitution and permits alpha-variation.  This change 
was purely an addition at the end and didn't involve changing any of the 
earlier code.  Your final challenge theorem for 'legalSubst' follows 
trivially from the way that I proved it, for the non-capture-avoiding 
'subst', by definition.

I think your objection is related to why I said that the challenge was 
"unfair."  There are many ways to formalize variable binding in Coq, but 
the _particular_ theorems that you requested seem binding-agnostic.  For 
most Coq binding formalization strategies, I believe that my proofs for 
your theorems would literally remain the same, since they use automation 
to do most of the work.  The definitions of the underlying ASTs and 
relations would change, but there aren't any "semantic" theorems in the 
challenge to provide a way to differentiate the approaches.  Perhaps an 
approach based on pervasive side conditions like mine has been shown to 
be intractable in practice, but I don't think that means that it didn't 
answer your challenge, especially with the additions.