[POPLmark] Twelf question

[Randy Pollack]

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 _).