(* Basic properties *********************************************************)
-lemma dxprs_refl: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ⦃h, L⦄ ⊢ T •*➡*[g] T.
-/3 width=3/ qed.
+lemma dxprs_refl: ∀h,g,L. reflexive … (dxprs h g L).
+/2 width=3/ qed.
lemma sstas_dxprs: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •*[g] T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2.
/2 width=3/ qed.
-lemma cprs_dxprs: ∀h,g,L,T1,T2,U,l. ⦃h, L⦄ ⊢ T1 •[g, l] U → L ⊢ T1 ➡* T2 →
- ⦃h, L⦄ ⊢ T1 •*➡*[g] T2.
-/3 width=3/ qed.
+lemma cprs_dxprs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2.
+/2 width=3/ qed.
lemma dxprs_strap1: ∀h,g,L,T1,T,T2.
⦃h, L⦄ ⊢ T1 •*➡*[g] T → L ⊢ T ➡ T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2.
lemma lsubss_dxprs_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
∀T1,T2. ⦃h, L2⦄ ⊢ T1 •*➡*[g] T2 → ⦃h, L1⦄ ⊢ T1 •*➡*[g] T2.
#h #g #L1 #L2 #HL12 #T1 #T2 *
-lapply (lsubss_fwd_lsubs2 … HL12) /4 width=5/
+lapply (lsubss_fwd_lsubs2 … HL12) /3 width=5/
qed-.
(**************************************************************************)
include "basic_2/computation/csn_aaa.ma".
-include "basic_2/computation/dxprs_lift.ma".
include "basic_2/computation/dxprs_aaa.ma".
include "basic_2/equivalence/cpcs_aaa.ma".
include "basic_2/dynamic/snv.ma".
| #I #L #K #V #i #HLK #_ * /3 width=6/
| #a * #L #V #T #_ #_ * #B #HV * #A #HA /3 width=2/
| #a #L #V #W #W0 #T #U #l #_ #_ #HVW #HW0 #HTU * #B #HV * #X #HT
- lapply (dxprs_aaa h g … HV W0 ?) [ -HTU /2 width=4/ ] -W #HW0 (**) (* auto fail without -HTU *)
+ lapply (dxprs_aaa h g … HV W0 ?) [ -HTU /3 width=4/ ] -W #HW0 (**) (* auto fail without -HTU *)
lapply (dxprs_aaa … HT … HTU) -HTU #H
elim (aaa_inv_abst … H) -H #B0 #A #H1 #HU #H2 destruct
lapply (aaa_mono … H1 … HW0) -W0 #H destruct /3 width=4/
elim (ltpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) -HLK1 #HLK1
- lapply (IH1 … HV1 … HK12 V2 ?) -IH1 -HV1 -HK12 // -L1 -K1 /4 width=1/ -HV12 /2 width=5/
+ lapply (IH1 … HV1 … HK12 V2 ?) -IH1 -HV1 -HK12 //
+ [ @cprs_dxprs /3 width=1/ (**) (* auto: /4 width=1/ fails *)
+ ] -HV12 /2 width=5/
| #p #Hn #H1 #L2 #HL12 #X #H2 destruct -IH2
elim (snv_inv_gref … H1)
| #a #I #V1 #T1 #Hn #H1 #L2 #HL12 #X #H2 destruct -IH2
[ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct
lapply (tps_lsubs_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02
lapply (cpr_intro (L2.ⓑ{I}V2) … T2 0 1 HT10 ?) -HT10 /2 width=1/ -HT02 #HT12
- lapply (IH1 … HV1 … HL12 V2 ?) -HV1 // /4 width=1/ #HV2
+ lapply (IH1 … HV1 … HL12 V2 ?) -HV1 //
+ [ @cprs_dxprs /3 width=1/ (**) (* auto: /4 width=1/ fails *)
+ ] #HV2
lapply (IH1 … HT1 (L2.ⓑ{I}V2) … T2 ?) -IH1 -HT1 /3 width=1/
| #T2 #HT12 #HXT2 #H1 #H2 destruct
- lapply (IH1 … HT1 (L2.ⓓV1) … T2 ?) -IH1 -HT1 // /4 width=1/ -HT12 -HL12 #HT2
+ lapply (IH1 … HT1 (L2.ⓓV1) … T2 ?) -IH1 -HT1 // /2 width=2/
+ [ @cprs_dxprs /3 width=1/ (**) (* auto: /4 width=1/ fails *)
+ ] -HT12 -HL12 #HT2
lapply (snv_inv_lift … HT2 L2 … HXT2) -T2 // /2 width=1/
]
| #V1 #T1 #Hn #H1 #L2 #HL12 #X #H2 destruct
elim (snv_inv_appl … H1) -H1 #a #W10 #W1 #U1 #l #HV1 #HT1 #HVW1 #HW10 #HTU1
elim (tpr_inv_appl1 … H2) -H2 *
[ #V2 #T2 #HV12 #HT12 #H destruct
- lapply (IH1 … HV1 … HL12 V2 ?) // /4 width=1/ #HV2
- lapply (IH1 … HT1 … HL12 T2 ?) // /4 width=1/ #HT2
+ lapply (IH1 … HV1 … HL12 V2 ?)
+ [ @cprs_dxprs /3 width=1/ (**) (* auto: /4 width=1/ fails *)
+ | //
+ ] #HV2
+ lapply (IH1 … HT1 … HL12 T2 ?)
+ [ @cprs_dxprs /3 width=1/ (**) (* auto: /4 width=1/ fails *)
+ | //
+ ] #HT2
lapply (IH1 … HT1 … HTU1) -IH1 // #H
elim (snv_inv_bind … H) -H #HW1 #HU1
elim (IH2 … HVW1 … HL12 … HV12 HV1) -IH2 -HVW1 -HV12 -HV1 // #W2 #HVW2 #HW12
interpretation "stratified static type assignment (term)"
'StaticType h g l L T U = (ssta h g l L T U).
+definition ssta_step: ∀h. sd h → lenv → relation term ≝ λh,g,L,T,U.
+ ∃l. ⦃h, L⦄ ⊢ T •[g, l+1] U.
+
(* Basic inversion lemmas ************************************************)
fact ssta_inv_sort1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀k0. T = ⋆k0 →
(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************)
-inductive sstas (h:sh) (g:sd h) (L:lenv): relation term ≝
-| sstas_refl: ∀T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → sstas h g L T T
-| sstas_step: ∀T,U1,U2,l. ⦃h, L⦄ ⊢ T •[g, l+1] U1 → sstas h g L U1 U2 →
- sstas h g L T U2.
+(* Note: includes: stass_refl *)
+definition sstas: ∀h. sd h → lenv → relation term ≝
+ λh,g,L. star … (ssta_step h g L).
interpretation "iterated stratified static type assignment (term)"
'StaticTypeStar h g L T U = (sstas h g L T U).
(* Basic eliminators ********************************************************)
-fact sstas_ind_alt_aux: ∀h,g,L,U2. ∀R:predicate term.
- (∀T,l. ⦃h, L⦄ ⊢ U2 •[g , l] T → R U2) →
- (∀T,U1,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U1 →
- ⦃h, L⦄ ⊢ U1 •* [g] U2 → R U1 → R T
- ) →
- ∀T,U. ⦃h, L⦄ ⊢ T •*[g] U → U = U2 → R T.
-#h #g #L #U2 #R #H1 #H2 #T #U #H elim H -H -T -U /2 width=3/ /3 width=5/
+lemma sstas_ind: ∀h,g,L,T. ∀R:predicate term.
+ R T → (
+ ∀U1,U2,l. ⦃h, L⦄ ⊢ T •* [g] U1 → ⦃h, L⦄ ⊢ U1 •[g, l + 1] U2 →
+ R U1 → R U2
+ ) →
+ ∀U. ⦃h, L⦄ ⊢ T •*[g] U → R U.
+#h #g #L #T #R #IH1 #IH2 #U #H elim H -U //
+#U1 #U2 #H * /2 width=5/
qed-.
-lemma sstas_ind_alt: ∀h,g,L,U2. ∀R:predicate term.
- (∀T,l. ⦃h, L⦄ ⊢ U2 •[g , l] T → R U2) →
- (∀T,U1,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U1 →
- ⦃h, L⦄ ⊢ U1 •* [g] U2 → R U1 → R T
- ) →
- ∀T. ⦃h, L⦄ ⊢ T •*[g] U2 → R T.
-/3 width=9 by sstas_ind_alt_aux/ qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact sstas_inv_bind1_aux: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U →
- ∀a,J,X,Y. T = ⓑ{a,J}Y.X →
- ∃∃Z. ⦃h, L.ⓑ{J}Y⦄ ⊢ X •*[g] Z & U = ⓑ{a,J}Y.Z.
-#h #g #L #T #U #H @(sstas_ind_alt … H) -T
-[ #U0 #l #HU0 #a #J #X #Y #H destruct
- elim (ssta_inv_bind1 … HU0) -HU0 #X0 #HX0 #H destruct /3 width=3/
-| #T0 #U0 #l #HTU0 #_ #IHU0 #a #J #X #Y #H destruct
- elim (ssta_inv_bind1 … HTU0) -HTU0 #X0 #HX0 #H destruct
- elim (IHU0 a J X0 Y …) -IHU0 // #X1 #HX01 #H destruct /3 width=4/
-]
+lemma sstas_ind_dx: ∀h,g,L,U2. ∀R:predicate term.
+ R U2 → (
+ ∀T,U1,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U1 → ⦃h, L⦄ ⊢ U1 •* [g] U2 →
+ R U1 → R T
+ ) →
+ ∀T. ⦃h, L⦄ ⊢ T •*[g] U2 → R T.
+#h #g #L #U2 #R #IH1 #IH2 #T #H @(star_ind_l … T H) -T //
+#T #T0 * /2 width=5/
qed-.
-lemma sstas_inv_bind1: ∀h,g,a,J,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{a,J}Y.X •*[g] U →
- ∃∃Z. ⦃h, L.ⓑ{J}Y⦄ ⊢ X •*[g] Z & U = ⓑ{a,J}Y.Z.
-/2 width=3 by sstas_inv_bind1_aux/ qed-.
+(* Basic properties *********************************************************)
+
+lemma ssta_sstas: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l+1] U → ⦃h, L⦄ ⊢ T •*[g] U.
+/3 width=2/ qed.
+
+lemma sstas_strap1: ∀h,g,L,T1,T2,U2,l. ⦃h, L⦄ ⊢ T1 •*[g] T2 → ⦃h, L⦄ ⊢ T2 •[g,l+1] U2 →
+ ⦃h, L⦄ ⊢ T1 •*[g] U2.
+/3 width=4 by sstep, ex_intro/ (**) (* auto fails without trace *)
+qed.
+
+lemma sstas_strap2: ∀h,g,L,T1,U1,U2,l. ⦃h, L⦄ ⊢ T1 •[g, l+1] U1 → ⦃h, L⦄ ⊢ U1 •*[g] U2 →
+ ⦃h, L⦄ ⊢ T1 •*[g] U2.
+/3 width=3 by star_compl, ex_intro/ (**) (* auto fails without trace *)
+qed.
-fact sstas_inv_appl1_aux: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → ∀X,Y. T = ⓐY.X →
- ∃∃Z. ⦃h, L⦄ ⊢ X •*[g] Z & U = ⓐY.Z.
-#h #g #L #T #U #H @(sstas_ind_alt … H) -T
-[ #U0 #l #HU0 #X #Y #H destruct
- elim (ssta_inv_appl1 … HU0) -HU0 #X0 #HX0 #H destruct /3 width=3/
-| #T0 #U0 #l #HTU0 #_ #IHU0 #X #Y #H destruct
- elim (ssta_inv_appl1 … HTU0) -HTU0 #X0 #HX0 #H destruct
- elim (IHU0 X0 Y ?) -IHU0 // #X1 #HX01 #H destruct /3 width=4/
-]
+(* Basic inversion lemmas ***************************************************)
+
+lemma sstas_inv_bind1: ∀h,g,a,I,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{a,I}Y.X •*[g] U →
+ ∃∃Z. ⦃h, L.ⓑ{I}Y⦄ ⊢ X •*[g] Z & U = ⓑ{a,I}Y.Z.
+#h #g #a #I #L #Y #X #U #H @(sstas_ind … H) -U /2 width=3/
+#T #U #l #_ #HTU * #Z #HXZ #H destruct
+elim (ssta_inv_bind1 … HTU) -HTU #Z0 #HZ0 #H destruct /3 width=4/
qed-.
lemma sstas_inv_appl1: ∀h,g,L,Y,X,U. ⦃h, L⦄ ⊢ ⓐY.X •*[g] U →
∃∃Z. ⦃h, L⦄ ⊢ X •*[g] Z & U = ⓐY.Z.
-/2 width=3 by sstas_inv_appl1_aux/ qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma sstas_fwd_correct: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U →
- ∃∃l,W. ⦃h, L⦄ ⊢ U •[g, l] W.
-#h #g #L #T #U #H @(sstas_ind_alt … H) -T // /2 width=3/
+#h #g #L #Y #X #U #H @(sstas_ind … H) -U /2 width=3/
+#T #U #l #_ #HTU * #Z #HXZ #H destruct
+elim (ssta_inv_appl1 … HTU) -HTU #Z0 #HZ0 #H destruct /3 width=4/
qed-.
lemma sstas_aaa: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U →
∀A. L ⊢ T ⁝ A → L ⊢ U ⁝ A.
-#h #g #L #T #U #H @(sstas_ind_alt … H) -T // /3 width=6/
+#h #g #L #T #U #H @(sstas_ind_dx … H) -T // /3 width=6/
qed.
(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************)
-(* Advanced properties ******************************************************)
-
-lemma ssta_sstas: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l+1] U → ⦃h, L⦄ ⊢ T •*[g] U.
-#h #g #L #T #U #l #HTU
-elim (ssta_fwd_correct … HTU) /3 width=4/
-qed.
-
(* Properties on relocation *************************************************)
lemma sstas_lift: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 →
∀L2,d,e. ⇩[d, e] L2 ≡ L1 → ∀T2. ⇧[d, e] T1 ≡ T2 →
∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 •*[g] U2.
-#h #g #L1 #T1 #U1 #H @(sstas_ind_alt … H) -T1
-[ #T1 #l #HUT1 #L2 #d #e #HL21 #X #HX #U2 #HU12
- >(lift_mono … HX … HU12) -X
- elim (lift_total T1 d e) /3 width=11/
+#h #g #L1 #T1 #U1 #H @(sstas_ind_dx … H) -T1
+[ #L2 #d #e #HL21 #X #HX #U2 #HU12
+ >(lift_mono … HX … HU12) -X //
| #T0 #U0 #l0 #HTU0 #_ #IHU01 #L2 #d #e #HL21 #T2 #HT02 #U2 #HU12
elim (lift_total U0 d e) /3 width=10/
]
lemma sstas_inv_lift1: ∀h,g,L2,T2,U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 →
∀L1,d,e. ⇩[d, e] L2 ≡ L1 → ∀T1. ⇧[d, e] T1 ≡ T2 →
∃∃U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 & ⇧[d, e] U1 ≡ U2.
-#h #g #L2 #T2 #U2 #H @(sstas_ind_alt … H) -T2
-[ #T2 #l #HUT2 #L1 #d #e #HL21 #U1 #HU12
- elim (ssta_inv_lift1 … HUT2 … HL21 … HU12) -HUT2 -HL21 /3 width=3/
-| #T0 #U0 #l0 #HTU0 #_ #IHU01 #L1 #d #e #HL21 #U1 #HU12
- elim (ssta_inv_lift1 … HTU0 … HL21 … HU12) -HTU0 -HU12 #U #HU1 #HU0
- elim (IHU01 … HL21 … HU0) -IHU01 -HL21 -U0 /3 width=4/
-]
+#h #g #L2 #T2 #U2 #H @(sstas_ind_dx … H) -T2 /2 width=3/
+#T0 #U0 #l0 #HTU0 #_ #IHU01 #L1 #d #e #HL21 #U1 #HU12
+elim (ssta_inv_lift1 … HTU0 … HL21 … HU12) -HTU0 -HU12 #U #HU1 #HU0
+elim (IHU01 … HL21 … HU0) -IHU01 -HL21 -U0 /3 width=4/
qed-.
lemma lsubss_sstas_trans: ∀h,g,L2,T,U. ⦃h, L2⦄ ⊢ T •*[g] U →
∀L1. h ⊢ L1 •⊑[g] L2 → ⦃h, L1⦄ ⊢ T •*[g] U.
-#h #g #L2 #T #U #H @(sstas_ind_alt … H) -T /3 width=4/ /3 width=5/
+#h #g #L2 #T #U #H @(sstas_ind_dx … H) -T // /3 width=5/
qed.
lemma lsubss_sstas_conf: ∀h,g,L1,T,U. ⦃h, L1⦄ ⊢ T •*[g] U →
∀L2. h ⊢ L1 •⊑[g] L2 → ⦃h, L2⦄ ⊢ T •*[g] U.
-#h #g #L2 #T #U #H @(sstas_ind_alt … H) -T /3 width=4/ /3 width=5/
+#h #g #L2 #T #U #H @(sstas_ind_dx … H) -T // /3 width=5/
qed.
∀T2. L2 ⊢ T1 ▶* [d, e] T2 →
∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 &
L2 ⊢ U1 ▶* [d, e] U2.
-#h #g #L1 #T1 #U1 #H @(sstas_ind_alt … H) -T1
-[ #T1 #l #HUT1 #L2 #d #e #HL12 #U2 #HU12
- elim (ssta_ltpss_dx_tpss_conf … HUT1 … HL12 … HU12) -HUT1 -HL12 /3 width=3/
-| #T0 #U0 #l0 #HTU0 #_ #IHU01 #L2 #d #e #HL12 #T #HT0
- elim (ssta_ltpss_dx_tpss_conf … HTU0 … HL12 … HT0) -HTU0 -HT0 #U #HTU #HU0
- elim (IHU01 … HL12 … HU0) -IHU01 -HL12 -U0 /3 width=4/
-]
+#h #g #L1 #T1 #U1 #H @(sstas_ind_dx … H) -T1 /2 width=3/
+#T0 #U0 #l0 #HTU0 #_ #IHU01 #L2 #d #e #HL12 #T #HT0
+elim (ssta_ltpss_dx_tpss_conf … HTU0 … HL12 … HT0) -HTU0 -HT0 #U #HTU #HU0
+elim (IHU01 … HL12 … HU0) -IHU01 -HL12 -U0 /3 width=4/
qed.
lemma sstas_ltpss_dx_tps_conf: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 →
∀L2,d,e. L1 ▶* [d, e] L2 →
∀T2. L2 ⊢ T1 ▶ [d, e] T2 →
∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 & L2 ⊢ U1 ▶* [d, e] U2.
-/3 width=5/ qed.
+/3 width=7 by step, sstas_ltpss_dx_tpss_conf/ qed. (**) (* auto fails without trace *)
lemma sstas_ltpss_dx_conf: ∀h,g,L1,T,U1. ⦃h, L1⦄ ⊢ T •*[g] U1 →
∀L2,d,e. L1 ▶* [d, e] L2 →
lemma sstas_inv_O: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U →
∀T0. ⦃h, L⦄ ⊢ T •[g , 0] T0 → U = T.
-#h #g #L #T #U #H @(sstas_ind_alt … H) -T //
+#h #g #L #T #U #H @(sstas_ind_dx … H) -T //
#T0 #U0 #l0 #HTU0 #_ #_ #T1 #HT01
elim (ssta_mono … HTU0 … HT01) <plus_n_Sm #H destruct
qed-.
lemma sstas_strip: ∀h,g,L,T,U1. ⦃h, L⦄ ⊢ T •*[g] U1 →
∀U2,l. ⦃h, L⦄ ⊢ T •[g, l] U2 →
⦃h, L⦄ ⊢ U1 •[g, l] U2 ∨ ⦃h, L⦄ ⊢ U2 •*[g] U1.
-#h #g #L #T #U1 #H1 @(sstas_ind_alt … H1) -T /2 width=1/
+#h #g #L #T #U1 #H1 @(sstas_ind_dx … H1) -T /2 width=1/
#T #U #l0 #HTU #HU1 #_ #U2 #l #H2
elim (ssta_mono … H2 … HTU) -H2 -HTU #H1 #H2 destruct /2 width=1/
qed-.
theorem sstas_trans: ∀h,g,L,T1,U. ⦃h, L⦄ ⊢ T1 •*[g] U →
∀T2. ⦃h, L⦄ ⊢ U •*[g] T2 → ⦃h, L⦄ ⊢ T1 •*[g] T2.
-#h #g #L #T1 #U #H1 @(sstas_ind_alt … H1) -T1 // /3 width=4/
-qed-.
+/2 width=3/ qed-.
theorem sstas_conf: ∀h,g,L,T,U1. ⦃h, L⦄ ⊢ T •*[g] U1 →
∀U2. ⦃h, L⦄ ⊢ T •*[g] U2 →
⦃h, L⦄ ⊢ U1 •*[g] U2 ∨ ⦃h, L⦄ ⊢ U2 •*[g] U1.
-#h #g #L #T #U1 #H1 @(sstas_ind_alt … H1) -T /2 width=1/
+#h #g #L #T #U1 #H1 @(sstas_ind_dx … H1) -T /2 width=1/
#T #U #l #HTU #HU1 #IHU1 #U2 #H2
elim (sstas_strip … H2 … HTU) -T /2 width=1/ -IHU1 /3 width=4/
qed-.
projects / helm.git / commitdiff