[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Dan Licata]

On May31, Daniel C. Wang wrote:
> Problem 1.
> Show height is a function.
> 
> Problem 2.
> Show that  
>   if height(e,n) and height(e',m) then
>       height(e[e'/x],n') and n' < (n -1) +  m
> where x is "free in e' ".

I wrote a quick Twelf solution last night. 

You can download it here:
http://www.cs.cmu.edu/~drl/lib/twelf/poplmark-height.tgz

The files are also unzipped in that directory for online reading; the
main part of the proof is here:
http://www.cs.cmu.edu/~drl/lib/twelf/lam-calc-height/height.elf

The syntax of the untyped lambda-calculus is encoded using standard HOAS
techniques; capture-avoiding substitution and alpha-conversion come "for
free" from the framework.  My height judgement is also hypothetical; see
the brief comments in the file for details.

The meta-theorem statements and proofs are standard Twelf fare; they
didn't require any tricks.  The proofs use several lemmas from my
arithmetic "library" (i.e., a bunch of definitions and meta-theorems in
a separate directory).  If you browse through the nat-library directory,
I think you'll agree that these are all theorems of independent
interest.  Some of them I had already proved; some of them I wrote for
this task---but now I won't have to prove them again the next time I do
a size metric with max and addition.

I haven't had time to comment very thoroughly, but the code should be
understandable to someone with a basic familiarity with Twelf; you might
find the following draft paper useful if the code confuses you:

http://www.cs.cmu.edu/~drl/pubs/hl06mechanizing/hl06mechanizing.pdf

Daniel, you mentioned in a previous e-mail that there is a system in
which you found this task "tedious".  Since you haven't made this
complaint about the Coq/Isabelle/HOL solutions, I wonder if Twelf is the
system you had in mind.  If so, I'm curious as to why.

-Dan