[POPLmark] Experience report with Twelf

[Michael Philip Ashley-Rollman]

>>> 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.
>>>
>>>
>>
>> This could be a property of the system you're formalizing, not just
>> the LF encoding.  That is, on paper, how do you *know* that the class
>> you get back doesn't mention some variable in the context?  Sometimes
>> I've glossed over things like this on paper only to have Twelf point
>> them out to me.
>>
>>
> This issue didn't come up in either the Coq version of the proof (that I
> did) or the Isabelle/HOL version
> (that two grad students here at Penn did).

This issue does not really come up in the twelf proof either. Rather than 
proving the lookupClass_strengthen or sub_strengthen lemmas, you can 
simply substitute unit in for exp for lookupClass_strengthen and any 
expression at all into sub_strengthen. A term with type (exp -> subtyping 
CT C D) is saying that for any expression, I can provide you with a proof 
of (subtyping CT C D). Thus, by providing any term with type exp, we may 
immediately get a derivation of (subtyping CT C D). Sometimes substituting 
in terms that don't matter can confuses twelf a little bit and it will 
give you an error like this:

Typing ambiguous -- unresolved constraints
C1 unit = C1 x;
CT1 unit = CT1 x;
CT1 unit = CT1 x;
CT1 unit = CT1 x.

In this case, providing the type of the term after substition usually 
resolves the issue. Thus we may change the last rule of narrowing_explist 
to this:

-:  narrowing_explist WCT TL1 SB TL2 ->
     sub_trans SB2 (SB1 unit : subtyping CT C D) SB4 ->
%%    sub_strengthen SB1 SB3 ->
      narrowing_exp WCT T1 SB T2 SB2 ->
      narrowing_explist WCT
      ([x][q] tl_cons (SB1 x) (TL1 x q) (T1 x q)) SB
      ([x][q] tl_cons SB4 (TL2 x q) (T2 x q)).

Othertimes Twelf is able to understand the substitution as in the 
narrowing_bexp cases.
 	-Michael