From 9c0d9ea5098c4b271fce972b685ea6a1ed4cd671 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 12 Oct 2007 09:57:49 +0000 Subject: [PATCH] Reorganization of results. --- matita/library/Z/dirichlet_product.ma | 509 +------------------------- matita/library/Z/moebius.ma | 5 + matita/library/Z/orders.ma | 115 ++++++ matita/library/Z/plus.ma | 24 ++ matita/library/Z/sigma_p.ma | 314 ++++++++++++++++ matita/library/Z/times.ma | 17 + matita/library/Z/z.ma | 5 + 7 files changed, 482 insertions(+), 507 deletions(-) diff --git a/matita/library/Z/dirichlet_product.ma b/matita/library/Z/dirichlet_product.ma index edc203761..6328bc7dc 100644 --- a/matita/library/Z/dirichlet_product.ma +++ b/matita/library/Z/dirichlet_product.ma @@ -23,417 +23,6 @@ definition dirichlet_product : (nat \to Z) \to (nat \to Z) \to nat \to Z \def sigma_p (S n) (\lambda d.divides_b d n) (\lambda d. (f d)*(g (div n d))). -(* da spostare *) - -(* spostati in div_and_mod.ma -theorem mod_SO: \forall n:nat. mod n (S O) = O. -intro. -apply sym_eq. -apply le_n_O_to_eq. -apply le_S_S_to_le. -apply lt_mod_m_m. -apply le_n. -qed. -theorem div_SO: \forall n:nat. div n (S O) = n. -intro. -rewrite > (div_mod ? (S O)) in \vdash (? ? ? %) - [rewrite > mod_SO. - rewrite < plus_n_O. - apply times_n_SO - |apply le_n - ] -qed.*) - -theorem and_true: \forall a,b:bool. -andb a b =true \to a =true \land b= true. -intro.elim a - [split - [reflexivity|assumption] - |apply False_ind. - apply not_eq_true_false. - apply sym_eq. - assumption - ] -qed. - -theorem lt_times_plus_times: \forall a,b,n,m:nat. -a < n \to b < m \to a*m + b < n*m. -intros 3. -apply (nat_case n) - [intros.apply False_ind.apply (not_le_Sn_O ? H) - |intros.simplify. - rewrite < sym_plus. - unfold. - change with (S b+a*m1 \leq m1+m*m1). - apply le_plus - [assumption - |apply le_times - [apply le_S_S_to_le.assumption - |apply le_n - ] - ] - ] -qed. - -theorem divides_to_divides_b_true1 : \forall n,m:nat. -O < m \to n \divides m \to divides_b n m = true. -intro. -elim (le_to_or_lt_eq O n (le_O_n n)) - [apply divides_to_divides_b_true - [assumption|assumption] - |apply False_ind. - rewrite < H in H2. - elim H2. - simplify in H3. - apply (not_le_Sn_O O). - rewrite > H3 in H1. - assumption - ] -qed. -(* spostato in primes.ma -theorem divides_to_div: \forall n,m.divides n m \to m/n*n = m. -intro. -elim (le_to_or_lt_eq O n (le_O_n n)) - [rewrite > plus_n_O. - rewrite < (divides_to_mod_O ? ? H H1). - apply sym_eq. - apply div_mod. - assumption - |elim H1. - generalize in match H2. - rewrite < H. - simplify. - intro. - rewrite > H3. - reflexivity - ] -qed.*) -(* spostato in div_and_mod.ma -theorem le_div: \forall n,m. O < n \to m/n \le m. -intros. -rewrite > (div_mod m n) in \vdash (? ? %) - [apply (trans_le ? (m/n*n)) - [rewrite > times_n_SO in \vdash (? % ?). - apply le_times - [apply le_n|assumption] - |apply le_plus_n_r - ] - |assumption - ] -qed.*) - -theorem sigma_p2_eq: -\forall g: nat \to nat \to Z. -\forall h11,h12,h21,h22: nat \to nat \to nat. -\forall n,m. -\forall p11,p21:nat \to bool. -\forall p12,p22:nat \to nat \to bool. -(\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to -p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true -\land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j -\land h11 i j < n \land h12 i j < m) \to -(\forall i,j. i < n \to j < m \to p11 i = true \to p12 i j = true \to -p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true -\land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j -\land (h21 i j) < n \land (h22 i j) < m) \to -sigma_p n p11 (\lambda x:nat .sigma_p m (p12 x) (\lambda y. g x y)) = -sigma_p n p21 (\lambda x:nat .sigma_p m (p22 x) (\lambda y. g (h11 x y) (h12 x y))). -intros. -rewrite < sigma_p2'. -rewrite < sigma_p2'. -apply sym_eq. -letin h := (\lambda x.(h11 (x/m) (x\mod m))*m + (h12 (x/m) (x\mod m))). -letin h1 := (\lambda x.(h21 (x/m) (x\mod m))*m + (h22 (x/m) (x\mod m))). -apply (trans_eq ? ? - (sigma_p (n*m) (\lambda x:nat.p21 (x/m)\land p22 (x/m) (x\mod m)) - (\lambda x:nat.g ((h x)/m) ((h x)\mod m)))) - [clear h.clear h1. - apply eq_sigma_p1 - [intros.reflexivity - |intros. - cut (O < m) - [cut (x/m < n) - [cut (x \mod m < m) - [elim (and_true ? ? H3). - elim (H ? ? Hcut1 Hcut2 H4 H5). - elim H6.clear H6. - elim H8.clear H8. - elim H6.clear H6. - elim H8.clear H8. - apply eq_f2 - [apply sym_eq. - apply div_plus_times. - assumption - |autobatch - ] - |apply lt_mod_m_m. - assumption - ] - |apply (lt_times_n_to_lt m) - [assumption - |apply (le_to_lt_to_lt ? x) - [apply (eq_plus_to_le ? ? (x \mod m)). - apply div_mod. - assumption - |assumption - ] - ] - ] - |apply not_le_to_lt.unfold.intro. - generalize in match H2. - apply (le_n_O_elim ? H4). - rewrite < times_n_O. - apply le_to_not_lt. - apply le_O_n - ] - ] - |apply (eq_sigma_p_gh ? h h1);intros - [cut (O < m) - [cut (i/m < n) - [cut (i \mod m < m) - [elim (and_true ? ? H3). - elim (H ? ? Hcut1 Hcut2 H4 H5). - elim H6.clear H6. - elim H8.clear H8. - elim H6.clear H6. - elim H8.clear H8. - cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))/m = - h11 (i/m) (i\mod m)) - [cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))\mod m = - h12 (i/m) (i\mod m)) - [rewrite > Hcut3. - rewrite > Hcut4. - rewrite > H6. - rewrite > H12. - reflexivity - |apply mod_plus_times. - assumption - ] - |apply div_plus_times. - assumption - ] - |apply lt_mod_m_m. - assumption - ] - |apply (lt_times_n_to_lt m) - [assumption - |apply (le_to_lt_to_lt ? i) - [apply (eq_plus_to_le ? ? (i \mod m)). - apply div_mod. - assumption - |assumption - ] - ] - ] - |apply not_le_to_lt.unfold.intro. - generalize in match H2. - apply (le_n_O_elim ? H4). - rewrite < times_n_O. - apply le_to_not_lt. - apply le_O_n - ] - |cut (O < m) - [cut (i/m < n) - [cut (i \mod m < m) - [elim (and_true ? ? H3). - elim (H ? ? Hcut1 Hcut2 H4 H5). - elim H6.clear H6. - elim H8.clear H8. - elim H6.clear H6. - elim H8.clear H8. - cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))/m = - h11 (i/m) (i\mod m)) - [cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))\mod m = - h12 (i/m) (i\mod m)) - [rewrite > Hcut3. - rewrite > Hcut4. - rewrite > H10. - rewrite > H11. - apply sym_eq. - apply div_mod. - assumption - |apply mod_plus_times. - assumption - ] - |apply div_plus_times. - assumption - ] - |apply lt_mod_m_m. - assumption - ] - |apply (lt_times_n_to_lt m) - [assumption - |apply (le_to_lt_to_lt ? i) - [apply (eq_plus_to_le ? ? (i \mod m)). - apply div_mod. - assumption - |assumption - ] - ] - ] - |apply not_le_to_lt.unfold.intro. - generalize in match H2. - apply (le_n_O_elim ? H4). - rewrite < times_n_O. - apply le_to_not_lt. - apply le_O_n - ] - |cut (O < m) - [cut (i/m < n) - [cut (i \mod m < m) - [elim (and_true ? ? H3). - elim (H ? ? Hcut1 Hcut2 H4 H5). - elim H6.clear H6. - elim H8.clear H8. - elim H6.clear H6. - elim H8.clear H8. - apply lt_times_plus_times - [assumption|assumption] - |apply lt_mod_m_m. - assumption - ] - |apply (lt_times_n_to_lt m) - [assumption - |apply (le_to_lt_to_lt ? i) - [apply (eq_plus_to_le ? ? (i \mod m)). - apply div_mod. - assumption - |assumption - ] - ] - ] - |apply not_le_to_lt.unfold.intro. - generalize in match H2. - apply (le_n_O_elim ? H4). - rewrite < times_n_O. - apply le_to_not_lt. - apply le_O_n - ] - |cut (O < m) - [cut (j/m < n) - [cut (j \mod m < m) - [elim (and_true ? ? H3). - elim (H1 ? ? Hcut1 Hcut2 H4 H5). - elim H6.clear H6. - elim H8.clear H8. - elim H6.clear H6. - elim H8.clear H8. - cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))/m = - h21 (j/m) (j\mod m)) - [cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))\mod m = - h22 (j/m) (j\mod m)) - [rewrite > Hcut3. - rewrite > Hcut4. - rewrite > H6. - rewrite > H12. - reflexivity - |apply mod_plus_times. - assumption - ] - |apply div_plus_times. - assumption - ] - |apply lt_mod_m_m. - assumption - ] - |apply (lt_times_n_to_lt m) - [assumption - |apply (le_to_lt_to_lt ? j) - [apply (eq_plus_to_le ? ? (j \mod m)). - apply div_mod. - assumption - |assumption - ] - ] - ] - |apply not_le_to_lt.unfold.intro. - generalize in match H2. - apply (le_n_O_elim ? H4). - rewrite < times_n_O. - apply le_to_not_lt. - apply le_O_n - ] - |cut (O < m) - [cut (j/m < n) - [cut (j \mod m < m) - [elim (and_true ? ? H3). - elim (H1 ? ? Hcut1 Hcut2 H4 H5). - elim H6.clear H6. - elim H8.clear H8. - elim H6.clear H6. - elim H8.clear H8. - cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))/m = - h21 (j/m) (j\mod m)) - [cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))\mod m = - h22 (j/m) (j\mod m)) - [rewrite > Hcut3. - rewrite > Hcut4. - rewrite > H10. - rewrite > H11. - apply sym_eq. - apply div_mod. - assumption - |apply mod_plus_times. - assumption - ] - |apply div_plus_times. - assumption - ] - |apply lt_mod_m_m. - assumption - ] - |apply (lt_times_n_to_lt m) - [assumption - |apply (le_to_lt_to_lt ? j) - [apply (eq_plus_to_le ? ? (j \mod m)). - apply div_mod. - assumption - |assumption - ] - ] - ] - |apply not_le_to_lt.unfold.intro. - generalize in match H2. - apply (le_n_O_elim ? H4). - rewrite < times_n_O. - apply le_to_not_lt. - apply le_O_n - ] - |cut (O < m) - [cut (j/m < n) - [cut (j \mod m < m) - [elim (and_true ? ? H3). - elim (H1 ? ? Hcut1 Hcut2 H4 H5). - elim H6.clear H6. - elim H8.clear H8. - elim H6.clear H6. - elim H8.clear H8. - apply (lt_times_plus_times ? ? ? m) - [assumption|assumption] - |apply lt_mod_m_m. - assumption - ] - |apply (lt_times_n_to_lt m) - [assumption - |apply (le_to_lt_to_lt ? j) - [apply (eq_plus_to_le ? ? (j \mod m)). - apply div_mod. - assumption - |assumption - ] - ] - ] - |apply not_le_to_lt.unfold.intro. - generalize in match H2. - apply (le_n_O_elim ? H4). - rewrite < times_n_O. - apply le_to_not_lt. - apply le_O_n - ] - ] - ] -qed. - (* dirichlet_product is associative only up to extensional equality *) theorem associative_dirichlet_product: \forall f,g,h:nat\to Z.\forall n:nat.O < n \to @@ -488,6 +77,8 @@ apply (trans_eq ? ? (\lambda d,d1:nat.d/d1) (S n) (S n) + (S n) + (S n) ? ? (\lambda d,d1:nat.divides_b d1 d) @@ -773,44 +364,6 @@ intro.apply (nat_case n) ] qed. -(* da spostare in times *) -definition Zone \def pos O. - -theorem Ztimes_Zone_l: \forall z:Z. Ztimes Zone z = z. -intro.unfold Zone.simplify. -elim z;simplify - [reflexivity - |rewrite < plus_n_O.reflexivity - |rewrite < plus_n_O.reflexivity - ] -qed. - -theorem Ztimes_Zone_r: \forall z:Z. Ztimes z Zone = z. -intro. -rewrite < sym_Ztimes. -apply Ztimes_Zone_l. -qed. - -theorem injective_Zplus_l: \forall x:Z.injective Z Z (\lambda y.y+x). -intro.simplify.intros (z y). -rewrite < Zplus_z_OZ. -rewrite < (Zplus_z_OZ y). -rewrite < (Zplus_Zopp x). -rewrite < (Zplus_Zopp x). -rewrite < assoc_Zplus. -rewrite < assoc_Zplus. -apply eq_f2 - [assumption|reflexivity] -qed. - -theorem injective_Zplus_r: \forall x:Z.injective Z Z (\lambda y.x+y). -intro.simplify.intros (z y). -apply (injective_Zplus_l x). -rewrite < sym_Zplus. -rewrite > H. -apply sym_Zplus. -qed. - theorem sigma_p_OZ: \forall p: nat \to bool.\forall n.sigma_p n p (\lambda m.OZ) = OZ. intros.elim n @@ -887,64 +440,6 @@ elim n ] qed. -(* da spostare *) -theorem notb_notb: \forall b:bool. notb (notb b) = b. -intros. -elim b;reflexivity. -qed. - -theorem injective_notb: injective bool bool notb. -unfold injective. -intros. -rewrite < notb_notb. -rewrite < (notb_notb y). -apply eq_f. -assumption. -qed. - -theorem divides_div: \forall d,n. divides d n \to divides (n/d) n. -intros. -apply (witness ? ? d). -apply sym_eq. -apply divides_to_div. -assumption. -qed. - -theorem divides_b_div_true: -\forall d,n. O < n \to - divides_b d n = true \to divides_b (n/d) n = true. -intros. -apply divides_to_divides_b_true1 - [assumption - |apply divides_div. - apply divides_b_true_to_divides. - assumption - ] -qed. - -(* spostato in primes.ma (non in div_and_mod.ma perche' serve il predicato divides) -theorem div_div: \forall n,d:nat. O < n \to divides d n \to -n/(n/d) = d. -intros. -apply (inj_times_l1 (n/d)) - [apply (lt_times_n_to_lt d) - [apply (divides_to_lt_O ? ? H H1). - |rewrite > divides_to_div;assumption - ] - |rewrite > divides_to_div - [rewrite > sym_times. - rewrite > divides_to_div - [reflexivity - |assumption - ] - |apply (witness ? ? d). - apply sym_eq. - apply divides_to_div. - assumption - ] - ] -qed. -*) theorem commutative_dirichlet_product: \forall f,g:nat \to Z.\forall n. O < n \to dirichlet_product f g n = dirichlet_product g f n. intros. diff --git a/matita/library/Z/moebius.ma b/matita/library/Z/moebius.ma index 33c9ad4be..d2c3765c3 100644 --- a/matita/library/Z/moebius.ma +++ b/matita/library/Z/moebius.ma @@ -40,6 +40,7 @@ definition moebius : nat \to Z \def let p \def (max n (\lambda p:nat.eqb (n \mod (nth_prime p)) O)) in moebius_aux (S p) n. +(* theorem moebius_O : moebius O = pos O. simplify. reflexivity. qed. @@ -56,6 +57,10 @@ theorem moebius_SSSO : moebius (S (S (S O))) = neg O. simplify.reflexivity. qed. +theorem moebius_SSSSO : moebius (S (S (S (S O)))) = OZ. +simplify.reflexivity. +qed. +*) theorem not_divides_to_p_ord_O: \forall n,i. Not (divides (nth_prime i) n) \to p_ord n (nth_prime i) = diff --git a/matita/library/Z/orders.ma b/matita/library/Z/orders.ma index 0a3cfbe1f..06b6a1ec4 100644 --- a/matita/library/Z/orders.ma +++ b/matita/library/Z/orders.ma @@ -76,6 +76,121 @@ cut (pos n < pos n \to False). apply Hcut.apply H.simplify.unfold lt.apply not_le_Sn_n. qed. +(* transitivity *) +theorem transitive_Zle : transitive Z Zle. +unfold transitive. +intros 3. +elim x 0 +[ (* x = OZ *) + elim y 0 + [ intros. assumption + | intro. + elim z + [ simplify. apply I + | simplify. apply I + | simplify. simplify in H1. assumption + ] + | intro. + elim z + [ simplify. apply I + | simplify. apply I + | simplify. simplify in H. assumption + ] + ] +| (* x = (pos n) *) + intro. + elim y 0 + [ intros. apply False_ind. apply H + | intros 2. + elim z 0 + [ simplify. intro. assumption + | intro. generalize in match H. simplify. apply trans_le + | intro. simplify. intro. assumption + ] + | intros 2. apply False_ind. apply H + ] +| (* x = (neg n) *) + intro. + elim y 0 + [ elim z 0 + [ simplify. intros. assumption + | intro. simplify. intros. assumption + | intro. simplify. intros. apply False_ind. apply H1 + ] + | intros 2. + elim z + [ apply False_ind. apply H1 + | simplify. apply I + | apply False_ind. apply H1 + ] + | intros 2. + elim z 0 + [ simplify. intro. assumption + | intro. simplify. intro. assumption + | intros. simplify. simplify in H. simplify in H1. + generalize in match H. generalize in match H1. apply trans_le + ] + ] +] +qed. + +variant trans_Zle: transitive Z Zle +\def transitive_Zle. + +theorem transitive_Zlt: transitive Z Zlt. +unfold. +intros 3. +elim x 0 +[ (* x = OZ *) + elim y 0 + [ intros. apply False_ind. apply H + | intro. + elim z + [ simplify. apply H1 + | simplify. apply I + | simplify. apply H1 + ] + | intros 2. apply False_ind. apply H + ] +| (* x = (pos n) *) + intro. + elim y 0 + [ intros. apply False_ind. apply H + | intros 2. + elim z 0 + [ simplify. intro. assumption + | intro. generalize in match H. simplify. apply trans_lt + | intro. simplify. intro. assumption + ] + | intros 2. apply False_ind. apply H + ] +| (* x = (neg n) *) + intro. + elim y 0 + [ elim z 0 + [ intros. simplify. apply I + | intro. simplify. intros. assumption + | intro. simplify. intros. apply False_ind. apply H1 + ] + | intros 2. + elim z + [ apply False_ind. apply H1 + | simplify. apply I + | apply False_ind. apply H1 + ] + | intros 2. + elim z 0 + [ simplify. intro. assumption + | intro. simplify. intro. assumption + | intros. simplify. simplify in H. simplify in H1. + generalize in match H. generalize in match H1. apply trans_lt + ] + ] +] +qed. + +variant trans_Zlt: transitive Z Zlt +\def transitive_Zlt. theorem irrefl_Zlt: irreflexive Z Zlt \def irreflexive_Zlt. diff --git a/matita/library/Z/plus.ma b/matita/library/Z/plus.ma index 2b439b92e..cd5651245 100644 --- a/matita/library/Z/plus.ma +++ b/matita/library/Z/plus.ma @@ -261,6 +261,10 @@ definition Zopp : Z \to Z \def (*CSC: the URI must disappear: there is a bug now *) interpretation "integer unary minus" 'uminus x = (cic:/matita/Z/plus/Zopp.con x). +theorem eq_OZ_Zopp_OZ : OZ = (- OZ). +reflexivity. +qed. + theorem Zopp_Zplus: \forall x,y:Z. -(x+y) = -x + -y. intros. elim x.elim y. @@ -299,6 +303,26 @@ rewrite > nat_compare_n_n. simplify.apply refl_eq. qed. +theorem injective_Zplus_l: \forall x:Z.injective Z Z (\lambda y.y+x). +intro.simplify.intros (z y). +rewrite < Zplus_z_OZ. +rewrite < (Zplus_z_OZ y). +rewrite < (Zplus_Zopp x). +rewrite < (Zplus_Zopp x). +rewrite < assoc_Zplus. +rewrite < assoc_Zplus. +apply eq_f2 + [assumption|reflexivity] +qed. + +theorem injective_Zplus_r: \forall x:Z.injective Z Z (\lambda y.x+y). +intro.simplify.intros (z y). +apply (injective_Zplus_l x). +rewrite < sym_Zplus. +rewrite > H. +apply sym_Zplus. +qed. + (* minus *) definition Zminus : Z \to Z \to Z \def \lambda x,y:Z. x + (-y). diff --git a/matita/library/Z/sigma_p.ma b/matita/library/Z/sigma_p.ma index b246b8444..8b4c87d3e 100644 --- a/matita/library/Z/sigma_p.ma +++ b/matita/library/Z/sigma_p.ma @@ -312,3 +312,317 @@ apply eq_sigma_p |intros.apply sym_Ztimes ] qed. + + +(* sigma from n1*m1 to n2*m2 *) +theorem sigma_p2_eq: +\forall g: nat \to nat \to Z. +\forall h11,h12,h21,h22: nat \to nat \to nat. +\forall n1,m1,n2,m2. +\forall p11,p21:nat \to bool. +\forall p12,p22:nat \to nat \to bool. +(\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to +p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true +\land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j +\land h11 i j < n1 \land h12 i j < m1) \to +(\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to +p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true +\land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j +\land (h21 i j) < n2 \land (h22 i j) < m2) \to +sigma_p n1 p11 (\lambda x:nat .sigma_p m1 (p12 x) (\lambda y. g x y)) = +sigma_p n2 p21 (\lambda x:nat .sigma_p m2 (p22 x) (\lambda y. g (h11 x y) (h12 x y))). +intros. +rewrite < sigma_p2'. +rewrite < sigma_p2'. +apply sym_eq. +letin h := (\lambda x.(h11 (x/m2) (x\mod m2))*m1 + (h12 (x/m2) (x\mod m2))). +letin h1 := (\lambda x.(h21 (x/m1) (x\mod m1))*m2 + (h22 (x/m1) (x\mod m1))). +apply (trans_eq ? ? + (sigma_p (n2*m2) (\lambda x:nat.p21 (x/m2)\land p22 (x/m2) (x\mod m2)) + (\lambda x:nat.g ((h x)/m1) ((h x)\mod m1)))) + [clear h.clear h1. + apply eq_sigma_p1 + [intros.reflexivity + |intros. + cut (O < m2) + [cut (x/m2 < n2) + [cut (x \mod m2 < m2) + [elim (and_true ? ? H3). + elim (H ? ? Hcut1 Hcut2 H4 H5). + elim H6.clear H6. + elim H8.clear H8. + elim H6.clear H6. + elim H8.clear H8. + apply eq_f2 + [apply sym_eq. + apply div_plus_times. + assumption + |autobatch + ] + |apply lt_mod_m_m. + assumption + ] + |apply (lt_times_n_to_lt m2) + [assumption + |apply (le_to_lt_to_lt ? x) + [apply (eq_plus_to_le ? ? (x \mod m2)). + apply div_mod. + assumption + |assumption + ] + ] + ] + |apply not_le_to_lt.unfold.intro. + generalize in match H2. + apply (le_n_O_elim ? H4). + rewrite < times_n_O. + apply le_to_not_lt. + apply le_O_n + ] + ] + |apply (eq_sigma_p_gh ? h h1);intros + [cut (O < m2) + [cut (i/m2 < n2) + [cut (i \mod m2 < m2) + [elim (and_true ? ? H3). + elim (H ? ? Hcut1 Hcut2 H4 H5). + elim H6.clear H6. + elim H8.clear H8. + elim H6.clear H6. + elim H8.clear H8. + cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 = + h11 (i/m2) (i\mod m2)) + [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 = + h12 (i/m2) (i\mod m2)) + [rewrite > Hcut3. + rewrite > Hcut4. + rewrite > H6. + rewrite > H12. + reflexivity + |apply mod_plus_times. + assumption + ] + |apply div_plus_times. + assumption + ] + |apply lt_mod_m_m. + assumption + ] + |apply (lt_times_n_to_lt m2) + [assumption + |apply (le_to_lt_to_lt ? i) + [apply (eq_plus_to_le ? ? (i \mod m2)). + apply div_mod. + assumption + |assumption + ] + ] + ] + |apply not_le_to_lt.unfold.intro. + generalize in match H2. + apply (le_n_O_elim ? H4). + rewrite < times_n_O. + apply le_to_not_lt. + apply le_O_n + ] + |cut (O < m2) + [cut (i/m2 < n2) + [cut (i \mod m2 < m2) + [elim (and_true ? ? H3). + elim (H ? ? Hcut1 Hcut2 H4 H5). + elim H6.clear H6. + elim H8.clear H8. + elim H6.clear H6. + elim H8.clear H8. + cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 = + h11 (i/m2) (i\mod m2)) + [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 = + h12 (i/m2) (i\mod m2)) + [rewrite > Hcut3. + rewrite > Hcut4. + rewrite > H10. + rewrite > H11. + apply sym_eq. + apply div_mod. + assumption + |apply mod_plus_times. + assumption + ] + |apply div_plus_times. + assumption + ] + |apply lt_mod_m_m. + assumption + ] + |apply (lt_times_n_to_lt m2) + [assumption + |apply (le_to_lt_to_lt ? i) + [apply (eq_plus_to_le ? ? (i \mod m2)). + apply div_mod. + assumption + |assumption + ] + ] + ] + |apply not_le_to_lt.unfold.intro. + generalize in match H2. + apply (le_n_O_elim ? H4). + rewrite < times_n_O. + apply le_to_not_lt. + apply le_O_n + ] + |cut (O < m2) + [cut (i/m2 < n2) + [cut (i \mod m2 < m2) + [elim (and_true ? ? H3). + elim (H ? ? Hcut1 Hcut2 H4 H5). + elim H6.clear H6. + elim H8.clear H8. + elim H6.clear H6. + elim H8.clear H8. + apply lt_times_plus_times + [assumption|assumption] + |apply lt_mod_m_m. + assumption + ] + |apply (lt_times_n_to_lt m2) + [assumption + |apply (le_to_lt_to_lt ? i) + [apply (eq_plus_to_le ? ? (i \mod m2)). + apply div_mod. + assumption + |assumption + ] + ] + ] + |apply not_le_to_lt.unfold.intro. + generalize in match H2. + apply (le_n_O_elim ? H4). + rewrite < times_n_O. + apply le_to_not_lt. + apply le_O_n + ] + |cut (O < m1) + [cut (j/m1 < n1) + [cut (j \mod m1 < m1) + [elim (and_true ? ? H3). + elim (H1 ? ? Hcut1 Hcut2 H4 H5). + elim H6.clear H6. + elim H8.clear H8. + elim H6.clear H6. + elim H8.clear H8. + cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 = + h21 (j/m1) (j\mod m1)) + [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 = + h22 (j/m1) (j\mod m1)) + [rewrite > Hcut3. + rewrite > Hcut4. + rewrite > H6. + rewrite > H12. + reflexivity + |apply mod_plus_times. + assumption + ] + |apply div_plus_times. + assumption + ] + |apply lt_mod_m_m. + assumption + ] + |apply (lt_times_n_to_lt m1) + [assumption + |apply (le_to_lt_to_lt ? j) + [apply (eq_plus_to_le ? ? (j \mod m1)). + apply div_mod. + assumption + |assumption + ] + ] + ] + |apply not_le_to_lt.unfold.intro. + generalize in match H2. + apply (le_n_O_elim ? H4). + rewrite < times_n_O. + apply le_to_not_lt. + apply le_O_n + ] + |cut (O < m1) + [cut (j/m1 < n1) + [cut (j \mod m1 < m1) + [elim (and_true ? ? H3). + elim (H1 ? ? Hcut1 Hcut2 H4 H5). + elim H6.clear H6. + elim H8.clear H8. + elim H6.clear H6. + elim H8.clear H8. + cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 = + h21 (j/m1) (j\mod m1)) + [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 = + h22 (j/m1) (j\mod m1)) + [rewrite > Hcut3. + rewrite > Hcut4. + rewrite > H10. + rewrite > H11. + apply sym_eq. + apply div_mod. + assumption + |apply mod_plus_times. + assumption + ] + |apply div_plus_times. + assumption + ] + |apply lt_mod_m_m. + assumption + ] + |apply (lt_times_n_to_lt m1) + [assumption + |apply (le_to_lt_to_lt ? j) + [apply (eq_plus_to_le ? ? (j \mod m1)). + apply div_mod. + assumption + |assumption + ] + ] + ] + |apply not_le_to_lt.unfold.intro. + generalize in match H2. + apply (le_n_O_elim ? H4). + rewrite < times_n_O. + apply le_to_not_lt. + apply le_O_n + ] + |cut (O < m1) + [cut (j/m1 < n1) + [cut (j \mod m1 < m1) + [elim (and_true ? ? H3). + elim (H1 ? ? Hcut1 Hcut2 H4 H5). + elim H6.clear H6. + elim H8.clear H8. + elim H6.clear H6. + elim H8.clear H8. + apply (lt_times_plus_times ? ? ? m2) + [assumption|assumption] + |apply lt_mod_m_m. + assumption + ] + |apply (lt_times_n_to_lt m1) + [assumption + |apply (le_to_lt_to_lt ? j) + [apply (eq_plus_to_le ? ? (j \mod m1)). + apply div_mod. + assumption + |assumption + ] + ] + ] + |apply not_le_to_lt.unfold.intro. + generalize in match H2. + apply (le_n_O_elim ? H4). + rewrite < times_n_O. + apply le_to_not_lt. + apply le_O_n + ] + ] + ] +qed. \ No newline at end of file diff --git a/matita/library/Z/times.ma b/matita/library/Z/times.ma index 58de9c827..90a71b520 100644 --- a/matita/library/Z/times.ma +++ b/matita/library/Z/times.ma @@ -42,6 +42,8 @@ simplify.reflexivity. simplify.reflexivity. qed. +definition Zone \def pos O. + theorem Ztimes_neg_Zopp: \forall n:nat.\forall x:Z. neg n * x = - (pos n * x). intros.elim x. @@ -68,6 +70,21 @@ qed. variant sym_Ztimes : \forall x,y:Z. x*y = y*x \def symmetric_Ztimes. +theorem Ztimes_Zone_l: \forall z:Z. Ztimes Zone z = z. +intro.unfold Zone.simplify. +elim z;simplify + [reflexivity + |rewrite < plus_n_O.reflexivity + |rewrite < plus_n_O.reflexivity + ] +qed. + +theorem Ztimes_Zone_r: \forall z:Z. Ztimes z Zone = z. +intro. +rewrite < sym_Ztimes. +apply Ztimes_Zone_l. +qed. + theorem associative_Ztimes: associative Z Ztimes. unfold associative. intros.elim x. diff --git a/matita/library/Z/z.ma b/matita/library/Z/z.ma index d8b829ec1..64b608cb9 100644 --- a/matita/library/Z/z.ma +++ b/matita/library/Z/z.ma @@ -34,6 +34,11 @@ definition neg_Z_of_nat \def [ O \Rightarrow OZ | (S n)\Rightarrow neg n]. +lemma pos_n_eq_S_n : \forall n : nat. + (pos n) = (S n). +intro.reflexivity. +qed. + definition abs \def \lambda z. match z with -- 2.39.2