From c4ac63d7ae22b2adcc7fe7b54286a0226296eabc Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 6 Dec 2011 19:49:59 +0000 Subject: [PATCH] other addition to the standard library removed --- .../Basic_2/substitution/ldrop.ma | 2 +- .../Basic_2/substitution/lift_lift.ma | 2 +- .../Basic_2/substitution/tps_lift.ma | 15 +-- .../contribs/lambda_delta/Ground_2/arith.ma | 105 +----------------- 4 files changed, 14 insertions(+), 110 deletions(-) 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 2b8f3f953..9d085fc05 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma @@ -183,7 +183,7 @@ qed-. lemma ldrop_fwd_lw: ∀L1,L2,d,e. ↓[d, e] L1 ≡ L2 → #[L2] ≤ #[L1]. #L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize -[ /2 width=1/ +[ /2 width=3/ | #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12 >(tw_lift … HV21) -HV21 /2 width=1/ ] diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma index 3f5b8ab6a..cfcf976e0 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma @@ -126,7 +126,7 @@ theorem lift_trans_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → elim (lift_inv_lref1 … HX) -HX * #Hid2 #HX destruct /3 width=3/ /4 width=3/ | #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #Hd21 lapply (transitive_le … Hd21 Hid1) -Hd21 #Hid2 - lapply (lift_inv_lref1_ge … HX ?) -HX /2 width=1/ #HX destruct + lapply (lift_inv_lref1_ge … HX ?) -HX /2 width=3/ #HX destruct >plus_plus_comm_23 /4 width=3/ | #p #d1 #e1 #d2 #e2 #X #HX #_ >(lift_inv_gref1 … HX) -HX /2 width=3/ 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 6e3565e73..aaecbbf3b 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 @@ -168,10 +168,11 @@ lemma tps_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → elim (lift_trans_le … HUV … HVW ?) -V // >minus_plus plus_minus // plus_minus // commutative_plus >plus_minus // /2 width=1/ ] ] (**) (* explicit constructor, uses monotonic_lt_minus_l *) ] | #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 @@ -199,12 +200,12 @@ lemma tps_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → | #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdedt lapply (transitive_le … Hdedt … Hdti) #Hdei elim (le_inv_plus_l … Hdedt) -Hdedt #_ #Hedt - elim (le_inv_plus_l … Hdei) #_ #Hei + elim (le_inv_plus_l … Hdei) #Hdie #Hei lapply (lift_inv_lref2_ge … H … Hdei) -H #H destruct lapply (ldrop_conf_ge … HLK … HLKV ?) -L // #HKV - elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hdei - #V0 #HV10 >plus_minus // plus_minus // plus_minus // /2 width=1/ ] ] (**) (* explicit constructor, uses monotonic_lt_minus_l *) | #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 elim (le_inv_plus_l … Hdetd) #_ #Hedt diff --git a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma b/matita/matita/contribs/lambda_delta/Ground_2/arith.ma index 5d14a43dd..80e23e695 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/arith.ma @@ -28,6 +28,9 @@ lemma le_plus_minus: ∀m,n,p. p ≤ n → m + n - p = m + (n - p). 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. + 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 // @@ -38,11 +41,8 @@ lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b. ] 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. - lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b. -#a #b #c1 #H >minus_plus @eq_f2 /2 width=1/ +#a #b #c1 #H >minus_plus /3 width=1/ qed. lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b. @@ -110,100 +110,3 @@ lemma le_fwd_plus_plus_ge: ∀m1,m2. m2 ≤ m1 → ∀n1,n2. m1 + n1 ≤ m2 + n2 | #m1 #_ #IHm1 #n1 #n2 #H @IHm1 /2 width=3/ ] qed-. - -(* backward lemmas **********************************************************) - -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 plus_minus // @monotonic_lt_minus_l // -qed. - -lemma arith10: ∀a,b,c,d,e. a ≤ b → c + (a - d - e) ≤ c + (b - d - e). -#a #b #c #d #e #H ->minus_plus >minus_plus @monotonic_le_plus_r @monotonic_le_minus_l // -qed. - -(* remove *******************************************************************) -(* -lemma minus_plus_comm: ∀a,b,c. a - b - c = a - (c + b). -// qed. - -lemma plus_S_le_to_pos: ∀n,m,p. n + S m ≤ p → 0 < p. -/2 by ltn_to_ltO/ qed. - -lemma minus_le: ∀m,n. m - n ≤ m. -/2 by monotonic_le_minus_l/ qed. - -lemma le_O_to_eq_O: ∀n. n ≤ 0 → n = 0. -/2 by le_n_O_to_eq/ qed. - -lemma lt_to_le: ∀a,b. a < b → a ≤ b. -/2 by le_plus_b/ qed. - -lemma le_to_lt_or_eq: ∀m,n. m ≤ n → m < n ∨ m = n. -/2 by le_to_or_lt_eq/ qed. - -lemma plus_le_weak: ∀m,n,p. m + n ≤ p → n ≤ p. -/2 by le_plus_b/ qed. - -lemma plus_le_minus: ∀a,b,c. a + b ≤ c → a ≤ c - b. -/2 by le_plus_to_minus_r/ qed. - -lemma lt_plus_minus: ∀i,u,d. u ≤ i → i < d + u → i - u < d. -/2 by monotonic_lt_minus_l/ qed. - -lemma arith_a2: ∀a,c1,c2. c1 + c2 ≤ a → a - c1 - c2 + (c1 + c2) = a. -/2 by plus_minus/ qed. - -lemma arith_c1: ∀a,b,c1. a + c1 - (b + c1) = a - b. -// qed. - -lemma arith_d1: ∀a,b,c1. c1 ≤ b → a + c1 + (b - c1) = a + b. -/2 by plus_minus/ qed. - -lemma arith_e2: ∀a,c1,c2. a ≤ c1 → c1 + c2 - (c1 - a + c2) = a. -/2 by minus_le_minus_minus_comm/ qed. - -lemma arith_f1: ∀a,b,c1. a + b ≤ c1 → c1 - (c1 - a - b) = a + b. -/2 by minus_le_minus_minus_comm/ -qed. - -lemma arith_g1: ∀a,b,c1. c1 ≤ b → a - (b - c1) - c1 = a - b. -/2 by arith_b1/ qed. - -lemma arith_i2: ∀a,c1,c2. c1 + c2 ≤ a → c1 + c2 + (a - c1 - c2) = a. -/2 by plus_minus_m_m/ qed. - -lemma arith_z1: ∀a,b,c1. a + c1 - b - c1 = a - b. -// qed. - -lemma arith1: ∀n,h,m,p. n + h + m ≤ p + h → n + m ≤ p. -/2 by le_plus_to_le/ qed. - -lemma arith3: ∀a1,a2,b,c1. a1 + a2 ≤ b → a1 + c1 + a2 ≤ b + c1. -/2 by le_minus_to_plus/ qed. - -lemma arith4: ∀h,d,e1,e2. d ≤ e1 + e2 → d + h ≤ e1 + h + e2. -/2 by arith3/ qed. - -lemma arith8: ∀a,b. a < a + b + 1. -// qed. - -lemma arith9: ∀a,b,c. c < a + (b + c + 1) + 1. -// qed. - -(* backward form of le_inv_plus_l *) -lemma P2: ∀x,y,z. x ≤ z - y → y ≤ z → x + y ≤ z. -/2 by le_minus_to_plus_r/ qed. -*) -- 2.39.2