[POPLmark] how to believe a twelf proof

[Randy Pollack]

Karl,

Okay, "sr" checks in every world for which the representations of
"tp", "tm", "of" and "red" are adequate, so we can read "sr" as a
theorem about the intended object language typing and reduction
relations.  Am I right that this is your point?

Similarly, Frank's proof of type preservation for cbv evaluation,
which hapens to check in a closed world, also checks in every world
for which the representations of "tp", "tm", "of" and "eval" are
adequate, so we can read "sr" as a theorem about the intended object
language typing and evaluation relations.

Now we are getting to my real question.  In your PoplMark solution,
file 1a.elf, the lemma "trans" does NOT check in every world in which
"tp", "assm" and "sub" are adequate representations of the intended
object language.  I believe you agreed with me in previous email that
the world in which "tp", "assm" and "sub" are adequate representations
is generated by the block

  %block pure : some {t:tp} block {x:tp} {d:assm x t}.

But "trans" also requires some other assumptions about "var" and
"assm_var" to check.  So, why should I consider "trans" as a theorem
about the intended object language subtyping relation???

Randy
--
Karl Crary writes:
 > 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
 > >
 > >
 > >  
 > >
 >