[POPLmark] How to believe the Twelf proof of 1a

[Michael Philip Ashley-Rollman]

Randy,

In order to believe the theorem, you want to believe that the world 
containing bind is just as good as the world for which the adequacy 
theorem holds. In this case, you need only believe that none of the extra 
assumptions in the world cannot appear in the output of the theorem. In 
this case, since sub S T cannot contain var x within it somewhere and it 
cannot contain assm_var d dv in it anywhere, you may conclude that the 
derivation of sub S T produced by the trans theorem can only contain x and 
d. Thus, if we were to remove all of the extra assumptions from the world, 
we would still have a valid derivation of sub S T in the world
some {t:tp} block {x:tp} {d:assm x t}.
 	-Michael

On Wed, 18 May 2005, Randy Pollack wrote:

> Karl,
>
> I'm still unclear on the meaning of "var".  Suppose I want to believe
> that the main formal result in file 1a.elf proves the intended
> property of the intended object system.
>
>  %block bind  : some {t:tp}
> 		 block {x:tp} {dv:var x} {d:assm x t} {thm:assm_var d dv}.
>  trans : sub S Q -> sub Q T -> sub S T -> type.
>  %mode trans +X1 +X2 -X3.
>  - : trans D1 D2 D3 <- trans* _ _ nat_eq_ D1 D2 D3.
>  %worlds (bind) (trans _ _ _).
>  %total {} (trans _ _ _).
>
> (You've pointed out that the world (bind) is part of the statement of
> this result.)
>
> I must believe some adequacy theorem about "sub" and "assm", which in
> this case resides in the world
>
>  some {t:tp} block {x:tp} {d:assm x t}
>
> (As we have discussed, by choosing the world of the adequacy theorem,
> I specify which of the possible object systems I'm interested in.
> E.g. one could consider the world
>
>  some {t:tp -> tp} block {x:tp} {d:assm x (t x)}  %% funny binding
>
> but that is not the intended object system.)
>
> QUESTION: what do I need to believe about "var" in order to believe
> the theorem?  "var" doesn't show up in the declaration of "sub" or in
> the adequacy theorem, but it does appear in the statement of "trans".
>
> Randy
> _______________________________________________
> Poplmark mailing list
> Poplmark at lists.seas.upenn.edu
> http://lists.seas.upenn.edu/mailman/listinfo/poplmark
>
>