[POPLmark] Experience report with Twelf

[Geoffrey Alan Washburn]

Dan Licata wrote:

>>More importantly, each time I'd like to use the fact that false
>>implies anything, I have to prove it as a separate lemma. (In my
>>preservation proof, this was 6 times). Each time I used Leibniz
>>equality, I also had to prove that (13 times). What is a simple tactic
>>in Coq ("subst") is 5 tedious lines of Twelf.  
>>    
>>
>
>I've had to do this too.  However, I find the (tacticless) style of
>Twelf proofs useful.  Because object-language derivations are isomorphic
>to canonical LF terms and meta-proofs proceed by induction over
>canonical forms, the meta-proofs have a close correspondence to the rule
>inductions over derivations that we do on paper.  When writing a Twelf
>proof, I more or less just write out the rule induction proof that I'd
>do on paper and Twelf checks it.  Also, it makes it easy to translate a
>Twelf proof, case by case, into a traditional paper proof.  Kevin
>Watkins has pointed this out on this list before.
>  
>
    I would agree that I prefer the direct proof term style to tactics, 
though maybe I just need more experience to see how to write tactics 
that behave well under extension.  However, the problem we had is 
orthogonal to writing tactics versus proof terms, what we are asking is 
why would we want to be writing

false_imp_nat_eq : {N1:nat} {N2:nat} false -> nat_eq N1 N2 -> type.
%mode false_imp_nat_eq +N1 +N2 +FALSE -NEQ.
%worlds () (false_imp_nat_eq N1 N2 F NEQ).
%total F (false_imp_nat_eq N1 N2 F NEQ).

false_imp_eq : false -> methodDef_eq MD1 MD2 -> type.
%mode +{MN1:methodName} +{MD1:methodDef MN1} +{MD2:methodDef MN1} +{F:false}
   -{EQ:methodDef_eq MD1 MD2} (false_imp_eq F EQ).
%worlds (b_bind | var ) (false_imp_eq F EQ).
%total F (false_imp_eq F EQ).

false_imp_eq_class : false -> classDef_eq MD1 MD2 -> type.
%mode +{MN1:className} +{MD1:classDef MN1} +{MD2:classDef MN1} +{F:false}
   -{EQ:classDef_eq MD1 MD2} (false_imp_eq_class F EQ).
%worlds (b_bind | var ) (false_imp_eq_class F EQ).
%total F (false_imp_eq_class F EQ).

false_imp_eq_className : false -> className_eq MD1 MD2 -> type.
%mode +{MD1:className} +{MD2:className} +{F:false}
   -{EQ:className_eq MD1 MD2} (false_imp_eq_className F EQ).
%worlds () (false_imp_eq_className F EQ).
%total F (false_imp_eq_className F EQ). 

false_imp_TBE : false -> typing_bexp CT (BE: bexp CS1) C0 object -> 
subtyping CT object R1 -> cnlist_eq CS1 DS -> type.
%mode +{N1:nat} +{CS1:cnlist N1} +{CT:classTable} +{BE:bexp CS1} 
+{C0:className}   +{R1:className} +{N2:nat} +{DS: cnlist N2}
   +{F:false} -{TBE:typing_bexp CT BE C0 object}
   -{SB:subtyping CT object C0} -{EQ:cnlist_eq CS1 DS}
   (false_imp_TBE F TBE SB EQ).
%worlds () (false_imp_TBE F TBE SB EQ).
%total F (false_imp_TBE F TBE SB EQ).  

false_imp_lookupMethod : false ->
   lookupMethod MR1 M (method D0 M (BE2: bexp DS)) ->
   lookupMethod MR1 M (method C0 M (BE3: bexp CS)) -> type.
%mode +{MR1:methodTable} +{M:methodName} +{N1:nat} +{DS:cnlist N1} 
+{D0:className}
   +{BE2:bexp DS} +{N2:nat} +{CS:cnlist N2} +{C0:className} -{BE3:bexp CS}
   +{F:false}
   +{LM1:lookupMethod MR1 M (method D0 M BE2)}
   -{LM2:lookupMethod MR1 M (method C0 M BE3)}
   (false_imp_lookupMethod F LM1 LM2).
%worlds (b_bind | var ) (false_imp_lookupMethod F L M).
%total F (false_imp_lookupMethod F L M). 

false_imp_really : false -> cnlist_eq CS1 CS2 -> type.
%mode +{N1:nat} +{N2:nat} +{CS1:cnlist N1} +{CS2:cnlist N2} +{F:false}
   -{CN2:cnlist_eq CS1 CS2} (false_imp_really F CN2).
%worlds () (false_imp_really  F CN2).
%total F (false_imp_really F CN2).

when if Twelf hypothetically had polymorphism we could have just written 
something like

false_imp_any : {T:type} false -> T -> type.
%mode false_imp_any +T +F -TOBJ.
%worlds () (false_imp_any T F TOBJ).
%total F (false_imp_any T F TOBJ).

However, even this is not entirely what we want because some of the 
above lemmas need to be proven under a world with some assumptions.  We 
can rewrite our lemma as

false_imp_any : {T:type} false -> T -> type.
%mode false_imp_any +T +F -TOBJ.
%worlds (b_bind_var | var) (false_imp_any T F TOBJ).
%total F (false_imp_any T F TOBJ).

but again the non-modularity of worlds penalize us.  We will need to 
keep adding new blocks to the worlds declaration as we use the lemma in 
more and more contexts.   Perhaps if it were a possible to specify a 
"greatest" world, the world subsumption would work out and we could 
define just one lemma once and for all.

More than once Stephanie and I thought of breaking down and writing m4 
macros to deal with this but decided against it.  Manipulating untyped 
strings kind of defeats the purpose of using a logical framework to 
begin with.  Furthermore, as far as I know, the forthcoming Twelf module 
system will not be able to address these sorts of reuse problems.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.seas.upenn.edu/pipermail/poplmark/attachments/20050818/6c8d799f/attachment-0001.html