L ⊢ T1 [d, 1] ≡ T2 → [d ← V] T1 = T2.
#K #V #T1 elim T1 -T1
[ * #i #L #T2 #d #HLK #H
- [ -HLK >(delift_fwd_sort1 … H) -H //
+ [ -HLK >(delift_inv_sort1 … H) -H //
| elim (lt_or_eq_or_gt i d) #Hid normalize
- [ -HLK >(delift_fwd_lref1_lt … H) -H // /2 width=1/
+ [ -HLK >(delift_inv_lref1_lt … H) -H // /2 width=1/
| destruct
- elim (delift_fwd_lref1_be … H ? ?) -H // #K0 #V0 #V2 #HLK0
+ elim (delift_inv_lref1_be … H ? ?) -H // #K0 #V0 #V2 #HLK0
lapply (ldrop_mono … HLK0 … HLK) -HLK0 -HLK #H >minus_plus <minus_n_n #HV2 #HVT2 destruct
>(delift_inv_refl_O2 … HV2) -V >(flift_inv_lift … HVT2) -V2 //
- | -HLK >(delift_fwd_lref1_ge … H) -H // /2 width=1/
+ | -HLK >(delift_inv_lref1_ge … H) -H // /2 width=1/
]
- | -HLK >(delift_fwd_gref1 … H) -H //
+ | -HLK >(delift_inv_gref1 … H) -H //
]
| * #I #V1 #T1 #IHV1 #IHT1 #L #X #d #HLK #H
- [ elim (delift_fwd_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ [ elim (delift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
<(IHV1 … HV12) -IHV1 -HV12 // <(IHT1 … HT12) -IHT1 -HT12 // /2 width=1/
- | elim (delift_fwd_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ | elim (delift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
<(IHV1 … HV12) -IHV1 -HV12 // <(IHT1 … HT12) -IHT1 -HT12 //
]
]
⇧[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_appl: ∀L,V,W,T,U. nta h L V W → nta h L (ⓛW.T) (ⓛW.U) →
+ nta h L (ⓐV.ⓛW.T) (ⓐV.ⓛW.U)
| 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
| #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 #V #W #T #U #_ #_ #_ #_ #k0 #H destruct
| #L #T #U #_ #_ #k0 #H destruct
| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #k0 #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 #V #W #T #U #_ #_ #_ #_ #j #H destruct
| #L #T #U #_ #_ #j #H destruct
| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #j #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 #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
| #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 #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 (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
+| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #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 *)
+ elim (lift_inv_bind1 … H1) -H1 #W2 #T2 #HW12 #HT12 #H destruct
+ elim (lift_inv_flat1 … H2) -H2 #Y2 #X #HY #H2 #H destruct
+ elim (lift_inv_bind1 … H2) -H2 #X2 #U2 #HX #HU12 #H destruct
+ lapply (lift_mono … HY … HV12) -HY #H destruct
+ lapply (lift_mono … HX … HW12) -HX #H destruct /4 width=6/
| #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 (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 #HVW #_ #_ * #X #H
+ elim (nta_inv_bind1 … H) -H /4 width=2/
| #L #V #W #T #U #_ #HUW * #T0 #HUT0 /3 width=2/
| #L #T #U #_ * /2 width=2/
| /2 width=2/
⦃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/
+elim (nta_inv_bind1 … H) -H /4 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/sta.ma".
+include "basic_2/dynamic/nta_lift.ma".
+
+(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
+
+axiom pippo: ∀h,L,X,Y1,U. ⦃h, L⦄ ⊢ ⓐX.Y1 : U → ∀Y2. L ⊢ Y1 ⬌* Y2 →
+ ∀U2. ⦃h, L⦄ ⊢ Y2 : U2 → ⦃h, L⦄ ⊢ ⓐX.Y2 : U.
+
+(* Properties on static type assignment *************************************)
+
+lemma nta_fwd_sta: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U →
+ ∃∃U0. ⦃h, L⦄ ⊢ T • U0 & L ⊢ U0 ⬌* U & ⦃h, L⦄ ⊢ T : U0.
+#h #L #T #U #H elim H -L -T -U
+[ /2 width=4/
+| #L #K #V #W1 #V1 #i #HLK #_ #HWV1 * #W0 #H1VW0 #HW01 #H2VW0
+ elim (lift_total W0 0 (i+1)) #V0 #HWV0
+ lapply (ldrop_fwd_ldrop2 … HLK) #HLK0
+ lapply (cpcs_lift … HLK0 … HWV0 … HWV1 HW01) -HLK0 -HWV1 -HW01 /3 width=9/
+| #L #K #W #V1 #W1 #i #HLK #HWV1 #HW1 * /3 width=9/
+| #I #L #V #W #T #U #_ #_ * #W0 #_ #_ #H2VW0 * /3 width=4/
+| #L #V #W #T #U #_ #_ * #W0 #_ #HW0 #H2VW0 * #X #H1 #HX #H2
+ elim (sta_inv_bind1 … H1) -H1 #U0 #HTU0 #H destruct
+ elim (nta_inv_bind1 … H2) /4 width=4/
+| #L #V #W #T #U #_ #_ * #U0 #H1TU0 #HU0 #H2TU0 * #W0 #_ #_ #H2UW0 -W
+ elim (nta_fwd_correct … H2TU0) #T0 #HUT0
+ @(ex3_1_intro … (ⓐV.U0)) /2 width=1/ -H1TU0
+ @(nta_pure … W0 … H2TU0) -T /3 width=3/
+| #L #T #U #HTU * #U0 #H1TU0 #HU0 #H2TU0
+ elim (nta_fwd_correct … H2TU0) -H2TU0 /4 width=8/
+| #L #T #U1 #U2 #V2 #_ #HU12 #_ * #U0 #H1TU0 #HU01 #H2TU0 #_
+ lapply (cpcs_trans … HU01 … HU12) -U1 /2 width=4/
+]
+qed-.
elim (cpcs_inv_cprs … HT12) -HT12 /3 width=5 by cprs_div, cprs_abbr1/ (**) (* /3 width=5/ is a bit slow *)
qed.
+lemma cpcs_bind_dx: ∀I,L,V,T1,T2. L.ⓑ{I}V ⊢ T1 ⬌* T2 →
+ L ⊢ ⓑ{I}V. T1 ⬌* ⓑ{I}V. T2.
+* /2 width=1/ /2 width=2/ qed.
+
lemma cpcs_abbr_sn: ∀L,V1,V2,T. L ⊢ V1 ⬌* V2 → L ⊢ ⓓV1. T ⬌* ⓓV2. T.
#L #V1 #V2 #T #HV12
elim (cpcs_inv_cprs … HV12) -HV12 /3 width=5 by cprs_div, cprs_abbr1/ (**) (* /3 width=5/ is a bit slow *)
non associative with precedence 45
for @{ 'TSubst $L $T1 $d $e $T2 }.
+notation "hvbox( T1 break [ d , break e ] ≡≡ break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'TSubstAlt $T1 $d $e $T2 }.
+
+notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ≡≡ break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'TSubstAlt $L $T1 $d $e $T2 }.
+
(* Static typing ************************************************************)
notation "hvbox( L ⊢ break term 90 T ÷ break A )"
>(tpr_inv_atom1 … H) -H //
| #I #L1 #K1 #V1 #B #i #HLK1 #HK1 #H1 #H2 #L2 #HL12 #T2 #H destruct
>(tpr_inv_atom1 … H) -T2
- lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1
+ lapply (ldrop_pair2_fwd_cw … HLK1 (#i)) #HKV1
elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H
elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
lapply (IH … HKV1 … HK1 … HK12 … HV12) // -L1 -K1 -V1 /2 width=5/
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
+| sta_cast: ∀L,W,T,U. sta h L T U → sta h L (ⓣW. T) U
.
interpretation "static type assignment (term)"
| #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
+| #L #W #T #U #_ #k0 #H destruct
qed.
(* Basic_1: was: sty0_gen_sort *)
| #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
+| #L #W #T #U #_ #j #H destruct
]
qed.
| #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
+| #L #W #T #U #_ #J #X #Y #H destruct
]
qed.
| #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
+| #L #W #T #U #_ #X #Y #H destruct
]
qed.
/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⦄ ⊢ X • U.
#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/
+| #L #W #T #U #HTU #X #Y #H destruct //
]
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-.
+lemma sta_inv_cast1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓣY.X • U → ⦃h, L⦄ ⊢ X • U.
+/2 width=4/ qed-.
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/
+| #L1 #W1 #T1 #U1 #_ #IHTU1 #L2 #d #e #HL21 #X #H #U2 #HU12
+ elim (lift_inv_flat1 … H) -H #W2 #T2 #_ #HT12 #H destruct /3 width=5/
]
qed.
| #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/
+| #L2 #W2 #T2 #U2 #_ #IHTU2 #L1 #d #e #HL21 #X #H
+ elim (lift_inv_flat2 … H) -H #W1 #T1 #_ #HT12 #H destruct
+ elim (IHTU2 … HL21 … HT12) -L2 -HT12 /3 width=3/
]
qed.
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/
+| #L #W #T #U #_ * /2 width=2/
]
qed-.
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 //
+| #L #W #T #U1 #_ #IHTU1 #U2 #H
+ lapply (sta_inv_cast1 … H) -H /2 width=1/
]
qed-.
#L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
qed.
+lemma ldrop_O1: ∀L,i. i < |L| → ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V.
+#L elim L -L
+[ #i #H elim (lt_zero_false … H)
+| #L #I #V #IHL #i @(nat_ind_plus … i) -i /2 width=4/ #i #_ #H
+ lapply (lt_plus_to_lt_l … H) -H #Hi
+ elim (IHL i ?) // /3 width=4/
+]
+qed.
+
lemma ldrop_lsubs_ldrop1_abbr: ∀L1,L2,d,e. L1 [d, e] ≼ L2 →
∀K1,V,i. ⇩[0, i] L1 ≡ K1. ⓓV →
d ≤ i → i < d + e →
]
qed-.
-lemma ldrop_pair2_fwd_fw: ∀I,L,K,V,d,e. ⇩[d, e] L ≡ K. ⓑ{I} V →
+lemma ldrop_pair2_fwd_cw: ∀I,L,K,V,d,e. ⇩[d, e] L ≡ K. ⓑ{I} V →
∀T. #[K, V] < #[L, T].
#I #L #K #V #d #e #H #T
lapply (ldrop_fwd_lw … H) -H #H
elim (IHT12 … HT20 ?) -IHT12 -HT20 // /3 width=5/
]
qed.
+
+(* Advanced properties ******************************************************)
+
+lemma lift_conf_le: ∀T,T1,d. ⇧[O, d] T ≡ T1 → ∀T2,e. ⇧[O, d + e] T ≡ T2 →
+ ⇧[d, e] T1 ≡ T2.
+#T #T1 #d #HT1 #T2 #e #HT2
+elim (lift_split … HT2 d d ? ? ?) -HT2 // #X #H
+>(lift_mono … H … HT1) -T //
+qed.
(* Basic properties *********************************************************)
+lemma delift_refl_O2: ∀L,T,d. L ⊢ T [d, 0] ≡ T.
+/2 width=3/ qed.
+
lemma delift_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≡ T2 →
∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ≡ T2.
#L1 #T1 #T2 #d #e * /3 width=3/
qed.
+lemma delift_sort: ∀L,d,e,k. L ⊢ ⋆k [d, e] ≡ ⋆k.
+/2 width=3/ qed.
+
+lemma delift_lref_lt: ∀L,d,e,i. i < d → L ⊢ #i [d, e] ≡ #i.
+/3 width=3/ qed.
+
+lemma delift_lref_ge: ∀L,d,e,i. d + e ≤ i → L ⊢ #i [d, e] ≡ #(i - e).
+/3 width=3/ qed.
+
+lemma delift_gref: ∀L,d,e,p. L ⊢ §p [d, e] ≡ §p.
+/2 width=3/ qed.
+
lemma delift_bind: ∀I,L,V1,V2,T1,T2,d,e.
L ⊢ V1 [d, e] ≡ V2 → L. ⓑ{I} V2 ⊢ T1 [d+1, e] ≡ T2 →
L ⊢ ⓑ{I} V1. T1 [d, e] ≡ ⓑ{I} V2. T2.
#I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * /3 width=5/
qed.
-(* Basic forward lemmas *****************************************************)
+(* Basic inversion lemmas ***************************************************)
-lemma delift_fwd_sort1: ∀L,U2,d,e,k. L ⊢ ⋆k [d, e] ≡ U2 → U2 = ⋆k.
+lemma delift_inv_sort1: ∀L,U2,d,e,k. L ⊢ ⋆k [d, e] ≡ U2 → U2 = ⋆k.
#L #U2 #d #e #k * #U #HU
>(tpss_inv_sort1 … HU) -HU #HU2
>(lift_inv_sort2 … HU2) -HU2 //
qed-.
-lemma delift_fwd_gref1: ∀L,U2,d,e,p. L ⊢ §p [d, e] ≡ U2 → U2 = §p.
+lemma delift_inv_gref1: ∀L,U2,d,e,p. L ⊢ §p [d, e] ≡ U2 → U2 = §p.
#L #U #d #e #p * #U #HU
>(tpss_inv_gref1 … HU) -HU #HU2
>(lift_inv_gref2 … HU2) -HU2 //
qed-.
-lemma delift_fwd_bind1: ∀I,L,V1,T1,U2,d,e. L ⊢ ⓑ{I} V1. T1 [d, e] ≡ U2 →
+lemma delift_inv_bind1: ∀I,L,V1,T1,U2,d,e. L ⊢ ⓑ{I} V1. T1 [d, e] ≡ U2 →
∃∃V2,T2. L ⊢ V1 [d, e] ≡ V2 &
L. ⓑ{I} V2 ⊢ T1 [d+1, e] ≡ T2 &
U2 = ⓑ{I} V2. T2.
lapply (tpss_lsubs_conf … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
qed-.
-lemma delift_fwd_flat1: ∀I,L,V1,T1,U2,d,e. L ⊢ ⓕ{I} V1. T1 [d, e] ≡ U2 →
+lemma delift_inv_flat1: ∀I,L,V1,T1,U2,d,e. L ⊢ ⓕ{I} V1. T1 [d, e] ≡ U2 →
∃∃V2,T2. L ⊢ V1 [d, e] ≡ V2 &
L ⊢ T1 [d, e] ≡ T2 &
U2 = ⓕ{I} V2. T2.
elim (lift_inv_flat2 … HU2) -HU2 /3 width=5/
qed-.
-(* Basic Inversion lemmas ***************************************************)
-
lemma delift_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 [d, 0] ≡ T2 → T1 = T2.
#L #T1 #T2 #d * #T #HT1
>(tpss_inv_refl_O2 … HT1) -HT1 #HT2
--- /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/unfold/delift_lift.ma".
+
+(* DELIFT ON TERMS **********************************************************)
+
+(* alternative definition of delift *)
+inductive delifta: nat → nat → lenv → relation term ≝
+| delifta_sort : ∀L,d,e,k. delifta d e L (⋆k) (⋆k)
+| delifta_lref_lt: ∀L,d,e,i. i < d → delifta d e L (#i) (#i)
+| delifta_lref_be: ∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e →
+ ⇩[0, i] L ≡ K. ⓓV1 → delifta 0 (d + e - i - 1) K V1 V2 →
+ ⇧[0, d] V2 ≡ W2 → delifta d e L (#i) W2
+| delifta_lref_ge: ∀L,d,e,i. d + e ≤ i → delifta d e L (#i) (#(i - e))
+| delifta_gref : ∀L,d,e,p. delifta d e L (§p) (§p)
+| delifta_bind : ∀L,I,V1,V2,T1,T2,d,e.
+ delifta d e L V1 V2 → delifta (d + 1) e (L. ⓑ{I} V2) T1 T2 →
+ delifta d e L (ⓑ{I} V1. T1) (ⓑ{I} V2. T2)
+| delifta_flat : ∀L,I,V1,V2,T1,T2,d,e.
+ delifta d e L V1 V2 → delifta d e L T1 T2 →
+ delifta d e L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
+.
+
+interpretation "delift (term) alternative"
+ 'TSubstAlt L T1 d e T2 = (delifta d e L T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma delifta_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≡≡ T2 →
+ ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ≡≡ T2.
+#L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e // /2 width=1/
+[ #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
+ elim (ldrop_lsubs_ldrop1_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
+| /4 width=1/
+| /3 width=1/
+]
+qed.
+
+lemma delift_delifta: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≡ T2 → L ⊢ T1 [d, e] ≡≡ T2.
+#L #T1 @(cw_wf_ind … L T1) -L -T1 #L #T1 elim T1 -T1
+[ * #i #IH #T2 #d #e #H
+ [ >(delift_inv_sort1 … H) -H //
+ | elim (delift_inv_lref1 … H) -H * /2 width=1/
+ #K #V1 #V2 #Hdi #Hide #HLK #HV12 #HVT2
+ lapply (ldrop_pair2_fwd_cw … HLK) #H
+ lapply (IH … HV12) // -H /2 width=6/
+ | >(delift_inv_gref1 … H) -H //
+ ]
+| * #I #V1 #T1 #_ #_ #IH #X #d #e #H
+ [ elim (delift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ lapply (delift_lsubs_conf … HT12 (L.ⓑ{I}V1) ?) -HT12 /2 width=1/ #HT12
+ lapply (IH … HV12) -HV12 // #HV12
+ lapply (IH … HT12) -IH -HT12 /2 width=1/ #HT12
+ lapply (delifta_lsubs_conf … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/
+ | elim (delift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ lapply (IH … HV12) -HV12 //
+ lapply (IH … HT12) -IH -HT12 // /2 width=1/
+ ]
+]
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma delifta_delift: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≡≡ T2 → L ⊢ T1 [d, e] ≡ T2.
+#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e // /2 width=1/ /2 width=6/
+qed-.
+
+lemma delift_ind_alt: ∀R:ℕ→ℕ→lenv→relation term.
+ (∀L,d,e,k. R d e L (⋆k) (⋆k)) →
+ (∀L,d,e,i. i < d → R d e L (#i) (#i)) →
+ (∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e →
+ ⇩[O, i] L ≡ K.ⓓV1 → K ⊢ V1 [O, d + e - i - 1] ≡ V2 →
+ ⇧[O, d] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L #i W2
+ ) →
+ (∀L,d,e,i. d + e ≤ i → R d e L (#i) (#(i - e))) →
+ (∀L,d,e,p. R d e L (§p) (§p)) →
+ (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 [d, e] ≡ V2 →
+ L.ⓑ{I}V2 ⊢ T1 [d + 1, e] ≡ T2 → R d e L V1 V2 →
+ R (d+1) e (L.ⓑ{I}V2) T1 T2 → R d e L (ⓑ{I}V1.T1) (ⓑ{I}V2.T2)
+ ) →
+ (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 [d, e] ≡ V2 →
+ L⊢ T1 [d, e] ≡ T2 → R d e L V1 V2 →
+ R d e L T1 T2 → R d e L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
+ ) →
+ ∀d,e,L,T1,T2. L ⊢ T1 [d, e] ≡ T2 → R d e L T1 T2.
+#R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #d #e #L #T1 #T2 #H elim (delift_delifta … H) -L -T1 -T2 -d -e
+// /2 width=1 by delifta_delift/ /3 width=1 by delifta_delift/ /3 width=7 by delifta_delift/
+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/unfold/tpss_tpss.ma".
+include "basic_2/unfold/delift.ma".
+
+(* DELIFT ON TERMS **********************************************************)
+
+(* Main properties **********************************************************)
+
+theorem delift_mono: ∀L,T,T1,T2,d,e.
+ L ⊢ T [d, e] ≡ T1 → L ⊢ T [d, e] ≡ T2 → T1 = T2.
+#L #T #T1 #T2 #d #e * #U1 #H1TU1 #H2TU1 * #U2 #H1TU2 #H2TU2
+elim (tpss_conf_eq … H1TU1 … H1TU2) -T #U #HU1 #HU2
+lapply (tpss_inv_lift1_eq … HU1 … H2TU1) -HU1 #H destruct
+lapply (tpss_inv_lift1_eq … HU2 … H2TU2) -HU2 #H destruct
+lapply (lift_inj … H2TU1 … H2TU2) //
+qed-.
(* DELIFT ON TERMS **********************************************************)
+(* Advanced properties ******************************************************)
+
+lemma delift_lref_be: ∀L,K,V1,V2,U2,i,d,e. d ≤ i → i < d + e →
+ ⇩[0, i] L ≡ K. ⓓV1 → K ⊢ V1 [0, d + e - i - 1] ≡ V2 →
+ ⇧[0, d] V2 ≡ U2 → L ⊢ #i [d, e] ≡ U2.
+#L #K #V1 #V2 #U2 #i #d #e #Hdi #Hide #HLK * #V #HV1 #HV2 #HVU2
+elim (lift_total V 0 (i+1)) #U #HVU
+lapply (lift_trans_be … HV2 … HVU ? ?) -HV2 // >minus_plus <plus_minus_m_m
+/2 width=1/ /3 width=6/
+qed.
+
(* Advanced forward lemmas **************************************************)
-lemma delift_fwd_lref1_lt: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 → i < d → U2 = #i.
+lemma delift_inv_lref1_lt: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 → i < d → U2 = #i.
#L #U2 #i #d #e * #U #HU #HU2 #Hid
elim (tpss_inv_lref1 … HU) -HU
[ #H destruct >(lift_inv_lref2_lt … HU2) //
]
qed-.
-lemma delift_fwd_lref1_be: ∀L,U2,d,e,i. L ⊢ #i [d, e] ≡ U2 →
+lemma delift_inv_lref1_be: ∀L,U2,d,e,i. L ⊢ #i [d, e] ≡ U2 →
d ≤ i → i < d + e →
∃∃K,V1,V2. ⇩[0, i] L ≡ K. ⓓV1 &
K ⊢ V1 [0, d + e - i - 1] ≡ V2 &
]
qed-.
-lemma delift_fwd_lref1_ge: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 →
+lemma delift_inv_lref1_ge: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 →
d + e ≤ i → U2 = #(i - e).
#L #U2 #i #d #e * #U #HU #HU2 #Hdei
elim (tpss_inv_lref1 … HU) -HU
elim (lt_refl_false … Hi)
]
qed-.
+
+lemma delift_inv_lref1: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 →
+ ∨∨ (i < d ∧ U2 = #i)
+ | (∃∃K,V1,V2. d ≤ i & i < d + e &
+ ⇩[0, i] L ≡ K. ⓓV1 &
+ K ⊢ V1 [0, d + e - i - 1] ≡ V2 &
+ ⇧[0, d] V2 ≡ U2
+ )
+ | (d + e ≤ i ∧ U2 = #(i - e)).
+#L #U2 #i #d #e #H
+elim (lt_or_ge i d) #Hdi
+[ elim (delift_inv_lref1_lt … H Hdi) -H /3 width=1/
+| elim (lt_or_ge i (d+e)) #Hide
+ [ elim (delift_inv_lref1_be … H Hdi Hide) -H /3 width=6/
+ | elim (delift_inv_lref1_ge … H Hide) -H /3 width=1/
+ ]
+]
+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/unfold/ltpss.ma".
+
+(* DELIFT ON LOCAL ENVIRONMENTS ********************************************)
+
+definition thin: nat → nat → relation lenv ≝
+ λd,e,L1,L2. ∃∃L. L1 [d, e] ▶* L & ⇩[d, e] L ≡ L2.
+
+interpretation "delift (local environment)"
+ 'TSubst L1 d e L2 = (thin d e L1 L2).
+
+(* Basic properties *********************************************************)
--- /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/unfold/tpss_alt.ma".
+include "basic_2/unfold/ltpss_ltpss.ma".
+include "basic_2/unfold/delift_alt.ma".
+include "basic_2/unfold/thin.ma".
+
+(* DELIFT ON LOCAL ENVIRONMENTS *********************************************)
+
+(* Properties on deflift on terms *******************************************)
+
+lemma thin_delift1: ∀L1,L2,d,e. L1 [d, e] ≡ L2 → ∀V1,V2. L1 ⊢ V1 [d, e] ≡ V2 →
+ ∀I. L1.ⓑ{I}V1 [d + 1, e] ≡ L2.ⓑ{I}V2.
+#L1 #L2 #d #e * #L #HL1 #HL2 #V1 #V2 * #V #HV1 #HV2 #I
+elim (ltpss_tpss_conf … HV1 … HL1) -HV1 #V0 #HV10 #HV0
+elim (tpss_inv_lift1_be … HV0 … HL2 … HV2 ? ?) -HV0 // <minus_n_n #X #H1 #H2
+lapply (tpss_inv_refl_O2 … H1) -H1 #H destruct
+lapply (lift_mono … H2 … HV2) -H2 #H destruct /3 width=5/
+qed.
+
+axiom delift_tpss_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 →
+ ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 → ∀K. L [dd, ee] ≡ K →
+ d ≤ dd → dd + ee ≤ d + e →
+ ∃∃T2. K ⊢ T1 [dd - d, e - ee] ▶* T2 & L ⊢ U2 [dd, ee] ≡ T2.
+(*
+#L #U1 #U2 #d #e #H @(tpss_ind_alt … H) -L -U1 -U2 -d -e
+[ #L * #i #d #e #X #dd #ee #H
+ [ >(delift_inv_sort1 … H) -X /2 width=3/
+ | elim (delift_inv_lref1 … H) -H * [1,3: /3 width=3/ | /3 width=6/ ]
+ | >(delift_inv_gref1 … H) -X /2 width=3/
+ ]
+| #L #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #T1 #dd #ee #H #K2 #HLK2 #Hdd #Hddee
+ lapply
+
+ @(ex2_1_intro … X) // /2 width=6/
+*)
<key name="notations">xoa_notation</key>
<key name="include">basics/pts.ma</key>
<key name="ex">1 2</key>
+ <key name="ex">1 3</key>
<key name="ex">2 1</key>
<key name="ex">2 2</key>
<key name="ex">2 3</key>
interpretation "multiple existental quantifier (1, 2)" 'Ex P0 = (ex1_2 ? ? P0).
+(* multiple existental quantifier (1, 3) *)
+
+inductive ex1_3 (A0,A1,A2:Type[0]) (P0:A0→A1→A2→Prop) : Prop ≝
+ | ex1_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → ex1_3 ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (1, 3)" 'Ex P0 = (ex1_3 ? ? ? P0).
+
(* multiple existental quantifier (2, 1) *)
inductive ex2_1 (A0:Type[0]) (P0,P1:A0→Prop) : Prop ≝
non associative with precedence 20
for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) }.
+(* multiple existental quantifier (1, 3) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) }.
+
(* multiple existental quantifier (2, 1) *)
notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)"
(* More general conclusion **************************************************)
+theorem nat_ind_plus: ∀R:predicate nat.
+ R 0 → (∀n. R n → R (n + 1)) → ∀n. R n.
+/3 width=1 by nat_ind/ qed-.
+
theorem lt_O_n_elim: ∀n:nat. 0 < n →
∀P:nat → Prop.(∀m:nat.P (S m)) → P n.
#n (elim n) // #abs @False_ind /2/ @absurd
projects / helm.git / commitdiff