From 035e3f52f8da3cb3cdb493aa20568ad673cc2cf5 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 19 Oct 2011 15:57:18 +0000 Subject: [PATCH] - the relocation properties of cpr are closed! - the support for global references is started ... - some refactoring. --- .../lambda_delta/Basic_2/grammar/item.ma | 1 + .../lambda_delta/Basic_2/grammar/term.ma | 2 + .../contribs/lambda_delta/Basic_2/names.txt | 2 + .../contribs/lambda_delta/Basic_2/notation.ma | 8 +- .../Basic_2/reduction/cpr_lift.ma | 31 ++- .../reduction/{ltpr_drop.ma => ltpr_ldrop.ma} | 8 +- .../Basic_2/reduction/tpr_lift.ma | 2 + .../Basic_2/reduction/tpr_tpss.ma | 4 +- .../lambda_delta/Basic_2/substitution/drop.ma | 231 ------------------ .../Basic_2/substitution/ldrop.ma | 231 ++++++++++++++++++ .../{drop_drop.ma => ldrop_ldrop.ma} | 86 +++---- .../lambda_delta/Basic_2/substitution/lift.ma | 30 +++ .../Basic_2/substitution/lift_lift.ma | 34 ++- .../lambda_delta/Basic_2/substitution/ltps.ma | 4 +- .../{ltps_drop.ma => ltps_ldrop.ma} | 52 ++-- .../Basic_2/substitution/ltps_tps.ma | 26 +- .../lambda_delta/Basic_2/substitution/tps.ma | 6 +- .../Basic_2/substitution/tps_lift.ma | 106 ++++++-- .../Basic_2/substitution/tps_tps.ma | 2 +- .../lambda_delta/Basic_2/unfold/ltpss.ma | 2 +- .../unfold/{ltpss_drop.ma => ltpss_ldrop.ma} | 22 +- .../lambda_delta/Basic_2/unfold/tpss_lift.ma | 53 +++- .../lambda_delta/Basic_2/unfold/tpss_ltps.ma | 4 +- .../contribs/lambda_delta/Ground_2/arith.ma | 12 +- 24 files changed, 577 insertions(+), 382 deletions(-) rename matita/matita/contribs/lambda_delta/Basic_2/reduction/{ltpr_drop.ma => ltpr_ldrop.ma} (91%) delete mode 100644 matita/matita/contribs/lambda_delta/Basic_2/substitution/drop.ma create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma rename matita/matita/contribs/lambda_delta/Basic_2/substitution/{drop_drop.ma => ldrop_ldrop.ma} (55%) rename matita/matita/contribs/lambda_delta/Basic_2/substitution/{ltps_drop.ma => ltps_ldrop.ma} (76%) rename matita/matita/contribs/lambda_delta/Basic_2/unfold/{ltpss_drop.ma => ltpss_ldrop.ma} (79%) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma index 4ee4731b1..7b35d0ca5 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma @@ -30,6 +30,7 @@ include "Basic_2/notation.ma". inductive item0: Type[0] ≝ | Sort: nat → item0 (* sort: starting at 0 *) | LRef: nat → item0 (* reference by index: starting at 0 *) + | GRef: nat → item0 (* reference by position: starting at 0 *) . (* binary binding items *) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma index 46ba2cef2..621dda225 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma @@ -26,6 +26,8 @@ interpretation "sort (term)" 'Star k = (TAtom (Sort k)). interpretation "local reference (term)" 'LRef i = (TAtom (LRef i)). +interpretation "global reference (term)" 'GRef p = (TAtom (GRef p)). + interpretation "term construction (atomic)" 'SItem I = (TAtom I). interpretation "term construction (binary)" 'SItem I T1 T2 = (TPair I T1 T2). diff --git a/matita/matita/contribs/lambda_delta/Basic_2/names.txt b/matita/matita/contribs/lambda_delta/Basic_2/names.txt index c33d5a8ea..9078f4aef 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/names.txt +++ b/matita/matita/contribs/lambda_delta/Basic_2/names.txt @@ -20,3 +20,5 @@ e : relocation height h : sort hierarchy parameter i,j : local reference position index (de Bruijn's) k : sort index +p,q : global reference position + diff --git a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma index aa5cba8b9..4383616be 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma @@ -24,9 +24,13 @@ notation "hvbox( ⋆ term 90 k )" non associative with precedence 90 for @{ 'Star $k }. -notation "hvbox( # term 90 k )" +notation "hvbox( # term 90 i )" non associative with precedence 90 - for @{ 'LRef $k }. + for @{ 'LRef $i }. + +notation "hvbox( § term 90 p )" + non associative with precedence 90 + for @{ 'GRef $p }. notation "hvbox( 𝕒 { I } )" non associative with precedence 90 diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr_lift.ma index cf0460971..885670fb4 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr_lift.ma @@ -20,9 +20,9 @@ include "Basic_2/reduction/cpr.ma". (* Advanced properties ******************************************************) -lemma cpr_delta: ∀L,K,V1,W1,W2,i. - ↓[0, i] L ≡ K. 𝕓{Abbr} V1 → K ⊢ V1 [0, |L| - i - 1] ≫* W1 → - ↑[0, i + 1] W1 ≡ W2 → L ⊢ #i ⇒ W2. +lemma cpr_cdelta: ∀L,K,V1,W1,W2,i. + ↓[0, i] L ≡ K. 𝕓{Abbr} V1 → K ⊢ V1 [0, |L| - i - 1] ≫* W1 → + ↑[0, i + 1] W1 ≡ W2 → L ⊢ #i ⇒ W2. #L #K #V1 #W1 #W2 #i #HLK #HVW1 #HW12 @ex2_1_intro [2: // | skip | @tpss_subst /2 width=6/ ] (**) (* /4 width=6/ is too slow *) qed. @@ -50,6 +50,29 @@ lemma cpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 → (* Relocation properties ****************************************************) (* Basic_1: was: pr2_lift *) +lemma cpr_lift: ∀L,K,d,e. ↓[d, e] L ≡ K → + ∀T1,U1. ↑[d, e] T1 ≡ U1 → ∀T2,U2. ↑[d, e] T2 ≡ U2 → + K ⊢ T1 ⇒ T2 → L ⊢ U1 ⇒ U2. +#L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 * #T #HT1 #HT2 +elim (lift_total T d e) #U #HTU +lapply (tpr_lift … HT1 … HTU1 … HTU) -T1 #HU1 +elim (lt_or_ge (|K|) d) #HKd +[ lapply (tpss_lift_le … HT2 … HLK HTU … HTU2) -T2 T HLK [ /2/ | /3/ ] +| lapply (tpss_lift_be … HT2 … HLK HTU … HTU2) -T2 T HLK // /3/ +] +qed. (* Basic_1: was: pr2_gen_lift *) - +lemma cpr_inv_lift: ∀L,K,d,e. ↓[d, e] L ≡ K → + ∀T1,U1. ↑[d, e] T1 ≡ U1 → ∀U2. L ⊢ U1 ⇒ U2 → + ∃∃T2. ↑[d, e] T2 ≡ U2 & K ⊢ T1 ⇒ T2. +#L #K #d #e #HLK #T1 #U1 #HTU1 #U2 * #U #HU1 #HU2 +elim (tpr_inv_lift … HU1 … HTU1) -U1 #T #HTU #T1 +elim (lt_or_ge (|L|) d) #HLd +[ elim (tpss_inv_lift1_le … HU2 … HLK … HTU ?) -U HLK [ /5/ | /2/ ] +| elim (lt_or_ge (|L|) (d + e)) #HLde + [ elim (tpss_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -U HLK // [ /5/ | /2/ ] + | elim (tpss_inv_lift1_be … HU2 … HLK … HTU ? ?) -U HLK // /5/ + ] +] +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/ltpr_drop.ma b/matita/matita/contribs/lambda_delta/Basic_2/reduction/ltpr_ldrop.ma similarity index 91% rename from matita/matita/contribs/lambda_delta/Basic_2/reduction/ltpr_drop.ma rename to matita/matita/contribs/lambda_delta/Basic_2/reduction/ltpr_ldrop.ma index a444fc624..956bf1871 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/ltpr_drop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reduction/ltpr_ldrop.ma @@ -17,8 +17,8 @@ include "Basic_2/reduction/ltpr.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) -(* Basic_1: was: wcpr0_drop *) -lemma ltpr_drop_conf: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀L2. L1 ⇒ L2 → +(* Basic_1: was: wcpr0_ldrop *) +lemma ltpr_ldrop_conf: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀L2. L1 ⇒ L2 → ∃∃K2. ↓[d, e] L2 ≡ K2 & K1 ⇒ K2. #L1 #K1 #d #e #H elim H -H L1 K1 d e [ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2/ @@ -34,8 +34,8 @@ lemma ltpr_drop_conf: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀L2. L1 ⇒ L2 → ] qed. -(* Basic_1: was: wcpr0_drop_back *) -lemma ltpr_drop_trans: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀K2. K1 ⇒ K2 → +(* Basic_1: was: wcpr0_ldrop_back *) +lemma ltpr_ldrop_trans: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀K2. K1 ⇒ K2 → ∃∃L2. ↓[d, e] L2 ≡ K2 & L1 ⇒ L2. #L1 #K1 #d #e #H elim H -H L1 K1 d e [ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2/ diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_lift.ma index f779870fc..7ebd4af8c 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_lift.ma @@ -27,6 +27,7 @@ lemma tpr_lift: ∀T1,T2. T1 ⇒ T2 → lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1 [ lapply (lift_inv_sort1 … HU2) -HU2 #H destruct -U2 // | lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct -U2 // + | lapply (lift_inv_gref1 … HU2) -HU2 #H destruct -U2 // ] | #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2 elim (lift_inv_flat1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1; @@ -63,6 +64,7 @@ lemma tpr_inv_lift: ∀T1,T2. T1 ⇒ T2 → [ * #i #d #e #U1 #HU1 [ lapply (lift_inv_sort2 … HU1) -HU1 #H destruct -U1 /2/ | lapply (lift_inv_lref2 … HU1) -HU1 * * #Hid #H destruct -U1 /3/ + | lapply (lift_inv_gref2 … HU1) -HU1 #H destruct -U1 /2/ ] | #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X #HX elim (lift_inv_flat2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X; diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_tpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_tpss.ma index e56c4a9a5..9aaf5c423 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_tpss.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_tpss.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "Basic_2/unfold/ltpss_ltpss.ma". -include "Basic_2/reduction/ltpr_drop.ma". +include "Basic_2/reduction/ltpr_ldrop.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) @@ -27,7 +27,7 @@ lemma tpr_tps_ltpr: ∀T1,T2. T1 ⇒ T2 → elim (tps_inv_atom1 … H) -H [ #H destruct -X /2/ | * #K1 #V1 #i #Hdi #Hide #HLK1 #HVU1 #H #L2 #HL12 destruct -I; - elim (ltpr_drop_conf … HLK1 … HL12) -HLK1 HL12 #X #HLK2 #H + elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 HL12 #X #HLK2 #H elim (ltpr_inv_pair1 … H) -H #K2 #V2 #_ #HV12 #H destruct -X; elim (lift_total V2 0 (i+1)) #U2 #HVU2 lapply (tpr_lift … HV12 … HVU1 … HVU2) -HV12 HVU1 #HU12 diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/drop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/drop.ma deleted file mode 100644 index f3163abb2..000000000 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/drop.ma +++ /dev/null @@ -1,231 +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/grammar/lenv_weight.ma". -include "Basic_2/grammar/lsubs.ma". -include "Basic_2/substitution/lift.ma". - -(* DROPPING *****************************************************************) - -(* Basic_1: includes: drop_skip_bind *) -inductive drop: nat → nat → relation lenv ≝ -| drop_atom: ∀d,e. drop d e (⋆) (⋆) -| drop_pair: ∀L,I,V. drop 0 0 (L. 𝕓{I} V) (L. 𝕓{I} V) -| drop_drop: ∀L1,L2,I,V,e. drop 0 e L1 L2 → drop 0 (e + 1) (L1. 𝕓{I} V) L2 -| drop_skip: ∀L1,L2,I,V1,V2,d,e. - drop d e L1 L2 → ↑[d,e] V2 ≡ V1 → - drop (d + 1) e (L1. 𝕓{I} V1) (L2. 𝕓{I} V2) -. - -interpretation "dropping" 'RDrop d e L1 L2 = (drop d e L1 L2). - -(* Basic inversion lemmas ***************************************************) - -fact drop_inv_refl_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → e = 0 → L1 = L2. -#d #e #L1 #L2 * -d e L1 L2 -[ // -| // -| #L1 #L2 #I #V #e #_ #_ #H - elim (plus_S_eq_O_false … H) -| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H - elim (plus_S_eq_O_false … H) -] -qed. - -(* Basic_1: was: drop_gen_refl *) -lemma drop_inv_refl: ∀L1,L2. ↓[0, 0] L1 ≡ L2 → L1 = L2. -/2 width=5/ qed. - -fact drop_inv_atom1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → L1 = ⋆ → - L2 = ⋆. -#d #e #L1 #L2 * -d e L1 L2 -[ // -| #L #I #V #H destruct -| #L1 #L2 #I #V #e #_ #H destruct -| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct -] -qed. - -(* Basic_1: was: drop_gen_sort *) -lemma drop_inv_atom1: ∀d,e,L2. ↓[d, e] ⋆ ≡ L2 → L2 = ⋆. -/2 width=5/ qed. - -fact drop_inv_O1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → - ∀K,I,V. L1 = K. 𝕓{I} V → - (e = 0 ∧ L2 = K. 𝕓{I} V) ∨ - (0 < e ∧ ↓[d, e - 1] K ≡ L2). -#d #e #L1 #L2 * -d e L1 L2 -[ #d #e #_ #K #I #V #H destruct -| #L #I #V #_ #K #J #W #HX destruct -L I V /3/ -| #L1 #L2 #I #V #e #HL12 #_ #K #J #W #H destruct -L1 I V /3/ -| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H elim (plus_S_eq_O_false … H) -] -qed. - -lemma drop_inv_O1: ∀e,K,I,V,L2. ↓[0, e] K. 𝕓{I} V ≡ L2 → - (e = 0 ∧ L2 = K. 𝕓{I} V) ∨ - (0 < e ∧ ↓[0, e - 1] K ≡ L2). -/2/ qed. - -(* Basic_1: was: drop_gen_drop *) -lemma drop_inv_drop1: ∀e,K,I,V,L2. - ↓[0, e] K. 𝕓{I} V ≡ L2 → 0 < e → ↓[0, e - 1] K ≡ L2. -#e #K #I #V #L2 #H #He -elim (drop_inv_O1 … H) -H * // #H destruct -e; -elim (lt_refl_false … He) -qed. - -fact drop_inv_skip1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → - ∀I,K1,V1. L1 = K1. 𝕓{I} V1 → - ∃∃K2,V2. ↓[d - 1, e] K1 ≡ K2 & - ↑[d - 1, e] V2 ≡ V1 & - L2 = K2. 𝕓{I} V2. -#d #e #L1 #L2 * -d e L1 L2 -[ #d #e #_ #I #K #V #H destruct -| #L #I #V #H elim (lt_refl_false … H) -| #L1 #L2 #I #V #e #_ #H elim (lt_refl_false … H) -| #X #L2 #Y #Z #V2 #d #e #HL12 #HV12 #_ #I #L1 #V1 #H destruct -X Y Z - /2 width=5/ -] -qed. - -(* Basic_1: was: drop_gen_skip_l *) -lemma drop_inv_skip1: ∀d,e,I,K1,V1,L2. ↓[d, e] K1. 𝕓{I} V1 ≡ L2 → 0 < d → - ∃∃K2,V2. ↓[d - 1, e] K1 ≡ K2 & - ↑[d - 1, e] V2 ≡ V1 & - L2 = K2. 𝕓{I} V2. -/2/ qed. - -fact drop_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → - ∀I,K2,V2. L2 = K2. 𝕓{I} V2 → - ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 & - ↑[d - 1, e] V2 ≡ V1 & - L1 = K1. 𝕓{I} V1. -#d #e #L1 #L2 * -d e L1 L2 -[ #d #e #_ #I #K #V #H destruct -| #L #I #V #H elim (lt_refl_false … H) -| #L1 #L2 #I #V #e #_ #H elim (lt_refl_false … H) -| #L1 #X #Y #V1 #Z #d #e #HL12 #HV12 #_ #I #L2 #V2 #H destruct -X Y Z - /2 width=5/ -] -qed. - -(* Basic_1: was: drop_gen_skip_r *) -lemma drop_inv_skip2: ∀d,e,I,L1,K2,V2. ↓[d, e] L1 ≡ K2. 𝕓{I} V2 → 0 < d → - ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 & ↑[d - 1, e] V2 ≡ V1 & - L1 = K1. 𝕓{I} V1. -/2/ qed. - -(* Basic properties *********************************************************) - -(* Basic_1: was by definition: drop_refl *) -lemma drop_refl: ∀L. ↓[0, 0] L ≡ L. -#L elim L -L // -qed. - -lemma drop_drop_lt: ∀L1,L2,I,V,e. - ↓[0, e - 1] L1 ≡ L2 → 0 < e → ↓[0, e] L1. 𝕓{I} V ≡ L2. -#L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) /2/ -qed. - -lemma drop_lsubs_drop1_abbr: ∀L1,L2,d,e. L1 [d, e] ≼ L2 → - ∀K1,V,i. ↓[0, i] L1 ≡ K1. 𝕓{Abbr} V → - d ≤ i → i < d + e → - ∃∃K2. K1 [0, d + e - i - 1] ≼ K2 & - ↓[0, i] L2 ≡ K2. 𝕓{Abbr} V. -#L1 #L2 #d #e #H elim H -H L1 L2 d e -[ #d #e #K1 #V #i #H - lapply (drop_inv_atom1 … H) -H #H destruct -| #L1 #L2 #K1 #V #i #_ #_ #H - elim (lt_zero_false … H) -| #L1 #L2 #V #e #HL12 #IHL12 #K1 #W #i #H #_ #Hie - elim (drop_inv_O1 … H) -H * #Hi #HLK1 - [ -IHL12 Hie; destruct -i K1 W; - arith_g1 // /3/ - ] -| #L1 #L2 #I #V1 #V2 #e #_ #IHL12 #K1 #W #i #H #_ #Hie - elim (drop_inv_O1 … H) -H * #Hi #HLK1 - [ -IHL12 Hie Hi; destruct - | elim (IHL12 … HLK1 ? ?) -IHL12 HLK1 // [2: /2/ ] -Hie >arith_g1 // /3/ - ] -| #L1 #L2 #I1 #I2 #V1 #V2 #d #e #_ #IHL12 #K1 #V #i #H #Hdi >plus_plus_comm_23 #Hide - lapply (plus_S_le_to_pos … Hdi) #Hi - lapply (drop_inv_drop1 … H ?) -H // #HLK1 - elim (IHL12 … HLK1 ? ?) -IHL12 HLK1 [2: /2/ |3: /2/ ] -Hdi Hide >arith_g1 // /3/ -] -qed. - -(* Basic forvard lemmas *****************************************************) - -(* Basic_1: was: drop_S *) -lemma drop_fwd_drop2: ∀L1,I2,K2,V2,e. ↓[O, e] L1 ≡ K2. 𝕓{I2} V2 → - ↓[O, e + 1] L1 ≡ K2. -#L1 elim L1 -L1 -[ #I2 #K2 #V2 #e #H lapply (drop_inv_atom1 … H) -H #H destruct -| #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H - elim (drop_inv_O1 … H) -H * #He #H - [ -IHL1; destruct -e K2 I2 V2 /2/ - | @drop_drop >(plus_minus_m_m e 1) /2/ - ] -] -qed. - -lemma drop_fwd_lw: ∀L1,L2,d,e. ↓[d, e] L1 ≡ L2 → #[L2] ≤ #[L1]. -#L1 #L2 #d #e #H elim H -H L1 L2 d e // normalize -[ /2/ -| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12 - >(tw_lift … HV21) -HV21 /2/ -] -qed. - -lemma drop_fwd_drop2_length: ∀L1,I2,K2,V2,e. - ↓[0, e] L1 ≡ K2. 𝕓{I2} V2 → e < |L1|. -#L1 elim L1 -L1 -[ #I2 #K2 #V2 #e #H lapply (drop_inv_atom1 … H) -H #H destruct -| #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H - elim (drop_inv_O1 … H) -H * #He #H - [ -IHL1; destruct -e K2 I2 V2 // - | lapply (IHL1 … H) -IHL1 H #HeK1 whd in ⊢ (? ? %) /2/ - ] -] -qed. - -lemma drop_fwd_O1_length: ∀L1,L2,e. ↓[0, e] L1 ≡ L2 → |L2| = |L1| - e. -#L1 elim L1 -L1 -[ #L2 #e #H >(drop_inv_atom1 … H) -H // -| #K1 #I1 #V1 #IHL1 #L2 #e #H - elim (drop_inv_O1 … H) -H * #He #H - [ -IHL1; destruct -e L2 // - | lapply (IHL1 … H) -IHL1 H #H >H -H; normalize - >minus_le_minus_minus_comm // - ] -] -qed. - -(* Basic_1: removed theorems 49: - drop_skip_flat - cimp_flat_sx cimp_flat_dx cimp_bind cimp_getl_conf - drop_clear drop_clear_O drop_clear_S - clear_gen_sort clear_gen_bind clear_gen_flat clear_gen_flat_r - clear_gen_all clear_clear clear_mono clear_trans clear_ctail clear_cle - getl_ctail_clen getl_gen_tail clear_getl_trans getl_clear_trans - getl_clear_bind getl_clear_conf getl_dec getl_drop getl_drop_conf_lt - getl_drop_conf_ge getl_conf_ge_drop getl_drop_conf_rev - drop_getl_trans_lt drop_getl_trans_le drop_getl_trans_ge - getl_drop_trans getl_flt getl_gen_all getl_gen_sort getl_gen_O - getl_gen_S getl_gen_2 getl_gen_flat getl_gen_bind getl_conf_le - getl_trans getl_refl getl_head getl_flat getl_ctail getl_mono -*) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma new file mode 100644 index 000000000..838ef0fed --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma @@ -0,0 +1,231 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/lenv_weight.ma". +include "Basic_2/grammar/lsubs.ma". +include "Basic_2/substitution/lift.ma". + +(* DROPPING *****************************************************************) + +(* Basic_1: includes: ldrop_skip_bind *) +inductive ldrop: nat → nat → relation lenv ≝ +| ldrop_atom: ∀d,e. ldrop d e (⋆) (⋆) +| ldrop_pair: ∀L,I,V. ldrop 0 0 (L. 𝕓{I} V) (L. 𝕓{I} V) +| ldrop_ldrop: ∀L1,L2,I,V,e. ldrop 0 e L1 L2 → ldrop 0 (e + 1) (L1. 𝕓{I} V) L2 +| ldrop_skip: ∀L1,L2,I,V1,V2,d,e. + ldrop d e L1 L2 → ↑[d,e] V2 ≡ V1 → + ldrop (d + 1) e (L1. 𝕓{I} V1) (L2. 𝕓{I} V2) +. + +interpretation "ldropping" 'RDrop d e L1 L2 = (ldrop d e L1 L2). + +(* Basic inversion lemmas ***************************************************) + +fact ldrop_inv_refl_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → e = 0 → L1 = L2. +#d #e #L1 #L2 * -d e L1 L2 +[ // +| // +| #L1 #L2 #I #V #e #_ #_ #H + elim (plus_S_eq_O_false … H) +| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H + elim (plus_S_eq_O_false … H) +] +qed. + +(* Basic_1: was: ldrop_gen_refl *) +lemma ldrop_inv_refl: ∀L1,L2. ↓[0, 0] L1 ≡ L2 → L1 = L2. +/2 width=5/ qed. + +fact ldrop_inv_atom1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → L1 = ⋆ → + L2 = ⋆. +#d #e #L1 #L2 * -d e L1 L2 +[ // +| #L #I #V #H destruct +| #L1 #L2 #I #V #e #_ #H destruct +| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct +] +qed. + +(* Basic_1: was: ldrop_gen_sort *) +lemma ldrop_inv_atom1: ∀d,e,L2. ↓[d, e] ⋆ ≡ L2 → L2 = ⋆. +/2 width=5/ qed. + +fact ldrop_inv_O1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → + ∀K,I,V. L1 = K. 𝕓{I} V → + (e = 0 ∧ L2 = K. 𝕓{I} V) ∨ + (0 < e ∧ ↓[d, e - 1] K ≡ L2). +#d #e #L1 #L2 * -d e L1 L2 +[ #d #e #_ #K #I #V #H destruct +| #L #I #V #_ #K #J #W #HX destruct -L I V /3/ +| #L1 #L2 #I #V #e #HL12 #_ #K #J #W #H destruct -L1 I V /3/ +| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H elim (plus_S_eq_O_false … H) +] +qed. + +lemma ldrop_inv_O1: ∀e,K,I,V,L2. ↓[0, e] K. 𝕓{I} V ≡ L2 → + (e = 0 ∧ L2 = K. 𝕓{I} V) ∨ + (0 < e ∧ ↓[0, e - 1] K ≡ L2). +/2/ qed. + +(* Basic_1: was: ldrop_gen_ldrop *) +lemma ldrop_inv_ldrop1: ∀e,K,I,V,L2. + ↓[0, e] K. 𝕓{I} V ≡ L2 → 0 < e → ↓[0, e - 1] K ≡ L2. +#e #K #I #V #L2 #H #He +elim (ldrop_inv_O1 … H) -H * // #H destruct -e; +elim (lt_refl_false … He) +qed. + +fact ldrop_inv_skip1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → + ∀I,K1,V1. L1 = K1. 𝕓{I} V1 → + ∃∃K2,V2. ↓[d - 1, e] K1 ≡ K2 & + ↑[d - 1, e] V2 ≡ V1 & + L2 = K2. 𝕓{I} V2. +#d #e #L1 #L2 * -d e L1 L2 +[ #d #e #_ #I #K #V #H destruct +| #L #I #V #H elim (lt_refl_false … H) +| #L1 #L2 #I #V #e #_ #H elim (lt_refl_false … H) +| #X #L2 #Y #Z #V2 #d #e #HL12 #HV12 #_ #I #L1 #V1 #H destruct -X Y Z + /2 width=5/ +] +qed. + +(* Basic_1: was: ldrop_gen_skip_l *) +lemma ldrop_inv_skip1: ∀d,e,I,K1,V1,L2. ↓[d, e] K1. 𝕓{I} V1 ≡ L2 → 0 < d → + ∃∃K2,V2. ↓[d - 1, e] K1 ≡ K2 & + ↑[d - 1, e] V2 ≡ V1 & + L2 = K2. 𝕓{I} V2. +/2/ qed. + +fact ldrop_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → + ∀I,K2,V2. L2 = K2. 𝕓{I} V2 → + ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 & + ↑[d - 1, e] V2 ≡ V1 & + L1 = K1. 𝕓{I} V1. +#d #e #L1 #L2 * -d e L1 L2 +[ #d #e #_ #I #K #V #H destruct +| #L #I #V #H elim (lt_refl_false … H) +| #L1 #L2 #I #V #e #_ #H elim (lt_refl_false … H) +| #L1 #X #Y #V1 #Z #d #e #HL12 #HV12 #_ #I #L2 #V2 #H destruct -X Y Z + /2 width=5/ +] +qed. + +(* Basic_1: was: ldrop_gen_skip_r *) +lemma ldrop_inv_skip2: ∀d,e,I,L1,K2,V2. ↓[d, e] L1 ≡ K2. 𝕓{I} V2 → 0 < d → + ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 & ↑[d - 1, e] V2 ≡ V1 & + L1 = K1. 𝕓{I} V1. +/2/ qed. + +(* Basic properties *********************************************************) + +(* Basic_1: was by definition: ldrop_refl *) +lemma ldrop_refl: ∀L. ↓[0, 0] L ≡ L. +#L elim L -L // +qed. + +lemma ldrop_ldrop_lt: ∀L1,L2,I,V,e. + ↓[0, e - 1] L1 ≡ L2 → 0 < e → ↓[0, e] L1. 𝕓{I} V ≡ L2. +#L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) /2/ +qed. + +lemma ldrop_lsubs_ldrop1_abbr: ∀L1,L2,d,e. L1 [d, e] ≼ L2 → + ∀K1,V,i. ↓[0, i] L1 ≡ K1. 𝕓{Abbr} V → + d ≤ i → i < d + e → + ∃∃K2. K1 [0, d + e - i - 1] ≼ K2 & + ↓[0, i] L2 ≡ K2. 𝕓{Abbr} V. +#L1 #L2 #d #e #H elim H -H L1 L2 d e +[ #d #e #K1 #V #i #H + lapply (ldrop_inv_atom1 … H) -H #H destruct +| #L1 #L2 #K1 #V #i #_ #_ #H + elim (lt_zero_false … H) +| #L1 #L2 #V #e #HL12 #IHL12 #K1 #W #i #H #_ #Hie + elim (ldrop_inv_O1 … H) -H * #Hi #HLK1 + [ -IHL12 Hie; destruct -i K1 W; + arith_g1 // /3/ + ] +| #L1 #L2 #I #V1 #V2 #e #_ #IHL12 #K1 #W #i #H #_ #Hie + elim (ldrop_inv_O1 … H) -H * #Hi #HLK1 + [ -IHL12 Hie Hi; destruct + | elim (IHL12 … HLK1 ? ?) -IHL12 HLK1 // [2: /2/ ] -Hie >arith_g1 // /3/ + ] +| #L1 #L2 #I1 #I2 #V1 #V2 #d #e #_ #IHL12 #K1 #V #i #H #Hdi >plus_plus_comm_23 #Hide + lapply (plus_S_le_to_pos … Hdi) #Hi + lapply (ldrop_inv_ldrop1 … H ?) -H // #HLK1 + elim (IHL12 … HLK1 ? ?) -IHL12 HLK1 [2: /2/ |3: /2/ ] -Hdi Hide >arith_g1 // /3/ +] +qed. + +(* Basic forvard lemmas *****************************************************) + +(* Basic_1: was: ldrop_S *) +lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ↓[O, e] L1 ≡ K2. 𝕓{I2} V2 → + ↓[O, e + 1] L1 ≡ K2. +#L1 elim L1 -L1 +[ #I2 #K2 #V2 #e #H lapply (ldrop_inv_atom1 … H) -H #H destruct +| #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H + elim (ldrop_inv_O1 … H) -H * #He #H + [ -IHL1; destruct -e K2 I2 V2 /2/ + | @ldrop_ldrop >(plus_minus_m_m e 1) /2/ + ] +] +qed. + +lemma ldrop_fwd_lw: ∀L1,L2,d,e. ↓[d, e] L1 ≡ L2 → #[L2] ≤ #[L1]. +#L1 #L2 #d #e #H elim H -H L1 L2 d e // normalize +[ /2/ +| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12 + >(tw_lift … HV21) -HV21 /2/ +] +qed. + +lemma ldrop_fwd_ldrop2_length: ∀L1,I2,K2,V2,e. + ↓[0, e] L1 ≡ K2. 𝕓{I2} V2 → e < |L1|. +#L1 elim L1 -L1 +[ #I2 #K2 #V2 #e #H lapply (ldrop_inv_atom1 … H) -H #H destruct +| #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H + elim (ldrop_inv_O1 … H) -H * #He #H + [ -IHL1; destruct -e K2 I2 V2 // + | lapply (IHL1 … H) -IHL1 H #HeK1 whd in ⊢ (? ? %) /2/ + ] +] +qed. + +lemma ldrop_fwd_O1_length: ∀L1,L2,e. ↓[0, e] L1 ≡ L2 → |L2| = |L1| - e. +#L1 elim L1 -L1 +[ #L2 #e #H >(ldrop_inv_atom1 … H) -H // +| #K1 #I1 #V1 #IHL1 #L2 #e #H + elim (ldrop_inv_O1 … H) -H * #He #H + [ -IHL1; destruct -e L2 // + | lapply (IHL1 … H) -IHL1 H #H >H -H; normalize + >minus_le_minus_minus_comm // + ] +] +qed. + +(* Basic_1: removed theorems 49: + ldrop_skip_flat + cimp_flat_sx cimp_flat_dx cimp_bind cimp_getl_conf + ldrop_clear ldrop_clear_O ldrop_clear_S + clear_gen_sort clear_gen_bind clear_gen_flat clear_gen_flat_r + clear_gen_all clear_clear clear_mono clear_trans clear_ctail clear_cle + getl_ctail_clen getl_gen_tail clear_getl_trans getl_clear_trans + getl_clear_bind getl_clear_conf getl_dec getl_ldrop getl_ldrop_conf_lt + getl_ldrop_conf_ge getl_conf_ge_ldrop getl_ldrop_conf_rev + ldrop_getl_trans_lt ldrop_getl_trans_le ldrop_getl_trans_ge + getl_ldrop_trans getl_flt getl_gen_all getl_gen_sort getl_gen_O + getl_gen_S getl_gen_2 getl_gen_flat getl_gen_bind getl_conf_le + getl_trans getl_refl getl_head getl_flat getl_ctail getl_mono +*) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/drop_drop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma similarity index 55% rename from matita/matita/contribs/lambda_delta/Basic_2/substitution/drop_drop.ma rename to matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma index b8a790fb5..1af7c0db8 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/drop_drop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma @@ -13,63 +13,63 @@ (**************************************************************************) include "Basic_2/substitution/lift_lift.ma". -include "Basic_2/substitution/drop.ma". +include "Basic_2/substitution/ldrop.ma". (* DROPPING *****************************************************************) (* Main properties **********************************************************) -(* Basic_1: was: drop_mono *) -theorem drop_mono: ∀d,e,L,L1. ↓[d, e] L ≡ L1 → - ∀L2. ↓[d, e] L ≡ L2 → L1 = L2. +(* Basic_1: was: ldrop_mono *) +theorem ldrop_mono: ∀d,e,L,L1. ↓[d, e] L ≡ L1 → + ∀L2. ↓[d, e] L ≡ L2 → L1 = L2. #d #e #L #L1 #H elim H -H d e L L1 [ #d #e #L2 #H - >(drop_inv_atom1 … H) -H L2 // + >(ldrop_inv_atom1 … H) -H L2 // | #K #I #V #L2 #HL12 - <(drop_inv_refl … HL12) -HL12 L2 // + <(ldrop_inv_refl … HL12) -HL12 L2 // | #L #K #I #V #e #_ #IHLK #L2 #H - lapply (drop_inv_drop1 … H ?) -H /2/ + lapply (ldrop_inv_ldrop1 … H ?) -H /2/ | #L #K1 #I #T #V1 #d #e #_ #HVT1 #IHLK1 #X #H - elim (drop_inv_skip1 … H ?) -H // (lift_inj … HVT1 … HVT2) -HVT1 HVT2 >(IHLK1 … HLK2) -IHLK1 HLK2 // ] qed. -(* Basic_1: was: drop_conf_ge *) -theorem drop_conf_ge: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 → - ∀e2,L2. ↓[0, e2] L ≡ L2 → d1 + e1 ≤ e2 → - ↓[0, e2 - e1] L1 ≡ L2. +(* Basic_1: was: ldrop_conf_ge *) +theorem ldrop_conf_ge: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 → + ∀e2,L2. ↓[0, e2] L ≡ L2 → d1 + e1 ≤ e2 → + ↓[0, e2 - e1] L1 ≡ L2. #d1 #e1 #L #L1 #H elim H -H d1 e1 L L1 [ #d #e #e2 #L2 #H - >(drop_inv_atom1 … H) -H L2 // + >(ldrop_inv_atom1 … H) -H L2 // | // | #L #K #I #V #e #_ #IHLK #e2 #L2 #H #He2 - lapply (drop_inv_drop1 … H ?) -H /2/ #HL2 + lapply (ldrop_inv_ldrop1 … H ?) -H /2/ #HL2 minus_minus_comm /3/ (**) (* explicit constructor *) + @ldrop_ldrop_lt >minus_minus_comm /3/ (**) (* explicit constructor *) ] qed. -(* Basic_1: was: drop_conf_lt *) -theorem drop_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. +(* Basic_1: was: ldrop_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 -H d1 e1 L L1 [ #d #e #e2 #K2 #I #V2 #H - lapply (drop_inv_atom1 … H) -H #H destruct + 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 - elim (drop_inv_O1 … H) -H * + elim (ldrop_inv_O1 … H) -H * [ -IHL12 He2d #H1 #H2 destruct -e2 K2 J V /2 width=5/ | -HL12 -HV12 #He #HLK elim (IHL12 … HLK ?) -IHL12 HLK [ (drop_inv_atom1 … H) -H L2 /2/ + >(ldrop_inv_atom1 … H) -H L2 /2/ | #K #I #V #e2 #L2 #HL2 #H lapply (le_O_to_eq_O … H) -H #H destruct -e2 /2/ | #L1 #L2 #I #V #e #_ #IHL12 #e2 #L #HL2 #H lapply (le_O_to_eq_O … H) -H #H destruct -e2; elim (IHL12 … HL2 ?) -IHL12 HL2 // #L0 #H #HL0 - lapply (drop_inv_refl … H) -H #H destruct -L1 /3 width=5/ + lapply (ldrop_inv_refl … H) -H #H destruct -L1 /3 width=5/ | #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #IHL12 #e2 #L #H #He2d - elim (drop_inv_O1 … H) -H * + elim (ldrop_inv_O1 … H) -H * [ -He2d IHL12 #H1 #H2 destruct -e2 L /3 width=5/ | -HL12 HV12 #He2 #HL2 elim (IHL12 … HL2 ?) -IHL12 HL2 L2 @@ -100,28 +100,28 @@ theorem drop_trans_le: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L → ] qed. -(* Basic_1: was: drop_trans_ge *) -theorem drop_trans_ge: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L → - ∀e2,L2. ↓[0, e2] L ≡ L2 → d1 ≤ e2 → ↓[0, e1 + e2] L1 ≡ L2. +(* Basic_1: was: ldrop_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 -H d1 e1 L1 L [ #d #e #e2 #L2 #H - >(drop_inv_atom1 … H) -H L2 // + >(ldrop_inv_atom1 … H) -H L2 // | // | /3/ | #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 (drop_inv_drop1 … H ?) -H // #HL2 - @drop_drop_lt // >le_plus_minus // @IHL12 /2/ (**) (* explicit constructor *) + lapply (ldrop_inv_ldrop1 … H ?) -H // #HL2 + @ldrop_ldrop_lt // >le_plus_minus // @IHL12 /2/ (**) (* explicit constructor *) ] qed. -theorem drop_trans_ge_comm: ∀d1,e1,e2,L1,L2,L. - ↓[d1, e1] L1 ≡ L → ↓[0, e2] L ≡ L2 → d1 ≤ e2 → - ↓[0, e2 + e1] L1 ≡ L2. +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. #e1 #e1 #e2 >commutative_plus /2 width=5/ qed. -(* Basic_1: was: drop_conf_rev *) -axiom drop_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: ldrop_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/substitution/lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma index 5f16e9aaf..1934c37bc 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma @@ -23,6 +23,7 @@ inductive lift: nat → nat → relation term ≝ | lift_sort : ∀k,d,e. lift d e (⋆k) (⋆k) | lift_lref_lt: ∀i,d,e. i < d → lift d e (#i) (#i) | lift_lref_ge: ∀i,d,e. d ≤ i → lift d e (#i) (#(i + e)) +| lift_gref : ∀p,d,e. lift d e (§p) (§p) | lift_bind : ∀I,V1,V2,T1,T2,d,e. lift d e V1 V2 → lift (d + 1) e T1 T2 → lift d e (𝕓{I} V1. T1) (𝕓{I} V2. T2) @@ -70,6 +71,7 @@ lemma lift_split: ∀d1,e2,T1,T2. ↑[d1, e2] T1 ≡ T2 → ∀d2,e1. | #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12 lapply (transitive_le …(i+e1) Hd21 ?) /2/ -Hd21 #Hd21 <(arith_d1 i e2 e1) // /3/ +| /3/ | #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12 elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b elim (IHT (d2+1) … ? ? He12) /3 width = 5/ @@ -111,6 +113,7 @@ fact lift_inv_lref1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T1 = #i → [ #k #d #e #i #H destruct | #j #d #e #Hj #i #Hi destruct /3/ | #j #d #e #Hj #i #Hi destruct /3/ +| #p #d #e #i #H destruct | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct ] @@ -132,6 +135,17 @@ lemma lift_inv_lref1_ge: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 → d ≤ i → T2 = #( elim (lt_refl_false … Hdd) qed. +fact lift_inv_gref1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀p. T1 = §p → T2 = §p. +#d #e #T1 #T2 * -d e T1 T2 // +[ #i #d #e #_ #k #H destruct +| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct +| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct +] +qed. + +lemma lift_inv_gref1: ∀d,e,T2,p. ↑[d,e] §p ≡ T2 → T2 = §p. +/2 width=5/ qed. + fact lift_inv_bind1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀I,V1,U1. T1 = 𝕓{I} V1.U1 → ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 & @@ -140,6 +154,7 @@ fact lift_inv_bind1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → [ #k #d #e #I #V1 #U1 #H destruct | #i #d #e #_ #I #V1 #U1 #H destruct | #i #d #e #_ #I #V1 #U1 #H destruct +| #p #d #e #I #V1 #U1 #H destruct | #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V1 #U1 #H destruct /2 width=5/ | #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V1 #U1 #H destruct ] @@ -158,6 +173,7 @@ fact lift_inv_flat1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → [ #k #d #e #I #V1 #U1 #H destruct | #i #d #e #_ #I #V1 #U1 #H destruct | #i #d #e #_ #I #V1 #U1 #H destruct +| #p #d #e #I #V1 #U1 #H destruct | #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V1 #U1 #H destruct | #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V1 #U1 #H destruct /2 width=5/ ] @@ -186,6 +202,7 @@ fact lift_inv_lref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T2 = #i → [ #k #d #e #i #H destruct | #j #d #e #Hj #i #Hi destruct /3/ | #j #d #e #Hj #i #Hi destruct le_plus_minus_comm [ @lift_lref_ge @(transitive_le … Hd12) -Hd12 /2/ | -Hd12 /2/ ] - | -Hd12 >(plus_minus_m_m i e2) in ⊢ (? ? ? ? %) /3/ + | -Hd12 >(plus_minus_m_m i e2) in ⊢ (? ? ? ? %) /2/ /3/ ] ] +| #p #d1 #e1 #d2 #e2 #T2 #Hk #Hd12 + lapply (lift_inv_gref2 … Hk) -Hk #Hk destruct -T2 /3/ | #I #W1 #W #U1 #U #d1 #e1 #_ #_ #IHW #IHU #d2 #e2 #T2 #H #Hd12 lapply (lift_inv_bind2 … H) -H * #W2 #U2 #HW2 #HU2 #H destruct -T2; elim (IHW … HW2 ?) // -IHW HW2 #W0 #HW2 #HW1 - >plus_plus_comm_23 in HU2 #HU2 elim (IHU … HU2 ?) /3 width = 5/ + >plus_plus_comm_23 in HU2 #HU2 elim (IHU … HU2 ?) /2/ /3 width = 5/ | #I #W1 #W #U1 #U #d1 #e1 #_ #_ #IHW #IHU #d2 #e2 #T2 #H #Hd12 lapply (lift_inv_flat2 … H) -H * #W2 #U2 #HW2 #HU2 #H destruct -T2; elim (IHW … HW2 ?) // -IHW HW2 #W0 #HW2 #HW1 - elim (IHU … HU2 ?) /3 width = 5/ + elim (IHU … HU2 ?) // /3 width = 5/ ] qed. @@ -73,6 +77,8 @@ theorem lift_mono: ∀d,e,T,U1. ↑[d,e] T ≡ U1 → ∀U2. ↑[d,e] T ≡ U2 lapply (lift_inv_lref1_lt … HX ?) -HX // | #i #d #e #Hdi #X #HX lapply (lift_inv_lref1_ge … HX ?) -HX // +| #p #d #e #X #HX + lapply (lift_inv_gref1 … HX) -HX // | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX elim (lift_inv_bind1 … HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/ | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX @@ -95,6 +101,8 @@ theorem lift_trans_be: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → [ @(transitive_le … Hd21 ?) -Hd21 /2/ | -Hd21 /2/ ] +| #p #d1 #e1 #d2 #e2 #T2 #HT2 #_ #_ + >(lift_inv_gref1 … HT2) -HT2 // | #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd12 #Hd21 elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X; lapply (IHV12 … HV20 ? ?) // -IHV12 HV20 #HV10 @@ -102,7 +110,7 @@ theorem lift_trans_be: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → | #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd12 #Hd21 elim (lift_inv_flat1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X; lapply (IHV12 … HV20 ? ?) // -IHV12 HV20 #HV10 - lapply (IHT12 … HT20 ? ?) /2/ + lapply (IHT12 … HT20 ? ?) // /2/ ] qed. @@ -115,19 +123,21 @@ theorem lift_trans_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → >(lift_inv_sort1 … HX) -HX /2/ | #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #_ lapply (lt_to_le_to_lt … (d1+e2) Hid1 ?) // #Hie2 - elim (lift_inv_lref1 … HX) -HX * #Hid2 #HX destruct -X /4/ + elim (lift_inv_lref1 … HX) -HX * #Hid2 #HX destruct -X /3/ /4/ | #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #Hd21 lapply (transitive_le … Hd21 Hid1) -Hd21 #Hid2 lapply (lift_inv_lref1_ge … HX ?) -HX /2/ #HX destruct -X; >plus_plus_comm_23 /4/ +| #p #d1 #e1 #d2 #e2 #X #HX #_ + >(lift_inv_gref1 … HX) -HX /2/ | #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd21 elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X; elim (IHV12 … HV20 ?) -IHV12 HV20 // - elim (IHT12 … HT20 ?) -IHT12 HT20 /3 width=5/ + elim (IHT12 … HT20 ?) -IHT12 HT20 /2/ /3 width=5/ | #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd21 elim (lift_inv_flat1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X; elim (IHV12 … HV20 ?) -IHV12 HV20 // - elim (IHT12 … HT20 ?) -IHT12 HT20 /3 width=5/ + elim (IHT12 … HT20 ?) -IHT12 HT20 // /3 width=5/ ] qed. @@ -145,15 +155,17 @@ theorem lift_trans_ge: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → lapply (lift_inv_lref1_lt … HX ?) -HX // #HX destruct -X /3/ | #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #_ elim (lift_inv_lref1 … HX) -HX * #Hied #HX destruct -X; - [2: >plus_plus_comm_23] /4/ + [ /4/ | >plus_plus_comm_23 /4/ ] +| #p #d1 #e1 #d2 #e2 #X #HX #_ + >(lift_inv_gref1 … HX) -HX /2/ | #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hded elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X; elim (IHV12 … HV20 ?) -IHV12 HV20 // elim (IHT12 … HT20 ?) -IHT12 HT20 /2/ #T - (drop_inv_atom1 … H) -H // +[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H // | // | normalize #K0 #K1 #I #V0 #V1 #e1 #_ #_ #IHK01 #L2 #e2 #H #He12 lapply (plus_le_weak … He12) #He2 - lapply (drop_inv_drop1 … H ?) -H // #HK0L2 + lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2 lapply (IHK01 … HK0L2 ?) -IHK01 HK0L2 /2/ | #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2 lapply (plus_le_weak … Hd1e2) #He2 - lapply (drop_inv_drop1 … H ?) -H // #HK0L2 + lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2 lapply (IHK01 … HK0L2 ?) -IHK01 HK0L2 /2/ ] qed. -lemma ltps_drop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 → +lemma ltps_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 -H L1 L0 d1 e1 -[ #d1 #e1 #L2 #e2 #H >(drop_inv_atom1 … H) -H // +[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H // | // | normalize #K1 #K0 #I #V1 #V0 #e1 #_ #_ #IHK10 #L2 #e2 #H #He12 lapply (plus_le_weak … He12) #He2 - lapply (drop_inv_drop1 … H ?) -H // #HK0L2 + lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2 lapply (IHK10 … HK0L2 ?) -IHK10 HK0L2 /2/ | #K0 #K1 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2 lapply (plus_le_weak … Hd1e2) #He2 - lapply (drop_inv_drop1 … H ?) -H // #HK0L2 + lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2 lapply (IHK10 … HK0L2 ?) -IHK10 HK0L2 /2/ ] qed. -lemma ltps_drop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → +lemma ltps_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 -H L0 L1 d1 e1 -[ #d1 #e1 #L2 #e2 #H >(drop_inv_atom1 … H) -H /2/ +[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2/ | normalize #L #I #V #L2 #e2 #HL2 #_ #He2 lapply (le_n_O_to_eq … He2) -He2 #H destruct -e2; - lapply (drop_inv_refl … HL2) -HL2 #H destruct -L2 /2/ + lapply (ldrop_inv_refl … HL2) -HL2 #H destruct -L2 /2/ | normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #_ #He21 - lapply (drop_inv_O1 … H) -H * * #He2 #HK0L2 + lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2 [ destruct -IHK01 He21 e2 L2 plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2 #He2de1 lapply (plus_le_weak … Hd1e2) #He2 (drop_inv_atom1 … H) -H /2/ +[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2/ | normalize #L #I #V #L2 #e2 #HL2 #_ #He2 lapply (le_n_O_to_eq … He2) -He2 #H destruct -e2; - lapply (drop_inv_refl … HL2) -HL2 #H destruct -L2 /2/ + lapply (ldrop_inv_refl … HL2) -HL2 #H destruct -L2 /2/ | normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #_ #He21 - lapply (drop_inv_O1 … H) -H * * #He2 #HK0L2 + lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2 [ destruct -IHK10 He21 e2 L2 plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2 #He2de1 lapply (plus_le_weak … Hd1e2) #He2 (drop_inv_atom1 … H) -H /2/ +[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2/ | /2/ | normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #_ #L2 #e2 #H #He2 lapply (le_n_O_to_eq … He2) -He2 #He2 destruct -e2; - lapply (drop_inv_refl … H) -H #H destruct -L2 /3/ + lapply (ldrop_inv_refl … H) -H #H destruct -L2 /3/ | #K0 #K1 #I #V0 #V1 #d1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #He2d1 - lapply (drop_inv_O1 … H) -H * * #He2 #HK0L2 + lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2 [ destruct -IHK01 He2d1 e2 L2 (drop_inv_atom1 … H) -H /2/ +[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2/ | /2/ | normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #_ #L2 #e2 #H #He2 lapply (le_n_O_to_eq … He2) -He2 #He2 destruct -e2; - lapply (drop_inv_refl … H) -H #H destruct -L2 /3/ + lapply (ldrop_inv_refl … H) -H #H destruct -L2 /3/ | #K1 #K0 #I #V1 #V0 #d1 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #He2d1 - lapply (drop_inv_O1 … H) -H * * #He2 #HK0L2 + lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2 [ destruct -IHK10 He2d1 e2 L2 arith_a2 /3/ | elim (lt_or_ge i2 (d1 + e1)) #Hde1i2 - [ elim (ltps_drop_conf_be … HL01 … HLK0 ? ?) -HL01 HLK0 [2,3: /2/ ] #X #H #HLK1 + [ elim (ltps_ldrop_conf_be … HL01 … HLK0 ? ?) -HL01 HLK0 [2,3: /2/ ] #X #H #HLK1 elim (ltps_inv_tps21 … H ?) -H [2: /2/ ] #K1 #V1 #_ #HV01 #H destruct -X; - lapply (drop_fwd_drop2 … HLK1) #H + lapply (ldrop_fwd_ldrop2 … HLK1) #H elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1 lapply (tps_lift_ge … HV01 … H HVW0 HVW1 ?) -H HV01 HVW0 // normalize #HW01 lapply (tps_weak … HW01 d1 e1 ? ?) [2,3: /3/ ] >arith_i2 // - | lapply (ltps_drop_conf_ge … HL01 … HLK0 ?) -HL01 HLK0 /3/ + | lapply (ltps_ldrop_conf_ge … HL01 … HLK0 ?) -HL01 HLK0 /3/ ] ] | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01 @@ -71,7 +71,7 @@ lemma ltps_tps_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 → [ // | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10 #Hde1d2 lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2 - lapply (ltps_drop_trans_ge … HL10 … HLK0 ?) -HL10 HLK0 /2/ + lapply (ltps_ldrop_trans_ge … HL10 … HLK0 ?) -HL10 HLK0 /2/ | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 #Hde1d2 @tps_bind [ /2/ | @IHTU2 [3: /2/ |1,2: skip | /2/ ] ] (**) (* /3/ is too slow *) | /3/ @@ -87,19 +87,19 @@ lemma ltps_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 → [ /2/ | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10 elim (lt_or_ge i2 d1) #Hi2d1 - [ elim (ltps_drop_trans_le … HL10 … HLK0 ?) -HL10 /2/ #X #H #HLK1 + [ elim (ltps_ldrop_trans_le … HL10 … HLK0 ?) -HL10 /2/ #X #H #HLK1 elim (ltps_inv_tps12 … H ?) -H [2: /2/ ] #K1 #V1 #_ #HV01 #H destruct -X; - lapply (drop_fwd_drop2 … HLK0) -HLK0 #H + lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #H elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1 lapply (tps_lift_ge … HV01 … H HVW1 HVW0 ?) -H HV01 HVW0 // >arith_a2 /3/ | elim (lt_or_ge i2 (d1 + e1)) #Hde1i2 - [ elim (ltps_drop_trans_be … HL10 … HLK0 ? ?) -HL10 [2,3: /2/ ] #X #H #HLK1 + [ elim (ltps_ldrop_trans_be … HL10 … HLK0 ? ?) -HL10 [2,3: /2/ ] #X #H #HLK1 elim (ltps_inv_tps22 … H ?) -H [2: /2/ ] #K1 #V1 #_ #HV01 #H destruct -X; - lapply (drop_fwd_drop2 … HLK0) -HLK0 #H + lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #H elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1 lapply (tps_lift_ge … HV01 … H HVW1 HVW0 ?) -H HV01 HVW0 // normalize #HW01 lapply (tps_weak … HW01 d1 e1 ? ?) [2,3: /3/ ] >arith_i2 // - | lapply (ltps_drop_trans_ge … HL10 … HLK0 ?) -HL10 HLK0 /3/ + | lapply (ltps_ldrop_trans_ge … HL10 … HLK0 ?) -HL10 HLK0 /3/ ] ] | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma index f364dda8b..7ab9fba13 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "Basic_2/grammar/cl_weight.ma". -include "Basic_2/substitution/drop.ma". +include "Basic_2/substitution/ldrop.ma". (* PARALLEL SUBSTITUTION ON TERMS *******************************************) @@ -39,7 +39,7 @@ lemma tps_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫ T2 → #L1 #T1 #T2 #d #e #H elim H -H L1 T1 T2 d e [ // | #L1 #K1 #V #W #i #d #e #Hdi #Hide #HLK1 #HVW #L2 #HL12 - elim (drop_lsubs_drop1_abbr … HL12 … HLK1 ? ?) -HL12 HLK1 // /2/ + elim (ldrop_lsubs_ldrop1_abbr … HL12 … HLK1 ? ?) -HL12 HLK1 // /2/ | /4/ | /3/ ] @@ -68,7 +68,7 @@ lemma tps_weak_top: ∀L,T1,T2,d,e. #L #T1 #T2 #d #e #H elim H -H L T1 T2 d e [ // | #L #K #V #W #i #d #e #Hdi #_ #HLK #HVW - lapply (drop_fwd_drop2_length … HLK) #Hi + lapply (ldrop_fwd_ldrop2_length … HLK) #Hi lapply (le_to_lt_to_lt … Hdi Hi) #Hd lapply (plus_minus_m_m_comm (|L|) d ?) /2/ | normalize /2/ diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_lift.ma index e7243c212..35cff3372 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_lift.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/drop_drop.ma". +include "Basic_2/substitution/ldrop_ldrop.ma". include "Basic_2/substitution/tps.ma". (* PARTIAL SUBSTITUTION ON TERMS ********************************************) @@ -25,9 +25,9 @@ fact tps_inv_refl_SO2_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → e = 1 → [ // | #L #K0 #V0 #W #i #d #e #Hdi #Hide #HLK0 #_ #H destruct -e; >(le_to_le_to_eq … Hdi ?) /2/ -d #K #V #HLK - lapply (drop_mono … HLK0 … HLK) #H destruct + lapply (ldrop_mono … HLK0 … HLK) #H destruct | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #H1 #K #V #HLK - >(IHV12 H1 … HLK) -IHV12 >(IHT12 H1 K V) -IHT12 /2/ + >(IHV12 H1 … HLK) -IHV12 >(IHT12 H1 K V) -IHT12 // /2/ | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #H1 #K #V #HLK >(IHV12 H1 … HLK) -IHV12 >(IHT12 H1 … HLK) -IHT12 // ] @@ -48,17 +48,49 @@ lemma tps_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 → #K #T1 #T2 #dt #et #H elim H -H K T1 T2 dt et [ #K #I #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_ >(lift_mono … H1 … H2) -H1 H2 // -| #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #d #e #HLK #H #HVU2 #Hdetd +| #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #d #e #HLK #H #HWU2 #Hdetd lapply (lt_to_le_to_lt … Hidet … Hdetd) -Hdetd #Hid lapply (lift_inv_lref1_lt … H … Hid) -H #H destruct -U1; - elim (lift_trans_ge … HVW … HVU2 ?) -HVW HVU2 W // (lift_mono … HVY … HVW) -HVY HVW Y #H destruct -X /2/ | #K #I #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdetd elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct -U1 U2; - @tps_bind [ /2 width=6/ | @IHT12 [3,4,5: /2/ |1,2: skip | /2/ ] ] (**) (* /3 width=6/ is too slow, arith3 needed to avoid crash *) + @tps_bind [ /2 width=6/ | @IHT12 [4,5: // |1,2: skip | /2/ | /2/ ] ] (**) (* /3 width=6/ is too slow, arith3 needed to avoid crash *) +| #K #I #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdetd + elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 + elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct -U1 U2; + /3 width=6/ +] +qed. + +lemma tps_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 → + ∀L,U1,U2,d,e. ↓[d, e] L ≡ K → + ↑[d, e] T1 ≡ U1 → ↑[d, e] T2 ≡ U2 → + dt ≤ d → d ≤ dt + et → + L ⊢ U1 [dt, et + e] ≫ U2. +#K #T1 #T2 #dt #et #H elim H -H K T1 T2 dt et +[ #K #I #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_ #_ + >(lift_mono … H1 … H2) -H1 H2 // +| #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #d #e #HLK #H #HWU2 #Hdtd #_ + elim (lift_inv_lref1 … H) -H * #Hid #H destruct -U1; + [ -Hdtd; + lapply (lt_to_le_to_lt … (dt+et+e) Hidet ?) // -Hidet #Hidete + elim (lift_trans_ge … HVW … HWU2 ?) -W // (lift_mono … HVY … HVW) -V #H destruct -X /2/ + | -Hdti; + lapply (transitive_le … Hdtd Hid) -Hdtd #Hdti + lapply (lift_trans_be … HVW … HWU2 ? ?) -W // [ /2/ ] >plus_plus_comm_23 #HVU2 + lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hid /3/ + ] +| #K #I #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdtd #Hddet + elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 + elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct -U1 U2; + @tps_bind [ /2 width=6/ | @IHT12 [3,4: // | skip |5,6: /2/ | /2/ ] ] (**) (* /3 width=6/ is too slow, arith3 needed to avoid crash *) | #K #I #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdetd elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct -U1 U2; @@ -79,7 +111,7 @@ lemma tps_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 → lapply (transitive_le … Hddt … Hdti) -Hddt #Hid lapply (lift_inv_lref1_ge … H … Hid) -H #H destruct -U1; lapply (lift_trans_be … HVW … HWU2 ? ?) -HVW HWU2 W // [ /2/ ] >plus_plus_comm_23 #HVU2 - lapply (drop_trans_ge_comm … HLK … HKV ?) -HLK HKV K // -Hid /3/ + lapply (ldrop_trans_ge_comm … HLK … HKV ?) -HLK HKV K // -Hid /3/ | #K #I #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hddt elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct -U1 U2; @@ -100,16 +132,17 @@ lemma tps_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → [ #L * #i #dt #et #K #d #e #_ #T1 #H #_ [ lapply (lift_inv_sort2 … H) -H #H destruct -T1 /2/ | elim (lift_inv_lref2 … H) -H * #Hid #H destruct -T1 /3/ + | lapply (lift_inv_gref2 … H) -H #H destruct -T1 /2/ ] | #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdetd lapply (lt_to_le_to_lt … Hidet … Hdetd) -Hdetd #Hid lapply (lift_inv_lref2_lt … H … Hid) -H #H destruct -T1; - elim (drop_conf_lt … HLK … HLKV ?) -HLK HLKV L // #L #U #HKL #_ #HUV + elim (ldrop_conf_lt … HLK … HLKV ?) -HLK HLKV L // #L #U #HKL #_ #HUV elim (lift_trans_le … HUV … HVW ?) -HUV HVW V // >arith_a2 // -Hid /3/ | #L #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct -X; elim (IHV12 … HLK … HWV1 ?) -IHV12 HWV1 // #W2 #HW12 #HWV2 - elim (IHU12 … HTU1 ?) -IHU12 HTU1 [3: /2/ |4: @drop_skip // |2: skip ] -HLK Hdetd (**) (* /3 width=5/ is too slow *) + elim (IHU12 … HTU1 ?) -IHU12 HTU1 [3: /2/ |4: @ldrop_skip // |2: skip ] -HLK Hdetd (**) (* /3 width=5/ is too slow *) /3 width=5/ | #L #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct -X; @@ -118,6 +151,41 @@ lemma tps_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → ] qed. +lemma tps_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → + ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 → + dt ≤ d → d + e ≤ dt + et → + ∃∃T2. K ⊢ T1 [dt, et - e] ≫ T2 & ↑[d, e] T2 ≡ U2. +#L #U1 #U2 #dt #et #H elim H -H L U1 U2 dt et +[ #L * #i #dt #et #K #d #e #_ #T1 #H #_ + [ lapply (lift_inv_sort2 … H) -H #H destruct -T1 /2/ + | elim (lift_inv_lref2 … H) -H * #Hid #H destruct -T1 /3/ + | lapply (lift_inv_gref2 … H) -H #H destruct -T1 /2/ + ] +| #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdtd #Hdedet + lapply (le_fwd_plus_plus_ge … Hdtd … Hdedet) #Heet + elim (lift_inv_lref2 … H) -H * #Hid #H destruct -T1 + [ -Hdtd Hidet; + lapply (lt_to_le_to_lt … (dt + (et - e)) Hid ?) [ arith_a2 // -Hid /3/ + | -Hdti Hdedet; + lapply (transitive_le … (i - e) Hdtd ?) [ /2/ ] -Hdtd #Hdtie + lapply (plus_le_weak … Hid) #Hei + lapply (ldrop_conf_ge … HLK … HLKV ?) -L // #HKV + elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW; [4: // |2,3: /2/ ] -Hid >arith_e2 // /4/ + ] +| #L #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet + elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct -X; + elim (IHV12 … HLK … HWV1 ? ?) -IHV12 HWV1 // #W2 #HW12 #HWV2 + elim (IHU12 … HTU1 ? ?) -IHU12 HTU1 [5: @ldrop_skip // |2: skip |3: >plus_plus_comm_23 >(plus_plus_comm_23 dt) /2/ ] + /3 width=5/ +| #L #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet + elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct -X; + elim (IHV12 … HLK … HWV1 ? ?) -IHV12 HWV1 // + elim (IHU12 … HLK … HTU1 ? ?) -IHU12 HLK HTU1 // /3 width=5/ +] +qed. + (* Basic_1: was: subst1_gen_lift_ge *) lemma tps_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 → @@ -127,14 +195,15 @@ lemma tps_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → [ #L * #i #dt #et #K #d #e #_ #T1 #H #_ [ lapply (lift_inv_sort2 … H) -H #H destruct -T1 /2/ | elim (lift_inv_lref2 … H) -H * #Hid #H destruct -T1 /3/ + | lapply (lift_inv_gref2 … H) -H #H destruct -T1 /2/ ] | #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdedt lapply (transitive_le … Hdedt … Hdti) #Hdei lapply (plus_le_weak … Hdedt) -Hdedt #Hedt lapply (plus_le_weak … Hdei) #Hei lapply (lift_inv_lref2_ge … H … Hdei) -H #H destruct -T1; - lapply (drop_conf_ge … HLK … HLKV ?) -HLK HLKV L // #HKV - elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW; [2,3,4: normalize /2/ ] -Hdei >arith_e2 // #V0 #HV10 #HV02 + lapply (ldrop_conf_ge … HLK … HLKV ?) -HLK HLKV L // #HKV + elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW; [4: // | 2,3: normalize /2/ ] -Hdei >arith_e2 // #V0 #HV10 #HV02 @ex2_1_intro [2: @tps_subst [3: /2/ |5,6: // |1,2: skip |4: @arith5 // ] |1: skip @@ -144,7 +213,7 @@ lemma tps_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct -X; lapply (plus_le_weak … Hdetd) #Hedt elim (IHV12 … HLK … HWV1 ?) -IHV12 HWV1 // #W2 #HW12 #HWV2 - elim (IHU12 … HTU1 ?) -IHU12 HTU1 [4: @drop_skip // |2: skip |3: /2/ ] + elim (IHU12 … HTU1 ?) -IHU12 HTU1 [4: @ldrop_skip // |2: skip |3: /2/ ] (lift_mono … HVT1 … HVT2) -HVT1 HVT2 /2/ ] | #L #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX 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 e63dbb9a4..eb7803efe 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma @@ -63,7 +63,7 @@ fact ltps_inv_atom2_aux: ∀d,e,L1,L2. ] qed. -lemma drop_inv_atom2: ∀d,e,L1. L1 [d, e] ≫ ⋆ → L1 = ⋆. +lemma ldrop_inv_atom2: ∀d,e,L1. L1 [d, e] ≫ ⋆ → L1 = ⋆. /2 width=5/ qed. fact ltps_inv_tps22_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → d = 0 → 0 < e → diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_drop.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ldrop.ma similarity index 79% rename from matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_drop.ma rename to matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ldrop.ma index 10ef14016..1fc4ed7e6 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_drop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ldrop.ma @@ -12,63 +12,63 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/ltps_drop.ma". +include "Basic_2/substitution/ltps_ldrop.ma". include "Basic_2/unfold/ltpss.ma". (* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************) -lemma ltpss_drop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 → +lemma ltpss_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 @(ltpss_ind … H) -L1 /3 width=6/ qed. -lemma ltpss_drop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 → +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. #L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 /3 width=6/ qed. -lemma ltpss_drop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 → +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. #L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1 [ /2/ | #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1 elim (IHL … HL02 Hd1e2 He2de1) -L0 #L0 #HL20 #HL0 - elim (ltps_drop_conf_be … HL1 … HL0 Hd1e2 He2de1) -L /3/ + elim (ltps_ldrop_conf_be … HL1 … HL0 Hd1e2 He2de1) -L /3/ ] qed. -lemma ltpss_drop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 → +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. #L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 [ /2/ | #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1 - elim (ltps_drop_trans_be … HL0 … HL02 Hd1e2 He2de1) -L0 #L0 #HL02 #HL0 + elim (ltps_ldrop_trans_be … HL0 … HL02 Hd1e2 He2de1) -L0 #L0 #HL02 #HL0 elim (IHL … HL0 Hd1e2 He2de1) -L /3/ ] qed. -lemma ltpss_drop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 → +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. #L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1 [ /2/ | #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #He2d1 elim (IHL … HL02 He2d1) -L0 #L0 #HL20 #HL0 - elim (ltps_drop_conf_le … HL1 … HL0 He2d1) -L /3/ + elim (ltps_ldrop_conf_le … HL1 … HL0 He2d1) -L /3/ ] qed. -lemma ltpss_drop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 → +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. #L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 [ /2/ | #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #He2d1 - elim (ltps_drop_trans_le … HL0 … HL02 He2d1) -L0 #L0 #HL02 #HL0 + elim (ltps_ldrop_trans_le … HL0 … HL02 He2d1) -L0 #L0 #HL02 #HL0 elim (IHL … HL0 He2d1) -L /3/ ] qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma index 4e1cfd5e6..244ad9e9e 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma @@ -28,7 +28,7 @@ lemma tpss_subst: ∀L,K,V,U1,i,d,e. | #U #U1 #_ #HU1 #IHU #U2 #HU12 elim (lift_total U 0 (i+1)) #U0 #HU0 lapply (IHU … HU0) -IHU #H - lapply (drop_fwd_drop2 … HLK) -HLK #HLK + lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK lapply (tps_lift_ge … HU1 … HLK HU0 HU12 ?) -HU1 HLK HU0 HU12 // normalize #HU02 lapply (tps_weak … HU02 d e ? ?) -HU02 [ >arith_i2 // | /2/ | /2/ ] ] @@ -49,7 +49,7 @@ lemma tpss_inv_atom1: ∀L,T2,I,d,e. L ⊢ 𝕒{I} [d, e] ≫* T2 → [ #H destruct -T; elim (tps_inv_atom1 … HT2) -HT2 [ /2/ | * /3 width=10/ ] | * #K #V1 #V #i #Hdi #Hide #HLK #HV1 #HVT #HI - lapply (drop_fwd_drop2 … HLK) #H + lapply (ldrop_fwd_ldrop2 … HLK) #H elim (tps_inv_lift1_up … HT2 … H … HVT ? ? ?) normalize -HT2 H HVT [2,3,4: /2/ ] #V2 (lift_mono … HTU1 … H) -H // | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2 elim (lift_total T d e) #U #HTU @@ -88,11 +88,24 @@ lemma tpss_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫* T2 → ] qed. +lemma tpss_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 → + ∀U2. ↑[d, e] T2 ≡ U2 → L ⊢ U1 [dt, et + e] ≫* U2. +#K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdtd #Hddet #HLK #HTU1 @(tpss_ind … H) -T2 +[ #U2 #H >(lift_mono … HTU1 … H) -H // +| -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2 + elim (lift_total T d e) #U #HTU + lapply (IHT … HTU) -IHT #HU1 + lapply (tps_lift_be … HT2 … HLK HTU HTU2 ? ?) -HT2 HLK HTU HTU2 /2/ +] +qed. + lemma tpss_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 #H #L #U1 #d #e #Hddt #HLK #HTU1 @(tpss_ind … H) -H T2 +#K #T1 #T2 #dt #et #H #L #U1 #d #e #Hddt #HLK #HTU1 @(tpss_ind … H) -T2 [ #U2 #H >(lift_mono … HTU1 … H) -H // | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2 elim (lift_total T d e) #U #HTU @@ -105,10 +118,21 @@ lemma tpss_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 → ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 → dt + et ≤ d → ∃∃T2. K ⊢ T1 [dt, et] ≫* T2 & ↑[d, e] T2 ≡ U2. -#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdetd @(tpss_ind … H) -H U2 +#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdetd @(tpss_ind … H) -U2 +[ /2/ +| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU + elim (tps_inv_lift1_le … HU2 … HLK … HTU ?) -HU2 HLK HTU // /3/ +] +qed. + +lemma tpss_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 → + ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 → + dt ≤ d → d + e ≤ dt + et → + ∃∃T2. K ⊢ T1 [dt, et - e] ≫* T2 & ↑[d, e] T2 ≡ U2. +#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet @(tpss_ind … H) -U2 [ /2/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU - elim (tps_inv_lift1_le … HU2 … HLK … HTU ?) -HU2 HLK HTU /3/ + elim (tps_inv_lift1_be … HU2 … HLK … HTU ? ?) -HU2 HLK HTU // /3/ ] qed. @@ -116,16 +140,27 @@ lemma tpss_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 → ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 → d + e ≤ dt → ∃∃T2. K ⊢ T1 [dt - e, et] ≫* T2 & ↑[d, e] T2 ≡ U2. -#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdedt @(tpss_ind … H) -H U2 +#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdedt @(tpss_ind … H) -U2 [ /2/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU - elim (tps_inv_lift1_ge … HU2 … HLK … HTU ?) -HU2 HLK HTU /3/ + elim (tps_inv_lift1_ge … HU2 … HLK … HTU ?) -HU2 HLK HTU // /3/ ] qed. lemma tpss_inv_lift1_eq: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ≫* U2 → ∀T1. ↑[d, e] T1 ≡ U1 → U1 = U2. -#L #U1 #U2 #d #e #H #T1 #HTU1 @(tpss_ind … H) -H U2 // +#L #U1 #U2 #d #e #H #T1 #HTU1 @(tpss_ind … H) -U2 // #U #U2 #_ #HU2 #IHU destruct -U1 <(tps_inv_lift1_eq … HU2 … HTU1) -HU2 HTU1 // qed. + +lemma tpss_inv_lift1_be_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 → + ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 → + dt ≤ d → dt + et ≤ d + e → + ∃∃T2. K ⊢ T1 [dt, d - dt] ≫* T2 & ↑[d, e] T2 ≡ U2. +#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde @(tpss_ind … H) -U2 +[ /2/ +| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU + elim (tps_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -HU2 HLK HTU // /3/ +] +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_ltps.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_ltps.ma index 1f4a2de3e..abaf3f7c0 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_ltps.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_ltps.ma @@ -66,8 +66,8 @@ fact ltps_tps_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e. #L1 #T2 #U2 #d #e * -L1 T2 U2 d e [ // | #L1 #K1 #V1 #W1 #i #d #e #Hdi #Hide #HLK1 #HVW1 #L0 #HL10 #H1 #H2 destruct -Y1 X2; - lapply (drop_fwd_lw … HLK1) normalize #H1 - elim (ltps_drop_trans_be … HL10 … HLK1 ? ?) -HL10 HLK1 [2,3: /2/ ] #X #H #HLK0 + lapply (ldrop_fwd_lw … HLK1) normalize #H1 + elim (ltps_ldrop_trans_be … HL10 … HLK1 ? ?) -HL10 HLK1 [2,3: /2/ ] #X #H #HLK0 elim (ltps_inv_tps22 … H ?) -H [2: /2/ ] #K0 #V0 #HK01 #HV01 #H destruct -X; lapply (tps_fwd_tw … HV01) #H2 lapply (transitive_le (#[K1] + #[V0]) … H1) -H1 [ /2/ ] -H2 #H diff --git a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma b/matita/matita/contribs/lambda_delta/Ground_2/arith.ma index c17ef80d0..a18844e9b 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/arith.ma @@ -52,11 +52,10 @@ lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m. | #m #IHm * [ /2/ ] #n elim (IHm n) -IHm #H [ @or3_intro0 | @or3_intro1 destruct | @or3_intro2 ] /2/ (**) (* /3/ is slow *) - qed. + qed. lemma le_to_lt_or_eq: ∀m,n. m ≤ n → m < n ∨ m = n. -#m #n * -n /3/ -qed. +/2/ qed. (**) (* REMOVE: this is le_to_or_lt_eq *) lemma plus_le_weak: ∀m,n,p. m + n ≤ p → n ≤ p. /2/ qed. @@ -67,6 +66,13 @@ lapply (le_to_lt_to_lt … H2 H1) -H2 H1 #H elim (lt_refl_false … H) qed. +lemma le_fwd_plus_plus_ge: ∀m1,m2. m2 ≤ m1 → ∀n1,n2. m1 + n1 ≤ m2 + n2 → n1 ≤ n2. +#m1 #m2 #H elim H -H m1 +[ /2/ +| #m1 #_ #IHm1 #n1 #n2 #H @IHm1 /2/ +] +qed. + lemma monotonic_lt_minus_l: ∀p,q,n. n ≤ q → q < p → q - n < p - n. #p #q #n #H1 #H2 @lt_plus_to_minus_r