[POPLmark] Twelf questions

[Penny Anderson]

Just add:

  iskEl_ofType_: iskEl_ofType (ElKnd Dt) Dt.


[Opening file ml.elf]
knd : type.
obj : type.
Type : knd.
El : obj -> knd.
app : obj -> obj -> obj.
isk : knd -> type.
eqk : knd -> knd -> type.
of : obj -> knd -> type.
eqo : obj -> obj -> knd -> type.
ElKnd : {M:obj} of M Type -> isk (El M).
eqkEl : {M:obj} {N:obj} eqo M N Type -> eqk (El M) (El N).
ofEqk : {K:knd} {L:knd} {M:obj} eqk K L -> of M K -> of M L.
eqoRfl : {M:obj} {K:knd} of M K -> eqo M M K.
iskEl_ofType : {M:obj} isk (El M) -> of M Type -> type.
iskEl_ofType_ : {M1:obj} {Dt:of M1 Type} iskEl_ofType (ElKnd Dt) Dt.
%mode +{M:obj} +{D:isk (El M)} -{E:of M Type} (iskEl_ofType D E).
%worlds () (iskEl_ofType _ _).
%total {} (iskEl_ofType _ _).
[Closing file ml.elf]
%% OK %%

However, in general the lack of a meta-equality causes annoyances,
*some* of which are ameliorated by uniqueness checking.

Regards,
Penny

> X-Mailman-Handler: $Id: mm-handler,v 1.2 2002/04/05 19:41:09 bwarsaw Exp $
> From: Randy Pollack <rap at inf.ed.ac.uk>
> Date: Thu, 5 May 2005 21:53:47 +0100
> X-Spam-Status: -0.001 SPF_PASS
> X-Scanned-By: MIMEDefang 2.49 on 158.130.65.164
> Reply-To: Discussion forum for the POPLmark challenge
> 	<poplmark at lists.seas.upenn.edu>
> Sender: poplmark-bounces at lists.seas.upenn.edu
> 
> 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.
> 
> 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?
> 
> 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.
> 
> 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?
> 
> Thanks,
> Randy
> _______________________________________________
> Poplmark mailing list
> Poplmark at lists.seas.upenn.edu
> http://lists.seas.upenn.edu/mailman/listinfo/poplmark
>