[POPLmark] Twelf questions

[Karl Crary]

Randy Pollack wrote:

>I am trying to learn to use Twelf.
>
>Maybe we there should be a Twelf users email list (like Coq and
>Isabelle have) rather than do this on PoplMark, but in the meantime
>here are two questions.
>  
>
I trust you won't be shocked to learn that there is a Twelf mailing list 
already.  I believe all the necessary information can be found at 
www.twelf.org.

>First, a short one.  I understand how to state and prove lemmas that
>have a conjunction in the conclusion, using two positions with output
>mode.  But how does one state a lemma with a disjunctive conclusion?
>  
>
You do it much the same way you return a disjunctive result in ML; 
define a new type with two cases and return a result of that type.

>Now a longer question.  How to prove inversion lemmas.  Here is a very
>cut down ELF formulation of Martin-Lof logical framework
>
>  %% syntax %%
>  knd : type.    %name knd K.
>  obj : type.    %name obj M.
>
>  %% kinds
>  Type : knd.
>  El   : obj -> knd.
>
>  %% objects
>  app  : obj -> obj -> obj.
>
>  %% judgements %%
>  isk : knd -> type.                  %% is kind
>  eqk : knd -> knd -> type.           %% equal kinds
>  of  : obj -> knd -> type.           %% typing judgement
>  eqo : obj -> obj -> knd -> type.    %% equal objects at a kind
>
>  %% kinds
>  ElKnd : isk (El M)
>	   <- of M Type.
>
>  %% kind equality
>  eqkEl :  eqk (El M) (El N)
>	    <- eqo M N Type.
>
>  %% object typing
>  ofEqk :  of M L
>	    <- of M K
>	    <- eqk K L.
>
>  %% object equality
>  eqoRfl : eqo M M K
>	    <- of M K.
>
>
>The question is how to prove that if (EL M) is a kind, then
>(of M Type)?
>
>  iskEl_ofType: isk (El M) -> of M Type -> type.
>  %mode iskEl_ofType +D -E.
>  %worlds () (iskEl_ofType _ _).
>  %total {} (iskEl_ofType _ _).
>
>With this context, Twelf gives 
>
>  Coverage error --- missing cases:
>  {M1:obj} {X1:of M1 Type} {X2:of M1 Type} |- iskEl_ofType (ElKnd X1) X2.
>
>  
>
It looks to me as though you don't have any of the theorem's cases 
implemented, so it's hardly surprising that it's not total.  Shooting 
from the hip (that is, I haven't run this through the checker), I think 
you want to add the case:

casename : iskEl_ofType (ElKind D) D.

This should make your theorem check.

Beyond that, however, there's no need to state such a theorem in the 
first place.  One of the conveniences of Twelf is that one never needs 
inversion lemmas.  If there is exactly one case by which a derivation 
can be constructed, you can simply pattern match on it and obtain the 
subderivation.  Thus, whenever you obtained the "isk" derivation, you 
could have just pattern matched on it with the pattern "ElKind D" (from 
above) to get the desired D.

>The proof in Coq or LEGO would use induction loading, with the
>definable Leibniz equality
>
>  {K}(isk K) -> {M} K = (El M) -> of M Type
>
>induct on the derivation of (isk K).  But what is the substitutive
>meta-equality in Twelf?
>
>  
>
I'm afraid I'm not familiar with the terminology "substitutive 
meta-equality".  Could you elaborate?

    -- Karl