From: Ferruccio Guidi Date: Thu, 14 Jan 2021 21:25:06 +0000 (+0100) Subject: arithmetics for λδ X-Git-Tag: make_still_working~163 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=19b0a814861157ba05f23877d5cd94059f52c2e8;p=helm.git arithmetics for λδ + arith.ma covered almost in full + minor additions and corrections --- diff --git a/matita/matita/contribs/lambdadelta/ground/arith/arith.txt b/matita/matita/contribs/lambdadelta/ground/arith/arith.txt index 1eda6fe22..f467cf7e5 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/arith.txt +++ b/matita/matita/contribs/lambdadelta/ground/arith/arith.txt @@ -1,125 +1,24 @@ (* Equalities ***************************************************************) -lemma minus_plus_m_m_commutative: ∀n,m:nat. n = m + n - m. -// qed-. - -lemma plus_minus_m_m_commutative (n) (m): m ≤ n → n = m+(n-m). -/2 width=1 by plus_minus_associative/ qed-. - -lemma plus_to_minus_2: ∀m1,m2,n1,n2. n1 ≤ m1 → n2 ≤ m2 → - m1+n2 = m2+n1 → m1-n1 = m2-n2. -#m1 #m2 #n1 #n2 #H1 #H2 #H -@plus_to_minus >plus_minus_associative // -qed-. - -(* Note: uses minus_minus_comm, minus_plus_m_m, commutative_plus, plus_minus *) -lemma plus_minus_minus_be: ∀x,y,z. y ≤ z → z ≤ x → (x - z) + (z - y) = x - y. -#x #z #y #Hzy #Hyx >plus_minus // >commutative_plus >plus_minus // -qed-. - -lemma lt_succ_pred: ∀m,n. n < m → m = ↑↓m. -#m #n #Hm >S_pred /2 width=2 by ltn_to_ltO/ -qed-. +(*** plus_minus_plus_plus_l *) (**) +lemma plus_minus_plus_plus_l: ∀z,x,y,h. z + (x + h) - (y + h) = z + x - y. +#H1 #H2 #H3 #H4 +(S_pred … Hm) -@le_S_S_to_le >S_pred /2 width=3 by transitive_lt/ -qed. - -lemma lt_S_S: ∀x,y. x < y → ↑x < ↑y. -/2 width=1 by le_S_S/ qed. - -lemma lt_S: ∀n,m. n < m → n < ↑m. -/2 width=1 by le_S/ qed. - -lemma monotonic_lt_minus_r: -∀p,q,n. q < n -> q < p → n-p < n-q. -#p #q #n #Hn #H -lapply (monotonic_le_minus_r … n H) -H #H -@(le_to_lt_to_lt … H) -H -/2 width=1 by lt_plus_to_minus/ -qed. - (* Inversion & forward lemmas ***********************************************) -lemma lt_refl_false: ∀n. n < n → ⊥. -#n #H elim (lt_to_not_eq … H) -H /2 width=1 by/ -qed-. - -lemma lt_zero_false: ∀n. n < 0 → ⊥. -#n #H elim (lt_to_not_le … H) -H /2 width=1 by/ -qed-. - -lemma lt_le_false: ∀x,y. x < y → y ≤ x → ⊥. -/3 width=4 by lt_refl_false, lt_to_le_to_lt/ qed-. - -lemma le_dec (n) (m): Decidable (n≤m). -#n elim n -n [ /2 width=1 by or_introl/ ] -#n #IH * [ /3 width=2 by lt_zero_false, or_intror/ ] -#m elim (IH m) -IH -[ /3 width=1 by or_introl, le_S_S/ -| /4 width=1 by or_intror, le_S_S_to_le/ -] -qed-. - -lemma succ_inv_refl_sn: ∀x. ↑x = x → ⊥. -#x #H @(lt_le_false x (↑x)) // -qed-. - -lemma le_plus_xSy_O_false: ∀x,y. x + S y ≤ 0 → ⊥. -#x #y #H lapply (le_n_O_to_eq … H) -H H -H -/2 width=2 by le_plus_to_le/ -qed-. - -lemma plus2_le_sn_dx: ∀m1,m2,n1,n2. m1 + n1 = n2 + m2 → m1 ≤ m2 → n2 ≤ n1. -/2 width=4 by plus2_le_sn_sn/ qed-. - -lemma plus2_le_dx_sn: ∀m1,m2,n1,n2. n1 + m1 = m2 + n2 → m1 ≤ m2 → n2 ≤ n1. -/2 width=4 by plus2_le_sn_sn/ qed-. - -lemma plus2_le_dx_dx: ∀m1,m2,n1,n2. n1 + m1 = n2 + m2 → m1 ≤ m2 → n2 ≤ n1. -/2 width=4 by plus2_le_sn_sn/ qed-. - -lemma lt_S_S_to_lt: ∀x,y. ↑x < ↑y → x < y. -/2 width=1 by le_S_S_to_le/ qed-. - -(* Note this should go in nat.ma *) -lemma discr_x_minus_xy: ∀x,y. x = x - y → x = 0 ∨ y = 0. -#x @(nat_ind_plus … x) -x /2 width=1 by or_introl/ -#x #_ #y @(nat_ind_plus … y) -y /2 width=1 by or_intror/ -#y #_ >minus_plus_plus_l -#H lapply (discr_plus_xy_minus_xz … H) -H -#H destruct -qed-. - -lemma lt_inv_O1: ∀n. 0 < n → ∃m. ↑m = n. -* /2 width=2 by ex_intro/ -#H cases (lt_le_false … H) -H // -qed-. - -lemma lt_inv_S1: ∀m,n. ↑m < n → ∃∃p. m < p & ↑p = n. -#m * /3 width=3 by lt_S_S_to_lt, ex2_intro/ -#H cases (lt_le_false … H) -H // -qed-. - -lemma lt_inv_gen: ∀y,x. x < y → ∃∃z. x ≤ z & ↑z = y. -* /3 width=3 by le_S_S_to_le, ex2_intro/ -#x #H elim (lt_le_false … H) -H // -qed-. - -lemma plus_inv_O3: ∀x,y. x + y = 0 → x = 0 ∧ y = 0. -/2 width=1 by plus_le_0/ qed-. - -lemma plus_inv_S3_sn: ∀x1,x2,x3. x1+x2 = ↑x3 → - ∨∨ ∧∧ x1 = 0 & x2 = ↑x3 - | ∃∃y1. x1 = ↑y1 & y1 + x2 = x3. -* /3 width=1 by or_introl, conj/ -#x1 #x2 #x3 (eq_inv_nsucc_bi … H) -n /2 width=1 by nle_inv_succ_sn/ +#x * -x +[ #H >(eq_inv_nsucc_bi … H) -n // +| #o #Ho #H >(eq_inv_nsucc_bi … H) -n + /2 width=1 by nle_des_succ_sn/ ] qed-. @@ -73,18 +76,19 @@ lemma nle_inv_zero_dx (m): m ≤ 𝟎 → 𝟎 = m. #m @(insert_eq_0 … (𝟎)) #y * -y [ #H destruct // -| #y #_ #H elim (eq_inv_nzero_succ … H) +| #y #_ #H elim (eq_inv_zero_nsucc … H) ] qed-. (* Advanced inversions ******************************************************) +(*** le_plus_xSy_O_false *) lemma nle_inv_succ_zero (m): ↑m ≤ 𝟎 → ⊥. -/3 width=2 by nle_inv_zero_dx, eq_inv_nzero_succ/ qed-. +/3 width=2 by nle_inv_zero_dx, eq_inv_zero_nsucc/ qed-. lemma nle_inv_succ_sn_refl (m): ↑m ≤ m → ⊥. #m @(nat_ind_succ … m) -m [| #m #IH ] #H -[ /3 width=2 by nle_inv_zero_dx, eq_inv_nzero_succ/ +[ /3 width=2 by nle_inv_zero_dx, eq_inv_zero_nsucc/ | /3 width=1 by nle_inv_succ_bi/ ] qed-. @@ -93,7 +97,7 @@ qed-. theorem nle_antisym (m) (n): m ≤ n → n ≤ m → m = n. #m #n #H elim H -n // #n #_ #IH #Hn -lapply (nle_inv_succ_sn … Hn) #H +lapply (nle_des_succ_sn … Hn) #H lapply (IH H) -IH -H #H destruct elim (nle_inv_succ_sn_refl … Hn) qed-. @@ -105,7 +109,7 @@ lemma nle_ind_alt (Q: relation2 nat nat): (∀n. Q (𝟎) (n)) → (∀m,n. m ≤ n → Q m n → Q (↑m) (↑n)) → ∀m,n. m ≤ n → Q m n. -#Q #IH1 #IH2 #m #n @(nat_ind_succ_2 … m n) -m -n // +#Q #IH1 #IH2 #m #n @(nat_ind_2_succ … m n) -m -n // [ #m #H elim (nle_inv_succ_zero … H) | /4 width=1 by nle_inv_succ_bi/ ] @@ -115,10 +119,10 @@ qed-. (*** transitive_le *) theorem nle_trans: Transitive … nle. -#m #n #H elim H -n /3 width=1 by nle_inv_succ_sn/ +#m #n #H elim H -n /3 width=1 by nle_des_succ_sn/ qed-. -(*** decidable_le *) +(*** decidable_le le_dec *) lemma nle_dec (m) (n): Decidable … (m ≤ n). #m #n elim (nle_ge_dis m n) [ /2 width=1 by or_introl/ ] #Hnm elim (eq_nat_dec m n) [ #H destruct /2 width=1 by nle_refl, or_introl/ ] diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_max.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_max.ma index 4f7886aa1..0ad906540 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_max.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_max.ma @@ -30,12 +30,12 @@ lemma nle_max_sn (n): qed. lemma nle_max_dx_refl_sn (m) (n): m ≤ (m ∨ n). -#m #n @(nat_ind_succ_2 … m n) -m -n // +#m #n @(nat_ind_2_succ … m n) -m -n // #m #n #IH (nminus_plus_sn_refl_sn m o) /2 width=1 by nle_minus_sn_bi/ qed. +(*** le_plus_to_minus_l *) +lemma nle_minus_dx_dx (o) (m) (n): o + m ≤ n → m ≤ n - o. +#o #m #n #H >(nminus_plus_sn_refl_dx m o) +/2 width=1 by nle_minus_sn_bi/ +qed. + (*** le_inv_plus_l *) lemma nle_minus_dx_full (o) (m) (n): m + o ≤ n → ∧∧ m ≤ n - o & o ≤ n. -/3 width=3 by nle_minus_dx, nle_trans, conj/ qed-. +/3 width=3 by nle_minus_dx_sn, nle_trans, conj/ qed-. (* Inversions with nminus and nplus *****************************************) @@ -53,6 +63,7 @@ lemma nplus_minus_sn_refl_sn (m) (n): m ≤ n → n = n - m + m. (nplus_minus_sn_refl_sn … Hm) in ⊢ (??%?); // qed-. + +(*** plus_minus_minus_be *) +lemma nplus_minus_be_be (m1) (m2) (m3): + m1 ≤ m2 → m2 ≤ m3 → (m3 - m2) + (m2 - m1) = m3 - m1. +#m1 #m2 #m3 #Hm12 #Hm23 +>nminus_assoc // H -H +/2 width=2 by nle_inv_plus_bi_sn/ +qed-. + +(*** plus2_le_sn_dx *) +lemma nplus_2_des_le_sn_dx (m1) (m2) (n1) (n2): + m1 + n1 = n2 + m2 → m1 ≤ m2 → n2 ≤ n1. +#m1 #m2 #n1 #n2 m < n → o-n < o-m. +#o #m #n #Ho #H +lapply (nle_minus_dx_bi … o H) -H #H +@(le_nlt_trans … H) -n +@nlt_i >(nminus_succ_sn … Ho) // +qed. + (* Destructions with nminus *************************************************) (*** minus_pred_pred *) lemma nminus_pred_bi (m) (n): 𝟎 < m → 𝟎 < n → n - m = ↓n - ↓m. #m #n #Hm #Hn ->(nlt_inv_zero_sn … Hm) in ⊢ (??%?); -Hm ->(nlt_inv_zero_sn … Hn) in ⊢ (??%?); -Hn +>(nlt_des_gen … Hm) in ⊢ (??%?); -Hm +>(nlt_des_gen … Hn) in ⊢ (??%?); -Hn // qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus_plus.ma index 61cc525ad..5fbbd53ea 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus_plus.ma @@ -22,13 +22,13 @@ include "ground/arith/nat_lt_minus.ma". (*** lt_plus_to_minus *) lemma nlt_minus_sn (o) (m) (n): m ≤ n → n < o + m → n - m < o. #o #m #n #Hmn #Ho -lapply (nle_minus_sn … Ho) -Ho +lapply (nle_minus_sn_sn … Ho) -Ho nplus_succ_dx /2 width=1 by nle_plus_bi_sn/ qed. -(*** lt_plus_Sn_r *) (**) -lemma lt_plus_Sn_r: ∀a,x,n. a < a + x + ↑n. -/2 width=1/ qed-. +lemma nlt_succ_plus_dx_refl_sn (m) (n): m < ↑(m + n). +/2 width=1/ qed. (* Inversions with nplus ****************************************************) diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_pred.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_pred.ma index c319006fc..cb7769758 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_pred.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_pred.ma @@ -17,22 +17,40 @@ include "ground/arith/nat_lt.ma". (* STRICT ORDER FOR NON-NEGATIVE INTEGERS ***********************************) -(* Constructions with npred *************************************************) +(* Destructions with npred **************************************************) -lemma nlt_zero_sn (m): m = ↑↓m → 𝟎 < m. -// qed. +(*** S_pred lt_succ_pred lt_inv_O1 *) +lemma nlt_des_gen (m) (n): m < n → n = ↑↓n. +#m #n @(nat_ind_succ … n) -n // +#H elim (nlt_inv_zero_dx … H) +qed-. (* Inversions with npred ****************************************************) -(*** S_pred *) -lemma nlt_inv_zero_sn (m): 𝟎 < m → m = ↑↓m. -#m @(nat_ind_succ … m) -m // -#H elim (nlt_inv_refl … H) -qed-. +(*** lt_inv_gen *) +lemma nlt_inv_gen (m) (n): m < n → ∧∧ m ≤ ↓n & n = ↑↓n. +/2 width=1 by nle_inv_succ_sn/ qed-. + +(*** lt_inv_S1 *) +lemma nlt_inv_succ_sn (m) (n): ↑m < n → ∧∧ m < ↓n & n = ↑↓n. +/2 width=1 by nle_inv_succ_sn/ qed-. lemma nlt_inv_pred_dx (m) (n): m < ↓n → ↑m < n. -#m #n #H >(nlt_inv_zero_sn n) +#m #n #H >(nlt_des_gen (𝟎) n) [ /2 width=1 by nlt_succ_bi/ | /3 width=3 by le_nlt_trans, nlt_le_trans/ ] qed-. + +(* Constructions with npred *************************************************) + +lemma nlt_zero_sn (n): n = ↑↓n → 𝟎 < n. +// qed. + +(*** monotonic_lt_pred *) +lemma nlt_pred_bi (m) (n): 𝟎 < m → m < n → ↓m < ↓n. +#m #n #Hm #Hmn +@nle_inv_succ_bi +<(nlt_des_gen … Hm) -Hm +<(nlt_des_gen … Hmn) // +qed. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma index 4e1e88280..c3ca75497 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "ground/notation/functions/zero_0.ma". include "ground/arith/nat_succ_tri.ma". (* MAXIMUM FOR NON-NEGATIVE INTEGERS ****************************************) @@ -40,7 +39,7 @@ qed. (*** max_SS *) lemma nmax_succ_bi (n1) (n2): ↑(n1 ∨ n2) = (↑n1 ∨ ↑n2). #n1 #n2 -@trans_eq [3: @ntri_succ_bi | skip ] (**) (* rewrite fails because δ-expansion gets in the way *) +@trans_eq [3: @ntri_succ_bi | skip ] (**) (* rewrite fails because δ-expansion gets in the way *) nplus_succ_shift #Ho elim (IH … Ho) -IH -Ho * #_ #H - elim (eq_inv_nzero_succ … H) + elim (eq_inv_zero_nsucc … H) ] qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma index f7d79ccdf..2df064a01 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma @@ -63,7 +63,7 @@ qed. (*** commutative_plus *) lemma nplus_comm: commutative … nplus. #m @(nat_ind_succ … m) -m // -qed-. +qed-. (**) (* gets in the way with auto *) (*** associative_plus *) lemma nplus_assoc: associative … nplus. @@ -91,11 +91,12 @@ qed-. (* Basic inversions *********************************************************) -lemma eq_inv_nzero_plus (m) (n): 𝟎 = m + n → ∧∧ 𝟎 = m & 𝟎 = n. +(*** plus_inv_O3 zero_eq_plus *) +lemma eq_inv_zero_nplus (m) (n): 𝟎 = m + n → ∧∧ 𝟎 = m & 𝟎 = n. #m #n @(nat_ind_succ … n) -n [ /2 width=1 by conj/ | #n #_