[POPLmark] how to believe a twelf proof

[Karl Crary]

Randy,

The %worlds declaration does not give only the interface to the theorem, 
it also gives the induction hypothesis.  So you are correct, the bind 
block is there because of the case that extends the context, and a 
different proof might use a different %worlds declaration.  As usual, if 
you want to weaken the result after the induction, you can declare 
another theorem that calls this one.

    -- Karl


Randy Pollack wrote:

>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 _ _).
>_______________________________________________
>Poplmark mailing list
>Poplmark at lists.seas.upenn.edu
>http://lists.seas.upenn.edu/mailman/listinfo/poplmark
>
>
>  
>