[POPLmark] how to believe a twelf proof

[Randy Pollack]

Bob and Karl,

I am appending below a completed version of your subject reduction
example.  I have added some annotations that might help other readers
new to Twelf.

The proof of subject reduction is checked in the world

  %block bind : some {t:tp} block {x:tm} {d:of x t}.
  %worlds (bind) (sr _ _ _).

just as you said.

But why must "sr" be checked in the world defined by bind?  Your note
seems to imply this is because the representation of the typing
judgement (namely "of") is adequate in this world.  But experimenting
with Twelf suggests that is irrelevant.  For example, Frank's proof of
type preservation for cbv evaluation (in the twelf release
examples/guide directory) checks in a *closed* world (no blocks),
although the representation of the typing judgement is essentially the
same.

I guess the real reason "sr" needs to be checked in the world defined
by bind is that the proof case "sr_lam" extends the context by a bind
block (which Frank's proof of type preservation does not do).

So might different proofs of the same lemma require different worlds
for checking?  I guess the answer is "yes".

In spite of reading your note closely, I'm still confused about the
relationship between adequacy of a representation, and the world in
which theorems about that represenation should be checked.

Randy
--
% Simple types
tp  : type.				%name tp T.
o   : tp.
arr : tp -> tp -> tp.

% Terms
tm  : type.				%name tm E.
lam : tp -> (tm -> tm) -> tm.
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.

% reduction
red       : tm -> tm -> type.
red_beta  : red (app (lam T F) E) (F E).
red_lam   : ({x} red (F x) (F' x)) -> red (lam T F) (lam T F').
red_app_1 : red E1 E1' -> red (app E1 E2) (app E1' E2).
red_app_2 : red E2 E2' -> red (app E1 E2) (app E1 E2').


% subject reduction
sr : red E1 E2 -> of E1 T -> of E2 T -> type.
%mode sr +D1 +D2 -D.

sr_lam   : sr (red_lam U') (of_lam V1') (of_lam V2')
            <- ({x}{d} sr (U' x) (V1' x d) (V2' x d)).
sr_app_1 : sr (red_app_1 (U': red E1 E1'))
              (of_app (U1: of E2 T) D1)
              (of_app U1 D2)
            <- sr U' (D1:of E1 (arr T S)) (D2:of E1' (arr T S)).
sr_app_2 : sr (red_app_2 (U': red E2 E2'))
              (of_app D1 (U2: of E1 (arr T S)))
              (of_app D2 U2)
            <- sr U' (D1: of E2 T) (D2: of E2' T).
sr_beta : sr (red_beta: red (app (lam T F) E) (F E))
               (of_app (Q: of E T)
                       (of_lam (R: {x}{d}of (F x) S) : of (lam T F) (arr T S))
                  : of (app (lam T F) E) S)
               (R E Q: of (F E) S).

%block bind : some {t:tp} block {x:tm} {d:of x t}.
%worlds () (sr _ _ _).
%total D (sr D _ _).