% tm-safety.elf: % % Type safety for target terms (using relations typeoftm and steptm). % % Contents: % % 1. eqtm: equality on terms, including a bunch of congruence rules; % 2. tm-safety: main type safety theorem for the target language; % 3. values-dont-step: lemma for tm-deterministic; % 4. absurd-eqtm: reasoning from contradiction, for tm-deterministic; % 5. tm-deterministic: steptm is deterministic. eqtm : tm -> tm -> type. eqtm/refl : eqtm M M. eqtm/pair : eqtm M1 N1 -> eqtm M2 N2 -> eqtm (pairtm M1 M2) (pairtm N1 N2). eqtm/proj : {k : 2er} eqtm M N -> eqtm (projtm k M) (projtm k N). eqtm/fst = eqtm/proj 1. eqtm/snd = eqtm/proj 2. eqtm/inj : {k : 2er} eqtm M N -> eqtm (injtm k M) (injtm k N). eqtm/inl = eqtm/inj 1. eqtm/inr = eqtm/inj 2. eqtm/case : eqtm M0 N0 -> eqtm (casetm M0 MN1 MN2) (casetm N0 MN1 MN2). % We don't need to reason under equivalence of the branches, % so casetms are equal only when their branches are identical. eqtm/lam : {EqBody : {m : tm} eqtm (M m) (M' m)} eqtm (lamtm ([m] M m)) (lamtm ([m] M' m)). eqtm/app : {Eq1 : eqtm M1 N1} {Eq2 : eqtm M2 N2} eqtm (apptm M1 M2) (apptm N1 N2). %freeze eqtm. % tm-safe M T: Either M is a value, or steps to a term of type T. tm-safe : tm -> ty -> type. tm-safe/val : is-valuetm M -> tm-safe M T. tm-safe/step : steptm M M' -> typeoftm M' T -> tm-safe M T. % % Type safety % tm-safety : % If typeoftm M T % then -> tm-safe M T -> type. %mode tm-safety +D -Safe. - : tm-safety (typeoftm/unitintro) (tm-safe/val is-valuetm/unit). - : tm-safety (typeoftm/arrintro D) (tm-safe/val is-valuetm/lam). tm-safety-app-lemma : % If tm-safe M1 (arr T U) -> tm-safe M2 T -> typeoftm M1 (arr T U) -> typeoftm M2 T % then -> tm-safe (apptm M1 M2) U -> type. %mode tm-safety-app-lemma +Safe1 +Safe2 +D1 +D2 -Safe. - : tm-safety-app-lemma (tm-safe/step Step1 D1') Safe2 D1 D2 (tm-safe/step (steptm/app1 Step1) (typeoftm/arrelim D1' D2)). - : tm-safety-app-lemma (tm-safe/val IsVal1) (tm-safe/step Step2 D2') D1 D2 (tm-safe/step (steptm/app2 IsVal1 Step2) (typeoftm/arrelim D1 D2')). - : tm-safety-app-lemma (tm-safe/val IsVal1) (tm-safe/val IsVal2) (typeoftm/arrintro DBody) D2 (tm-safe/step (steptm/beta IsVal2) (DBody M2 D2)). %worlds () (tm-safety-app-lemma _ _ _ _ _). %total {} (tm-safety-app-lemma _ _ _ _ _). - : tm-safety (typeoftm/arrelim D1 D2) Safe <- tm-safety D1 Safe1 <- tm-safety D2 Safe2 <- tm-safety-app-lemma Safe1 Safe2 D1 D2 Safe. tm-safety-fst-lemma : % If tm-safe M (prod T1 T2) -> typeoftm M (prod T1 T2) % then -> tm-safe (fsttm M) T1 -> type. %mode tm-safety-fst-lemma +SafeIn +D -SafeOut. - : tm-safety-fst-lemma (tm-safe/val IsVal) (typeoftm/prodintro D1 D2) (tm-safe/step (steptm/fst IsVal) D1). - : tm-safety-fst-lemma (tm-safe/step Step1 D1) D (tm-safe/step (steptm/fst0 Step1) (typeoftm/prodelim1 D1)). %worlds () (tm-safety-fst-lemma _ _ _). %total {} (tm-safety-fst-lemma _ _ _). - : tm-safety (typeoftm/prodelim1 D) Safe <- tm-safety D SafePair <- tm-safety-fst-lemma SafePair D Safe. tm-safety-snd-lemma : % If tm-safe M (prod T1 T2) -> typeoftm M (prod T1 T2) % then -> tm-safe (sndtm M) T2 -> type. %mode tm-safety-snd-lemma +SafeIn +D -SafeOut. - : tm-safety-snd-lemma (tm-safe/val IsVal) (typeoftm/prodintro D1 D2) (tm-safe/step (steptm/snd IsVal) D2). - : tm-safety-snd-lemma (tm-safe/step Step1 D1) D (tm-safe/step (steptm/snd0 Step1) (typeoftm/prodelim2 D1)). %worlds () (tm-safety-snd-lemma _ _ _). %total {} (tm-safety-snd-lemma _ _ _). - : tm-safety (typeoftm/prodelim2 D) Safe <- tm-safety D SafePair <- tm-safety-snd-lemma SafePair D Safe. tm-safety-prod-lemma : % If tm-safe M1 T1 -> tm-safe M2 T2 -> typeoftm M1 T1 -> typeoftm M2 T2 % then -> tm-safe (pairtm M1 M2) (prod T1 T2) -> type. %mode tm-safety-prod-lemma +Safe1 +Safe2 +D1 +D2 -Safe. - : tm-safety-prod-lemma (tm-safe/step Step1 D1') Safe2 D1 D2 (tm-safe/step (steptm/pair1 Step1) (typeoftm/prodintro D1' D2)). - : tm-safety-prod-lemma (tm-safe/val IsVal1) (tm-safe/step Step2 D2') D1 D2 (tm-safe/step (steptm/pair2 IsVal1 Step2) (typeoftm/prodintro D1 D2')). - : tm-safety-prod-lemma (tm-safe/val IsVal1) (tm-safe/val IsVal2) D1 D2 (tm-safe/val (is-valuetm/pair IsVal1 IsVal2)). %worlds () (tm-safety-prod-lemma _ _ _ _ _). %total {} (tm-safety-prod-lemma _ _ _ _ _). - : tm-safety (typeoftm/prodintro D1 D2) Safe <- tm-safety D1 Safe1 <- tm-safety D2 Safe2 <- tm-safety-prod-lemma Safe1 Safe2 D1 D2 Safe. - : tm-safety (typeoftm/fix Dfix) (tm-safe/step (steptm/fix) (Dfix _ (typeoftm/fix Dfix))). tm-safety-inl-lemma : % If {T2 : ty} tm-safe M T1 -> typeoftm M T1 % then -> tm-safe (inltm M) (sumty T1 T2) -> type. %mode tm-safety-inl-lemma +T2 +SafeIn +D -SafeOut. - : tm-safety-inl-lemma _ (tm-safe/val IsVal) D1 (tm-safe/val (is-valuetm/inl IsVal)). - : tm-safety-inl-lemma _ (tm-safe/step Step1 D1) D (tm-safe/step (steptm/inl0 Step1) (typeoftm/sumintro1 D1)). %worlds () (tm-safety-inl-lemma _ _ _ _). %total {} (tm-safety-inl-lemma _ _ _ _). - : tm-safety (typeoftm/sumintro1 D) Safe <- tm-safety D SafeInl <- tm-safety-inl-lemma _ SafeInl D Safe. tm-safety-inr-lemma : % If {T1 : ty} tm-safe M T2 -> typeoftm M T2 % then -> tm-safe (inrtm M) (sumty T1 T2) -> type. %mode tm-safety-inr-lemma +T1 +SafeIn +D -SafeOut. - : tm-safety-inr-lemma _ (tm-safe/val IsVal) D2 (tm-safe/val (is-valuetm/inr IsVal)). - : tm-safety-inr-lemma _ (tm-safe/step Step2 D2) D (tm-safe/step (steptm/inr0 Step2) (typeoftm/sumintro2 D2)). %worlds () (tm-safety-inr-lemma _ _ _ _). %total {} (tm-safety-inr-lemma _ _ _ _). - : tm-safety (typeoftm/sumintro2 D) Safe <- tm-safety D SafeInr <- tm-safety-inr-lemma _ SafeInr D Safe. tm-safety-case-lemma : % If tm-safe M (sumty T1 T2) -> typeoftm M (sumty T1 T2) -> ({m1 : tm} {d1 : typeoftm m1 T1} typeoftm (N1 m1) C) -> ({m2 : tm} {d2 : typeoftm m2 T2} typeoftm (N2 m2) C) % then -> tm-safe (casetm M N1 N2) C -> type. %mode tm-safety-case-lemma +Safe0 +D0 +D1 +D2 -Safe. - : tm-safety-case-lemma (tm-safe/step Step0 D0') D0 D1 D2 (tm-safe/step (steptm/case0 Step0) (typeoftm/sumelim D0' D1 D2)). - : {U : ty} {D1 : {m1 : tm} {d1 : typeoftm m1 T1} typeoftm (N1 m1) U} {D2 : {m2 : tm} {d2 : typeoftm m2 T2} typeoftm (N2 m2) U} {M0 : tm} {D0' : typeoftm M0 T1} {IsVal0 : is-valuetm M0} tm-safety-case-lemma (tm-safe/val (is-valuetm/inl IsVal0)) (typeoftm/sumintro1 D0') D1 D2 (tm-safe/step (steptm/case1 IsVal0) (D1 M0 D0')) . - : {U : ty} {D1 : {m1 : tm} {d1 : typeoftm m1 T1} typeoftm (N1 m1) U} {D2 : {m2 : tm} {d2 : typeoftm m2 T2} typeoftm (N2 m2) U} {M0 : tm} {D0' : typeoftm M0 T2} {IsVal0 : is-valuetm M0} tm-safety-case-lemma (tm-safe/val (is-valuetm/inr IsVal0)) (typeoftm/sumintro2 D0') D1 D2 (tm-safe/step (steptm/case2 IsVal0) (D2 M0 D0')) . %worlds () (tm-safety-case-lemma _ _ _ _ _). %total {} (tm-safety-case-lemma _ _ _ _ _). - : tm-safety (typeoftm/sumelim D0 D1 D2) Safe <- tm-safety D0 Safe0 <- tm-safety-case-lemma Safe0 D0 D1 D2 Safe. %worlds () (tm-safety _ _). %total D (tm-safety D _). % % values-dont-steptm % values-dont-steptm : % If steptm M N -> is-valuetm M % then -> absurd -> type. %mode values-dont-steptm +Step +IsVal -ABSURD. - : values-dont-steptm (steptm/pair1 Step1) (is-valuetm/pair IsVal1 _) ABSURD <- values-dont-steptm Step1 IsVal1 ABSURD. - : values-dont-steptm (steptm/pair2 IsVal1' Step2) (is-valuetm/pair IsVal1 IsVal2) ABSURD <- values-dont-steptm Step2 IsVal2 ABSURD. - : values-dont-steptm (steptm/inl0 Step) (is-valuetm/inl IsVal) ABSURD <- values-dont-steptm Step IsVal ABSURD. - : values-dont-steptm (steptm/inr0 Step) (is-valuetm/inr IsVal) ABSURD <- values-dont-steptm Step IsVal ABSURD. %worlds () (values-dont-steptm _ _ _). %total [Step IsVal] (values-dont-steptm Step IsVal _). absurd-eqtm : % If {M : tm} {N : tm} absurd % then -> eqtm M N -> type. %mode absurd-eqtm +M +N +ABSURD -Eq. %worlds () (absurd-eqtm _ _ _ _). %total {} (absurd-eqtm _ _ _ _). % % tm-deterministic % tm-deterministic : % If steptm M N1 -> steptm M N2 % then -> eqtm N1 N2 -> type. %mode tm-deterministic +Step1 +Step2 -Eq. - : tm-deterministic (steptm/pair1 Step11) (steptm/pair1 Step21) (eqtm/pair Eq1 (eqtm/refl)) <- tm-deterministic Step11 Step21 Eq1. - : tm-deterministic (steptm/pair2 IsVal11 Step12) (steptm/pair2 IsVal21 Step22) (eqtm/pair (eqtm/refl) Eq2) <- tm-deterministic Step12 Step22 Eq2. - : tm-deterministic (steptm/pair2 IsVal1 _) (steptm/pair1 Step) Eq <- values-dont-steptm Step IsVal1 ABSURD <- absurd-eqtm _ _ ABSURD Eq. - : tm-deterministic (steptm/pair1 Step) (steptm/pair2 IsVal1 _) Eq <- values-dont-steptm Step IsVal1 ABSURD <- absurd-eqtm _ _ ABSURD Eq. - : tm-deterministic (steptm/fst IsVal1) (steptm/fst IsVal2) (eqtm/refl). - : tm-deterministic (steptm/snd IsVal1) (steptm/snd IsVal2) (eqtm/refl). - : tm-deterministic (steptm/fst0 Step1) (steptm/fst0 Step2) (eqtm/fst Eq) <- tm-deterministic Step1 Step2 Eq. - : tm-deterministic (steptm/snd0 Step1) (steptm/snd0 Step2) (eqtm/snd Eq) <- tm-deterministic Step1 Step2 Eq. - : tm-deterministic (steptm/fst0 Step) (steptm/fst IsVal) Eq <- values-dont-steptm Step IsVal ABSURD <- absurd-eqtm _ _ ABSURD Eq. - : tm-deterministic (steptm/fst IsVal) (steptm/fst0 Step) Eq <- values-dont-steptm Step IsVal ABSURD <- absurd-eqtm _ _ ABSURD Eq. - : tm-deterministic (steptm/snd0 Step) (steptm/snd IsVal) Eq <- values-dont-steptm Step IsVal ABSURD <- absurd-eqtm _ _ ABSURD Eq. - : tm-deterministic (steptm/snd IsVal) (steptm/snd0 Step) Eq <- values-dont-steptm Step IsVal ABSURD <- absurd-eqtm _ _ ABSURD Eq. - : tm-deterministic (steptm/app1 Step1) (steptm/app1 Step2) (eqtm/app Eq1 (eqtm/refl)) <- tm-deterministic Step1 Step2 Eq1. - : tm-deterministic (steptm/app2 IsVal1 Step1) (steptm/app2 IsVal2 Step2) (eqtm/app (eqtm/refl) Eq2) <- tm-deterministic Step1 Step2 Eq2. - : tm-deterministic (steptm/beta IsVal1) (steptm/beta IsVal2) (eqtm/refl). - : tm-deterministic (steptm/beta IsVal1) (steptm/app2 IsVal2 Step2) Eq <- values-dont-steptm Step2 IsVal1 ABSURD <- absurd-eqtm _ _ ABSURD Eq. - : tm-deterministic (steptm/app2 IsVal2 Step2) (steptm/beta IsVal1) Eq <- values-dont-steptm Step2 IsVal1 ABSURD <- absurd-eqtm _ _ ABSURD Eq. - : tm-deterministic (steptm/app2 IsVal1 _) (steptm/app1 Step) Eq <- values-dont-steptm Step IsVal1 ABSURD <- absurd-eqtm _ _ ABSURD Eq. - : tm-deterministic (steptm/app1 Step) (steptm/app2 IsVal1 _) Eq <- values-dont-steptm Step IsVal1 ABSURD <- absurd-eqtm _ _ ABSURD Eq. - : tm-deterministic (steptm/fix) (steptm/fix) (eqtm/refl). - : tm-deterministic (steptm/inl0 Step1) (steptm/inl0 Step2) (eqtm/inl Eq) <- tm-deterministic Step1 Step2 Eq. - : tm-deterministic (steptm/inr0 Step1) (steptm/inr0 Step2) (eqtm/inr Eq) <- tm-deterministic Step1 Step2 Eq. - : tm-deterministic (steptm/case0 Step1) (steptm/case0 Step2) (eqtm/case Eq0) <- tm-deterministic Step1 Step2 Eq0. - : tm-deterministic (steptm/case1 IsVal1) (steptm/case1 IsVal2) (eqtm/refl). - : tm-deterministic (steptm/case2 IsVal1) (steptm/case2 IsVal2) (eqtm/refl). - : tm-deterministic (steptm/case0 Step) (steptm/case1 IsVal) Eq <- values-dont-steptm Step (is-valuetm/inl IsVal) ABSURD <- absurd-eqtm _ _ ABSURD Eq. - : tm-deterministic (steptm/case0 Step) (steptm/case2 IsVal) Eq <- values-dont-steptm Step (is-valuetm/inr IsVal) ABSURD <- absurd-eqtm _ _ ABSURD Eq. - : tm-deterministic (steptm/case1 IsVal) (steptm/case0 Step) Eq <- values-dont-steptm Step (is-valuetm/inl IsVal) ABSURD <- absurd-eqtm _ _ ABSURD Eq. - : tm-deterministic (steptm/case2 IsVal) (steptm/case0 Step) Eq <- values-dont-steptm Step (is-valuetm/inr IsVal) ABSURD <- absurd-eqtm _ _ ABSURD Eq. %worlds () (tm-deterministic _ _ _). %total [Step1 Step2] (tm-deterministic Step1 Step2 _).