[POPLmark] Twelf questions

[Randy Pollack]

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