[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Dan Licata]

On Jun01, Daniel C. Wang wrote:
> 1. There isn't a nice "nat" library I could just include.

What we have works okay---I've used parts of the nat "library" from this
task in several other projects, for example.  There are definitely
issues of namespace management and parametrization and reuse (not as
much for nat, but for other types), though.  To that end, we're working
on a module system for Twelf this summer, so check back in September.

> 2.
> 
> height_of_subst : ({x : tm} {dx : height x (s z)} height (E1 x) N1)
> 		   -> height E2 N2
> 		   -> height (E1 E2) NSubst
> 		   -> sum N1 N2 N12
> 		   -> lt NSubst N12
> 		   -> type.
> %mode height_of_subst +X1 +X2 -X3 -X4 -X5.
> 
> is the Twelfized version of my challenge problem. It takes me a while
> to convince my self that's really the theorem I had in my head before
> I twelfized it.

While I agree that reading Twelf meta-theory can be confusing until you
get the hang of it, there is a formal sense in which this theorem
statement corresponds to what you originally wrote.  Let me phrase your
original theorem statement like this:

Let X stand for a list of distinct variables.  

if e1 has free variables in (X,x) and e2 has free variables in X, 
then
for all derivations of
   height(e1) = n1 and
   height(e2) = n2
there exist derivations of 
   height([e2/x]e1) = n,
   n1 + n2 = n12, and
   n < n12

Associate with each list of free variables X an LF context Gamma:
   . >> .
   X,x >> Gamma,x:tm,dx:height x (s z)   if X >> Gamma

By the adequacy of the encoding of the informal presentation into my LF
signature, the theorem statement in question is equivalent to the following:

for all canonical forms D1 and D2 such that
   Gamma, x:tm, dx:height x (s z) |- D1 : height Me1 Mn1 and
   Gamma |- D2 : height Me2 Mn2
there exist canonical forms Dsubst, Dsum, and Dlt such that
   Gamma |- Dsubst : height ([Me2/x] Me1) Mn, 
   Gamma |- Dsum : sum Mn1 Mn2 Mn12, and
   Gamma |- Dlt : lt Msubst M12

(here I intend Me1 to be the LF encoding of e1, etc.).  I'm not spelling
out the encoding fully in this e-mail, but you should be able to infer
it from what I just wrote; it's very similar to the examples in the
paper I mentioned in the previous e-mail.

The meta-theorem statement (the type declaration, mode declaration, and
world declaration) for height_of_subst corresponds to the following
forall-exists-sentence:  

for all Gamma of the form above,
for all canonical forms D1' and D2 such that
   Gamma |- D1' : {x:tm} {dx:height x (s z)} height Me1 Mn1 and
   Gamma |- D2 : height Me2 Mn2
there exist canonical forms Dsubst, Dsum, and Dlt such that
   Gamma |- DSubst : height ([Me2/x] Me1) Mn, 
   Gamma |- Dsum : sum Mn1 Mn2 Mn12, and
   Gamma |- Dlt : lt Msubst M12

Note that this differs from the above only in that the first premise now
has the free variables internalized as a term of Pi-type.  The LF
constants inhabiting height_of_subst are a proof of this meta-theorem
statement, and the %total declaration asks Twelf to check this proof.

The meta-theorem height_of_subst implies the former statement as
follows: starting from the premises of the former, use LF's lambda rule
to introduce a canonical form of the Pi-type, and then height_of_subst
shows that the necessary canonical forms exist.  Thus, by adequacy, the
Twelf proof of height_of_subst proves your on-paper statement as well.

I've been relatively brief in this e-mail and elided some details
(particularly transport of adequacy---why are sum and lt and tm adequate
in the contexts Gamma used above?).  Bob and I attempted to explain
these details in the Mechanizing Language Definitions draft that I've
mentioned; it's linked from my Web page.  I'd be happy to explain these
issues further if anyone has questions!

-Dan