(0 < e ∧ ⇩[0, e - 1] K ≡ L2).
/2 width=3/ qed-.
+lemma ldrop_inv_pair1: ∀K,I,V,L2. ⇩[0, 0] K. ⓑ{I} V ≡ L2 → L2 = K. ⓑ{I} V.
+#K #I #V #L2 #H
+elim (ldrop_inv_O1 … H) -H * // #H destruct
+elim (lt_refl_false … H)
+qed-.
+
(* Basic_1: was: drop_gen_drop *)
lemma ldrop_inv_ldrop1: ∀e,K,I,V,L2.
⇩[0, e] K. ⓑ{I} V ≡ L2 → 0 < e → ⇩[0, e - 1] K ≡ L2.
]
qed.
-(* Basic_1: was: drop_conf_lt *)
-theorem ldrop_conf_lt: ∀d1,e1,L,L1. ⇩[d1, e1] L ≡ L1 →
- ∀e2,K2,I,V2. ⇩[0, e2] L ≡ K2. ⓑ{I} V2 →
- e2 < d1 → let d ≝ d1 - e2 - 1 in
- ∃∃K1,V1. ⇩[0, e2] L1 ≡ K1. ⓑ{I} V1 &
- ⇩[d, e1] K2 ≡ K1 & ⇧[d, e1] V1 ≡ V2.
-#d1 #e1 #L #L1 #H elim H -d1 -e1 -L -L1
-[ #d #e #e2 #K2 #I #V2 #H
- lapply (ldrop_inv_atom1 … H) -H #H destruct
-| #L #I #V #e2 #K2 #J #V2 #_ #H
- elim (lt_zero_false … H)
-| #L1 #L2 #I #V #e #_ #_ #e2 #K2 #J #V2 #_ #H
- elim (lt_zero_false … H)
-| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #IHL12 #e2 #K2 #J #V #H #He2d
+(* Note: apparently this was missing in basic_1 *)
+theorem ldrop_conf_be: ∀L0,L1,d1,e1. ⇩[d1, e1] L0 ≡ L1 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
+ ∃∃L. ⇩[0, d1 + e1 - e2] L2 ≡ L & ⇩[0, d1] L1 ≡ L.
+#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
+[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
+| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
+ lapply (le_n_O_to_eq … He2) -He2 #H destruct
+ lapply (ldrop_inv_refl … HL2) -HL2 #H destruct /2 width=3/
+| normalize #L0 #K0 #I #V1 #e1 #HLK0 #IHLK0 #L2 #e2 #H #_ #He21
+ lapply (ldrop_inv_O1 … H) -H * * #He2 #HL20
+ [ -IHLK0 -He21 destruct <minus_n_O /3 width=3/
+ | -HLK0 <minus_le_minus_minus_comm //
+ elim (IHLK0 … HL20 ? ?) -L0 // /2 width=1/ /2 width=3/
+ ]
+| #L0 #K0 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHLK0 #L2 #e2 #H #Hd1e2 #He2de1
+ elim (le_inv_plus_l … Hd1e2) #_ #He2
+ <minus_le_minus_minus_comm //
+ lapply (ldrop_inv_ldrop1 … H ?) -H // #HL02
+ elim (IHLK0 … HL02 ? ?) -L0 /2 width=1/ /3 width=3/
+]
+qed.
+
+(* Note: apparently this was missing in basic_1 *)
+theorem ldrop_conf_le: ∀L0,L1,d1,e1. ⇩[d1, e1] L0 ≡ L1 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
+ ∃∃L. ⇩[0, e2] L1 ≡ L & ⇩[d1 - e2, e1] L2 ≡ L.
+#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
+[ #d1 #e1 #L2 #e2 #H
+ lapply (ldrop_inv_atom1 … H) -H #H destruct /2 width=3/
+| #K0 #I #V0 #L2 #e2 #H1 #H2
+ lapply (le_n_O_to_eq … H2) -H2 #H destruct
+ lapply (ldrop_inv_pair1 … H1) -H1 #H destruct /2 width=3/
+| #K0 #K1 #I #V0 #e1 #HK01 #_ #L2 #e2 #H1 #H2
+ lapply (le_n_O_to_eq … H2) -H2 #H destruct
+ lapply (ldrop_inv_pair1 … H1) -H1 #H destruct /3 width=3/
+| #K0 #K1 #I #V0 #V1 #d1 #e1 #HK01 #HV10 #IHK01 #L2 #e2 #H #He2d1
elim (ldrop_inv_O1 … H) -H *
- [ -IHL12 -He2d #H1 #H2 destruct /2 width=5/
- | -HL12 -HV12 #He #HLK
- elim (IHL12 … HLK ?) -IHL12 -HLK [ <minus_minus /3 width=5/ | /2 width=1/ ] (**) (* a bit slow *)
+ [ -IHK01 -He2d1 #H1 #H2 destruct /3 width=5/
+ | -HK01 -HV10 #He2 #HK0L2
+ elim (IHK01 … HK0L2 ?) -IHK01 -HK0L2 /2 width=1/ >minus_le_minus_minus_comm // /3 width=3/
]
]
qed.
+(* Basic_1: was: drop_trans_ge *)
+theorem ldrop_trans_ge: ∀d1,e1,L1,L. ⇩[d1, e1] L1 ≡ L →
+ ∀e2,L2. ⇩[0, e2] L ≡ L2 → d1 ≤ e2 → ⇩[0, e1 + e2] L1 ≡ L2.
+#d1 #e1 #L1 #L #H elim H -d1 -e1 -L1 -L
+[ #d #e #e2 #L2 #H
+ >(ldrop_inv_atom1 … H) -H -L2 //
+| //
+| /3 width=1/
+| #L1 #L2 #I #V1 #V2 #d #e #H_ #_ #IHL12 #e2 #L #H #Hde2
+ lapply (lt_to_le_to_lt 0 … Hde2) // #He2
+ lapply (lt_to_le_to_lt … (e + e2) He2 ?) // #Hee2
+ lapply (ldrop_inv_ldrop1 … H ?) -H // #HL2
+ @ldrop_ldrop_lt // >le_plus_minus // @IHL12 /2 width=1/ (**) (* explicit constructor *)
+]
+qed.
+
(* Basic_1: was: drop_trans_le *)
theorem ldrop_trans_le: ∀d1,e1,L1,L. ⇩[d1, e1] L1 ≡ L →
∀e2,L2. ⇩[0, e2] L ≡ L2 → e2 ≤ d1 →
]
qed.
-(* Basic_1: was: drop_trans_ge *)
-theorem ldrop_trans_ge: ∀d1,e1,L1,L. ⇩[d1, e1] L1 ≡ L →
- ∀e2,L2. ⇩[0, e2] L ≡ L2 → d1 ≤ e2 → ⇩[0, e1 + e2] L1 ≡ L2.
-#d1 #e1 #L1 #L #H elim H -d1 -e1 -L1 -L
-[ #d #e #e2 #L2 #H
- >(ldrop_inv_atom1 … H) -H -L2 //
-| //
-| /3 width=1/
-| #L1 #L2 #I #V1 #V2 #d #e #H_ #_ #IHL12 #e2 #L #H #Hde2
- lapply (lt_to_le_to_lt 0 … Hde2) // #He2
- lapply (lt_to_le_to_lt … (e + e2) He2 ?) // #Hee2
- lapply (ldrop_inv_ldrop1 … H ?) -H // #HL2
- @ldrop_ldrop_lt // >le_plus_minus // @IHL12 /2 width=1/ (**) (* explicit constructor *)
-]
+(* Basic_1: was: drop_conf_rev *)
+axiom ldrop_div: ∀e1,L1,L. ⇩[0, e1] L1 ≡ L → ∀e2,L2. ⇩[0, e2] L2 ≡ L →
+ ∃∃L0. ⇩[0, e1] L0 ≡ L2 & ⇩[e1, e2] L0 ≡ L1.
+
+(* Basic_1: was: drop_conf_lt *)
+lemma ldrop_conf_lt: ∀d1,e1,L,L1. ⇩[d1, e1] L ≡ L1 →
+ ∀e2,K2,I,V2. ⇩[0, e2] L ≡ K2. ⓑ{I} V2 →
+ e2 < d1 → let d ≝ d1 - e2 - 1 in
+ ∃∃K1,V1. ⇩[0, e2] L1 ≡ K1. ⓑ{I} V1 &
+ ⇩[d, e1] K2 ≡ K1 & ⇧[d, e1] V1 ≡ V2.
+#d1 #e1 #L #L1 #H1 #e2 #K2 #I #V2 #H2 #He2d1
+elim (ldrop_conf_le … H1 … H2 ?) -L [2: /2 width=2/] #K #HL1K #HK2
+elim (ldrop_inv_skip1 … HK2 ?) -HK2 [2: /2 width=1/] #K1 #V1 #HK21 #HV12 #H destruct /2 width=5/
qed.
-theorem ldrop_trans_ge_comm: ∀d1,e1,e2,L1,L2,L.
- ⇩[d1, e1] L1 ≡ L → ⇩[0, e2] L ≡ L2 → d1 ≤ e2 →
- ⇩[0, e2 + e1] L1 ≡ L2.
+lemma ldrop_trans_ge_comm: ∀d1,e1,e2,L1,L2,L.
+ ⇩[d1, e1] L1 ≡ L → ⇩[0, e2] L ≡ L2 → d1 ≤ e2 →
+ ⇩[0, e2 + e1] L1 ≡ L2.
#e1 #e1 #e2 >commutative_plus /2 width=5/
qed.
-
-(* Basic_1: was: drop_conf_rev *)
-axiom ldrop_div: ∀e1,L1,L. ⇩[0, e1] L1 ≡ L → ∀e2,L2. ⇩[0, e2] L2 ≡ L →
- ∃∃L0. ⇩[0, e1] L0 ≡ L2 & ⇩[e1, e2] L0 ≡ L1.
include "basic_2/unfold/tpss.ma".
-(* DELIFT ON TERMS **********************************************************)
+(* INVERSE TERM RELOCATION *************************************************)
definition delift: nat → nat → lenv → relation term ≝
λd,e,L,T1,T2. ∃∃T. L ⊢ T1 [d, e] ▶* T & ⇧[d, e] T2 ≡ T.
-interpretation "delift (term)"
+interpretation "inverse relocation (term)"
'TSubst L T1 d e T2 = (delift d e L T1 T2).
(* Basic properties *********************************************************)
+lemma lift_delift: ∀T1,T2,d,e. ⇧[d, e] T1 ≡ T2 →
+ ∀L. L ⊢ T2 [d, e] ≡ T1.
+/2 width=3/ qed.
+
lemma delift_refl_O2: ∀L,T,d. L ⊢ T [d, 0] ≡ T.
/2 width=3/ qed.
include "basic_2/unfold/delift_lift.ma".
-(* DELIFT ON TERMS **********************************************************)
+(* INVERSE TERM RELOCATION *************************************************)
-(* alternative definition of delift *)
+(* alternative definition of inverse relocation *)
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 d e L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
.
-interpretation "delift (term) alternative"
+interpretation "inverse relocation (term) alternative"
'TSubstAlt L T1 d e T2 = (delifta d e L T1 T2).
(* Basic properties *********************************************************)
include "basic_2/unfold/tpss_tpss.ma".
include "basic_2/unfold/delift.ma".
-(* DELIFT ON TERMS **********************************************************)
+(* INVERSE TERM RELOCATION *************************************************)
(* Main properties **********************************************************)
include "basic_2/unfold/tpss_lift.ma".
include "basic_2/unfold/delift.ma".
-(* DELIFT ON TERMS **********************************************************)
+(* INVERSE TERM RELOCATION *************************************************)
(* Advanced properties ******************************************************)
]
]
qed-.
+
+(* Relocation properties ****************************************************)
+
+lemma delift_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≡ T2 →
+ ∀L,U1,d,e. dt + et ≤ d → ⇩[d, e] L ≡ K →
+ ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d - et, e] T2 ≡ U2 →
+ L ⊢ U1 [dt, et] ≡ U2.
+#K #T1 #T2 #dt #et * #T #HT1 #HT2 #L #U1 #d #e #Hdetd #HLK #HTU1 #U2 #HTU2
+elim (lift_total T d e) #U #HTU
+lapply (tpss_lift_le … HT1 … HLK HTU1 … HTU) -T1 -HLK // #HU1
+elim (lift_trans_ge … HT2 … HTU ?) -T // -Hdetd #T #HT2 #HTU
+>(lift_mono … HTU2 … HT2) -T2 /2 width=3/
+qed.
+
+lemma delift_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≡ T2 →
+ ∀L,U1,d,e. dt ≤ d → d ≤ dt + et →
+ ⇩[d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 →
+ L ⊢ U1 [dt, et + e] ≡ T2.
+#K #T1 #T2 #dt #et * #T #HT1 #HT2 #L #U1 #d #e #Hdtd #Hddet #HLK #HTU1
+elim (lift_total T d e) #U #HTU
+lapply (tpss_lift_be … HT1 … HLK HTU1 … HTU) -T1 -HLK // #HU1
+lapply (lift_trans_be … HT2 … HTU ? ?) -T // -Hdtd -Hddet /2 width=3/
+qed.
+
+lemma delift_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≡ T2 →
+ ∀L,U1,d,e. d ≤ dt → ⇩[d, e] L ≡ K →
+ ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 →
+ L ⊢ U1 [dt + e, et] ≡ U2.
+#K #T1 #T2 #dt #et * #T #HT1 #HT2 #L #U1 #d #e #Hddt #HLK #HTU1 #U2 #HTU2
+elim (lift_total T d e) #U #HTU
+lapply (tpss_lift_ge … HT1 … HLK HTU1 … HTU) -T1 -HLK // #HU1
+elim (lift_trans_le … HT2 … HTU ?) -T // -Hddt #T #HT2 #HTU
+>(lift_mono … HTU2 … HT2) -T2 /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/unfold/ltpss_ltpss.ma".
+include "basic_2/unfold/delift.ma".
+
+(* INVERSE TERM RELOCATION *************************************************)
+
+(* Properties on partial unfold on local environments ***********************)
+
+lemma delift_ltpss_conf_eq: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≡ T2 →
+ ∀K. L [d, e] ▶* K → K ⊢ T1 [d, e] ≡ T2.
+#L #T1 #T2 #d #e * #T #HT1 #HT2 #K #HLK
+elim (ltpss_tpss_conf … HT1 … HLK) -L #T0 #HT10 #HT0
+lapply (tpss_inv_lift1_eq … HT0 … HT2) -HT0 #H destruct /2 width=3/
+qed.
+
+lemma ltpss_delift_trans_eq: ∀L,K,d,e. L [d, e] ▶* K →
+ ∀T1,T2. K ⊢ T1 [d, e] ≡ T2 → L ⊢ T1 [d, e] ≡ T2.
+#L #K #d #e #HLK #T1 #T2 * #T #HT1 #HT2
+lapply (ltpss_tpss_trans_eq … HT1 … HLK) -K /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/unfold/tpss_tpss.ma".
+include "basic_2/unfold/delift.ma".
+
+(* INVERSE TERM RELOCATION *************************************************)
+
+(* Properties on partial unfold on terms ************************************)
+
+lemma delift_tpss_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 →
+ ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+ ∀K. ⇩[dd, ee] L ≡ K → d ≤ dd → dd + ee ≤ d + e →
+ ∃∃T2. K ⊢ T1 [d, e - ee] ▶* T2 &
+ L ⊢ U2 [dd, ee] ≡ T2.
+#L #U1 #U2 #d #e #HU12 #T1 #dd #ee * #X1 #HUX1 #HTX1 #K #HLK #H1 #H2
+elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1
+elim (tpss_inv_lift1_be … HXU1 … HLK … HTX1 ? ?) -X1 -HLK // /3 width=5/
+qed.
+
+lemma delift_tps_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 →
+ ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+ ∀K. ⇩[dd, ee] L ≡ K → d ≤ dd → dd + ee ≤ d + e →
+ ∃∃T2. K ⊢ T1 [d, e - ee] ▶* T2 &
+ L ⊢ U2 [dd, ee] ≡ T2.
+/3 width=3/ qed.
+
+lemma delift_tpss_conf_eq: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 →
+ ∀T. L ⊢ U1 [d, e] ≡ T → L ⊢ U2 [d, e] ≡ T.
+#L #U1 #U2 #d #e #HU12 #T * #X1 #HUX1 #HTX1
+elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1
+lapply (tpss_inv_lift1_eq … HXU1 … HTX1) -HXU1 #H destruct /2 width=3/
+qed.
+
+lemma delift_tps_conf_eq: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 →
+ ∀T. L ⊢ U1 [d, e] ≡ T → L ⊢ U2 [d, e] ≡ T.
+/3 width=3/ qed.
+
+lemma tpss_delift_trans_eq: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 →
+ ∀T. L ⊢ U2 [d, e] ≡ T → L ⊢ U1 [d, e] ≡ T.
+#L #U1 #U2 #d #e #HU12 #T * #X1 #HUX1 #HTX1
+lapply (tpss_trans_eq … HU12 … HUX1) -U2 /2 width=3/
+qed.
+
+lemma tps_delift_trans_eq: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 →
+ ∀T. L ⊢ U2 [d, e] ≡ T → L ⊢ U1 [d, e] ≡ T.
+/3 width=3/ qed.
#L #I #V #IHL * /2 width=1/ * /2 width=1/
qed.
+lemma ltpss_weak: ∀L1,L2,d1,e1. L1 [d1, e1] ▶* L2 →
+ ∀d2,e2. d2 ≤ d1 → d1 + e1 ≤ d2 + e2 → L1 [d2, e2] ▶* L2.
+#L1 #L2 #d1 #e1 #H elim H -L1 -L2 -d1 -e1 //
+[ #L1 #L2 #I #V1 #V2 #e1 #_ #HV12 #IHL12 #d2 #e2 #Hd2 #Hde2
+ lapply (le_n_O_to_eq … Hd2) #H destruct normalize in Hde2;
+ lapply (lt_to_le_to_lt 0 … Hde2) // #He2
+ lapply (le_plus_to_minus_r … Hde2) -Hde2 /3 width=5/
+| #L1 #L2 #I #V1 #V2 #d1 #e1 #_ #HV12 #IHL12 #d2 #e2 #Hd21 #Hde12
+ >plus_plus_comm_23 in Hde12; #Hde12
+ elim (le_to_or_lt_eq 0 d2 ?) // #H destruct
+ [ lapply (le_plus_to_minus_r … Hde12) -Hde12 <plus_minus // #Hde12
+ lapply (le_plus_to_minus … Hd21) -Hd21 #Hd21 /3 width=5/
+ | -Hd21 normalize in Hde12;
+ lapply (lt_to_le_to_lt 0 … Hde12) // #He2
+ lapply (le_plus_to_minus_r … Hde12) -Hde12 /3 width=5/
+ ]
+]
+qed.
+
lemma ltpss_weak_all: ∀L1,L2,d,e. L1 [d, e] ▶* L2 → L1 [0, |L2|] ▶* L2.
#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
// /3 width=2/ /3 width=3/
include "basic_2/unfold/ltpss.ma".
-(* DELIFT ON LOCAL ENVIRONMENTS ********************************************)
+(* LOCAL ENVIRONMENT THINNING ***********************************************)
definition thin: nat → nat → relation lenv ≝
λd,e,L1,L2. ∃∃L. L1 [d, e] ▶* L & ⇩[d, e] L ≡ L2.
-interpretation "delift (local environment)"
+interpretation "thinning (local environment)"
'TSubst L1 d e L2 = (thin d e L1 L2).
(* Basic properties *********************************************************)
+
+lemma ldrop_thin: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → L1 [d, e] ≡ L2.
+/2 width=3/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma thin_inv_thin1: ∀I,K1,V1,L2,e. K1. ⓑ{I} V1 [0, e] ≡ L2 → 0 < e →
+ K1 [0, e - 1] ≡ L2.
+#I #K1 #V1 #L2 #e * #X #HK1 #HL2 #e
+elim (ltpss_inv_tpss21 … HK1 ?) -HK1 // #K #V #HK1 #_ #H destruct
+lapply (ldrop_inv_ldrop1 … HL2 ?) -HL2 // /2 width=3/
+qed-.
(* *)
(**************************************************************************)
-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/delift_tpss.ma".
+include "basic_2/unfold/delift_ltpss.ma".
include "basic_2/unfold/thin.ma".
(* DELIFT ON LOCAL ENVIRONMENTS *********************************************)
-(* Properties on deflift on terms *******************************************)
+(* Properties on inverse term relocation ************************************)
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.
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/
-*)
+lemma thin_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 [d, e - ee] ▶* T2 &
+ L ⊢ U2 [dd, ee] ≡ T2.
+#L #U1 #U2 #d #e #HU12 #T1 #dd #ee #HUT1 #K * #Y #HLY #HYK #Hdd #Hddee
+lapply (delift_ltpss_conf_eq … HUT1 … HLY) -HUT1 #HUT1
+elim (ltpss_tpss_conf … HU12 … HLY) -HU12 #U #HU1 #HU2
+elim (delift_tpss_conf_be … HU1 … HUT1 … HYK ? ?) -HU1 -HUT1 // -Hdd -Hddee #T #HT1 #HUT
+lapply (tpss_delift_trans_eq … HU2 … HUT) -U #HU2T
+lapply (ltpss_delift_trans_eq … HLY … HU2T) -Y /2 width=3/
+qed.
+
+lemma thin_delift_tps_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 [d, e - ee] ▶* T2 &
+ L ⊢ U2 [dd, ee] ≡ T2.
+/3 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/unfold/ltpss_ldrop.ma".
+include "basic_2/unfold/thin.ma".
+
+(* LOCAL ENVIRONMENT THINNING ***********************************************)
+
+(* Properties on local environment slicing **********************************)
+
+lemma thin_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≡ L1 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
+ d1 + e1 ≤ e2 → ⇩[0, e2 - e1] L1 ≡ L2.
+#L0 #L1 #d1 #e1 * /3 width=8 by ltpss_ldrop_conf_ge, ldrop_conf_ge/
+qed.
+
+lemma thin_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≡ L1 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
+ ∃∃L. L2 [0, d1 + e1 - e2] ≡ L & ⇩[0, d1] L1 ≡ L.
+#L0 #L1 #d1 #e1 * #L #HL0 #HL1 #L2 #e2 #HL02 #Hd1e2 #He2de1
+elim (ltpss_ldrop_conf_be … HL0 … HL02 ? ?) -L0 // #L0 #HL20 #HL0
+elim (ldrop_conf_be … HL1 … HL0 ? ?) -L // -Hd1e2 -He2de1 /3 width=3/
+qed.
+
+lemma thin_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ≡ L1 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
+ ∃∃L. L2 [d1 - e2, e1] ≡ L & ⇩[0, e2] L1 ≡ L.
+#L0 #L1 #d1 #e1 * #L #HL0 #HL1 #L2 #e2 #HL02 #He2d1
+elim (ltpss_ldrop_conf_le … HL0 … HL02 ?) -L0 // #L0 #HL20 #HL0
+elim (ldrop_conf_le … HL1 … HL0 ?) -L // -He2d1 /3 width=3/
+qed.
+
+lemma thin_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≡ L0 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
+ d1 ≤ e2 → ⇩[0, e1 + e2] L1 ≡ L2.
+#L1 #L0 #d1 #e1 * #L #HL1 #HL0 #L2 #e2 #HL02 #Hd1e2
+lapply (ldrop_trans_ge … HL0 … HL02 ?) -L0 // #HL2
+lapply (ltpss_ldrop_trans_ge … HL1 … HL2 ?) -L // /2 width=1/
+qed.
+
+lemma thin_ldrop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ≡ L0 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
+ ∃∃L. L [d1 - e2, e1] ≡ L2 & ⇩[0, e2] L1 ≡ L.
+#L1 #L0 #d1 #e1 * #L #HL1 #HL0 #L2 #e2 #HL02 #He2d1
+elim (ldrop_trans_le … HL0 … HL02 He2d1) -L0 #L0 #HL0 #HL02
+elim (ltpss_ldrop_trans_le … HL1 … HL0 He2d1) -L -He2d1 /3 width=3/
+qed.
projects / helm.git / commitdiff