From fc5a0d62ece398d8547dda0f429b9f1e24bca306 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 3 May 2012 15:27:32 +0000 Subject: [PATCH] - more properties on lifting, slicing, delifting and thinning --- .../basic_2/substitution/ldrop.ma | 6 + .../basic_2/substitution/ldrop_ldrop.ma | 110 ++++++++++++------ .../lambda_delta/basic_2/unfold/delift.ma | 8 +- .../lambda_delta/basic_2/unfold/delift_alt.ma | 6 +- .../basic_2/unfold/delift_delift.ma | 2 +- .../basic_2/unfold/delift_lift.ma | 36 +++++- .../basic_2/unfold/delift_ltpss.ma | 33 ++++++ .../basic_2/unfold/delift_tpss.ma | 58 +++++++++ .../lambda_delta/basic_2/unfold/ltpss.ma | 19 +++ .../lambda_delta/basic_2/unfold/thin.ma | 16 ++- .../basic_2/unfold/thin_delift.ma | 42 +++---- .../lambda_delta/basic_2/unfold/thin_ldrop.ma | 59 ++++++++++ 12 files changed, 328 insertions(+), 67 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unfold/delift_tpss.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unfold/thin_ldrop.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma index 73a9ff92e..7ac2c8657 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma @@ -76,6 +76,12 @@ lemma ldrop_inv_O1: ∀e,K,I,V,L2. ⇩[0, e] K. ⓑ{I} V ≡ L2 → (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. diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_ldrop.ma index 17b40f947..b7862fcbf 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_ldrop.ma @@ -55,28 +55,67 @@ theorem ldrop_conf_ge: ∀d1,e1,L,L1. ⇩[d1, e1] L ≡ L1 → ] 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 plus_plus_comm_23 #_ #_ #IHLK0 #L2 #e2 #H #Hd1e2 #He2de1 + elim (le_inv_plus_l … Hd1e2) #_ #He2 + 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 → @@ -99,28 +138,23 @@ theorem ldrop_trans_le: ∀d1,e1,L1,L. ⇩[d1, e1] L1 ≡ L → ] 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. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma index 7620ae092..7fbf16fbd 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma @@ -14,16 +14,20 @@ 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. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma index c5fdcaadd..a53fd9f5d 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma @@ -14,9 +14,9 @@ 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) @@ -33,7 +33,7 @@ inductive delifta: nat → nat → lenv → relation term ≝ 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 *********************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma index 9ae9831c8..a23501653 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma @@ -15,7 +15,7 @@ include "basic_2/unfold/tpss_tpss.ma". include "basic_2/unfold/delift.ma". -(* DELIFT ON TERMS **********************************************************) +(* INVERSE TERM RELOCATION *************************************************) (* Main properties **********************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma index 8266a9ae3..a7f31fb80 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma @@ -15,7 +15,7 @@ include "basic_2/unfold/tpss_lift.ma". include "basic_2/unfold/delift.ma". -(* DELIFT ON TERMS **********************************************************) +(* INVERSE TERM RELOCATION *************************************************) (* Advanced properties ******************************************************) @@ -81,3 +81,37 @@ elim (lt_or_ge i d) #Hdi ] ] 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. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma new file mode 100644 index 000000000..7bcab46fa --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||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. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_tpss.ma new file mode 100644 index 000000000..b7bc126df --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_tpss.ma @@ -0,0 +1,58 @@ +(**************************************************************************) +(* ___ *) +(* ||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. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma index cc54ed5c0..6b44d74f6 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma @@ -73,6 +73,25 @@ lemma ltpss_refl: ∀L,d,e. L [d, e] ▶* L. #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 (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. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_ldrop.ma new file mode 100644 index 000000000..ef0f9f8c9 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_ldrop.ma @@ -0,0 +1,59 @@ +(**************************************************************************) +(* ___ *) +(* ||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. -- 2.39.2