[POPLmark] Twelf question

[Karl Crary]

There are two derivations of interest here: D3 (called D1 in your proof 
case tps_app), and P2 (called P1 in tps_app).  D3 has the type "eval E1 
(lam T2 E4)" and P2 has the type "of E1 (arr T3 T1)".  In fact, T2 and 
T3 will always be the same, but that requires proof.  As far as Twelf is 
concerned, they can be different.

Your problem is that when you use the pattern (of_lam Q1') to match the 
output of type "of (lam T2 E4) (arr T3 T1)", you cause the variables T2 
and T3 to be unified.  Therefore, Twelf complains because the case where 
they are different is uncovered.

What you need to do is employ an inversion lemma such as:

of_lam_invert : of (lam T E) (arr T1 T2) -> ({x} of x T1 -> of (E x) T2) 
-> type.
%mode of_lam_invert +X1 -X2.

You can use this to dig out the Q1' you need without unifying T2 and T3:

... <- tps D1 P1 D4 <- of_lam_invert D4 Q1' <- ...

If you like, of_lam_invert can also return the fact that T1 and T are 
the same, but that's not necessary here.

    -- Karl


Randy Pollack wrote:

>Thanks, Karl.
>
>Below is another Twelf question that I emailed to twelf-list 2 days
>ago, but it hasn't passed the moderator yet.  I apologise if people
>think I'm polluting the poplmark list with technical questions about
>Twelf.
>
>Thanks,
>Randy
>--
>I have appended below a Twelf script for type preservation of cbv
>evaluation of simply typed lambda calculus.  It follows the example
>from the distribution `examples/guide/lam.elf' EXCEPT that there is a
>Church-style type tag on the constructor "lam" (which shows up in the
>typing rule "of_lam" and the evaluation rule "ev_lam").
>
>This script typechecks, but the type preservation theorem "tps" fails
>coverage checking.
>
> Coverage error --- missing cases:
> {E1:tm} {E2:tm} {E3:tm} {T1:tp} {E4:tm -> tm} {E5:tm} {T2:tp}
>    {D1:eval (E4 E5) E3} {D2:eval E2 E5} {D3:eval E1 (lam T2 ([e:tm] E4 e))}
>    {T3:tp} {P1:of E2 T3} {P2:of E1 (arr T3 T1)} {P3:of E3 T1}
>    |- tps (ev_app D1 D2 D3) (of_app P1 P2) P3.
>
>Why does this fail?
>
>BTW, the automatic proof (copied from `examples/guide/lam.elf')
>succeeds:
>
> %theorem
> tpsa : forall* {E:tm} {V:tm} {T:tp}
>	forall {D:eval E V} {P:of E T}
>	exists {Q:of V T}
>	true.
> %prove 5 D (tpsa D P Q).
>
>If we change the typing rule "of_lam" to
>
>  of_lam : of (lam _ E) (arr T1 T2) <- ({x:tm} of x T1 -> of (E x) T2).
>  %%%%%%           ^      %%% free type tag
>
>Then the coverage (and totality) check succeeds.  (Perhaps this last
>is not surprising, because coverage checking succeeds for the
>Curry-style system in `examples/guide/lam.elf'.)
>
>Randy
>--
>% Simple types
>tp  : type.				%name tp T.
>arr : tp -> tp -> tp.
>
>% Terms
>tm  : type.				%name tm E.
>lam : tp -> (tm -> tm) -> tm.
>%%%   ^^                        %%%% Church-style type tag!
>app : tm -> tm -> tm.
>
>% Typing judgement
>of     : tm -> tp -> type.		%name of P.
>of_lam : of (lam T1 E) (arr T1 T2)
>	  <- ({x:tm} of x T1 -> of (E x) T2).
>of_app : of (app E1 E2) T1
>	  <- of E1 (arr T2 T1)
>	  <- of E2 T2.
>
>% Evaluation (call-by-value) 
>eval   : tm -> tm -> type.		%name eval D.
>ev_lam : eval (lam T E) (lam T E).
>ev_app : eval (app E1 E2) V
>	    <- eval E1 (lam T E1')
>	    <- eval E2 V2
>	    <- eval (E1' V2) V.
>
>
>% Type preservation as higher-level family
>tps : eval E V -> of E T -> of V T -> type.
>%mode tps +D +P -Q.
>
>tps_lam : tps ev_lam (of_lam P) (of_lam P).
>tps_app : tps (ev_app D3 D2 D1) (of_app P2 P1) Q
>	   <- tps D1 P1 (of_lam Q1')
>	   <- tps D2 P2 Q2
>	   <- tps D3 (Q1' V2 Q2) Q.
>
>%worlds () (tps D P _).
>%total D (tps DP _).
>
>
>
>  
>