From 38a7664fd355705596cb63cac87779688790fcb1 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 28 Sep 2012 17:07:46 +0000 Subject: [PATCH] - partial commit (unfold component only) we introduced the transitive closure of ltpss, which we now use in the definition of thin --- .../basic_2/etc/ltpsss/ltpsss.etc | 83 ------ .../basic_2/etc/ltpsss/ltpsss_ldrop.etc | 74 ----- .../basic_2/etc/ltpsss/ltpsss_ltpsss.etc | 153 ----------- .../basic_2/etc/ltpsss/ltpsss_tps.etc | 36 --- .../basic_2/etc/ltpsss/ltpsss_tpss.etc | 74 ----- .../basic_2/etc/ltpsss/notation.etc | 21 -- .../contribs/lambda_delta/basic_2/notation.ma | 8 + .../basic_2/unfold/delift_ltpss.ma | 16 +- .../basic_2/unfold/{ltpss.ma => ltpss_dx.ma} | 202 +++++++------- .../{ltpss_ldrop.ma => ltpss_dx_ldrop.ma} | 40 +-- .../{ltpss_ltpss.ma => ltpss_dx_ltpss_dx.ma} | 79 +++--- .../unfold/{ltpss_tps.ma => ltpss_dx_tps.ma} | 24 +- .../{ltpss_tpss.ma => ltpss_dx_tpss.ma} | 56 ++-- .../lambda_delta/basic_2/unfold/ltpss_sn.ma | 254 ++++++++++++++++++ .../basic_2/unfold/ltpss_sn_alt.ma | 156 +++++++++++ .../basic_2/unfold/ltpss_sn_ldrop.ma | 131 +++++++++ .../basic_2/unfold/ltpss_sn_ltpss_sn.ma | 83 ++++++ .../basic_2/unfold/ltpss_sn_tps.ma | 47 ++++ .../basic_2/unfold/ltpss_sn_tpss.ma | 102 +++++++ .../lambda_delta/basic_2/unfold/thin.ma | 6 +- .../basic_2/unfold/thin_delift.ma | 46 ++-- .../lambda_delta/basic_2/unfold/thin_ldrop.ma | 12 +- .../lambda_delta/basic_2/unfold/tpss.ma | 4 + 23 files changed, 1009 insertions(+), 698 deletions(-) delete mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss.etc delete mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_ldrop.etc delete mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_ltpsss.etc delete mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_tps.etc delete mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_tpss.etc delete mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/notation.etc rename matita/matita/contribs/lambda_delta/basic_2/unfold/{ltpss.ma => ltpss_dx.ma} (53%) rename matita/matita/contribs/lambda_delta/basic_2/unfold/{ltpss_ldrop.ma => ltpss_dx_ldrop.ma} (76%) rename matita/matita/contribs/lambda_delta/basic_2/unfold/{ltpss_ltpss.ma => ltpss_dx_ltpss_dx.ma} (63%) rename matita/matita/contribs/lambda_delta/basic_2/unfold/{ltpss_tps.ma => ltpss_dx_tps.ma} (68%) rename matita/matita/contribs/lambda_delta/basic_2/unfold/{ltpss_tpss.ma => ltpss_dx_tpss.ma} (64%) create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_alt.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_ldrop.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_ltpss_sn.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_tps.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_tpss.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss.etc deleted file mode 100644 index 58fb3e20b..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss.etc +++ /dev/null @@ -1,83 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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". - -(* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************) - -definition ltpsss: nat → nat → relation lenv ≝ - λd,e. TC … (ltpss d e). - -interpretation "repeated partial unfold (local environment)" - 'PSubstStars L1 d e L2 = (ltpsss d e L1 L2). - -(* Basic eliminators ********************************************************) - -lemma ltpsss_ind: ∀d,e,L1. ∀R:predicate lenv. R L1 → - (∀L,L2. L1 [d, e] ▶** L → L [d, e] ▶* L2 → R L → R L2) → - ∀L2. L1 [d, e] ▶** L2 → R L2. -#d #e #L1 #R #HL1 #IHL1 #L2 #HL12 @(TC_star_ind … HL1 IHL1 … HL12) // -qed-. - -lemma ltpsss_ind_dx: ∀d,e,L2. ∀R:predicate lenv. R L2 → - (∀L1,L. L1 [d, e] ▶* L → L [d, e] ▶** L2 → R L → R L1) → - ∀L1. L1 [d, e] ▶** L2 → R L1. -#d #e #L2 #R #HL2 #IHL2 #L1 #HL12 @(TC_star_ind_dx … HL2 IHL2 … HL12) // -qed-. - -(* Basic properties *********************************************************) - -lemma ltpsss_strap1: ∀L1,L,L2,d,e. - L1 [d, e] ▶** L → L [d, e] ▶* L2 → L1 [d, e] ▶** L2. -/2 width=3/ qed. - -lemma ltpsss_strap2: ∀L1,L,L2,d,e. - L1 [d, e] ▶* L → L [d, e] ▶** L2 → L1 [d, e] ▶** L2. -/2 width=3/ qed. - -lemma ltpsss_refl: ∀L,d,e. L [d, e] ▶** L. -/2 width=1/ qed. - -lemma ltpsss_weak_all: ∀L1,L2,d,e. L1 [d, e] ▶** L2 → L1 [0, |L2|] ▶** L2. -#L1 #L2 #d #e #H @(ltpsss_ind … H) -L2 // -#L #L2 #_ #HL2 ->(ltpss_fwd_length … HL2) /3 width=5/ -qed. - -(* Basic forward lemmas *****************************************************) - -lemma ltpsss_fwd_length: ∀L1,L2,d,e. L1 [d, e] ▶** L2 → |L1| = |L2|. -#L1 #L2 #d #e #H @(ltpsss_ind … H) -L2 // -#L #L2 #_ #HL2 #IHL12 >IHL12 -IHL12 -/2 width=3 by ltpss_fwd_length/ -qed-. - -(* Basic inversion lemmas ***************************************************) - -lemma ltpsss_inv_refl_O2: ∀d,L1,L2. L1 [d, 0] ▶** L2 → L1 = L2. -#d #L1 #L2 #H @(ltpsss_ind … H) -L2 // -#L #L2 #_ #HL2 #IHL <(ltpss_inv_refl_O2 … HL2) -HL2 // -qed-. - -lemma ltpsss_inv_atom1: ∀d,e,L2. ⋆ [d, e] ▶** L2 → L2 = ⋆. -#d #e #L2 #H @(ltpsss_ind … H) -L2 // -#L #L2 #_ #HL2 #IHL destruct ->(ltpss_inv_atom1 … HL2) -HL2 // -qed-. - -lemma ltpsss_inv_atom2: ∀d,e,L1. L1 [d, e] ▶** ⋆ → L1 = ⋆. -#d #e #L1 #H @(ltpsss_ind_dx … H) -L1 // -#L1 #L #HL1 #_ #IHL2 destruct ->(ltpss_inv_atom2 … HL1) -HL1 // -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_ldrop.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_ldrop.etc deleted file mode 100644 index e4923f9be..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_ldrop.etc +++ /dev/null @@ -1,74 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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_ldrop.ma". -include "basic_2/unfold/ltpsss.ma". - -(* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************) - -lemma ltpsss_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ▶** L1 → - ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → - d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2. -#L0 #L1 #d1 #e1 #H @(ltpsss_ind … H) -L1 // /3 width=6/ -qed. - -lemma ltpsss_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 → - ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → - d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2. -#L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0 // /3 width=6/ -qed. - -lemma ltpsss_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, e2] L1 ≡ L. -#L0 #L1 #d1 #e1 #H @(ltpsss_ind … H) -L1 -[ /2 width=3/ -| #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1 - elim (IHL … HL02 Hd1e2 He2de1) -L0 #L0 #HL20 #HL0 - elim (ltpss_ldrop_conf_be … HL1 … HL0 Hd1e2 He2de1) -L /3 width=3/ -] -qed. - -lemma ltpsss_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 → - ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → - ∃∃L. L [0, d1 + e1 - e2] ▶** L2 & ⇩[0, e2] L1 ≡ L. -#L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0 -[ /2 width=3/ -| #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1 - elim (ltpss_ldrop_trans_be … HL0 … HL02 Hd1e2 He2de1) -L0 #L0 #HL02 #HL0 - elim (IHL … HL0 Hd1e2 He2de1) -L /3 width=3/ -] -qed. - -lemma ltpsss_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 #H @(ltpsss_ind … H) -L1 -[ /2 width=3/ -| #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #He2d1 - elim (IHL … HL02 He2d1) -L0 #L0 #HL20 #HL0 - elim (ltpss_ldrop_conf_le … HL1 … HL0 He2d1) -L /3 width=3/ -] -qed. - -lemma ltpsss_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 #H @(ltpsss_ind … H) -L0 -[ /2 width=3/ -| #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #He2d1 - elim (ltpss_ldrop_trans_le … HL0 … HL02 He2d1) -L0 #L0 #HL02 #HL0 - elim (IHL … HL0 He2d1) -L /3 width=3/ -] -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_ltpsss.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_ltpsss.etc deleted file mode 100644 index 36a036727..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_ltpsss.etc +++ /dev/null @@ -1,153 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/ltpsss_tpss.ma". - -(* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************) - -(* Advanced properties ******************************************************) - -lemma ltpsss_strip: ∀L0,L1,d1,e1. L0 [d1, e1] ▶** L1 → - ∀L2,d2,e2. L0 [d2, e2] ▶* L2 → - ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶** L. -/3 width=3/ qed. - -lemma ltpsss_tpss_trans_eq: ∀L0,L1,d,e. L0 [d, e] ▶** L1 → - ∀T2,U2. L1 ⊢ T2 [d, e] ▶* U2 → L0 ⊢ T2 [d, e] ▶* U2. -#L0 #L1 #d #e #H @(ltpsss_ind … H) -L1 -[ /2 width=1/ -| #L #L1 #_ #HL1 #IHL #T2 #U2 #HTU2 - lapply (ltpss_tpss_trans_eq … HTU2 … HL1) -HL1 -HTU2 /2 width=1/ -] -qed. - -lemma ltpsss_tps_trans_eq: ∀L0,L1,d,e. L0 [d, e] ▶** L1 → - ∀T2,U2. L1 ⊢ T2 [d, e] ▶ U2 → L0 ⊢ T2 [d, e] ▶* U2. -/3 width=3/ qed. - -lemma ltpsss_tpss_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶* T2 → - ∀L2,ds,es. L1 [ds, es] ▶** L2 → - ∃∃T. L2 ⊢ T1 [d, e] ▶* T & L1 ⊢ T2 [ds, es] ▶* T. -#L1 #T1 #T2 #d #e #HT12 #L2 #ds #es #H @(ltpsss_ind … H) -L2 -[ /2 width=3/ -| -HT12 #L #L2 #HL1 #HL2 * #T #HT1 #HT2 - lapply (ltpsss_strap1 … HL1 HL2) -HL1 #HL12 - elim (ltpss_tpss_conf … HT1 … HL2) -L #T0 #HT10 #HT0 - lapply (ltpsss_tpss_trans_eq … HL12 … HT0) -HL12 -HT0 #HT0 - lapply (tpss_trans_eq … HT2 HT0) -T /2 width=3/ -] -qed. - -lemma ltpsss_tps_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶ T2 → - ∀L2,ds,es. L1 [ds, es] ▶** L2 → - ∃∃T. L2 ⊢ T1 [d, e] ▶* T & L1 ⊢ T2 [ds, es] ▶* T. -/3 width=1/ qed. - -(* Advanced forward lemmas **************************************************) - -lemma ltpsss_fwd_tpss21: ∀e,K1,I,V1,L2. 0 < e → K1. ⓑ{I} V1 [0, e] ▶** L2 → - ∃∃K2,V2. K1 [0, e - 1] ▶** K2 & - K1 ⊢ V1 [0, e - 1] ▶* V2 & - L2 = K2. ⓑ{I} V2. -#e #K1 #I #V1 #L2 #He #H @(ltpsss_ind … H) -L2 -[ /2 width=5/ -| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct - elim (ltpss_inv_tpss21 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H - lapply (ltpss_tpss_trans_eq … HV2 … HK2) -HV2 #HV2 - lapply (ltpsss_tpss_trans_eq … HK1 … HV2) -HV2 /3 width=5/ -] -qed-. - -lemma ltpsss_fwd_tpss11: ∀d,e,I,K1,V1,L2. 0 < d → K1. ⓑ{I} V1 [d, e] ▶** L2 → - ∃∃K2,V2. K1 [d - 1, e] ▶** K2 & - K1 ⊢ V1 [d - 1, e] ▶* V2 & - L2 = K2. ⓑ{I} V2. -#d #e #K1 #I #V1 #L2 #Hd #H @(ltpsss_ind … H) -L2 -[ /2 width=5/ -| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct - elim (ltpss_inv_tpss11 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H - lapply (ltpss_tpss_trans_eq … HV2 … HK2) -HV2 #HV2 - lapply (ltpsss_tpss_trans_eq … HK1 … HV2) -HV2 /3 width=5/ -] -qed-. - -lemma ltpsss_fwd_tpss22: ∀I,L1,K2,V2,e. L1 [0, e] ▶** K2. ⓑ{I} V2 → 0 < e → - ∃∃K1,V1. K1 [0, e - 1] ▶** K2 & - K1 ⊢ V1 [0, e - 1] ▶* V2 & - L1 = K1. ⓑ{I} V1. -#I #L1 #K2 #V2 #e #H #He @(ltpsss_ind_dx … H) -L1 -[ /2 width=5/ -| #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct - elim (ltpss_inv_tpss22 … HL1 ?) -HL1 // #K1 #V1 #HK1 #HV1 #H destruct - lapply (tpss_trans_eq … HV1 HV2) -V #HV12 - lapply (ltpss_tpss_trans_eq … HV12 … HK1) -HV12 /3 width=5/ -] -qed-. - -lemma ltpsss_inv_tpss12: ∀I,L1,K2,V2,d,e. L1 [d, e] ▶** K2. ⓑ{I} V2 → 0 < d → - ∃∃K1,V1. K1 [d - 1, e] ▶** K2 & - K1 ⊢ V1 [d - 1, e] ▶* V2 & - L1 = K1. ⓑ{I} V1. -#I #L1 #K2 #V2 #d #e #H #Hd @(ltpsss_ind_dx … H) -L1 -[ /2 width=5/ -| #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct - elim (ltpss_inv_tpss12 … HL1 ?) -HL1 // #K1 #V1 #HK1 #HV1 #H destruct - lapply (tpss_trans_eq … HV1 HV2) -V #HV12 - lapply (ltpss_tpss_trans_eq … HV12 … HK1) -HV12 /3 width=5/ -] -qed-. - -(* Main properties **********************************************************) - -theorem ltpsss_conf: ∀L0,L1,d1,e1. L0 [d1, e1] ▶** L1 → - ∀L2,d2,e2. L0 [d2, e2] ▶** L2 → - ∃∃L. L1 [d2, e2] ▶** L & L2 [d1, e1] ▶** L. -/3 width=3/ qed. - -theorem ltpsss_trans_eq: ∀L1,L,L2,d,e. - L1 [d, e] ▶** L → L [d, e] ▶** L2 → L1 [d, e] ▶** L2. -/2 width=3/ qed. - -lemma ltpsss_tpss2: ∀L1,L2,I,V1,V2,e. - L1 [0, e] ▶** L2 → L2 ⊢ V1 [0, e] ▶* V2 → - L1. ⓑ{I} V1 [0, e + 1] ▶** L2. ⓑ{I} V2. -#L1 #L2 #I #V1 #V2 #e #HL12 #H @(tpss_ind … H) -V2 -[ /2 width=1/ -| #V #V2 #_ #HV2 #IHV @(ltpsss_trans_eq … IHV) /2 width=1/ -] -qed. - -lemma ltpsss_tpss2_lt: ∀L1,L2,I,V1,V2,e. - L1 [0, e - 1] ▶** L2 → L2 ⊢ V1 [0, e - 1] ▶* V2 → - 0 < e → L1. ⓑ{I} V1 [0, e] ▶** L2. ⓑ{I} V2. -#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He ->(plus_minus_m_m e 1) // /2 width=1/ -qed. - -lemma ltpsss_tpss1: ∀L1,L2,I,V1,V2,d,e. - L1 [d, e] ▶** L2 → L2 ⊢ V1 [d, e] ▶* V2 → - L1. ⓑ{I} V1 [d + 1, e] ▶** L2. ⓑ{I} V2. -#L1 #L2 #I #V1 #V2 #d #e #HL12 #H @(tpss_ind … H) -V2 -[ /2 width=1/ -| #V #V2 #_ #HV2 #IHV @(ltpsss_trans_eq … IHV) /2 width=1/ -] -qed. - -lemma ltpsss_tpss1_lt: ∀L1,L2,I,V1,V2,d,e. - L1 [d - 1, e] ▶** L2 → L2 ⊢ V1 [d - 1, e] ▶* V2 → - 0 < d → L1. ⓑ{I} V1 [d, e] ▶** L2. ⓑ{I} V2. -#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd ->(plus_minus_m_m d 1) // /2 width=1/ -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_tps.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_tps.etc deleted file mode 100644 index 3f0e25ae9..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_tps.etc +++ /dev/null @@ -1,36 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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_tps.ma". -include "basic_2/unfold/ltpsss.ma". - -(* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************) - -(* Properties concerning partial substitution on terms **********************) - -lemma ltpsss_tps_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 → - ∀T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 → - d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ▶ U2. -#L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0 // -#L #L0 #_ #HL0 #IHL #T2 #U2 #d2 #e2 #HTU2 #Hde1d2 -lapply (ltpss_tps_trans_ge … HTU2 … HL0 ?) -HL0 -HTU2 // /2 width=1/ -qed. - -lemma ltpsss_tps_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 → - L0 ⊢ T2 [d2, e2] ▶ U2 → L0 [d1, e1] ▶** L1 → - L1 ⊢ T2 [d2, e2] ▶ U2. -#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #H @(ltpsss_ind … H) -L1 // --HTU2 #L #L1 #_ #HL1 #IHL -lapply (ltpss_tps_conf_ge … IHL … HL1 ?) -HL1 -IHL // -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_tpss.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_tpss.etc deleted file mode 100644 index 251a1a186..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_tpss.etc +++ /dev/null @@ -1,74 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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_tpss.ma". -include "basic_2/unfold/ltpsss.ma". - -(* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************) - -(* Properties concerning partial substitution on terms **********************) - -lemma ltpsss_tps2: ∀L1,L2,I,e. - L1 [0, e] ▶** L2 → ∀V1,V2. L2 ⊢ V1 [0, e] ▶ V2 → - L1. ⓑ{I} V1 [0, e + 1] ▶** L2. ⓑ{I} V2. -#L1 #L2 #I #e #H @(ltpsss_ind … H) -L2 -[ /3 width=1/ -| #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12 - elim (ltpss_tps_trans … HV12 … HL2) -HV12 #V #HV1 #HV2 - lapply (IHL … HV1) -IHL -HV1 /3 width=5/ -] -qed. - -lemma ltpsss_tps2_lt: ∀L1,L2,I,V1,V2,e. - L1 [0, e - 1] ▶** L2 → L2 ⊢ V1 [0, e - 1] ▶ V2 → - 0 < e → L1. ⓑ{I} V1 [0, e] ▶** L2. ⓑ{I} V2. -#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He ->(plus_minus_m_m e 1) // /2 width=1/ -qed. - -lemma ltpsss_tps1: ∀L1,L2,I,d,e. L1 [d, e] ▶** L2 → - ∀V1,V2. L2 ⊢ V1 [d, e] ▶ V2 → - L1. ⓑ{I} V1 [d + 1, e] ▶** L2. ⓑ{I} V2. -#L1 #L2 #I #d #e #H @(ltpsss_ind … H) -L2 -[ /3 width=1/ -| #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12 - elim (ltpss_tps_trans … HV12 … HL2) -HV12 #V #HV1 #HV2 - lapply (IHL … HV1) -IHL -HV1 /3 width=5/ -] -qed. - -lemma ltpsss_tps1_lt: ∀L1,L2,I,V1,V2,d,e. - L1 [d - 1, e] ▶** L2 → L2 ⊢ V1 [d - 1, e] ▶ V2 → - 0 < d → L1. ⓑ{I} V1 [d, e] ▶** L2. ⓑ{I} V2. -#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd ->(plus_minus_m_m d 1) // /2 width=1/ -qed. - -(* Properties concerning partial unfold on terms ****************************) - -lemma ltpsss_tpss_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 → - L0 ⊢ T2 [d2, e2] ▶* U2 → L0 [d1, e1] ▶** L1 → - L1 ⊢ T2 [d2, e2] ▶* U2. -#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #H @(ltpsss_ind … H) -L1 // --HTU2 #L #L1 #_ #HL1 #IHL -lapply (ltpss_tpss_conf_ge … IHL … HL1 ?) -HL1 -IHL // -qed. - -lemma ltpsss_tpss_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 → - ∀T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶* U2 → - d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ▶* U2. -#L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0 // -#L #L0 #_ #HL0 #IHL #T2 #U2 #d2 #e2 #HTU2 #Hde1d2 -lapply (ltpss_tpss_trans_ge … HTU2 … HL0 ?) -HL0 -HTU2 // /2 width=1/ -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/notation.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/notation.etc deleted file mode 100644 index 6846b7670..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/notation.etc +++ /dev/null @@ -1,21 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -(* Unfold *******************************************************************) - -notation "hvbox( T1 break [ d , break e ] ▶** break T2 )" - non associative with precedence 45 - for @{ 'PSubstStars $T1 $d $e $T2 }. diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma index 1b64f3c90..ab02943a8 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma @@ -200,6 +200,14 @@ notation "hvbox( L ⊢ break term 46 T1 break ▶ ▶ * [ d , break e ] break te non associative with precedence 45 for @{ 'PSubstStarAlt $L $T1 $d $e $T2 }. +notation "hvbox( T1 break ⊢ ▶ * [ d , break e ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'PSubstStarSn $T1 $d $e $T2 }. + +notation "hvbox( T1 break ⊢ ▶ ▶ * [ d , break e ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'PSubstStarSnAlt $T1 $d $e $T2 }. + notation "hvbox( ▼ * [ d , break e ] break term 46 T1 ≡ break term 46 T2 )" non associative with precedence 45 for @{ 'TSubst $T1 $d $e $T2 }. 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 index ba4cae69d..a0ac3cf47 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma @@ -12,22 +12,22 @@ (* *) (**************************************************************************) -include "basic_2/unfold/ltpss_ltpss.ma". +include "basic_2/unfold/ltpss_sn_alt.ma". include "basic_2/unfold/delift.ma". (* INVERSE BASIC TERM RELOCATION *******************************************) -(* Properties on partial unfold on local environments ***********************) +(* Properties on sn partial unfold on local environments ********************) -lemma delift_ltpss_conf_eq: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → - ∀K. L ▶* [d, e] K → K ⊢ ▼*[d, e] T1 ≡ T2. +lemma delift_ltpss_sn_conf_eq: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → + ∀K. L ⊢ ▶* [d, e] K → K ⊢ ▼*[d, e] T1 ≡ T2. #L #T1 #T2 #d #e * #T #HT1 #HT2 #K #HLK -elim (ltpss_tpss_conf … HT1 … HLK) -L #T0 #HT10 #HT0 +elim (ltpss_sn_tpss_conf … HT1 … HLK) -HT1 -HLK #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 ⊢ ▼*[d, e] T1 ≡ T2 → L ⊢ ▼*[d, e] T1 ≡ T2. +lemma ltpss_sn_delift_trans_eq: ∀L,K,d,e. L ⊢ ▶* [d, e] K → + ∀T1,T2. K ⊢ ▼*[d, e] T1 ≡ T2 → L ⊢ ▼*[d, e] T1 ≡ T2. #L #K #d #e #HLK #T1 #T2 * #T #HT1 #HT2 -lapply (ltpss_tpss_trans_eq … HT1 … HLK) -K /2 width=3/ +lapply (ltpss_sn_tpss_trans_eq … HT1 … HLK) -K /2 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_dx.ma similarity index 53% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma rename to matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx.ma index dfd1a19f6..ad0c002b4 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx.ma @@ -14,26 +14,26 @@ include "basic_2/unfold/tpss.ma". -(* PARALLEL UNFOLD ON LOCAL ENVIRONMENTS ************************************) +(* DX PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************) (* Basic_1: includes: csubst1_bind *) -inductive ltpss: nat → nat → relation lenv ≝ -| ltpss_atom : ∀d,e. ltpss d e (⋆) (⋆) -| ltpss_pair : ∀L,I,V. ltpss 0 0 (L. ⓑ{I} V) (L. ⓑ{I} V) -| ltpss_tpss2: ∀L1,L2,I,V1,V2,e. - ltpss 0 e L1 L2 → L2 ⊢ V1 ▶* [0, e] V2 → - ltpss 0 (e + 1) (L1. ⓑ{I} V1) (L2. ⓑ{I} V2) -| ltpss_tpss1: ∀L1,L2,I,V1,V2,d,e. - ltpss d e L1 L2 → L2 ⊢ V1 ▶* [d, e] V2 → - ltpss (d + 1) e (L1. ⓑ{I} V1) (L2. ⓑ{I} V2) +inductive ltpss_dx: nat → nat → relation lenv ≝ +| ltpss_dx_atom : ∀d,e. ltpss_dx d e (⋆) (⋆) +| ltpss_dx_pair : ∀L,I,V. ltpss_dx 0 0 (L. ⓑ{I} V) (L. ⓑ{I} V) +| ltpss_dx_tpss2: ∀L1,L2,I,V1,V2,e. + ltpss_dx 0 e L1 L2 → L2 ⊢ V1 ▶* [0, e] V2 → + ltpss_dx 0 (e + 1) (L1. ⓑ{I} V1) (L2. ⓑ{I} V2) +| ltpss_dx_tpss1: ∀L1,L2,I,V1,V2,d,e. + ltpss_dx d e L1 L2 → L2 ⊢ V1 ▶* [d, e] V2 → + ltpss_dx (d + 1) e (L1. ⓑ{I} V1) (L2. ⓑ{I} V2) . -interpretation "parallel unfold (local environment)" - 'PSubstStar L1 d e L2 = (ltpss d e L1 L2). +interpretation "parallel unfold (local environment, dx variant)" + 'PSubstStar L1 d e L2 = (ltpss_dx d e L1 L2). (* Basic inversion lemmas ***************************************************) -fact ltpss_inv_refl_O2_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → e = 0 → L1 = L2. +fact ltpss_dx_inv_refl_O2_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → e = 0 → L1 = L2. #d #e #L1 #L2 #H elim H -d -e -L1 -L2 // [ #L1 #L2 #I #V1 #V2 #e #_ #_ #_ >commutative_plus normalize #H destruct | #L1 #L2 #I #V1 #V2 #d #e #_ #HV12 #IHL12 #He destruct @@ -41,11 +41,11 @@ fact ltpss_inv_refl_O2_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → e = 0 → L1 = L ] qed. -lemma ltpss_inv_refl_O2: ∀d,L1,L2. L1 ▶* [d, 0] L2 → L1 = L2. +lemma ltpss_dx_inv_refl_O2: ∀d,L1,L2. L1 ▶* [d, 0] L2 → L1 = L2. /2 width=4/ qed-. -fact ltpss_inv_atom1_aux: ∀d,e,L1,L2. - L1 ▶* [d, e] L2 → L1 = ⋆ → L2 = ⋆. +fact ltpss_dx_inv_atom1_aux: ∀d,e,L1,L2. + L1 ▶* [d, e] L2 → L1 = ⋆ → L2 = ⋆. #d #e #L1 #L2 * -d -e -L1 -L2 [ // | #L #I #V #H destruct @@ -54,14 +54,14 @@ fact ltpss_inv_atom1_aux: ∀d,e,L1,L2. ] qed. -lemma ltpss_inv_atom1: ∀d,e,L2. ⋆ ▶* [d, e] L2 → L2 = ⋆. +lemma ltpss_dx_inv_atom1: ∀d,e,L2. ⋆ ▶* [d, e] L2 → L2 = ⋆. /2 width=5/ qed-. -fact ltpss_inv_tpss21_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → d = 0 → 0 < e → - ∀K1,I,V1. L1 = K1. ⓑ{I} V1 → - ∃∃K2,V2. K1 ▶* [0, e - 1] K2 & - K2 ⊢ V1 ▶* [0, e - 1] V2 & - L2 = K2. ⓑ{I} V2. +fact ltpss_dx_inv_tpss21_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → d = 0 → 0 < e → + ∀K1,I,V1. L1 = K1. ⓑ{I} V1 → + ∃∃K2,V2. K1 ▶* [0, e - 1] K2 & + K2 ⊢ V1 ▶* [0, e - 1] V2 & + L2 = K2. ⓑ{I} V2. #d #e #L1 #L2 * -d -e -L1 -L2 [ #d #e #_ #_ #K1 #I #V1 #H destruct | #L1 #I #V #_ #H elim (lt_refl_false … H) @@ -70,17 +70,17 @@ fact ltpss_inv_tpss21_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → d = 0 → 0 < e ] qed. -lemma ltpss_inv_tpss21: ∀e,K1,I,V1,L2. K1. ⓑ{I} V1 ▶* [0, e] L2 → 0 < e → - ∃∃K2,V2. K1 ▶* [0, e - 1] K2 & - K2 ⊢ V1 ▶* [0, e - 1] V2 & - L2 = K2. ⓑ{I} V2. +lemma ltpss_dx_inv_tpss21: ∀e,K1,I,V1,L2. K1. ⓑ{I} V1 ▶* [0, e] L2 → 0 < e → + ∃∃K2,V2. K1 ▶* [0, e - 1] K2 & + K2 ⊢ V1 ▶* [0, e - 1] V2 & + L2 = K2. ⓑ{I} V2. /2 width=5/ qed-. -fact ltpss_inv_tpss11_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → 0 < d → - ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → - ∃∃K2,V2. K1 ▶* [d - 1, e] K2 & - K2 ⊢ V1 ▶* [d - 1, e] V2 & - L2 = K2. ⓑ{I} V2. +fact ltpss_dx_inv_tpss11_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → 0 < d → + ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → + ∃∃K2,V2. K1 ▶* [d - 1, e] K2 & + K2 ⊢ V1 ▶* [d - 1, e] V2 & + L2 = K2. ⓑ{I} V2. #d #e #L1 #L2 * -d -e -L1 -L2 [ #d #e #_ #I #K1 #V1 #H destruct | #L #I #V #H elim (lt_refl_false … H) @@ -89,14 +89,14 @@ fact ltpss_inv_tpss11_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → 0 < d → ] qed. -lemma ltpss_inv_tpss11: ∀d,e,I,K1,V1,L2. K1. ⓑ{I} V1 ▶* [d, e] L2 → 0 < d → - ∃∃K2,V2. K1 ▶* [d - 1, e] K2 & - K2 ⊢ V1 ▶* [d - 1, e] V2 & - L2 = K2. ⓑ{I} V2. +lemma ltpss_dx_inv_tpss11: ∀d,e,I,K1,V1,L2. K1. ⓑ{I} V1 ▶* [d, e] L2 → 0 < d → + ∃∃K2,V2. K1 ▶* [d - 1, e] K2 & + K2 ⊢ V1 ▶* [d - 1, e] V2 & + L2 = K2. ⓑ{I} V2. /2 width=3/ qed-. -fact ltpss_inv_atom2_aux: ∀d,e,L1,L2. - L1 ▶* [d, e] L2 → L2 = ⋆ → L1 = ⋆. +fact ltpss_dx_inv_atom2_aux: ∀d,e,L1,L2. + L1 ▶* [d, e] L2 → L2 = ⋆ → L1 = ⋆. #d #e #L1 #L2 * -d -e -L1 -L2 [ // | #L #I #V #H destruct @@ -105,14 +105,14 @@ fact ltpss_inv_atom2_aux: ∀d,e,L1,L2. ] qed. -lemma ltpss_inv_atom2: ∀d,e,L1. L1 ▶* [d, e] ⋆ → L1 = ⋆. +lemma ltpss_dx_inv_atom2: ∀d,e,L1. L1 ▶* [d, e] ⋆ → L1 = ⋆. /2 width=5/ qed-. -fact ltpss_inv_tpss22_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → d = 0 → 0 < e → - ∀K2,I,V2. L2 = K2. ⓑ{I} V2 → - ∃∃K1,V1. K1 ▶* [0, e - 1] K2 & - K2 ⊢ V1 ▶* [0, e - 1] V2 & - L1 = K1. ⓑ{I} V1. +fact ltpss_dx_inv_tpss22_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → d = 0 → 0 < e → + ∀K2,I,V2. L2 = K2. ⓑ{I} V2 → + ∃∃K1,V1. K1 ▶* [0, e - 1] K2 & + K2 ⊢ V1 ▶* [0, e - 1] V2 & + L1 = K1. ⓑ{I} V1. #d #e #L1 #L2 * -d -e -L1 -L2 [ #d #e #_ #_ #K1 #I #V1 #H destruct | #L1 #I #V #_ #H elim (lt_refl_false … H) @@ -121,17 +121,17 @@ fact ltpss_inv_tpss22_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → d = 0 → 0 < e ] qed. -lemma ltpss_inv_tpss22: ∀e,L1,K2,I,V2. L1 ▶* [0, e] K2. ⓑ{I} V2 → 0 < e → - ∃∃K1,V1. K1 ▶* [0, e - 1] K2 & - K2 ⊢ V1 ▶* [0, e - 1] V2 & - L1 = K1. ⓑ{I} V1. +lemma ltpss_dx_inv_tpss22: ∀e,L1,K2,I,V2. L1 ▶* [0, e] K2. ⓑ{I} V2 → 0 < e → + ∃∃K1,V1. K1 ▶* [0, e - 1] K2 & + K2 ⊢ V1 ▶* [0, e - 1] V2 & + L1 = K1. ⓑ{I} V1. /2 width=5/ qed-. -fact ltpss_inv_tpss12_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → 0 < d → - ∀I,K2,V2. L2 = K2. ⓑ{I} V2 → - ∃∃K1,V1. K1 ▶* [d - 1, e] K2 & - K2 ⊢ V1 ▶* [d - 1, e] V2 & - L1 = K1. ⓑ{I} V1. +fact ltpss_dx_inv_tpss12_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → 0 < d → + ∀I,K2,V2. L2 = K2. ⓑ{I} V2 → + ∃∃K1,V1. K1 ▶* [d - 1, e] K2 & + K2 ⊢ V1 ▶* [d - 1, e] V2 & + L1 = K1. ⓑ{I} V1. #d #e #L1 #L2 * -d -e -L1 -L2 [ #d #e #_ #I #K2 #V2 #H destruct | #L #I #V #H elim (lt_refl_false … H) @@ -140,56 +140,56 @@ fact ltpss_inv_tpss12_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → 0 < d → ] qed. -lemma ltpss_inv_tpss12: ∀L1,K2,I,V2,d,e. L1 ▶* [d, e] K2. ⓑ{I} V2 → 0 < d → - ∃∃K1,V1. K1 ▶* [d - 1, e] K2 & - K2 ⊢ V1 ▶* [d - 1, e] V2 & - L1 = K1. ⓑ{I} V1. +lemma ltpss_dx_inv_tpss12: ∀L1,K2,I,V2,d,e. L1 ▶* [d, e] K2. ⓑ{I} V2 → 0 < d → + ∃∃K1,V1. K1 ▶* [d - 1, e] K2 & + K2 ⊢ V1 ▶* [d - 1, e] V2 & + L1 = K1. ⓑ{I} V1. /2 width=3/ qed-. (* Basic properties *********************************************************) -lemma ltpss_tps2: ∀L1,L2,I,V1,V2,e. - L1 ▶* [0, e] L2 → L2 ⊢ V1 ▶ [0, e] V2 → - L1. ⓑ{I} V1 ▶* [0, e + 1] L2. ⓑ{I} V2. +lemma ltpss_dx_tps2: ∀L1,L2,I,V1,V2,e. + L1 ▶* [0, e] L2 → L2 ⊢ V1 ▶ [0, e] V2 → + L1. ⓑ{I} V1 ▶* [0, e + 1] L2. ⓑ{I} V2. /3 width=1/ qed. -lemma ltpss_tps1: ∀L1,L2,I,V1,V2,d,e. - L1 ▶* [d, e] L2 → L2 ⊢ V1 ▶ [d, e] V2 → - L1. ⓑ{I} V1 ▶* [d + 1, e] L2. ⓑ{I} V2. +lemma ltpss_dx_tps1: ∀L1,L2,I,V1,V2,d,e. + L1 ▶* [d, e] L2 → L2 ⊢ V1 ▶ [d, e] V2 → + L1. ⓑ{I} V1 ▶* [d + 1, e] L2. ⓑ{I} V2. /3 width=1/ qed. -lemma ltpss_tpss2_lt: ∀L1,L2,I,V1,V2,e. - L1 ▶* [0, e - 1] L2 → L2 ⊢ V1 ▶* [0, e - 1] V2 → - 0 < e → L1. ⓑ{I} V1 ▶* [0, e] L2. ⓑ{I} V2. +lemma ltpss_dx_tpss2_lt: ∀L1,L2,I,V1,V2,e. + L1 ▶* [0, e - 1] L2 → L2 ⊢ V1 ▶* [0, e - 1] V2 → + 0 < e → L1. ⓑ{I} V1 ▶* [0, e] L2. ⓑ{I} V2. #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He >(plus_minus_m_m e 1) /2 width=1/ qed. -lemma ltpss_tpss1_lt: ∀L1,L2,I,V1,V2,d,e. - L1 ▶* [d - 1, e] L2 → L2 ⊢ V1 ▶* [d - 1, e] V2 → - 0 < d → L1. ⓑ{I} V1 ▶* [d, e] L2. ⓑ{I} V2. +lemma ltpss_dx_tpss1_lt: ∀L1,L2,I,V1,V2,d,e. + L1 ▶* [d - 1, e] L2 → L2 ⊢ V1 ▶* [d - 1, e] V2 → + 0 < d → L1. ⓑ{I} V1 ▶* [d, e] L2. ⓑ{I} V2. #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd >(plus_minus_m_m d 1) /2 width=1/ qed. -lemma ltpss_tps2_lt: ∀L1,L2,I,V1,V2,e. - L1 ▶* [0, e - 1] L2 → L2 ⊢ V1 ▶ [0, e - 1] V2 → - 0 < e → L1. ⓑ{I} V1 ▶* [0, e] L2. ⓑ{I} V2. +lemma ltpss_dx_tps2_lt: ∀L1,L2,I,V1,V2,e. + L1 ▶* [0, e - 1] L2 → L2 ⊢ V1 ▶ [0, e - 1] V2 → + 0 < e → L1. ⓑ{I} V1 ▶* [0, e] L2. ⓑ{I} V2. /3 width=1/ qed. -lemma ltpss_tps1_lt: ∀L1,L2,I,V1,V2,d,e. - L1 ▶* [d - 1, e] L2 → L2 ⊢ V1 ▶ [d - 1, e] V2 → - 0 < d → L1. ⓑ{I} V1 ▶* [d, e] L2. ⓑ{I} V2. +lemma ltpss_dx_tps1_lt: ∀L1,L2,I,V1,V2,d,e. + L1 ▶* [d - 1, e] L2 → L2 ⊢ V1 ▶ [d - 1, e] V2 → + 0 < d → L1. ⓑ{I} V1 ▶* [d, e] L2. ⓑ{I} V2. /3 width=1/ qed. (* Basic_1: was by definition: csubst1_refl *) -lemma ltpss_refl: ∀L,d,e. L ▶* [d, e] L. +lemma ltpss_dx_refl: ∀L,d,e. L ▶* [d, e] L. #L elim L -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. +lemma ltpss_dx_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; @@ -207,35 +207,35 @@ lemma ltpss_weak: ∀L1,L2,d1,e1. L1 ▶* [d1, e1] L2 → ] qed. -lemma ltpss_weak_all: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → L1 ▶* [0, |L2|] L2. +lemma ltpss_dx_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/ qed. -fact ltpss_append_le_aux: ∀K1,K2,d,x. K1 ▶* [d, x] K2 → x = |K1| - d → - ∀L1,L2,e. L1 ▶* [0, e] L2 → d ≤ |K1| → - L1 @@ K1 ▶* [d, x + e] L2 @@ K2. +fact ltpss_dx_append_le_aux: ∀K1,K2,d,x. K1 ▶* [d, x] K2 → x = |K1| - d → + ∀L1,L2,e. L1 ▶* [0, e] L2 → d ≤ |K1| → + L1 @@ K1 ▶* [d, x + e] L2 @@ K2. #K1 #K2 #d #x #H elim H -K1 -K2 -d -x [ #d #x #H1 #L1 #L2 #e #HL12 #H2 destruct lapply (le_n_O_to_eq … H2) -H2 #H destruct // | #K #I #V plus_plus_comm_23 - /4 width=5 by ltpss_tpss2, tpss_append, tpss_weak, monotonic_le_plus_r/ (**) (* too slow without trace *) + /4 width=5 by ltpss_dx_tpss2, tpss_append, tpss_weak, monotonic_le_plus_r/ (**) (* too slow without trace *) | #K1 #K2 #I #V1 #V2 #d #x #_ #HV12 #IHK12 normalize shift_append_assoc #H - elim (tps_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct - elim (IH … HT12) -IH -T1 #L2 #T #HL12 #H destruct - append_length (ldrop_inv_atom1 … H) -H // | // @@ -33,9 +33,9 @@ lemma ltpss_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 ▶* [d1, e1] L1 → ] qed. -lemma ltpss_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 ▶* [d1, e1] L0 → - ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → - d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2. +lemma ltpss_dx_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 ▶* [d1, e1] L0 → + ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → + d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2. #L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H // | // @@ -50,9 +50,9 @@ lemma ltpss_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 ▶* [d1, e1] L0 → ] qed. -lemma ltpss_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, e2] L1 ≡ L. +lemma ltpss_dx_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, e2] 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 @@ -72,9 +72,9 @@ lemma ltpss_ldrop_conf_be: ∀L0,L1,d1,e1. L0 ▶* [d1, e1] L1 → ] qed. -lemma ltpss_ldrop_trans_be: ∀L1,L0,d1,e1. L1 ▶* [d1, e1] L0 → - ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → - ∃∃L. L ▶* [0, d1 + e1 - e2] L2 & ⇩[0, e2] L1 ≡ L. +lemma ltpss_dx_ldrop_trans_be: ∀L1,L0,d1,e1. L1 ▶* [d1, e1] L0 → + ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → + ∃∃L. L ▶* [0, d1 + e1 - e2] L2 & ⇩[0, e2] L1 ≡ L. #L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/ | normalize #L #I #V #L2 #e2 #HL2 #_ #He2 @@ -94,9 +94,9 @@ lemma ltpss_ldrop_trans_be: ∀L1,L0,d1,e1. L1 ▶* [d1, e1] L0 → ] qed. -lemma ltpss_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. +lemma ltpss_dx_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 #H elim H -L0 -L1 -d1 -e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/ | /2 width=3/ @@ -112,9 +112,9 @@ lemma ltpss_ldrop_conf_le: ∀L0,L1,d1,e1. L0 ▶* [d1, e1] L1 → ] qed. -lemma ltpss_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. +lemma ltpss_dx_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 #H elim H -L1 -L0 -d1 -e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/ | /2 width=3/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx_ltpss_dx.ma similarity index 63% rename from matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma rename to matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx_ltpss_dx.ma index f866adc12..22fa61ffc 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx_ltpss_dx.ma @@ -14,45 +14,45 @@ include "basic_2/unfold/tpss_tpss.ma". include "basic_2/unfold/tpss_alt.ma". -include "basic_2/unfold/ltpss_tpss.ma". +include "basic_2/unfold/ltpss_dx_tpss.ma". -(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************) +(* DX PARTIAL UNFOLD ON LOCAL ENVIRONMENTS **********************************) (* Advanced properties ******************************************************) -lemma ltpss_tpss_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶* [d2, e2] U2 → - ∀L1,d1,e1. L0 ▶* [d1, e1] L1 → - ∃∃T. L1 ⊢ T2 ▶* [d2, e2] T & - L1 ⊢ U2 ▶* [d1, e1] T. +lemma ltpss_dx_tpss_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶* [d2, e2] U2 → + ∀L1,d1,e1. L0 ▶* [d1, e1] L1 → + ∃∃T. L1 ⊢ T2 ▶* [d2, e2] T & + L1 ⊢ U2 ▶* [d1, e1] T. #L0 #T2 #U2 #d2 #e2 #H #L1 #d1 #e1 #HL01 @(tpss_ind … H) -U2 /2 width=3/ #U #U2 #_ #HU2 * #X2 #HTX2 #HUX2 -elim (ltpss_tps_conf … HU2 … HL01) -L0 #X1 #HUX1 #HU2X1 +elim (ltpss_dx_tps_conf … HU2 … HL01) -L0 #X1 #HUX1 #HU2X1 elim (tpss_strip_eq … HUX2 … HUX1) -U #X #HX2 #HX1 lapply (tpss_trans_eq … HU2X1 … HX1) -X1 /3 width=3/ qed. -lemma ltpss_tpss_trans_down: ∀L0,L1,T2,U2,d1,e1,d2,e2. d2 + e2 ≤ d1 → - L1 ▶* [d1, e1] L0 → L0 ⊢ T2 ▶* [d2, e2] U2 → - ∃∃T. L1 ⊢ T2 ▶* [d2, e2] T & L0 ⊢ T ▶* [d1, e1] U2. +lemma ltpss_dx_tpss_trans_down: ∀L0,L1,T2,U2,d1,e1,d2,e2. d2 + e2 ≤ d1 → + L1 ▶* [d1, e1] L0 → L0 ⊢ T2 ▶* [d2, e2] U2 → + ∃∃T. L1 ⊢ T2 ▶* [d2, e2] T & L0 ⊢ T ▶* [d1, e1] U2. #L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde2d1 #HL10 #H @(tpss_ind … H) -U2 [ /2 width=3/ | #U #U2 #_ #HU2 * #T #HT2 #HTU elim (tpss_strap1_down … HTU … HU2 ?) -U // #U #HTU #HU2 - elim (ltpss_tps_trans … HTU … HL10) -HTU -HL10 #X #HTX #HXU + elim (ltpss_dx_tps_trans … HTU … HL10) -HTU -HL10 #X #HTX #HXU lapply (tpss_trans_eq … HXU HU2) -U /3 width=3/ ] qed. -fact ltpss_tpss_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e. - L1 ⊢ T2 ▶* [d, e] U2 → ∀L0. L0 ▶* [d, e] L1 → - Y1 = L1 → X2 = T2 → L0 ⊢ T2 ▶* [d, e] U2. +fact ltpss_dx_tpss_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e. + L1 ⊢ T2 ▶* [d, e] U2 → ∀L0. L0 ▶* [d, e] L1 → + Y1 = L1 → X2 = T2 → L0 ⊢ T2 ▶* [d, e] U2. #Y1 #X2 @(cw_wf_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH #L1 #T2 #U2 #d #e #H @(tpss_ind_alt … H) -L1 -T2 -U2 -d -e [ // | #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #HV12 #HVW2 #_ #L0 #HL01 #H1 #H2 destruct lapply (ldrop_fwd_lw … HLK1) #H1 normalize in H1; - elim (ltpss_ldrop_trans_be … HL01 … HLK1 ? ?) -HL01 -HLK1 // /2 width=2/ #X #H #HLK0 - elim (ltpss_inv_tpss22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct + elim (ltpss_dx_ldrop_trans_be … HL01 … HLK1 ? ?) -HL01 -HLK1 // /2 width=2/ #X #H #HLK0 + elim (ltpss_dx_inv_tpss22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct lapply (tpss_fwd_tw … HV01) #H2 lapply (transitive_le (#{K1} + #{V0}) … H1) -H1 /2 width=1/ -H2 #H lapply (tpss_trans_eq … HV01 HV12) -V1 #HV02 @@ -69,19 +69,19 @@ fact ltpss_tpss_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e. ] qed. -lemma ltpss_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 ▶* [d, e] U2 → - ∀L0. L0 ▶* [d, e] L1 → L0 ⊢ T2 ▶* [d, e] U2. +lemma ltpss_dx_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 ▶* [d, e] U2 → + ∀L0. L0 ▶* [d, e] L1 → L0 ⊢ T2 ▶* [d, e] U2. /2 width=5/ qed. -lemma ltpss_tps_trans_eq: ∀L0,L1,T2,U2,d,e. L0 ▶* [d, e] L1 → - L1 ⊢ T2 ▶ [d, e] U2 → L0 ⊢ T2 ▶* [d, e] U2. +lemma ltpss_dx_tps_trans_eq: ∀L0,L1,T2,U2,d,e. L0 ▶* [d, e] L1 → + L1 ⊢ T2 ▶ [d, e] U2 → L0 ⊢ T2 ▶* [d, e] U2. /3 width=3/ qed. (* Main properties **********************************************************) -fact ltpss_conf_aux: ∀K,K1,L1,d1,e1. K1 ▶* [d1, e1] L1 → - ∀K2,L2,d2,e2. K2 ▶* [d2, e2] L2 → K1 = K → K2 = K → - ∃∃L. L1 ▶* [d2, e2] L & L2 ▶* [d1, e1] L. +fact ltpss_dx_conf_aux: ∀K,K1,L1,d1,e1. K1 ▶* [d1, e1] L1 → + ∀K2,L2,d2,e2. K2 ▶* [d2, e2] L2 → K1 = K → K2 = K → + ∃∃L. L1 ▶* [d2, e2] L & L2 ▶* [d1, e1] L. #K @(lw_wf_ind … K) -K #K #IH #K1 #L1 #d1 #e1 * -K1 -L1 -d1 -e1 [ -IH /2 width=3/ | -IH #K1 #I1 #V1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2 @@ -95,15 +95,15 @@ fact ltpss_conf_aux: ∀K,K1,L1,d1,e1. K1 ▶* [d1, e1] L1 → | -IH #K2 #I2 #V2 #H1 #H2 destruct /3 width=5/ | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2 - elim (ltpss_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1 - elim (ltpss_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2 + elim (ltpss_dx_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1 + elim (ltpss_dx_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2 elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W lapply (tpss_trans_eq … HVU1 HU1W) -U1 lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/ | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2 - elim (ltpss_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1 - elim (ltpss_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2 + elim (ltpss_dx_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1 + elim (ltpss_dx_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2 elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W lapply (tpss_trans_eq … HVU1 HU1W) -U1 lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/ @@ -113,15 +113,15 @@ fact ltpss_conf_aux: ∀K,K1,L1,d1,e1. K1 ▶* [d1, e1] L1 → | -IH #K2 #I2 #V2 #H1 #H2 destruct /3 width=5/ | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2 - elim (ltpss_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1 - elim (ltpss_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2 + elim (ltpss_dx_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1 + elim (ltpss_dx_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2 elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W lapply (tpss_trans_eq … HVU1 HU1W) -U1 lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/ | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2 - elim (ltpss_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1 - elim (ltpss_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2 + elim (ltpss_dx_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1 + elim (ltpss_dx_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2 elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W lapply (tpss_trans_eq … HVU1 HU1W) -U1 lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/ @@ -129,18 +129,7 @@ fact ltpss_conf_aux: ∀K,K1,L1,d1,e1. K1 ▶* [d1, e1] L1 → ] qed. -lemma ltpss_conf: ∀L0,L1,d1,e1. L0 ▶* [d1, e1] L1 → - ∀L2,d2,e2. L0 ▶* [d2, e2] L2 → - ∃∃L. L1 ▶* [d2, e2] L & L2 ▶* [d1, e1] L. +theorem ltpss_dx_conf: ∀L0,L1,d1,e1. L0 ▶* [d1, e1] L1 → + ∀L2,d2,e2. L0 ▶* [d2, e2] L2 → + ∃∃L. L1 ▶* [d2, e2] L & L2 ▶* [d1, e1] L. /2 width=7/ qed. - -theorem ltpss_trans_eq: ∀L1,L,d,e. L1 ▶* [d, e] L → - ∀L2. L ▶* [d, e] L2 → L1 ▶* [d, e] L2. -#L1 #L #d #e #H elim H -L1 -L -d -e // -[ #L1 #L #I #V1 #V #e #_ #HV1 #IHL1 #X #H - elim (ltpss_inv_tpss21 … H ?) -H // minus_plus minus_plus >commutative_plus /2 width=1/ - | lapply (ltpss_ldrop_conf_ge … HL01 … HLK0 ?) -L0 // /3 width=4/ + | lapply (ltpss_dx_ldrop_conf_ge … HL01 … HLK0 ?) -L0 // /3 width=4/ ] ] | #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01 @@ -60,36 +60,36 @@ lemma ltpss_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 → ] qed. -lemma ltpss_tpss_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶* [d2, e2] U2 → - ∀L1,d1,e1. L1 ▶* [d1, e1] L0 → d1 + e1 ≤ d2 → - L1 ⊢ T2 ▶* [d2, e2] U2. +lemma ltpss_dx_tpss_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶* [d2, e2] U2 → + ∀L1,d1,e1. L1 ▶* [d1, e1] L0 → d1 + e1 ≤ d2 → + L1 ⊢ T2 ▶* [d2, e2] U2. #L0 #T2 #U2 #d2 #e2 #H #L1 #d1 #e1 #HL01 #Hde1d2 @(tpss_ind … H) -U2 // #U #U2 #_ #HU2 #IHU -lapply (ltpss_tps_trans_ge … HU2 … HL01 ?) -L0 // -Hde1d2 /2 width=3/ +lapply (ltpss_dx_tps_trans_ge … HU2 … HL01 ?) -L0 // -Hde1d2 /2 width=3/ qed. (* Basic_1: was: subst1_subst1 *) -lemma ltpss_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 → - ∀L1,d1,e1. L1 ▶* [d1, e1] L0 → - ∃∃T. L1 ⊢ T2 ▶ [d2, e2] T & - L0 ⊢ T ▶* [d1, e1] U2. +lemma ltpss_dx_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 → + ∀L1,d1,e1. L1 ▶* [d1, e1] L0 → + ∃∃T. L1 ⊢ T2 ▶ [d2, e2] T & + L0 ⊢ T ▶* [d1, e1] U2. #L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2 [ /2 width=3/ | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10 elim (lt_or_ge i2 d1) #Hi2d1 - [ elim (ltpss_ldrop_trans_le … HL10 … HLK0 ?) -HL10 /2 width=2/ #X #H #HLK1 - elim (ltpss_inv_tpss12 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct + [ elim (ltpss_dx_ldrop_trans_le … HL10 … HLK0 ?) -HL10 /2 width=2/ #X #H #HLK1 + elim (ltpss_dx_inv_tpss12 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #H elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1 lapply (tpss_lift_ge … HV01 … H HVW1 … HVW0) -V0 -H // >minus_plus minus_plus >commutative_plus /2 width=1/ - | lapply (ltpss_ldrop_trans_ge … HL10 … HLK0 ?) -HL10 -HLK0 // /3 width=4/ + | lapply (ltpss_dx_ldrop_trans_ge … HL10 … HLK0 ?) -HL10 -HLK0 // /3 width=4/ ] ] | #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn.ma new file mode 100644 index 000000000..95eb9efd9 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn.ma @@ -0,0 +1,254 @@ +(**************************************************************************) +(* ___ *) +(* ||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.ma". + +(* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************) + +inductive ltpss_sn: nat → nat → relation lenv ≝ +| ltpss_sn_atom : ∀d,e. ltpss_sn d e (⋆) (⋆) +| ltpss_sn_pair : ∀L,I,V. ltpss_sn 0 0 (L. ⓑ{I} V) (L. ⓑ{I} V) +| ltpss_sn_tpss2: ∀L1,L2,I,V1,V2,e. + ltpss_sn 0 e L1 L2 → L1 ⊢ V1 ▶* [0, e] V2 → + ltpss_sn 0 (e + 1) (L1. ⓑ{I} V1) (L2. ⓑ{I} V2) +| ltpss_sn_tpss1: ∀L1,L2,I,V1,V2,d,e. + ltpss_sn d e L1 L2 → L1 ⊢ V1 ▶* [d, e] V2 → + ltpss_sn (d + 1) e (L1. ⓑ{I} V1) (L2. ⓑ{I} V2) +. + +interpretation "parallel unfold (local environment, sn variant)" + 'PSubstStarSn L1 d e L2 = (ltpss_sn d e L1 L2). + +(* Basic inversion lemmas ***************************************************) + +fact ltpss_sn_inv_refl_O2_aux: ∀d,e,L1,L2. L1 ⊢ ▶* [d, e] L2 → e = 0 → L1 = L2. +#d #e #L1 #L2 #H elim H -d -e -L1 -L2 // +[ #L1 #L2 #I #V1 #V2 #e #_ #_ #_ >commutative_plus normalize #H destruct +| #L1 #L2 #I #V1 #V2 #d #e #_ #HV12 #IHL12 #He destruct + >(IHL12 ?) -IHL12 // >(tpss_inv_refl_O2 … HV12) // +] +qed. + +lemma ltpss_sn_inv_refl_O2: ∀d,L1,L2. L1 ⊢ ▶* [d, 0] L2 → L1 = L2. +/2 width=4/ qed-. + +fact ltpss_sn_inv_atom1_aux: ∀d,e,L1,L2. + L1 ⊢ ▶* [d, e] L2 → L1 = ⋆ → L2 = ⋆. +#d #e #L1 #L2 * -d -e -L1 -L2 +[ // +| #L #I #V #H destruct +| #L1 #L2 #I #V1 #V2 #e #_ #_ #H destruct +| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct +] +qed. + +lemma ltpss_sn_inv_atom1: ∀d,e,L2. ⋆ ⊢ ▶* [d, e] L2 → L2 = ⋆. +/2 width=5/ qed-. + +fact ltpss_sn_inv_tpss21_aux: ∀d,e,L1,L2. L1 ⊢ ▶* [d, e] L2 → d = 0 → 0 < e → + ∀K1,I,V1. L1 = K1. ⓑ{I} V1 → + ∃∃K2,V2. K1 ⊢ ▶* [0, e - 1] K2 & + K1 ⊢ V1 ▶* [0, e - 1] V2 & + L2 = K2. ⓑ{I} V2. +#d #e #L1 #L2 * -d -e -L1 -L2 +[ #d #e #_ #_ #K1 #I #V1 #H destruct +| #L1 #I #V #_ #H elim (lt_refl_false … H) +| #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K1 #J #W1 #H destruct /2 width=5/ +| #L1 #L2 #I #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct +] +qed. + +lemma ltpss_sn_inv_tpss21: ∀e,K1,I,V1,L2. K1. ⓑ{I} V1 ⊢ ▶* [0, e] L2 → 0 < e → + ∃∃K2,V2. K1 ⊢ ▶* [0, e - 1] K2 & + K1 ⊢ V1 ▶* [0, e - 1] V2 & + L2 = K2. ⓑ{I} V2. +/2 width=5/ qed-. + +fact ltpss_sn_inv_tpss11_aux: ∀d,e,L1,L2. L1 ⊢ ▶* [d, e] L2 → 0 < d → + ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → + ∃∃K2,V2. K1 ⊢ ▶* [d - 1, e] K2 & + K1 ⊢ V1 ▶* [d - 1, e] V2 & + L2 = K2. ⓑ{I} V2. +#d #e #L1 #L2 * -d -e -L1 -L2 +[ #d #e #_ #I #K1 #V1 #H destruct +| #L #I #V #H elim (lt_refl_false … H) +| #L1 #L2 #I #V1 #V2 #e #_ #_ #H elim (lt_refl_false … H) +| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #_ #J #K1 #W1 #H destruct /2 width=5/ +] +qed. + +lemma ltpss_sn_inv_tpss11: ∀d,e,I,K1,V1,L2. K1. ⓑ{I} V1 ⊢ ▶* [d, e] L2 → 0 < d → + ∃∃K2,V2. K1 ⊢ ▶* [d - 1, e] K2 & + K1 ⊢ V1 ▶* [d - 1, e] V2 & + L2 = K2. ⓑ{I} V2. +/2 width=3/ qed-. + +fact ltpss_sn_inv_atom2_aux: ∀d,e,L1,L2. + L1 ⊢ ▶* [d, e] L2 → L2 = ⋆ → L1 = ⋆. +#d #e #L1 #L2 * -d -e -L1 -L2 +[ // +| #L #I #V #H destruct +| #L1 #L2 #I #V1 #V2 #e #_ #_ #H destruct +| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct +] +qed. + +lemma ltpss_sn_inv_atom2: ∀d,e,L1. L1 ⊢ ▶* [d, e] ⋆ → L1 = ⋆. +/2 width=5/ qed-. + +fact ltpss_sn_inv_tpss22_aux: ∀d,e,L1,L2. L1 ⊢ ▶* [d, e] L2 → d = 0 → 0 < e → + ∀K2,I,V2. L2 = K2. ⓑ{I} V2 → + ∃∃K1,V1. K1 ⊢ ▶* [0, e - 1] K2 & + K1 ⊢ V1 ▶* [0, e - 1] V2 & + L1 = K1. ⓑ{I} V1. +#d #e #L1 #L2 * -d -e -L1 -L2 +[ #d #e #_ #_ #K1 #I #V1 #H destruct +| #L1 #I #V #_ #H elim (lt_refl_false … H) +| #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K2 #J #W2 #H destruct /2 width=5/ +| #L1 #L2 #I #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct +] +qed. + +lemma ltpss_sn_inv_tpss22: ∀e,L1,K2,I,V2. L1 ⊢ ▶* [0, e] K2. ⓑ{I} V2 → 0 < e → + ∃∃K1,V1. K1 ⊢ ▶* [0, e - 1] K2 & + K1 ⊢ V1 ▶* [0, e - 1] V2 & + L1 = K1. ⓑ{I} V1. +/2 width=5/ qed-. + +fact ltpss_sn_inv_tpss12_aux: ∀d,e,L1,L2. L1 ⊢ ▶* [d, e] L2 → 0 < d → + ∀I,K2,V2. L2 = K2. ⓑ{I} V2 → + ∃∃K1,V1. K1 ⊢ ▶* [d - 1, e] K2 & + K1 ⊢ V1 ▶* [d - 1, e] V2 & + L1 = K1. ⓑ{I} V1. +#d #e #L1 #L2 * -d -e -L1 -L2 +[ #d #e #_ #I #K2 #V2 #H destruct +| #L #I #V #H elim (lt_refl_false … H) +| #L1 #L2 #I #V1 #V2 #e #_ #_ #H elim (lt_refl_false … H) +| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #_ #J #K2 #W2 #H destruct /2 width=5/ +] +qed. + +lemma ltpss_sn_inv_tpss12: ∀L1,K2,I,V2,d,e. L1 ⊢ ▶* [d, e] K2. ⓑ{I} V2 → 0 < d → + ∃∃K1,V1. K1 ⊢ ▶* [d - 1, e] K2 & + K1 ⊢ V1 ▶* [d - 1, e] V2 & + L1 = K1. ⓑ{I} V1. +/2 width=3/ qed-. + +(* Basic properties *********************************************************) + +lemma ltpss_sn_tps2: ∀L1,L2,I,V1,V2,e. + L1 ⊢ ▶* [0, e] L2 → L1 ⊢ V1 ▶ [0, e] V2 → + L1. ⓑ{I} V1 ⊢ ▶* [0, e + 1] L2. ⓑ{I} V2. +/3 width=1/ qed. + +lemma ltpss_sn_tps1: ∀L1,L2,I,V1,V2,d,e. + L1 ⊢ ▶* [d, e] L2 → L1 ⊢ V1 ▶ [d, e] V2 → + L1. ⓑ{I} V1 ⊢ ▶* [d + 1, e] L2. ⓑ{I} V2. +/3 width=1/ qed. + +lemma ltpss_sn_tpss2_lt: ∀L1,L2,I,V1,V2,e. + L1 ⊢ ▶* [0, e - 1] L2 → L1 ⊢ V1 ▶* [0, e - 1] V2 → + 0 < e → L1. ⓑ{I} V1 ⊢ ▶* [0, e] L2. ⓑ{I} V2. +#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He +>(plus_minus_m_m e 1) /2 width=1/ +qed. + +lemma ltpss_sn_tpss1_lt: ∀L1,L2,I,V1,V2,d,e. + L1 ⊢ ▶* [d - 1, e] L2 → L1 ⊢ V1 ▶* [d - 1, e] V2 → + 0 < d → L1. ⓑ{I} V1 ⊢ ▶* [d, e] L2. ⓑ{I} V2. +#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd +>(plus_minus_m_m d 1) /2 width=1/ +qed. + +lemma ltpss_sn_tps2_lt: ∀L1,L2,I,V1,V2,e. + L1 ⊢ ▶* [0, e - 1] L2 → L1 ⊢ V1 ▶ [0, e - 1] V2 → + 0 < e → L1. ⓑ{I} V1 ⊢ ▶* [0, e] L2. ⓑ{I} V2. +/3 width=1/ qed. + +lemma ltpss_sn_tps1_lt: ∀L1,L2,I,V1,V2,d,e. + L1 ⊢ ▶* [d - 1, e] L2 → L1 ⊢ V1 ▶ [d - 1, e] V2 → + 0 < d → L1. ⓑ{I} V1 ⊢ ▶* [d, e] L2. ⓑ{I} V2. +/3 width=1/ qed. + +lemma ltpss_sn_refl: ∀L,d,e. L ⊢ ▶* [d, e] L. +#L elim L -L // +#L #I #V #IHL * /2 width=1/ * /2 width=1/ +qed. + +lemma ltpss_sn_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_plus_comm_23 + /4 width=5 by ltpss_sn_tpss2, tpss_append, tpss_weak, monotonic_le_plus_r/ (**) (* too slow without trace *) +| #K1 #K2 #I #V1 #V2 #d #x #_ #HV12 #IHK12 normalize (ldrop_inv_atom1 … H) -H // +| // +| normalize #K0 #K1 #I #V0 #V1 #e1 #_ #_ #IHK01 #L2 #e2 #H #He12 + elim (le_inv_plus_l … He12) #_ #He2 + lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2 + lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/ +| #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2 + elim (le_inv_plus_l … Hd1e2) #_ #He2 + lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2 + lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/ +] +qed. + +lemma ltpss_sn_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 ⊢ ▶* [d1, e1] L0 → + ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → + d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2. +#L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1 +[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H // +| // +| normalize #K1 #K0 #I #V1 #V0 #e1 #_ #_ #IHK10 #L2 #e2 #H #He12 + elim (le_inv_plus_l … He12) #_ #He2 + lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2 + lapply (IHK10 … HK0L2 ?) -K0 /2 width=1/ +| #K0 #K1 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2 + elim (le_inv_plus_l … Hd1e2) #_ #He2 + lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2 + lapply (IHK10 … HK0L2 ?) -IHK10 -HK0L2 /2 width=1/ +] +qed. + +lemma ltpss_sn_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, e2] 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 #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #_ #He21 + lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2 + [ -IHK01 -He21 destruct plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2 #He2de1 + elim (le_inv_plus_l … Hd1e2) #_ #He2 + (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 #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #_ #He21 + lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2 + [ -IHK10 -He21 destruct plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2 #He2de1 + elim (le_inv_plus_l … Hd1e2) #_ #He2 + (ldrop_inv_atom1 … H) -H /2 width=3/ +| /2 width=3/ +| normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #_ #L2 #e2 #H #He2 + lapply (le_n_O_to_eq … He2) -He2 #He2 destruct + lapply (ldrop_inv_refl … H) -H #H destruct /3 width=3/ +| #K0 #K1 #I #V0 #V1 #d1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #He2d1 + lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2 + [ -IHK01 -He2d1 destruct (ldrop_inv_atom1 … H) -H /2 width=3/ +| /2 width=3/ +| normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #_ #L2 #e2 #H #He2 + lapply (le_n_O_to_eq … He2) -He2 #He2 destruct + lapply (ldrop_inv_refl … H) -H #H destruct /3 width=3/ +| #K1 #K0 #I #V1 #V0 #d1 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #He2d1 + lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2 + [ -IHK10 -He2d1 destruct shift_append_assoc #H + elim (tps_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + elim (IH … HT12) -IH -T1 #L2 #T #HL12 #H destruct + append_length minus_plus minus_plus >commutative_plus /2 width=1/ + | lapply (ltpss_sn_ldrop_conf_ge … HL01 … HLK0 ?) -HL01 -HLK0 // /3 width=4/ + ] + ] +| #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01 + elim (IHVW2 … HL01) -IHVW2 #V #HV2 #HVW2 + elim (IHTU2 (L1. ⓑ{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL01 #T #HT2 #H + lapply (tpss_lsubs_trans … H (L0.ⓑ{I}V) ?) -H /2 width=1/ /3 width=5/ +| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01 + elim (IHVW2 … HL01) -IHVW2 + elim (IHTU2 … HL01) -IHTU2 -HL01 /3 width=5/ +] +qed. + +lemma ltpss_sn_tpss_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶* [d2, e2] U2 → + ∀L1,d1,e1. L1 ⊢ ▶* [d1, e1] L0 → d1 + e1 ≤ d2 → + L1 ⊢ T2 ▶* [d2, e2] U2. +#L0 #T2 #U2 #d2 #e2 #H #L1 #d1 #e1 #HL01 #Hde1d2 @(tpss_ind … H) -U2 // +#U #U2 #_ #HU2 #IHU +lapply (ltpss_sn_tps_trans_ge … HU2 … HL01 ?) -L0 // -Hde1d2 /2 width=3/ +qed. + +lemma ltpss_sn_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 → + ∀L1,d1,e1. L1 ⊢ ▶* [d1, e1] L0 → + ∃∃T. L1 ⊢ T2 ▶ [d2, e2] T & + L1 ⊢ T ▶* [d1, e1] U2. +#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2 +[ /2 width=3/ +| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10 + elim (lt_or_ge i2 d1) #Hi2d1 + [ elim (ltpss_sn_ldrop_trans_le … HL10 … HLK0 ?) -L0 /2 width=2/ #X #H #HLK1 + elim (ltpss_sn_inv_tpss12 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct + lapply (ldrop_fwd_ldrop2 … HLK1) #H + elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1 + lapply (tpss_lift_ge … HV01 … H HVW1 … HVW0) -V0 -H // >minus_plus minus_plus >commutative_plus /2 width=1/ + | lapply (ltpss_sn_ldrop_trans_ge … HL10 … HLK0 ?) -HL10 -HLK0 // /3 width=4/ + ] + ] +| #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 + elim (IHVW2 … HL10) -IHVW2 #V #HV2 #HVW2 + elim (IHTU2 (L1. ⓑ{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL10 #T #HT2 #H + lapply (tpss_lsubs_trans … H (L1.ⓑ{I}W2) ?) -H /2 width=1/ /3 width=5/ +| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 + elim (IHVW2 … HL10) -IHVW2 + elim (IHTU2 … HL10) -IHTU2 -HL10 /3 width=5/ +] +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma index 54ec6a581..65fb76fe0 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma @@ -12,12 +12,12 @@ (* *) (**************************************************************************) -include "basic_2/unfold/ltpss.ma". +include "basic_2/unfold/ltpss_sn.ma". (* BASIC LOCAL ENVIRONMENT THINNING *****************************************) definition thin: nat → nat → relation lenv ≝ - λd,e,L1,L2. ∃∃L. L1 ▶* [d, e] L & ⇩[d, e] L ≡ L2. + λd,e,L1,L2. ∃∃L. L1 ⊢ ▶* [d, e] L & ⇩[d, e] L ≡ L2. interpretation "basic thinning (local environment)" 'TSubst L1 d e L2 = (thin d e L1 L2). @@ -32,6 +32,6 @@ lemma ldrop_thin: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ▼*[d, e] L1 ≡ L2. lemma thin_inv_thin1: ∀I,K1,V1,L2,e. ▼*[0, e] K1.ⓑ{I} V1 ≡ L2 → 0 < e → ▼*[0, e - 1] K1 ≡ L2. #I #K1 #V1 #L2 #e * #X #HK1 #HL2 #e -elim (ltpss_inv_tpss21 … HK1 ?) -HK1 // #K #V #HK1 #_ #H destruct +elim (ltpss_sn_inv_tpss21 … HK1 ?) -HK1 // #K #V #HK1 #_ #H destruct lapply (ldrop_inv_ldrop1 … HL2 ?) -HL2 // /2 width=3/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma index faf9f4506..b5ffc5e4f 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma @@ -25,20 +25,18 @@ lemma thin_inv_delift1: ∀I,K1,V1,L2,d,e. ▼*[d, e] K1. ⓑ{I} V1 ≡ L2 → 0 K1 ⊢ ▼*[d - 1, e] V1 ≡ V2 & L2 = K2. ⓑ{I} V2. #I #K1 #V1 #L2 #d #e * #X #HK1 #HL2 #e -elim (ltpss_inv_tpss11 … HK1 ?) -HK1 // #K #V #HK1 #HV1 #H destruct -elim (ldrop_inv_skip1 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H destruct -lapply (ltpss_tpss_trans_eq … HV1 … HK1) -HV1 /3 width=5/ +elim (ltpss_sn_inv_tpss11 … HK1 ?) -HK1 // #K #V #HK1 #HV1 #H destruct +elim (ldrop_inv_skip1 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H destruct /3 width=5/ qed-. (* Properties on inverse basic term relocation ******************************) -lemma thin_delift1: ∀L1,L2,d,e. ▼*[d, e] L1 ≡ L2 → ∀V1,V2. L1 ⊢ ▼*[d, e] V1 ≡ V2 → - ∀I. ▼*[d + 1, e] L1.ⓑ{I}V1 ≡ L2.ⓑ{I}V2. +lemma thin_delift: ∀L1,L2,d,e. ▼*[d, e] L1 ≡ L2 → ∀V1,V2. L1 ⊢ ▼*[d, e] V1 ≡ V2 → + ∀I. ▼*[d + 1, e] L1.ⓑ{I}V1 ≡ 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 //