[POPLmark] Experience report with Twelf

[Stephanie Weirich]

Hi Dan,

Thanks for your reply! You've written a lot of nice clarifications here,
that I think will be useful for others learning Twelf. I just want to  
address
a few of the points that you made.

>
>> The proof of the progress theorem includes a case analysis of whether
>> A is a subtype of B or not. In constructive logic, we have to show
>> that subtyping is decidable. In Coq, I used "apply Classic." In  
>> Twelf,
>> Geoff wrote 300 lines of code. Granted, these extra lines actually
>> proved more: we got a proof that subtyping is decidable in FJ.  
>> But, as
>> I was just interested in the type soundness of FJ, so being forced to
>> prove more properties was annoying.
>>
>
> Intuitionistically, what you're proving when you don't actually do the
> decidability proof is "the law of the excluded middle (for subtyping)
> implies progress".
>
> You could do this in Twelf by leaving an unproven meta-theorem stating
> decidability:
>
> lem-for-subtyping : {a : tp} {b : tp} sub-or-not a b -> type.
>
> (where sub-or-not is essentially a sum of subtyping and not,  
> however you
> define them).

Yes, the "lem-for-subtyping" lemma is exactly the lemma we proved. We  
didn't
see how to assert it so that it could be used by the coverage checker  
in the
progress lemma, though.

A side note:  I don't think that this is exactly the law of the excluded
middle. I think it says something like "at least one of the  
'subtyping' and
'notsubtyping' judgments are derivable. For true classical reasoning, I
found that I also needed the related lemma, that asserts that "at  
most one
of the judgements is derivable".

subtyping-exclusive: subtyping A B -> not-subtyping A B -> false ->  
type.

(For progress, we didn't need the subtyping-exclusive lemma, but we did
need a related version of this lemma elsewhere in the proof.)
Is it possible to combine these two together into one lemma? I  
couldn't think
how to do that.

>
> Or, you could state progress with an extra premise of type ({a :  
> tp} {b
> : tp} sub-or-not a b), though I don't immediately see that it would be
> easy to satisfy this premise once you've proven decidability as a
> meta-theorem.
>

I agree, I don't think you can manipulate proofs like that in Twelf.  
Things like
this get me too. As I understand it, a Twelf proof of the  
decidability of
subtyping is not an LF element of type
     ({a : tp} {b: tp} sub-or-not a b)
it is some meta reasoning that the Twelf logic program is a total  
function.

>
>> 3) HOAS, non-modularity and strengthening
>>
>
>
> Cartsen Schurmann's forthcoming Delphin system is supposed to address
> these problems.  As I understand it, it will allow you to write
> meta-proofs as total functional programs over the canonical LF terms;
> you'll be able to supply the cases for variables directly and locally,
> rather than in the context.

Great! I hope that Delphin can address these issues.

>
> Sometimes strengthening does come up.  More than once, though, I've
> thought I needed strengthening when really I had corrupted my
> subordination relation (i.e., Twelf thought types were subordinate  
> when
> they shouldn't have been).  The subordination relation tells you when
> objects of one type can appear in another.  You can use the command  
> (in
> the Twelf server directly) Print.subord to print the subordination
> relation and inspect it.  I'm not sure that it shows the transitive
> closure, so you may have to compute that yourself.

Thanks for the hint about Print.subord.

lookupClass_strengthen :
    ({x:exp} lookupClass CT C (class C D FS (MT x)))
      -> lookupClass CT C (class C D FS (MT unit)) -> type.

However, I think this is a case where strengthening is unavoidable.  
The type exp
is subordinate to the type methodTable, but since the methodTable MT  
comes from
the classTable CT (which does not depend on x) in this case, it can't  
depend on x.
>

> It took me a little while to get used to the input coverage checker.

I agree entirely. This is exactly what I was talking about, it's an  
issue of
learning curve. After a while, I was going through roughly the same  
processes
that you describe (alpha renaming the error message so that I could  
understand them,
adding type annotations to make sure that variables are not unified).  
However,
even when I had taught myself these practices, I found writing proofs  
a little
backwards....Coq tells me what to prove, but in Twelf, I have to  
guess, and then
interpret the error messages when I guess wrong.

Thanks for writing a careful description of how to go about  
addressing coverage
errors---this is something that should appear in the Twelf wiki.

--Stephanie