From 6ed2537d49a307259db46481469fa44b2cfc56e6 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 11 Dec 2011 18:19:13 +0000 Subject: [PATCH] - slicing relation for the global environment defined (gdrop) - two arithmetical lemmas inlined --- .../lambda_delta/Basic_2/grammar/lsubs.ma | 6 +-- .../contribs/lambda_delta/Basic_2/notation.ma | 4 ++ .../Basic_2/substitution/gdrop.ma | 43 +++++++++++++++++ .../Basic_2/substitution/ldrop.ma | 10 ++-- .../lambda_delta/Basic_2/substitution/lift.ma | 6 ++- .../lambda_delta/Basic_2/substitution/ltps.ma | 7 ++- .../contribs/lambda_delta/Ground_2/arith.ma | 47 +++++++------------ 7 files changed, 78 insertions(+), 45 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma index 1f750064e..6f3ec1513 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma @@ -74,8 +74,7 @@ fact lsubs_fwd_length_full1_aux: ∀L1,L2,d,e. L1 [d, e] ≼ L2 → | /2 width=1/ | /3 width=1/ | /3 width=1/ -| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ #H - elim (plus_S_eq_O_false … H) +| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ >commutative_plus normalize #H destruct ] qed. @@ -89,8 +88,7 @@ fact lsubs_fwd_length_full2_aux: ∀L1,L2,d,e. L1 [d, e] ≼ L2 → | /2 width=1/ | /3 width=1/ | /3 width=1/ -| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ #H - elim (plus_S_eq_O_false … H) +| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ >commutative_plus normalize #H destruct ] qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma index 0ec1b1466..8e1d4362a 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma @@ -86,6 +86,10 @@ notation "hvbox( ↑ [ d , break e ] break T1 ≡ break T2 )" non associative with precedence 45 for @{ 'RLift $d $e $T1 $T2 }. +notation "hvbox( ↓ [ e ] break L1 ≡ break L2 )" + non associative with precedence 45 + for @{ 'RDrop $e $L1 $L2 }. + notation "hvbox( ↓ [ d , break e ] break L1 ≡ break L2 )" non associative with precedence 45 for @{ 'RDrop $d $e $L1 $L2 }. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma new file mode 100644 index 000000000..47d75a4ea --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma @@ -0,0 +1,43 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "Basic_2/substitution/ldrop.ma". + +(* GLOBAL ENVIRONMENT SLICING ***********************************************) + +inductive gdrop (e:nat) (G1:lenv) : predicate lenv ≝ +| gdrop_lt: ∀G2. e < |G1| → ↓[0, |G1| - (e + 1)] G1 ≡ G2 → gdrop e G1 G2 +| gdrop_ge: |G1| ≤ e → gdrop e G1 (⋆) +. + +interpretation "global slicing" 'RDrop e G1 G2 = (gdrop e G1 G2). + +(* basic inversion lemmas ***************************************************) + +fact gdrop_inv_atom2_aux: ∀G1,G2,e. ↓[e] G1 ≡ G2 → G2 = ⋆ → |G1| ≤ e. +#G1 #G2 #e * -G2 // +#G2 #He #HG12 #H destruct +lapply (ldrop_fwd_O1_length … HG12) -HG12 +>minus_le_minus_minus_comm // -He >le_plus_minus_comm // (commutative_plus e) normalize #H destruct +qed. + +lemma gdrop_inv_atom2: ∀G1,e. ↓[e] G1 ≡ ⋆ → |G1| ≤ e. +/2 width=3/ qed-. + +lemma gdrop_inv_ge: ∀G1,G2,e. ↓[e] G1 ≡ G2 → |G1| ≤ e → G2 = ⋆. +#G1 #G2 #e * // #G2 #H1 #_ #H2 +lapply (lt_to_le_to_lt … H1 H2) -H1 -H2 #He +elim (lt_refl_false … He) +qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma index 9d085fc05..b4d3355d6 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma @@ -28,7 +28,7 @@ inductive ldrop: nat → nat → relation lenv ≝ ldrop (d + 1) e (L1. 𝕓{I} V1) (L2. 𝕓{I} V2) . -interpretation "ldropping" 'RDrop d e L1 L2 = (ldrop d e L1 L2). +interpretation "local slicing" 'RDrop d e L1 L2 = (ldrop d e L1 L2). (* Basic inversion lemmas ***************************************************) @@ -36,10 +36,8 @@ fact ldrop_inv_refl_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → e = 0 #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) +| #L1 #L2 #I #V #e #_ #_ >commutative_plus normalize #H destruct +| #L1 #L2 #I #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct ] qed. @@ -69,7 +67,7 @@ fact ldrop_inv_O1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → [ #d #e #_ #K #I #V #H destruct | #L #I #V #_ #K #J #W #HX destruct /3 width=1/ | #L1 #L2 #I #V #e #HL12 #_ #K #J #W #H destruct /3 width=1/ -| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H elim (plus_S_eq_O_false … H) +| #L1 #L2 #I #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct ] qed. 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 30296c685..fa1dfae28 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma @@ -164,7 +164,8 @@ lemma lift_inv_lref2: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i → lemma lift_inv_lref2_lt: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i → i < d → T1 = #i. #d #e #T1 #i #H elim (lift_inv_lref2 … H) -H * // #Hdi #_ #Hid lapply (le_to_lt_to_lt … Hdi Hid) -Hdi -Hid #Hdd -elim (plus_lt_false … Hdd) +elim (lt_inv_plus_l … Hdd) -Hdd #Hdd +elim (lt_refl_false … Hdd) qed-. (* Basic_1: was: lift_gen_lref_false *) @@ -180,7 +181,8 @@ qed-. lemma lift_inv_lref2_ge: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i → d + e ≤ i → T1 = #(i - e). #d #e #T1 #i #H elim (lift_inv_lref2 … H) -H * // #Hid #_ #Hdi lapply (le_to_lt_to_lt … Hdi Hid) -Hdi -Hid #Hdd -elim (plus_lt_false … Hdd) +elim (lt_inv_plus_l … Hdd) -Hdd #Hdd +elim (lt_refl_false … Hdd) qed-. fact lift_inv_gref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀p. T2 = §p → T1 = §p. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma index ccb460654..c804efa41 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma @@ -57,8 +57,7 @@ qed. fact ltps_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 #_ #_ #_ #H - elim (plus_S_eq_O_false … H) +[ #L1 #L2 #I #V1 #V2 #e #_ #_ #_ >commutative_plus normalize #H destruct | #L1 #L2 #I #V1 #V2 #d #e #_ #HV12 #IHL12 #He destruct >(IHL12 ?) -IHL12 // >(tps_inv_refl_O2 … HV12) // ] @@ -89,7 +88,7 @@ fact ltps_inv_tps21_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → d = 0 → 0 < e → [ #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 #_ #_ #H elim (plus_S_eq_O_false … H) +| #L1 #L2 #I #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct ] qed. @@ -139,7 +138,7 @@ fact ltps_inv_tps22_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → d = 0 → 0 < e → [ #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 #_ #_ #H elim (plus_S_eq_O_false … H) +| #L1 #L2 #I #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct ] qed. diff --git a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma b/matita/matita/contribs/lambda_delta/Ground_2/arith.ma index 80e23e695..37fac204b 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/arith.ma @@ -29,20 +29,14 @@ lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → m + n - p = m - p + n. /2 by plus_minus/ qed. lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b. - /3 by monotonic_le_minus_l, le_to_le_to_eq/ qed. +/3 by monotonic_le_minus_l, le_to_le_to_eq/ qed. lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b. -#b elim b -b -[ #c #a #H >(le_n_O_to_eq … H) -H // -| #b #IHb #c elim c -c // - #c #_ #a #Hcb - lapply (le_S_S_to_le … Hcb) -Hcb #Hcb - (plus_minus_m_m b c) in ⊢ (? ? ?%); // qed. lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b. -#a #b #c1 #H >minus_plus /3 width=1/ +#a #b #c1 #H >minus_minus_comm >minus_le_minus_minus_comm // qed. lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b. @@ -68,11 +62,9 @@ lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m. qed-. lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m. -#m elim m -m -[ * /2 width=1/ -| #m #IHm * /2 width=1/ - #n elim (IHm n) -IHm #H - [ @or3_intro0 | @or3_intro1 destruct | @or3_intro2 ] // /2 width=1/ (**) (* /3 width=1/ is slow *) +#m #n elim (lt_or_ge m n) /2 width=1/ +#H elim H -m /2 width=1/ +#m #Hm * #H /2 width=1/ /3 width=1/ qed-. lemma le_inv_plus_plus_r: ∀x,y,z. x + z ≤ y + z → x ≤ y. @@ -81,6 +73,9 @@ lemma le_inv_plus_plus_r: ∀x,y,z. x + z ≤ y + z → x ≤ y. lemma le_inv_plus_l: ∀x,y,z. x + y ≤ z → x ≤ z - y ∧ y ≤ z. /3 width=2/ qed-. +lemma lt_inv_plus_l: ∀x,y,z. x + y < z → x < z ∧ y < z - x. +/3 width=2/ qed-. + lemma lt_refl_false: ∀n. n < n → False. #n #H elim (lt_to_not_eq … H) -H /2 width=1/ qed-. @@ -89,24 +84,18 @@ lemma lt_zero_false: ∀n. n < 0 → False. #n #H elim (lt_to_not_le … H) -H /2 width=1/ qed-. -lemma plus_S_eq_O_false: ∀n,m. n + S m = 0 → False. -#n #m commutative_plus +#H elim (le_inv_plus_l … H) -H >commutative_plus