pr3/props pr3_eta
pr3/subst1 pr3_gen_cabbr
sn3/props sns3_lifts
-sty0/fwd sty0_gen_sort
-sty0/fwd sty0_gen_lref
-sty0/fwd sty0_gen_bind
-sty0/fwd sty0_gen_appl
-sty0/fwd sty0_gen_cast
-sty0/props sty0_lift
-sty0/props sty0_correct
sty1/cnt sty1_cnt
sty1/props sty1_trans
sty1/props sty1_bind
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/static/sh.ma".
+include "basic_2/equivalence/cpcs.ma".
+
+(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
+
+inductive nta (h:sh): lenv → relation term ≝
+| nta_sort: ∀L,k. nta h L (⋆k) (⋆(next h k))
+| nta_ldef: ∀L,K,V,W,U,i. ⇩[0, i] L ≡ K. ⓓV → nta h K V W →
+ ⇧[0, i + 1] W ≡ U → nta h L (#i) U
+| nta_ldec: ∀L,K,W,V,U,i. ⇩[0, i] L ≡ K. ⓛW → nta h K W V →
+ ⇧[0, i + 1] W ≡ U → nta h L (#i) U
+| nta_bind: ∀I,L,V,W,T,U. nta h L V W → nta h (L. ⓑ{I} V) T U →
+ nta h L (ⓑ{I}V.T) (ⓑ{I}V.U)
+| nta_appl: ∀L,V,W,U,T1,T2. nta h L V W → nta h L W U → nta h (L.ⓛW) T1 T2 →
+ nta h L (ⓐV.ⓛW.T1) (ⓐV.ⓛW.T2)
+| nta_pure: ∀L,V,W,T,U. nta h L T U → nta h L (ⓐV.U) W →
+ nta h L (ⓐV.T) (ⓐV.U)
+| nta_cast: ∀L,T,U. nta h L T U → nta h L (ⓣU. T) U
+| nta_conv: ∀L,T,U1,U2,V2. nta h L T U1 → L ⊢ U1 ⬌* U2 → nta h L U2 V2 →
+ nta h L T U2
+.
+
+interpretation "native type assignment (term)"
+ 'NativeType h L T U = (nta h L T U).
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was: ty3_cast *)
+lemma nta_cast_old: ∀h,L,W,T,U.
+ ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ U : W → ⦃h, L⦄ ⊢ ⓣU.T : ⓣW.U.
+/4 width=3/ qed.
+
+(* Basic_1: was: ty3_typecheck *)
+lemma nta_typecheck: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃T0. ⦃h, L⦄ ⊢ ⓣU.T : T0.
+/3 width=2/ qed.
+
+(* Basic_1: removed theorems 1: ty3_getl_subst0 *)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/equivalence/cpcs_cpcs.ma".
+include "basic_2/dynamic/nta.ma".
+
+(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
+
+(* Advanced inversion lemmas ************************************************)
+
+fact nta_inv_sort1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀k0. T = ⋆k0 →
+ L ⊢ ⋆(next h k0) ⬌* U.
+#h #L #T #U #H elim H -L -T -U
+[ #L #k #k0 #H destruct //
+| #L #K #V #W #U #i #_ #_ #_ #_ #k0 #H destruct
+| #L #K #W #V #U #i #_ #_ #_ #_ #k0 #H destruct
+| #I #L #V #W #T #U #_ #_ #_ #_ #k0 #H destruct
+| #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #k0 #H destruct
+| #L #V #W #T #U #_ #_ #_ #_ #k0 #H destruct
+| #L #T #U #_ #_ #k0 #H destruct
+| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #k0 #H destruct
+ lapply (IHTU1 ??) -IHTU1 [ // | skip ] #Hk0
+ lapply (cpcs_trans … Hk0 … HU12) -U1 //
+]
+qed.
+
+(* Basic_1: was: ty3_gen_sort *)
+lemma nta_inv_sort1: ∀h,L,U,k. ⦃h, L⦄ ⊢ ⋆k : U → L ⊢ ⋆(next h k) ⬌* U.
+/2 width=3/ qed-.
+
+fact nta_inv_lref1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀j. T = #j →
+ (∃∃K,V,W,U0. ⇩[0, j] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W &
+ ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U
+ ) ∨
+ (∃∃K,W,V,U0. ⇩[0, j] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V &
+ ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U
+ ).
+#h #L #T #U #H elim H -L -T -U
+[ #L #k #j #H destruct
+| #L #K #V #W #U #i #HLK #HVW #HWU #_ #j #H destruct /3 width=8/
+| #L #K #W #V #U #i #HLK #HWV #HWU #_ #j #H destruct /3 width=8/
+| #I #L #V #W #T #U #_ #_ #_ #_ #j #H destruct
+| #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #j #H destruct
+| #L #V #W #T #U #_ #_ #_ #_ #j #H destruct
+| #L #T #U #_ #_ #j #H destruct
+| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #j #H destruct
+ elim (IHTU1 ??) -IHTU1 [4: // |2: skip ] * #K #V #W #U0 #HLK #HVW #HWU0 #HU01
+ lapply (cpcs_trans … HU01 … HU12) -U1 /3 width=8/
+]
+qed.
+
+(* Basic_1: was ty3_gen_lref *)
+lemma nta_inv_lref1: ∀h,L,U,i. ⦃h, L⦄ ⊢ #i : U →
+ (∃∃K,V,W,U0. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W &
+ ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U
+ ) ∨
+ (∃∃K,W,V,U0. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V &
+ ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U
+ ).
+/2 width=3/ qed-.
+
+fact nta_inv_bind1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀J,X,Y. T = ⓑ{J}Y.X →
+ ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y : Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X : Z2 &
+ L ⊢ ⓑ{J}Y.Z2 ⬌* U.
+#h #L #T #U #H elim H -L -T -U
+[ #L #k #J #X #Y #H destruct
+| #L #K #V #W #U #i #_ #_ #_ #_ #J #X #Y #H destruct
+| #L #K #W #V #U #i #_ #_ #_ #_ #J #X #Y #H destruct
+| #I #L #V #W #T #U #HVW #HTU #_ #_ #J #X #Y #H destruct /2 width=3/
+| #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #J #X #Y #H destruct
+| #L #V #W #T #U #_ #_ #_ #_ #J #X #Y #H destruct
+| #L #T #U #_ #_ #J #X #Y #H destruct
+| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #J #X #Y #H destruct
+ elim (IHTU1 ????) -IHTU1 [5: // |2,3,4: skip ] #Z1 #Z2 #HZ1 #HZ2 #HU1
+ lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=3/
+]
+qed.
+
+(* Basic_1: was: ty3_gen_bind *)
+lemma nta_inv_bind1: ∀h,J,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{J}Y.X : U →
+ ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y : Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X : Z2 &
+ L ⊢ ⓑ{J}Y.Z2 ⬌* U.
+/2 width=3/ qed-.
+
+fact nta_inv_cast1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓣY.X →
+ ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
+#h #L #T #U #H elim H -L -T -U
+[ #L #k #X #Y #H destruct
+| #L #K #V #W #U #i #_ #_ #_ #_ #X #Y #H destruct
+| #L #K #W #V #U #i #_ #_ #_ #_ #X #Y #H destruct
+| #I #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct
+| #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #X #Y #H destruct
+| #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct
+| #L #T #U #HTU #_ #X #Y #H destruct /2 width=1/
+| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #X #Y #H destruct
+ elim (IHTU1 ???) -IHTU1 [4: // |2,3: skip ] #HXY #HU1
+ lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=1/
+]
+qed.
+
+(* Basic_1: was: ty3_gen_cast *)
+lemma nta_inv_cast1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓣY.X : U → ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
+/2 width=3/ qed-.
+
+(* Properties on relocation *************************************************)
+
+(* Basic_1: was: ty3_lift *)
+lemma nta_lift: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 →
+ ∀T2. ⇧[d, e] T1 ≡ T2 → ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 : U2.
+#h #L1 #T1 #U1 #H elim H -L1 -T1 -U1
+[ #L1 #k #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+ >(lift_inv_sort1 … H1) -X1
+ >(lift_inv_sort1 … H2) -X2 //
+| #L1 #K1 #V1 #W1 #W #i #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2
+ elim (lift_inv_lref1 … H) * #Hid #H destruct
+ [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // #W2 #HW12 #HWU2
+ elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
+ elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct
+ /3 width=8/
+ | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
+ lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
+ ]
+| #L1 #K1 #W1 #V1 #W #i #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2
+ elim (lift_inv_lref1 … H) * #Hid #H destruct
+ [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // <minus_plus #W #HW1 #HWU2
+ elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
+ elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #W2 #HK21 #HW12 #H destruct
+ lapply (lift_mono … HW1 … HW12) -HW1 #H destruct
+ elim (lift_total V1 (d-i-1) e) /3 width=8/
+ | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
+ lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
+ ]
+| #I #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+ elim (lift_inv_bind1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
+ elim (lift_inv_bind1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
+ lapply (lift_mono … H1 … HV12) -H1 #H destruct
+ elim (lift_total W1 d e) /4 width=6/
+| #L1 #V1 #W1 #U1 #T11 #T12 #_ #_ #_ #IHVW1 #IHWU1 #IHT112 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+ elim (lift_inv_flat1 … H1) -H1 #V2 #X #HV12 #H1 #H destruct
+ elim (lift_inv_bind1 … H1) -H1 #W2 #T12 #HW12 #HT112 #H destruct
+ elim (lift_inv_flat1 … H2) -H2 #X0 #X #H0 #H2 #H destruct
+ elim (lift_inv_bind1 … H2) -H2 #Y0 #T22 #H2 #HT122 #H destruct
+ lapply (lift_mono … H0 … HV12) -H0 #H destruct
+ lapply (lift_mono … H2 … HW12) -H2 #H destruct
+ elim (lift_total U1 d e) #U2 #HU12
+ @nta_appl [2,3: /2 width=5/ | skip | /3 width=5/ ] (**) (* explicit constructor, /4 width=6/ is too slow *)
+| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+ elim (lift_inv_flat1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
+ elim (lift_inv_flat1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
+ lapply (lift_mono … H1 … HV12) -H1 #H destruct
+ elim (lift_total W1 d e) /4 width=6/
+| #L1 #T1 #U1 #_ #IHTU1 #L2 #d #e #HL21 #X #H #U2 #HU12
+ elim (lift_inv_flat1 … H) -H #X2 #T2 #HUX2 #HT12 #H destruct
+ lapply (lift_mono … HUX2 … HU12) -HUX2 #H destruct /3 width=5/
+| #L1 #T1 #U11 #U12 #V12 #_ #HU112 #_ #IHTU11 #IHUV12 #L2 #d #e #HL21 #U1 #HTU1 #U2 #HU12
+ elim (lift_total U11 d e) #U #HU11
+ elim (lift_total V12 d e) #V22 #HV122
+ lapply (cpcs_lift … HL21 … HU11 … HU12 HU112) -HU112 /3 width=6/
+]
+qed.
+
+(* Advanced forvard lemmas **************************************************)
+
+(* Basic_1: was: ty3_correct *)
+lemma nta_fwd_correct: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃T0. ⦃h, L⦄ ⊢ U : T0.
+#h #L #T #U #H elim H -L -T -U
+[ /2 width=2/
+| #L #K #V #W #W0 #i #HLK #_ #HW0 * #V0 #HWV0
+ lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+ elim (lift_total V0 0 (i+1)) /3 width=10/
+| #L #K #W #V #V0 #i #HLK #HWV #HWV0 #_
+ lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+ elim (lift_total V 0 (i+1)) /3 width=10/
+| #I #L #V #W #T #U #HVW #_ #_ * /3 width=2/
+| #L #V #W #U #T1 #T2 #HVW #HWU #_ #_ #_ * /3 width=2/
+| #L #V #W #T #U #_ #HUW * #T0 #HUT0 /3 width=2/
+| #L #T #U #_ * /2 width=2/
+| /2 width=2/
+]
+qed-.
+
+(* Advanced properties ******************************************************)
+
+(* Basic_1: was: ty3_appl *)
+lemma nta_appl_old: ∀h,L,V,W,T,U. ⦃h, L⦄ ⊢ V : W → ⦃h, L⦄ ⊢ T : ⓛW.U →
+ ⦃h, L⦄ ⊢ ⓐV.T : ⓐV.ⓛW.U.
+#h #L #V #W #T #U #HVW #HTU
+elim (nta_fwd_correct … HTU) #X #H
+elim (nta_inv_bind1 … H) -H #V0 #T0 #HWV0 #HUT0 #_ -X /3 width=2/
+qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/static/sh.ma".
-include "basic_2/equivalence/cpcs.ma".
-
-(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
-
-inductive nta (h:sh): lenv → relation term ≝
-| nta_sort: ∀L,k. nta h L (⋆k) (⋆(next h k))
-| nta_ldef: ∀L,K,V,W,U,i. ⇩[0, i] L ≡ K. ⓓV → nta h K V W →
- ⇧[0, i + 1] W ≡ U → nta h L (#i) U
-| nta_ldec: ∀L,K,W,V,U,i. ⇩[0, i] L ≡ K. ⓛW → nta h K W V →
- ⇧[0, i + 1] W ≡ U → nta h L (#i) U
-| nta_bind: ∀I,L,V,W,T,U. nta h L V W → nta h (L. ⓑ{I} V) T U →
- nta h L (ⓑ{I}V.T) (ⓑ{I}V.U)
-| nta_appl: ∀L,V,W,U,T1,T2. nta h L V W → nta h L W U → nta h (L.ⓛW) T1 T2 →
- nta h L (ⓐV.ⓛW.T1) (ⓐV.ⓛW.T2)
-| nta_pure: ∀L,V,W,T,U. nta h L T U → nta h L (ⓐV.U) W →
- nta h L (ⓐV.T) (ⓐV.U)
-| nta_cast: ∀L,T,U. nta h L T U → nta h L (ⓣU. T) U
-| nta_conv: ∀L,T,U1,U2,V2. nta h L T U1 → L ⊢ U1 ⬌* U2 → nta h L U2 V2 →
- nta h L T U2
-.
-
-interpretation "native type assignment (term)"
- 'NativeType h L T U = (nta h L T U).
-
-(* Basic properties *********************************************************)
-
-(* Basic_1: was: ty3_cast *)
-lemma nta_cast_old: ∀h,L,W,T,U.
- ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ U : W → ⦃h, L⦄ ⊢ ⓣU.T : ⓣW.U.
-/4 width=3/ qed.
-
-(* Basic_1: was: ty3_typecheck *)
-lemma nta_typecheck: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃T0. ⦃h, L⦄ ⊢ ⓣU.T : T0.
-/3 width=2/ qed.
-
-(* Basic_1: removed theorems 1: ty3_getl_subst0 *)
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/equivalence/cpcs_cpcs.ma".
-include "basic_2/native/nta.ma".
-
-(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
-
-(* Advanced inversion lemmas ************************************************)
-
-fact nta_inv_sort_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀k0. T = ⋆k0 →
- L ⊢ ⋆(next h k0) ⬌* U.
-#h #L #T #U #H elim H -L -T -U
-[ #L #k #k0 #H destruct //
-| #L #K #V #W #U #i #_ #_ #_ #_ #k0 #H destruct
-| #L #K #W #V #U #i #_ #_ #_ #_ #k0 #H destruct
-| #I #L #V #W #T #U #_ #_ #_ #_ #k0 #H destruct
-| #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #k0 #H destruct
-| #L #V #W #T #U #_ #_ #_ #_ #k0 #H destruct
-| #L #T #U #_ #_ #k0 #H destruct
-| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #k0 #H destruct
- lapply (IHTU1 ??) -IHTU1 [ // | skip ] #Hk0
- lapply (cpcs_trans … Hk0 … HU12) -U1 //
-]
-qed.
-
-(* Basic_1: was: ty3_gen_sort *)
-lemma nta_inv_sort: ∀h,L,U,k. ⦃h, L⦄ ⊢ ⋆k : U → L ⊢ ⋆(next h k) ⬌* U.
-/2 width=3/ qed-.
-
-fact nta_inv_lref_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀j. T = #j →
- (∃∃K,V,W,U0. ⇩[0, j] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W &
- ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U
- ) ∨
- (∃∃K,W,V,U0. ⇩[0, j] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V &
- ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U
- ).
-#h #L #T #U #H elim H -L -T -U
-[ #L #k #j #H destruct
-| #L #K #V #W #U #i #HLK #HVW #HWU #_ #j #H destruct /3 width=8/
-| #L #K #W #V #U #i #HLK #HWV #HWU #_ #j #H destruct /3 width=8/
-| #I #L #V #W #T #U #_ #_ #_ #_ #j #H destruct
-| #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #j #H destruct
-| #L #V #W #T #U #_ #_ #_ #_ #j #H destruct
-| #L #T #U #_ #_ #j #H destruct
-| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #j #H destruct
- elim (IHTU1 ??) -IHTU1 [4: // |2: skip ] * #K #V #W #U0 #HLK #HVW #HWU0 #HU01
- lapply (cpcs_trans … HU01 … HU12) -U1 /3 width=8/
-]
-qed.
-
-(* Basic_1: was ty3_gen_lref *)
-lemma nta_inv_lref: ∀h,L,U,i. ⦃h, L⦄ ⊢ #i : U →
- (∃∃K,V,W,U0. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W &
- ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U
- ) ∨
- (∃∃K,W,V,U0. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V &
- ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U
- ).
-/2 width=3/ qed-.
-
-fact nta_inv_bind_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀J,X,Y. T = ⓑ{J}Y.X →
- ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y : Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X : Z2 &
- L ⊢ ⓑ{J}Y.Z2 ⬌* U.
-#h #L #T #U #H elim H -L -T -U
-[ #L #k #J #X #Y #H destruct
-| #L #K #V #W #U #i #_ #_ #_ #_ #J #X #Y #H destruct
-| #L #K #W #V #U #i #_ #_ #_ #_ #J #X #Y #H destruct
-| #I #L #V #W #T #U #HVW #HTU #_ #_ #J #X #Y #H destruct /2 width=3/
-| #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #J #X #Y #H destruct
-| #L #V #W #T #U #_ #_ #_ #_ #J #X #Y #H destruct
-| #L #T #U #_ #_ #J #X #Y #H destruct
-| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #J #X #Y #H destruct
- elim (IHTU1 ????) -IHTU1 [5: // |2,3,4: skip ] #Z1 #Z2 #HZ1 #HZ2 #HU1
- lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=3/
-]
-qed.
-
-(* Basic_1: was: ty3_gen_bind *)
-lemma nta_inv_bind: ∀h,J,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{J}Y.X : U →
- ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y : Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X : Z2 &
- L ⊢ ⓑ{J}Y.Z2 ⬌* U.
-/2 width=3/ qed-.
-
-fact nta_inv_cast_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓣY.X →
- ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
-#h #L #T #U #H elim H -L -T -U
-[ #L #k #X #Y #H destruct
-| #L #K #V #W #U #i #_ #_ #_ #_ #X #Y #H destruct
-| #L #K #W #V #U #i #_ #_ #_ #_ #X #Y #H destruct
-| #I #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct
-| #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #X #Y #H destruct
-| #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct
-| #L #T #U #HTU #_ #X #Y #H destruct /2 width=1/
-| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #X #Y #H destruct
- elim (IHTU1 ???) -IHTU1 [4: // |2,3: skip ] #HXY #HU1
- lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=1/
-]
-qed.
-
-(* Basic_1: was: ty3_gen_cast *)
-lemma nta_inv_cast: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓣY.X : U → ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
-/2 width=3/ qed-.
-
-(* Properties on relocation *************************************************)
-
-(* Basic_1: was: ty3_lift *)
-lemma nta_lift: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 →
- ∀T2. ⇧[d, e] T1 ≡ T2 → ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 : U2.
-#h #L1 #T1 #U1 #H elim H -L1 -T1 -U1
-[ #L1 #k #L2 #d #e #HL21 #X1 #H1 #X2 #H2
- >(lift_inv_sort1 … H1) -X1
- >(lift_inv_sort1 … H2) -X2 //
-| #L1 #K1 #V1 #W1 #W #i #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2
- elim (lift_inv_lref1 … H) * #Hid #H destruct
- [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // #W2 #HW12 #HWU2
- elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
- elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct
- /3 width=8/
- | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
- lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
- ]
-| #L1 #K1 #W1 #V1 #W #i #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2
- elim (lift_inv_lref1 … H) * #Hid #H destruct
- [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // <minus_plus #W #HW1 #HWU2
- elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
- elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #W2 #HK21 #HW12 #H destruct
- lapply (lift_mono … HW1 … HW12) -HW1 #H destruct
- elim (lift_total V1 (d-i-1) e) /3 width=8/
- | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
- lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
- ]
-| #I #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
- elim (lift_inv_bind1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
- elim (lift_inv_bind1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
- lapply (lift_mono … H1 … HV12) -H1 #H destruct
- elim (lift_total W1 d e) /4 width=6/
-| #L1 #V1 #W1 #U1 #T11 #T12 #_ #_ #_ #IHVW1 #IHWU1 #IHT112 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
- elim (lift_inv_flat1 … H1) -H1 #V2 #X #HV12 #H1 #H destruct
- elim (lift_inv_bind1 … H1) -H1 #W2 #T12 #HW12 #HT112 #H destruct
- elim (lift_inv_flat1 … H2) -H2 #X0 #X #H0 #H2 #H destruct
- elim (lift_inv_bind1 … H2) -H2 #Y0 #T22 #H2 #HT122 #H destruct
- lapply (lift_mono … H0 … HV12) -H0 #H destruct
- lapply (lift_mono … H2 … HW12) -H2 #H destruct
- elim (lift_total U1 d e) #U2 #HU12
- @nta_appl [2,3: /2 width=5/ | skip | /3 width=5/ ] (**) (* explicit constructor, /4 width=6/ is too slow *)
-| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
- elim (lift_inv_flat1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
- elim (lift_inv_flat1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
- lapply (lift_mono … H1 … HV12) -H1 #H destruct
- elim (lift_total W1 d e) /4 width=6/
-| #L1 #T1 #U1 #_ #IHTU1 #L2 #d #e #HL21 #X #H #U2 #HU12
- elim (lift_inv_flat1 … H) -H #X2 #T2 #HUX2 #HT12 #H destruct
- lapply (lift_mono … HUX2 … HU12) -HUX2 #H destruct /3 width=5/
-| #L1 #T1 #U11 #U12 #V12 #_ #HU112 #_ #IHTU11 #IHUV12 #L2 #d #e #HL21 #U1 #HTU1 #U2 #HU12
- elim (lift_total U11 d e) #U #HU11
- elim (lift_total V12 d e) #V22 #HV122
- lapply (cpcs_lift … HL21 … HU11 … HU12 HU112) -HU112 /3 width=6/
-]
-qed.
-
-(* Advanced forvard lemmas **************************************************)
-
-(* Basic_1: was: ty3_correct *)
-lemma nta_fwd_correct: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃T0. ⦃h, L⦄ ⊢ U : T0.
-#h #L #T #U #H elim H -L -T -U
-[ /2 width=2/
-| #L #K #V #W #W0 #i #HLK #_ #HW0 * #V0 #HWV0
- lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
- elim (lift_total V0 0 (i+1)) /3 width=10/
-| #L #K #W #V #V0 #i #HLK #HWV #HWV0 #_
- lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
- elim (lift_total V 0 (i+1)) /3 width=10/
-| #I #L #V #W #T #U #HVW #_ #_ * /3 width=2/
-| #L #V #W #U #T1 #T2 #HVW #HWU #_ #_ #_ * /3 width=2/
-| #L #V #W #T #U #_ #HUW * #T0 #HUT0 /3 width=2/
-| #L #T #U #_ * /2 width=2/
-| /2 width=2/
-]
-qed-.
-
-(* Advanced properties ******************************************************)
-
-(* Basic_1: was: ty3_appl *)
-lemma nta_appl_old: ∀h,L,V,W,T,U. ⦃h, L⦄ ⊢ V : W → ⦃h, L⦄ ⊢ T : ⓛW.U →
- ⦃h, L⦄ ⊢ ⓐV.T : ⓐV.ⓛW.U.
-#h #L #V #W #T #U #HVW #HTU
-elim (nta_fwd_correct … HTU) #X #H
-elim (nta_inv_bind … H) -H #V0 #T0 #HWV0 #HUT0 #_ -X /3 width=2/
-qed.
non associative with precedence 45
for @{ 'TSubst $L $T1 $d $e $T2 }.
-(* Static Typing ************************************************************)
+(* Static typing ************************************************************)
notation "hvbox( L ⊢ break term 90 T ÷ break A )"
non associative with precedence 45
non associative with precedence 45
for @{ 'CrSubEqA $T1 $T2 }.
+notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 90 T1 • break T2 )"
+ non associative with precedence 45
+ for @{ 'StaticType $h $L $T1 $T2 }.
+
+(* Unwind *******************************************************************)
+
+notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 90 T1 •* break T2 )"
+ non associative with precedence 45
+ for @{ 'StaticTypeStar $h $L $T1 $T2 }.
+
(* Reducibility *************************************************************)
notation "hvbox( 𝐑 [ T ] )"
non associative with precedence 45
for @{ 'CPConvStar $T1 $T2 }.
-(* Native typing ************************************************************)
+(* Dynamic typing ***********************************************************)
notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 90 T1 : break T2 )"
non associative with precedence 45
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/substitution/ldrop.ma".
+include "basic_2/static/sh.ma".
+
+(* STATIC TYPE ASSIGNMENT ON TERMS ******************************************)
+
+inductive sta (h:sh): lenv → relation term ≝
+| sta_sort: ∀L,k. sta h L (⋆k) (⋆(next h k))
+| sta_ldef: ∀L,K,V,W,U,i. ⇩[0, i] L ≡ K. ⓓV → sta h K V W →
+ ⇧[0, i + 1] W ≡ U → sta h L (#i) U
+| sta_ldec: ∀L,K,W,V,U,i. ⇩[0, i] L ≡ K. ⓛW → sta h K W V →
+ ⇧[0, i + 1] W ≡ U → sta h L (#i) U
+| sta_bind: ∀I,L,V,T,U. sta h (L. ⓑ{I} V) T U →
+ sta h L (ⓑ{I}V.T) (ⓑ{I}V.U)
+| sta_appl: ∀L,V,T,U. sta h L T U →
+ sta h L (ⓐV.T) (ⓐV.U)
+| sta_cast: ∀L,T,U. sta h L T U → sta h L (ⓣU. T) U
+.
+
+interpretation "static type assignment (term)"
+ 'StaticType h L T U = (sta h L T U).
+
+(* Basic inversion lemmas ************************************************)
+
+fact sta_inv_sort1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∀k0. T = ⋆k0 →
+ U = ⋆(next h k0).
+#h #L #T #U * -L -T -U
+[ #L #k #k0 #H destruct //
+| #L #K #V #W #U #i #_ #_ #_ #k0 #H destruct
+| #L #K #W #V #U #i #_ #_ #_ #k0 #H destruct
+| #I #L #V #T #U #_ #k0 #H destruct
+| #L #V #T #U #_ #k0 #H destruct
+| #L #T #U #_ #k0 #H destruct
+qed.
+
+(* Basic_1: was: sty0_gen_sort *)
+lemma sta_inv_sort1: ∀h,L,U,k. ⦃h, L⦄ ⊢ ⋆k • U → U = ⋆(next h k).
+/2 width=4/ qed-.
+
+fact sta_inv_lref1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∀j. T = #j →
+ (∃∃K,V,W. ⇩[0, j] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V • W &
+ ⇧[0, j + 1] W ≡ U
+ ) ∨
+ (∃∃K,W,V. ⇩[0, j] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W • V &
+ ⇧[0, j + 1] W ≡ U
+ ).
+#h #L #T #U * -L -T -U
+[ #L #k #j #H destruct
+| #L #K #V #W #U #i #HLK #HVW #HWU #j #H destruct /3 width=6/
+| #L #K #W #V #U #i #HLK #HWV #HWU #j #H destruct /3 width=6/
+| #I #L #V #T #U #_ #j #H destruct
+| #L #V #T #U #_ #j #H destruct
+| #L #T #U #_ #j #H destruct
+]
+qed.
+
+(* Basic_1: was sty0_gen_lref *)
+lemma sta_inv_lref1: ∀h,L,U,i. ⦃h, L⦄ ⊢ #i • U →
+ (∃∃K,V,W. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V • W &
+ ⇧[0, i + 1] W ≡ U
+ ) ∨
+ (∃∃K,W,V. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W • V &
+ ⇧[0, i + 1] W ≡ U
+ ).
+/2 width=3/ qed-.
+
+fact sta_inv_bind1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∀J,X,Y. T = ⓑ{J}Y.X →
+ ∃∃Z. ⦃h, L.ⓑ{J}Y⦄ ⊢ X • Z & U = ⓑ{J}Y.Z.
+#h #L #T #U * -L -T -U
+[ #L #k #J #X #Y #H destruct
+| #L #K #V #W #U #i #_ #_ #_ #J #X #Y #H destruct
+| #L #K #W #V #U #i #_ #_ #_ #J #X #Y #H destruct
+| #I #L #V #T #U #HTU #J #X #Y #H destruct /2 width=3/
+| #L #V #T #U #_ #J #X #Y #H destruct
+| #L #T #U #_ #J #X #Y #H destruct
+]
+qed.
+
+(* Basic_1: was: sty0_gen_bind *)
+lemma sta_inv_bind1: ∀h,J,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{J}Y.X • U →
+ ∃∃Z. ⦃h, L.ⓑ{J}Y⦄ ⊢ X • Z & U = ⓑ{J}Y.Z.
+/2 width=3/ qed-.
+
+fact sta_inv_appl1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∀X,Y. T = ⓐY.X →
+ ∃∃Z. ⦃h, L⦄ ⊢ X • Z & U = ⓐY.Z.
+#h #L #T #U * -L -T -U
+[ #L #k #X #Y #H destruct
+| #L #K #V #W #U #i #_ #_ #_ #X #Y #H destruct
+| #L #K #W #V #U #i #_ #_ #_ #X #Y #H destruct
+| #I #L #V #T #U #_ #X #Y #H destruct
+| #L #V #T #U #HTU #X #Y #H destruct /2 width=3/
+| #L #T #U #_ #X #Y #H destruct
+]
+qed.
+
+(* Basic_1: was: sty0_gen_appl *)
+lemma sta_inv_appl1: ∀h,L,Y,X,U. ⦃h, L⦄ ⊢ ⓐY.X • U →
+ ∃∃Z. ⦃h, L⦄ ⊢ X • Z & U = ⓐY.Z.
+/2 width=3/ qed-.
+
+fact sta_inv_cast1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∀X,Y. T = ⓣY.X →
+ ⦃h, L⦄ ⊢ X • Y ∧ U = Y.
+#h #L #T #U * -L -T -U
+[ #L #k #X #Y #H destruct
+| #L #K #V #W #U #i #_ #_ #_ #X #Y #H destruct
+| #L #K #W #V #U #i #_ #_ #_ #X #Y #H destruct
+| #I #L #V #T #U #_ #X #Y #H destruct
+| #L #V #T #U #_ #X #Y #H destruct
+| #L #T #U #HTU #X #Y #H destruct /2 width=1/
+]
+qed.
+
+(* Basic_1: was: sty0_gen_cast *)
+lemma sta_inv_cast1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓣY.X • U → ⦃h, L⦄ ⊢ X • Y ∧ U = Y.
+/2 width=3/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/substitution/ldrop_ldrop.ma".
+include "basic_2/static/sta.ma".
+
+(* STATIC TYPE ASSIGNMENT ON TERMS ******************************************)
+
+(* Properties on relocation *************************************************)
+
+(* Basic_1: was: sty0_lift *)
+lemma sta_lift: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 • U1 → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 →
+ ∀T2. ⇧[d, e] T1 ≡ T2 → ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 • U2.
+#h #L1 #T1 #U1 #H elim H -L1 -T1 -U1
+[ #L1 #k #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+ >(lift_inv_sort1 … H1) -X1
+ >(lift_inv_sort1 … H2) -X2 //
+| #L1 #K1 #V1 #W1 #W #i #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2
+ elim (lift_inv_lref1 … H) * #Hid #H destruct
+ [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // #W2 #HW12 #HWU2
+ elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
+ elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct
+ /3 width=8/
+ | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
+ lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
+ ]
+| #L1 #K1 #W1 #V1 #W #i #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2
+ elim (lift_inv_lref1 … H) * #Hid #H destruct
+ [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // <minus_plus #W #HW1 #HWU2
+ elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
+ elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #W2 #HK21 #HW12 #H destruct
+ lapply (lift_mono … HW1 … HW12) -HW1 #H destruct
+ elim (lift_total V1 (d-i-1) e) /3 width=8/
+ | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
+ lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
+ ]
+| #I #L1 #V1 #T1 #U1 #_ #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+ elim (lift_inv_bind1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
+ elim (lift_inv_bind1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
+ lapply (lift_mono … H1 … HV12) -H1 #H destruct /4 width=5/
+| #L1 #V1 #T1 #U1 #_ #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+ elim (lift_inv_flat1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
+ elim (lift_inv_flat1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
+ lapply (lift_mono … H1 … HV12) -H1 #H destruct /4 width=5/
+| #L1 #T1 #U1 #_ #IHTU1 #L2 #d #e #HL21 #X #H #U2 #HU12
+ elim (lift_inv_flat1 … H) -H #X2 #T2 #HUX2 #HT12 #H destruct
+ lapply (lift_mono … HUX2 … HU12) -HUX2 #H destruct /3 width=5/
+]
+qed.
+
+(* Note: apparently this was missing in basic_1 *)
+lemma sta_inv_lift: ∀h,L2,T2,U2. ⦃h, L2⦄ ⊢ T2 • U2 → ∀L1,d,e. ⇩[d, e] L2 ≡ L1 →
+ ∀T1. ⇧[d, e] T1 ≡ T2 →
+ ∃∃U1. ⦃h, L1⦄ ⊢ T1 • U1 & ⇧[d, e] U1 ≡ U2.
+#h #L2 #T2 #U2 #H elim H -L2 -T2 -U2
+[ #L2 #k #L1 #d #e #_ #X #H
+ >(lift_inv_sort2 … H) -X /2 width=3/
+| #L2 #K2 #V2 #W2 #W #i #HLK2 #HVW2 #HW2 #IHVW2 #L1 #d #e #HL21 #X #H
+ elim (lift_inv_lref2 … H) * #Hid #H destruct [ -HVW2 | -IHVW2 ]
+ [ elim (ldrop_conf_lt … HL21 … HLK2 ?) -L2 // #K1 #V1 #HLK1 #HK21 #HV12
+ elim (IHVW2 … HK21 … HV12) -K2 -V2 #W1 #HVW1 #HW12
+ elim (lift_trans_le … HW12 … HW2 ?) -W2 // >minus_plus <plus_minus_m_m // -Hid /3 width=6/
+ | lapply (ldrop_conf_ge … HL21 … HLK2 ?) -L2 // #HL1K2
+ elim (le_inv_plus_l … Hid) -Hid #Hdie #ei
+ elim (lift_split … HW2 d (i-e+1) ? ? ?) -HW2 // [3: /2 width=1/ ]
+ [ #W0 #HW20 <le_plus_minus_comm // >minus_minus_m_m /2 width=1/ /3 width=6/
+ | <le_plus_minus_comm // /2 width=1/
+ ]
+ ]
+| #L2 #K2 #W2 #V2 #W #i #HLK2 #HWV2 #HW2 #IHWV2 #L1 #d #e #HL21 #X #H
+ elim (lift_inv_lref2 … H) * #Hid #H destruct [ -HWV2 | -IHWV2 ]
+ [ elim (ldrop_conf_lt … HL21 … HLK2 ?) -L2 // #K1 #W1 #HLK1 #HK21 #HW12
+ elim (IHWV2 … HK21 … HW12) -K2 #V1 #HWV1 #_
+ elim (lift_trans_le … HW12 … HW2 ?) -W2 // >minus_plus <plus_minus_m_m // -Hid /3 width=6/
+ | lapply (ldrop_conf_ge … HL21 … HLK2 ?) -L2 // #HL1K2
+ elim (le_inv_plus_l … Hid) -Hid #Hdie #ei
+ elim (lift_split … HW2 d (i-e+1) ? ? ?) -HW2 // [3: /2 width=1/ ]
+ [ #W0 #HW20 <le_plus_minus_comm // >minus_minus_m_m /2 width=1/ /3 width=6/
+ | <le_plus_minus_comm // /2 width=1/
+ ]
+ ]
+| #I #L2 #V2 #T2 #U2 #_ #IHTU2 #L1 #d #e #HL21 #X #H
+ elim (lift_inv_bind2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
+ elim (IHTU2 (L1.ⓑ{I}V1) … HT12) -IHTU2 -HT12 /2 width=1/ -HL21 /3 width=5/
+| #L2 #V2 #T2 #U2 #_ #IHTU2 #L1 #d #e #HL21 #X #H
+ elim (lift_inv_flat2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
+ elim (IHTU2 … HL21 … HT12) -L2 -HT12 /3 width=5/
+| #L2 #T2 #U2 #_ #IHTU2 #L1 #d #e #HL21 #X #H
+ elim (lift_inv_flat2 … H) -H #U1 #T1 #HU12 #HT12 #H destruct
+ elim (IHTU2 … HL21 … HT12) -L2 -HT12 #U0 #HTU0 #HU02
+ lapply (lift_inj … HU02 … HU12) -HU02 #H destruct /3 width=3/
+]
+qed.
+
+(* Advanced forvard lemmas **************************************************)
+
+(* Basic_1: was: sty0_correct *)
+lemma sta_fwd_correct: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∃T0. ⦃h, L⦄ ⊢ U • T0.
+#h #L #T #U #H elim H -L -T -U
+[ /2 width=2/
+| #L #K #V #W #W0 #i #HLK #_ #HW0 * #V0 #HWV0
+ lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+ elim (lift_total V0 0 (i+1)) /3 width=10/
+| #L #K #W #V #V0 #i #HLK #HWV #HWV0 #_
+ lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+ elim (lift_total V 0 (i+1)) /3 width=10/
+| #I #L #V #T #U #_ * /3 width=2/
+| #L #V #T #U #_ * #T0 #HUT0 /3 width=2/
+| #L #T #U #_ * /2 width=2/
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/substitution/ldrop_ldrop.ma".
+include "basic_2/static/sta.ma".
+
+(* STATIC TYPE ASSIGNMENT ON TERMS ******************************************)
+
+(* Main properties **********************************************************)
+
+(* Note: apparently this was missing in basic_1 *)
+theorem sta_mono: ∀h,L,T,U1. ⦃h, L⦄ ⊢ T • U1 →
+ ∀U2. ⦃h, L⦄ ⊢ T • U2 → U1 = U2.
+#h #L #T #U1 #H elim H -L -T -U1
+[ #L #k #X #H >(sta_inv_sort1 … H) -X //
+| #L #K #V #W #U1 #i #HLK #_ #HWU1 #IHVW #U2 #H
+ elim (sta_inv_lref1 … H) -H * #K0 #V0 #W0 #HLK0 #HVW0 #HW0U2
+ lapply (ldrop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct
+ lapply (IHVW … HVW0) -IHVW -HVW0 #H destruct
+ >(lift_mono … HWU1 … HW0U2) -W0 -U1 //
+| #L #K #W #V #U1 #i #HLK #_ #HWU1 #IHWV #U2 #H
+ elim (sta_inv_lref1 … H) -H * #K0 #W0 #V0 #HLK0 #HWV0 #HV0U2
+ lapply (ldrop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct
+ lapply (IHWV … HWV0) -IHWV -HWV0 #H destruct
+ >(lift_mono … HWU1 … HV0U2) -W -U1 //
+| #I #L #V #T #U1 #_ #IHTU1 #X #H
+ elim (sta_inv_bind1 … H) -H #U2 #HTU2 #H destruct /3 width=1/
+| #L #V #T #U1 #_ #IHTU1 #X #H
+ elim (sta_inv_appl1 … H) -H #U2 #HTU2 #H destruct /3 width=1/
+| #L #T #U1 #_ #_ #U2 #H
+ elim (sta_inv_cast1 … H) -H //
+]
+qed-.
#b #c #a #H >(plus_minus_m_m b c) in ⊢ (? ? ?%); //
qed.
+lemma minus_minus_m_m: ∀m,n. n ≤ m → m - (m - n) = n.
+/2 width=1/ qed.
+
(* Stilll more atomic conclusion ********************************************)
(* le *)
;;
let predefined_classes = [
+ ["."; "•"; "◦"; ];
["#"; "⌘"; ];
["-"; "÷"; "⊢"; ];
["="; "≃"; "≈"; "≝"; "≡"; "≅"; "≐"; "≑"; ];
projects / helm.git / commitdiff