% % typeof-elab.elf % % Theorems relating `typeof' and `elab' judgments: % % elab-complete says that if typeof E A then elab E A M (i.e., elab is complete with respect to typeof). % % typeof-erase says that if elab E A M then typeof E A (i.e., the elaborated term M can be erased). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % elab-complete % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% elab-complete : % If typeof E A % then -> elab E A M -> type. %mode elab-complete +D -Elab. - : elab-complete (typeof/topintro IsVal) (elab/topintro IsVal). - : elab-complete (typeof/arrelim D1 D2) (elab/arrelim Elab1 Elab2) <- elab-complete D1 Elab1 <- elab-complete D2 Elab2. - : elab-complete (typeof/merge1 D1) (elab/merge1 Elab1) <- elab-complete D1 Elab1. - : elab-complete (typeof/merge2 D2) (elab/merge2 Elab2) <- elab-complete D2 Elab2. - : elab-complete (typeof/sectintro D1 D2) (elab/sectintro Elab1 Elab2) <- elab-complete D1 Elab1 <- elab-complete D2 Elab2. - : elab-complete (typeof/sectelim1 D1) (elab/sectelim1 Elab1) <- elab-complete D1 Elab1. - : elab-complete (typeof/sectelim2 D2) (elab/sectelim2 Elab2) <- elab-complete D2 Elab2. - : elab-complete (typeof/unintro1 D1) (elab/unintro1 Elab1) <- elab-complete D1 Elab1. - : elab-complete (typeof/unintro2 D2) (elab/unintro2 Elab2) <- elab-complete D2 Elab2. - : {A1 : ty} {A2 : ty} {C : ty} {E : exp -> exp} {N1 : tm -> tm} {D1 : {e1:exp} typeof e1 A1 -> typeof (E e1) C} {Elab1 : {e1:exp} {m1:tm} elab e1 A1 m1 -> elab (E e1) C (N1 m1)} {N2 : tm -> tm} {D2 : {e2:exp} typeof e2 A2 -> typeof (E e2) C} {Elab2 : {e2:exp} {m2:tm} elab e2 A2 m2 -> elab (E e2) C (N2 m2)} {E' : exp} {M':tm} {D' : typeof E' (unty A1 A2)} {Elab' : elab E' (unty A1 A2) M'} {EC : eval-context} {Fill : fill EC E} elab-complete (typeof/unelim EC Fill D' D1 D2) (elab/unelim Fill Elab' Elab1 Elab2) <- elab-complete D' Elab' <- ({x1:exp} {Dx1:typeof x1 A1} {m1:tm} {Elabx1:elab x1 A1 m1} elab-complete Dx1 Elabx1 -> elab-complete (D1 x1 Dx1) (Elab1 x1 m1 Elabx1)) <- ({x2:exp} {Dx2:typeof x2 A2} {m2:tm} {Elabx2:elab x2 A2 m2} elab-complete Dx2 Elabx2 -> elab-complete (D2 x2 Dx2) (Elab2 x2 m2 Elabx2)) . - : {A : ty} {C : ty} {E : exp -> exp} {N1 : tm -> tm} {D1 : {e1:exp} typeof e1 A -> typeof (E e1) C} {Elab1 : {e1:exp} {m1:tm} elab e1 A m1 -> elab (E e1) C (N1 m1)} {E' : exp} {M':tm} {D' : typeof E' A} {Elab' : elab E' A M'} {EC : eval-context} {Fill : fill EC E} elab-complete (typeof/direct _ Fill D' D1) (elab/direct Fill Elab' Elab1) <- elab-complete D' Elab' <- ({x1:exp} {Dx1:typeof x1 A} {m1:tm} {Elabx1:elab x1 A m1} elab-complete Dx1 Elabx1 -> elab-complete (D1 x1 Dx1) (Elab1 x1 m1 Elabx1)) . - : {A : ty} {E1:exp -> exp} {M1:tm -> tm} {Elab : {e : exp} {m : tm} elab e A m -> elab (E1 e) A (M1 m)} {D : {e : exp} typeof e A -> typeof (E1 e) A} elab-complete (typeof/fix D) (elab/fix Elab) <- ({e : exp} {D0 : typeof e A} {m : tm} {Elab0 : elab e A m} elab-complete D0 Elab0 -> elab-complete (D e D0) (Elab e m Elab0)). - : {E1 : exp -> exp} {A : ty} {B : ty} {D : {e:exp} typeof e A -> typeof (E1 e) B} {M1 : tm -> tm} {Elab : {e:exp} {m:tm} elab e A m -> elab (E1 e) B (M1 m)} elab-complete (typeof/arrintro D) (elab/arrintro Elab) <- ({e:exp} {DArg : typeof e A} {m : tm} {ElabArg : elab e A m} {_ : elab-complete DArg ElabArg} elab-complete (D e DArg) (Elab e m ElabArg)). %block elab-complete\block : some {A : ty} block {e : exp} {D : typeof e A} {m : tm} {Elab : elab e A m} {_ : elab-complete D Elab}. %worlds (elab-complete\block) (elab-complete _ _). %total D (elab-complete D _). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % typeof-erase: If elab E A M then typeof E A. % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% typeof-erase : typeof E A % *** implied-by *** -> elab E A M -> type. % % I reversed the usual % If ... % then structure so I could copy and paste % the proof of elab-complete, substituting "typeof-erase" for "elab-complete". % %mode typeof-erase -D +Elab. % Output first, then input! - : typeof-erase (typeof/topintro IsVal) (elab/topintro IsVal). - : typeof-erase (typeof/arrelim D1 D2) (elab/arrelim Elab1 Elab2) <- typeof-erase D1 Elab1 <- typeof-erase D2 Elab2. - : typeof-erase (typeof/merge1 D1) (elab/merge1 Elab1) <- typeof-erase D1 Elab1. - : typeof-erase (typeof/merge2 D2) (elab/merge2 Elab2) <- typeof-erase D2 Elab2. - : typeof-erase (typeof/sectintro D1 D2) (elab/sectintro Elab1 Elab2) <- typeof-erase D1 Elab1 <- typeof-erase D2 Elab2. - : typeof-erase (typeof/sectelim1 D1) (elab/sectelim1 Elab1) <- typeof-erase D1 Elab1. - : typeof-erase (typeof/sectelim2 D2) (elab/sectelim2 Elab2) <- typeof-erase D2 Elab2. - : typeof-erase (typeof/unintro1 D1) (elab/unintro1 Elab1) <- typeof-erase D1 Elab1. - : typeof-erase (typeof/unintro2 D2) (elab/unintro2 Elab2) <- typeof-erase D2 Elab2. - : {A1 : ty} {A2 : ty} {C : ty} {E : exp -> exp} {N1 : tm -> tm} {D1 : {e1:exp} typeof e1 A1 -> typeof (E e1) C} {Elab1 : {e1:exp} {m1:tm} elab e1 A1 m1 -> elab (E e1) C (N1 m1)} {N2 : tm -> tm} {D2 : {e2:exp} typeof e2 A2 -> typeof (E e2) C} {Elab2 : {e2:exp} {m2:tm} elab e2 A2 m2 -> elab (E e2) C (N2 m2)} {E' : exp} {M':tm} {D' : typeof E' (unty A1 A2)} {Elab' : elab E' (unty A1 A2) M'} {EC : eval-context} {Fill : fill EC E} typeof-erase (typeof/unelim EC Fill D' D1 D2) (elab/unelim Fill Elab' Elab1 Elab2) <- typeof-erase D' Elab' <- ({x1:exp} {Dx1:typeof x1 A1} {m1:tm} {Elabx1:elab x1 A1 m1} typeof-erase Dx1 Elabx1 -> typeof-erase (D1 x1 Dx1) (Elab1 x1 m1 Elabx1)) <- ({x2:exp} {Dx2:typeof x2 A2} {m2:tm} {Elabx2:elab x2 A2 m2} typeof-erase Dx2 Elabx2 -> typeof-erase (D2 x2 Dx2) (Elab2 x2 m2 Elabx2)) . - : {A : ty} {C : ty} {E : exp -> exp} {N1 : tm -> tm} {D1 : {e1:exp} typeof e1 A -> typeof (E e1) C} {Elab1 : {e1:exp} {m1:tm} elab e1 A m1 -> elab (E e1) C (N1 m1)} {E' : exp} {M':tm} {D' : typeof E' A} {Elab' : elab E' A M'} {EC : eval-context} {Fill : fill EC E} typeof-erase (typeof/direct _ Fill D' D1) (elab/direct Fill Elab' Elab1) <- typeof-erase D' Elab' <- ({x1:exp} {Dx1:typeof x1 A} {m1:tm} {Elabx1:elab x1 A m1} typeof-erase Dx1 Elabx1 -> typeof-erase (D1 x1 Dx1) (Elab1 x1 m1 Elabx1)) . - : {A : ty} {E1:exp -> exp} {M1:tm -> tm} {Elab : {e : exp} {m : tm} elab e A m -> elab (E1 e) A (M1 m)} {D : {e : exp} typeof e A -> typeof (E1 e) A} typeof-erase (typeof/fix D) (elab/fix Elab) <- ({e : exp} {D0 : typeof e A} {m : tm} {Elab0 : elab e A m} typeof-erase D0 Elab0 -> typeof-erase (D e D0) (Elab e m Elab0)). - : {E1 : exp -> exp} {A : ty} {B : ty} {D : {e:exp} typeof e A -> typeof (E1 e) B} {M1 : tm -> tm} {Elab : {e:exp} {m:tm} elab e A m -> elab (E1 e) B (M1 m)} typeof-erase (typeof/arrintro D) (elab/arrintro Elab) <- ({e:exp} {DArg : typeof e A} {m : tm} {ElabArg : elab e A m} {_ : typeof-erase DArg ElabArg} typeof-erase (D e DArg) (Elab e m ElabArg)). %block typeof-erase\block : some {A : ty} block {e : exp} {D : typeof e A} {m : tm} {Elab : elab e A m} {_ : typeof-erase D Elab}. %worlds (typeof-erase\block) (typeof-erase _ _). %total Elab (typeof-erase _ Elab).