X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Flib%2Farith.ma;h=79bcc2548bca92b905b524c6adfda5ae919040cc;hb=d8d00d6f6694155be5be486a8239f5953efe28b7;hp=e3ec5c5040847cd64f141efd9aede61dcee4f658;hpb=1083ac3b1acac5f1ac1fa40a9a417dd9d268dced;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index e3ec5c504..79bcc2548 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -12,9 +12,12 @@ (* *) (**************************************************************************) +include "arithmetics/nat.ma". +include "ground_2/xoa/ex_3_1.ma". +include "ground_2/xoa/or_3.ma". include "ground_2/notation/functions/uparrow_1.ma". include "ground_2/notation/functions/downarrow_1.ma". -include "arithmetics/nat.ma". +include "ground_2/pull/pull_2.ma". include "ground_2/lib/relations.ma". (* ARITHMETICAL PROPERTIES **************************************************) @@ -49,20 +52,25 @@ lemma max_SS: ∀n1,n2. ↑(n1∨n2) = (↑n1 ∨ ↑n2). [ >(le_to_leb_true … H) | >(not_le_to_leb_false … H) ] -H // qed. -(* Equations ****************************************************************) +(* Equalities ***************************************************************) + +lemma plus_SO_sn (n): 1 + n = ↑n. +// qed-. -lemma plus_SO: ∀n. n + 1 = ↑n. +lemma plus_SO_dx (n): n + 1 = ↑n. // qed. lemma minus_plus_m_m_commutative: ∀n,m:nat. n = m + n - m. // qed-. -lemma plus_n_2: ∀n. n + 2 = n + 1 + 1. -// qed. +lemma plus_minus_m_m_commutative (n) (m): m ≤ n → n = m+(n-m). +/2 width=1 by plus_minus_associative/ qed-. -lemma arith_l: ∀x. 1 = 1-x+(x-(x-1)). -* // #x >minus_S_S >minus_S_S 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. @@ -85,29 +93,6 @@ lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → m + n - p = m - p + n. lemma minus_minus_comm3: ∀n,x,y,z. n-x-y-z = n-y-z-x. // qed. -lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b. -#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. -#a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2 width=1 by arith_b1/ -qed-. - -lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b. -/3 by monotonic_le_minus_l, le_to_le_to_eq, le_n/ qed. - -lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b → - a1 - c1 + a2 - (b - c1) = a1 + a2 - b. -#a1 #a2 #b #c1 #H1 #H2 >plus_minus /2 width=1 by arith_b2/ -qed-. - -lemma arith_i: ∀x,y,z. y < x → x+z-y-1 = x-y-1+z. -/2 width=1 by plus_minus/ qed-. - -lemma plus_to_minus_2: ∀m1,m2,n1,n2. n1 ≤ m1 → n2 ≤ m2 → - m1+n2 = m2+n1 → m1-n1 = m2-n2. -/2 width=1 by arith_b1/ qed-. - lemma idempotent_max: ∀n:nat. n = (n ∨ n). #n normalize >le_to_leb_true // qed. @@ -138,18 +123,27 @@ lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m. #m #Hm * /3 width=1 by not_le_to_lt, le_S_S, or3_intro2/ qed-. -fact le_repl_sn_conf_aux: ∀x,y,z:nat. x ≤ z → x = y → y ≤ z. -// qed-. - -fact le_repl_sn_trans_aux: ∀x,y,z:nat. x ≤ z → y = x → y ≤ z. -// qed-. - lemma monotonic_le_minus_l2: ∀x1,x2,y,z. x1 ≤ x2 → x1 - y - z ≤ x2 - y - z. /3 width=1 by monotonic_le_minus_l/ qed. lemma minus_le_trans_sn: ∀x1,x2. x1 ≤ x2 → ∀x. x1-x ≤ x2. /2 width=3 by transitive_le/ qed. +lemma le_plus_to_minus_l: ∀a,b,c. a + b ≤ c → b ≤ c-a. +/2 width=1 by le_plus_to_minus_r/ +qed-. + +lemma le_plus_to_minus_comm: ∀n,m,p. n ≤ p+m → n-p ≤ m. +/2 width=1 by le_plus_to_minus/ qed-. + +lemma le_inv_S1: ∀m,n. ↑m ≤ n → ∃∃p. m ≤ p & ↑p = n. +#m * +[ #H lapply (le_n_O_to_eq … H) -H + #H destruct +| /3 width=3 by monotonic_pred, ex2_intro/ +] +qed-. + (* Note: this might interfere with nat.ma *) lemma monotonic_lt_pred: ∀m,n. m < n → 0 < m → pred m < pred n. #m #n #Hmn #Hm whd >(S_pred … Hm) @@ -162,29 +156,20 @@ lemma lt_S_S: ∀x,y. x < y → ↑x < ↑y. 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. + lemma max_S1_le_S: ∀n1,n2,n. (n1 ∨ n2) ≤ n → (↑n1 ∨ n2) ≤ ↑n. /4 width=2 by to_max, le_maxr, le_S_S, le_S/ qed-. lemma max_S2_le_S: ∀n1,n2,n. (n1 ∨ n2) ≤ n → (n1 ∨ ↑n2) ≤ ↑n. /2 width=1 by max_S1_le_S/ qed-. -lemma arith_j: ∀x,y,z. x-y-1 ≤ x-(y-z)-1. -/3 width=1 by monotonic_le_minus_l, monotonic_le_minus_r/ qed. - -lemma arith_k_sn: ∀z,x,y,n. z < x → x+n ≤ y → x-z-1+n ≤ y-z-1. -#z #x #y #n #Hzx #Hxny ->plus_minus [2: /2 width=1 by monotonic_le_minus_r/ ] ->plus_minus [2: /2 width=1 by lt_to_le/ ] -/2 width=1 by monotonic_le_minus_l2/ -qed. - -lemma arith_k_dx: ∀z,x,y,n. z < x → y ≤ x+n → y-z-1 ≤ x-z-1+n. -#z #x #y #n #Hzx #Hyxn ->plus_minus [2: /2 width=1 by monotonic_le_minus_r/ ] ->plus_minus [2: /2 width=1 by lt_to_le/ ] -/2 width=1 by monotonic_le_minus_l2/ -qed. - (* Inversion & forward lemmas ***********************************************) lemma lt_refl_false: ∀n. n < n → ⊥. @@ -198,6 +183,15 @@ 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-. @@ -217,8 +211,9 @@ lemma plus_xySz_x_false: ∀z,x,y. x + y + S z = x → ⊥. lemma plus_xSy_x_false: ∀y,x. x + S y = x → ⊥. /2 width=4 by plus_xySz_x_false/ qed-. -lemma pred_inv_refl: ∀m. pred m = m → m = 0. -* // normalize #m #H elim (lt_refl_false m) // +lemma pred_inv_fix_sn: ∀x. ↓x = x → 0 = x. +* // #x H -H @@ -313,6 +305,21 @@ lemma le_elim: ∀R:relation nat. #n1 #H elim (lt_le_false … H) -H // qed-. +lemma nat_elim_le_sn (Q:relation …): + (∀m1,m2. (∀m. m < m2-m1 → Q (m2-m) m2) → m1 ≤ m2 → Q m1 m2) → + ∀n1,n2. n1 ≤ n2 → Q n1 n2. +#Q #IH #n1 #n2 #Hn +<(minus_minus_m_m … Hn) -Hn +lapply (minus_le n2 n1) +let d ≝ (n2-n1) +@(nat_elim1 … d) -d -n1 #d +@pull_2 #Hd +<(minus_minus_m_m … Hd) in ⊢ (%→?); -Hd +let n1 ≝ (n2-d) #IHd +@IH -IH [| // ] #m #Hn +/4 width=3 by lt_to_le, lt_to_le_to_lt/ +qed-. + (* Iterators ****************************************************************) (* Note: see also: lib/arithemetics/bigops.ma *) @@ -330,10 +337,6 @@ lemma iter_O: ∀B:Type[0]. ∀f:B→B.∀b. f^0 b = b. lemma iter_S: ∀B:Type[0]. ∀f:B→B.∀b,l. f^(S l) b = f (f^l b). // qed. -lemma iter_SO: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^(l+1) b = f (f^l b). -#B #f #b #l >commutative_plus // -qed. - lemma iter_n_Sm: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^l (f b) = f (f^l b). #B #f #b #l elim l -l normalize // qed. @@ -368,3 +371,34 @@ lemma tri_gt: ∀A,a1,a2,a3,n1,n2. n2 < n1 → tri A n1 n2 a1 a2 a3 = a3. | #n1 #IH #n2 elim n2 -n2 /3 width=1 by monotonic_lt_pred/ ] qed. + +(* Decidability of predicates ***********************************************) + +lemma dec_lt (R:predicate nat): + (∀n. Decidable … (R n)) → + ∀n. Decidable … (∃∃m. m < n & R m). +#R #HR #n elim n -n [| #n * ] +[ @or_intror * /2 width=2 by lt_zero_false/ +| * /4 width=3 by lt_S, or_introl, ex2_intro/ +| #H0 elim (HR n) -HR + [ /3 width=3 by or_introl, ex2_intro/ + | #Hn @or_intror * #m #Hmn #Hm + elim (le_to_or_lt_eq … Hmn) -Hmn #H destruct [ -Hn | -H0 ] + /4 width=3 by lt_S_S_to_lt, ex2_intro/ + ] +] +qed-. + +lemma dec_min (R:predicate nat): + (∀n. Decidable … (R n)) → ∀n. R n → + ∃∃m. m ≤ n & R m & (∀p. p < m → R p → ⊥). +#R #HR #n +@(nat_elim1 n) -n #n #IH #Hn +elim (dec_lt … HR n) -HR [ -Hn | -IH ] +[ * #p #Hpn #Hp + elim (IH … Hpn Hp) -IH -Hp #m #Hmp #Hm #HNm + @(ex3_intro … Hm HNm) -HNm + /3 width=3 by lt_to_le, le_to_lt_to_lt/ +| /4 width=4 by ex3_intro, ex2_intro/ +] +qed-.