<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta content="text/html;charset=UTF-8" http-equiv="Content-Type">
</head>
<body bgcolor="#ffffff" text="#000000">
Dan Licata wrote:
<blockquote cite="mid20050818025832.GA22380@cs.cmu.edu" type="cite">
<blockquote type="cite">
<pre wrap="">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.
</pre>
</blockquote>
<pre wrap=""><!---->
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.
</pre>
</blockquote>
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<br>
<br>
false_imp_nat_eq : {N1:nat} {N2:nat} false -> nat_eq N1 N2 ->
type.<br>
%mode false_imp_nat_eq +N1 +N2 +FALSE -NEQ.<br>
%worlds () (false_imp_nat_eq N1 N2 F NEQ).<br>
%total F (false_imp_nat_eq N1 N2 F NEQ).<br>
<br>
false_imp_eq : false -> methodDef_eq MD1 MD2 -> type.<br>
%mode +{MN1:methodName} +{MD1:methodDef MN1} +{MD2:methodDef MN1}
+{F:false}<br>
-{EQ:methodDef_eq MD1 MD2} (false_imp_eq F EQ).<br>
%worlds (b_bind | var ) (false_imp_eq F EQ).<br>
%total F (false_imp_eq F EQ).<br>
<br>
false_imp_eq_class : false -> classDef_eq MD1 MD2 -> type.<br>
%mode +{MN1:className} +{MD1:classDef MN1} +{MD2:classDef MN1}
+{F:false}<br>
-{EQ:classDef_eq MD1 MD2} (false_imp_eq_class F EQ).<br>
%worlds (b_bind | var ) (false_imp_eq_class F EQ).<br>
%total F (false_imp_eq_class F EQ).<br>
<br>
false_imp_eq_className : false -> className_eq MD1 MD2 -> type.<br>
%mode +{MD1:className} +{MD2:className} +{F:false}<br>
-{EQ:className_eq MD1 MD2} (false_imp_eq_className F EQ).<br>
%worlds () (false_imp_eq_className F EQ).<br>
%total F (false_imp_eq_className F EQ). <br>
<br>
false_imp_TBE : false -> typing_bexp CT (BE: bexp CS1) C0 object
-> subtyping CT object R1 -> cnlist_eq CS1 DS -> type.<br>
%mode +{N1:nat} +{CS1:cnlist N1} +{CT:classTable} +{BE:bexp CS1}
+{C0:className} +{R1:className} +{N2:nat} +{DS: cnlist N2}<br>
+{F:false} -{TBE:typing_bexp CT BE C0 object}<br>
-{SB:subtyping CT object C0} -{EQ:cnlist_eq CS1 DS}<br>
(false_imp_TBE F TBE SB EQ).<br>
%worlds () (false_imp_TBE F TBE SB EQ).<br>
%total F (false_imp_TBE F TBE SB EQ). <br>
<br>
false_imp_lookupMethod : false -><br>
lookupMethod MR1 M (method D0 M (BE2: bexp DS)) -><br>
lookupMethod MR1 M (method C0 M (BE3: bexp CS)) -> type.<br>
%mode +{MR1:methodTable} +{M:methodName} +{N1:nat} +{DS:cnlist N1}
+{D0:className}<br>
+{BE2:bexp DS} +{N2:nat} +{CS:cnlist N2} +{C0:className} -{BE3:bexp
CS}<br>
+{F:false} <br>
+{LM1:lookupMethod MR1 M (method D0 M BE2)}<br>
-{LM2:lookupMethod MR1 M (method C0 M BE3)}<br>
(false_imp_lookupMethod F LM1 LM2).<br>
%worlds (b_bind | var ) (false_imp_lookupMethod F L M).<br>
%total F (false_imp_lookupMethod F L M). <br>
<br>
false_imp_really : false -> cnlist_eq CS1 CS2 -> type.<br>
%mode +{N1:nat} +{N2:nat} +{CS1:cnlist N1} +{CS2:cnlist N2} +{F:false}<br>
-{CN2:cnlist_eq CS1 CS2} (false_imp_really F CN2).<br>
%worlds () (false_imp_really F CN2).<br>
%total F (false_imp_really F CN2). <br>
<br>
when if Twelf hypothetically had polymorphism we could have just
written something like<br>
<br>
false_imp_any : {T:type} false -> T -> type.<br>
%mode false_imp_any +T +F -TOBJ.<br>
%worlds () (false_imp_any T F TOBJ).<br>
%total F (false_imp_any T F TOBJ).<br>
<br>
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 <br>
<br>
false_imp_any : {T:type} false -> T -> type.<br>
%mode false_imp_any +T +F -TOBJ.<br>
%worlds (b_bind_var | var) (false_imp_any T F TOBJ).<br>
%total F (false_imp_any T F TOBJ).<br>
<br>
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.<br>
<br>
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.<br>
<br>
</body>
</html>