From deec6d7e7a26f2165b17b95a932036325d9a47fe Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 9 May 2007 10:53:28 +0000 Subject: [PATCH] Proof of the moebius inversion theorem --- .../matita/library/Z/dirichlet_product.ma | 1022 +++++++++++++++++ helm/software/matita/library/Z/inversion.ma | 101 ++ helm/software/matita/library/Z/moebius.ma | 3 + helm/software/matita/library/Z/sigma_p.ma | 144 ++- 4 files changed, 1227 insertions(+), 43 deletions(-) create mode 100644 helm/software/matita/library/Z/dirichlet_product.ma create mode 100644 helm/software/matita/library/Z/inversion.ma diff --git a/helm/software/matita/library/Z/dirichlet_product.ma b/helm/software/matita/library/Z/dirichlet_product.ma new file mode 100644 index 000000000..c4706378c --- /dev/null +++ b/helm/software/matita/library/Z/dirichlet_product.ma @@ -0,0 +1,1022 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / Matita is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/Z/dirichlet_product". + +include "Z/sigma_p.ma". +include "Z/times.ma". + +definition dirichlet_product : (nat \to Z) \to (nat \to Z) \to nat \to Z \def +\lambda f,g.\lambda n. +sigma_p (S n) + (\lambda d.divides_b d n) (\lambda d. (f d)*(g (div n d))). + +(* da spostare *) + +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. + +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. + +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 + |auto + ] + |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 +dirichlet_product (dirichlet_product f g) h n + = dirichlet_product f (dirichlet_product g h) n. +intros. +unfold dirichlet_product. +unfold dirichlet_product. +apply (trans_eq ? ? +(sigma_p (S n) (\lambda d:nat.divides_b d n) +(\lambda d:nat + .sigma_p (S n) (\lambda d1:nat.divides_b d1 d) (\lambda d1:nat.f d1*g (d/d1)*h (n/d))))) + [apply eq_sigma_p1 + [intros.reflexivity + |intros. + apply (trans_eq ? ? + (sigma_p (S x) (\lambda d1:nat.divides_b d1 x) (\lambda d1:nat.f d1*g (x/d1)*h (n/x)))) + [apply Ztimes_sigma_pr + |(* hint solleva unification uncertain ?? *) + apply sym_eq. + apply false_to_eq_sigma_p + [assumption + |intros. + apply not_divides_to_divides_b_false + [apply (lt_to_le_to_lt ? (S x)) + [apply lt_O_S|assumption] + |unfold Not. intro. + apply (lt_to_not_le ? ? H3). + apply divides_to_le + [apply (divides_b_true_to_lt_O ? ? H H2). + |assumption + ] + ] + ] + ] + ] + |apply (trans_eq ? ? + (sigma_p (S n) (\lambda d:nat.divides_b d n) + (\lambda d:nat + .sigma_p (S n) (\lambda d1:nat.divides_b d1 (n/d)) + (\lambda d1:nat.f d*g d1*h ((n/d)/d1))))) + [apply (trans_eq ? ? + (sigma_p (S n) (\lambda d:nat.divides_b d n) + (\lambda d:nat + .sigma_p (S n) (\lambda d1:nat.divides_b d1 (n/d)) + (\lambda d1:nat.f d*g ((times d d1)/d)*h ((n/times d d1)))))) + [apply (sigma_p2_eq + (\lambda d,d1.f d1*g (d/d1)*h (n/d)) + (\lambda d,d1:nat.times d d1) + (\lambda d,d1:nat.d) + (\lambda d,d1:nat.d1) + (\lambda d,d1:nat.d/d1) + (S n) + (S n) + ? + ? + (\lambda d,d1:nat.divides_b d1 d) + (\lambda d,d1:nat.divides_b d1 (n/d)) + ) + [intros. + split + [split + [split + [split + [split + [apply divides_to_divides_b_true1 + [assumption + |apply (witness ? ? ((n/i)/j)). + rewrite > assoc_times. + rewrite > sym_times in \vdash (? ? ? (? ? %)). + rewrite > divides_to_div + [rewrite > sym_times. + rewrite > divides_to_div + [reflexivity + |apply divides_b_true_to_divides. + assumption + ] + |apply divides_b_true_to_divides. + assumption + ] + ] + |apply divides_to_divides_b_true + [apply (divides_b_true_to_lt_O ? ? H H3) + |apply (witness ? ? j). + reflexivity + ] + ] + |reflexivity + ] + |rewrite < sym_times. + rewrite > (plus_n_O (j*i)). + apply div_plus_times. + apply (divides_b_true_to_lt_O ? ? H H3) + ] + |apply (le_to_lt_to_lt ? (i*(n/i))) + [apply le_times + [apply le_n + |apply divides_to_le + [elim (le_to_or_lt_eq ? ? (le_O_n (n/i))) + [assumption + |apply False_ind. + apply (lt_to_not_le ? ? H). + rewrite < (divides_to_div i n) + [rewrite < H5. + apply le_n + |apply divides_b_true_to_divides. + assumption + ] + ] + |apply divides_b_true_to_divides. + assumption + ] + ] + |rewrite < sym_times. + rewrite > divides_to_div + [apply le_n + |apply divides_b_true_to_divides. + assumption + ] + ] + ] + |assumption + ] + |intros. + split + [split + [split + [split + [split + [apply divides_to_divides_b_true1 + [assumption + |apply (transitive_divides ? i) + [apply divides_b_true_to_divides. + assumption + |apply divides_b_true_to_divides. + assumption + ] + ] + |apply divides_to_divides_b_true + [apply (divides_b_true_to_lt_O i (i/j)) + [apply (divides_b_true_to_lt_O ? ? ? H3). + assumption + |apply divides_to_divides_b_true1 + [apply (divides_b_true_to_lt_O ? ? ? H3). + assumption + |apply (witness ? ? j). + apply sym_eq. + apply divides_to_div. + apply divides_b_true_to_divides. + assumption + ] + ] + |apply (witness ? ? (n/i)). + apply (inj_times_l1 j) + [apply (divides_b_true_to_lt_O ? ? ? H4). + apply (divides_b_true_to_lt_O ? ? ? H3). + assumption + |rewrite > divides_to_div + [rewrite > sym_times in \vdash (? ? ? (? % ?)). + rewrite > assoc_times. + rewrite > divides_to_div + [rewrite > divides_to_div + [reflexivity + |apply divides_b_true_to_divides. + assumption + ] + |apply divides_b_true_to_divides. + assumption + ] + |apply (transitive_divides ? i) + [apply divides_b_true_to_divides. + assumption + |apply divides_b_true_to_divides. + assumption + ] + ] + ] + ] + ] + |rewrite < sym_times. + apply divides_to_div. + apply divides_b_true_to_divides. + assumption + ] + |reflexivity + ] + |assumption + ] + |apply (le_to_lt_to_lt ? i) + [apply le_div. + apply (divides_b_true_to_lt_O ? ? ? H4). + apply (divides_b_true_to_lt_O ? ? ? H3). + assumption + |assumption + ] + ] + ] + |apply eq_sigma_p1 + [intros.reflexivity + |intros. + apply eq_sigma_p1 + [intros.reflexivity + |intros. + apply eq_f2 + [apply eq_f2 + [reflexivity + |apply eq_f. + rewrite > sym_times. + rewrite > (plus_n_O (x1*x)). + apply div_plus_times. + apply (divides_b_true_to_lt_O ? ? ? H2). + assumption + ] + |apply eq_f. + cut (O < x) + [cut (O < x1) + [apply (inj_times_l1 (x*x1)) + [rewrite > (times_n_O O). + apply lt_times;assumption + |rewrite > divides_to_div + [rewrite > sym_times in \vdash (? ? ? (? ? %)). + rewrite < assoc_times. + rewrite > divides_to_div + [rewrite > divides_to_div + [reflexivity + |apply divides_b_true_to_divides. + assumption + ] + |apply divides_b_true_to_divides. + assumption + ] + |elim (divides_b_true_to_divides ? ? H4). + apply (witness ? ? n2). + rewrite > assoc_times. + rewrite < H5. + rewrite < sym_times. + apply sym_eq. + apply divides_to_div. + apply divides_b_true_to_divides. + assumption + ] + ] + |apply (divides_b_true_to_lt_O ? ? ? H4). + apply (lt_times_n_to_lt x) + [assumption + |simplify. + rewrite > divides_to_div + [assumption + |apply (divides_b_true_to_divides ? ? H2). + assumption + ] + ] + ] + |apply (divides_b_true_to_lt_O ? ? ? H2). + assumption + ] + ] + ] + ] + ] + |apply eq_sigma_p1 + [intros.reflexivity + |intros. + apply (trans_eq ? ? + (sigma_p (S n) (\lambda d1:nat.divides_b d1 (n/x)) (\lambda d1:nat.f x*(g d1*h (n/x/d1))))) + [apply eq_sigma_p + [intros.reflexivity + |intros.apply assoc_Ztimes + ] + |apply (trans_eq ? ? + (sigma_p (S (n/x)) (\lambda d1:nat.divides_b d1 (n/x)) (\lambda d1:nat.f x*(g d1*h (n/x/d1))))) + [apply false_to_eq_sigma_p + [apply le_S_S. + cut (O < x) + [apply (le_times_to_le x) + [assumption + |rewrite > sym_times. + rewrite > divides_to_div + [apply le_times_n. + assumption + |apply divides_b_true_to_divides. + assumption + ] + ] + |apply (divides_b_true_to_lt_O ? ? ? H2). + assumption + ] + |intros. + apply not_divides_to_divides_b_false + [apply (trans_le ? ? ? ? H3). + apply le_S_S. + apply le_O_n + |unfold Not.intro. + apply (le_to_not_lt ? ? H3). + apply le_S_S. + apply divides_to_le + [apply (lt_times_n_to_lt x) + [apply (divides_b_true_to_lt_O ? ? ? H2). + assumption + |simplify. + rewrite > divides_to_div + [assumption + |apply (divides_b_true_to_divides ? ? H2). + assumption + ] + ] + |assumption + ] + ] + ] + |apply sym_eq. + apply Ztimes_sigma_pl + ] + ] + ] + ] + ] +qed. + +definition is_one: nat \to Z \def +\lambda n. + match n with + [O \Rightarrow OZ + | (S p) \Rightarrow + match p with + [ O \Rightarrow pos O + | (S q) \Rightarrow OZ]] +. + +theorem is_one_OZ: \forall n. n \neq S O \to is_one n = OZ. +intro.apply (nat_case n) + [intro.reflexivity + |intro. apply (nat_case m) + [intro.apply False_ind.apply H.reflexivity + |intros.reflexivity + ] + ] +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 + [reflexivity + |apply (bool_elim ? (p n1));intro + [rewrite > true_to_sigma_p_Sn + [rewrite > sym_Zplus. + rewrite > Zplus_z_OZ. + assumption + |assumption + ] + |rewrite > false_to_sigma_p_Sn + [assumption + |assumption + ] + ] + ] +qed. + +theorem dirichlet_product_is_one_r: +\forall f:nat\to Z.\forall n:nat. + dirichlet_product f is_one n = f n. +intros. +elim n + [unfold dirichlet_product. + rewrite > true_to_sigma_p_Sn + [rewrite > Ztimes_Zone_r. + rewrite > Zplus_z_OZ. + reflexivity + |reflexivity + ] + |unfold dirichlet_product. + rewrite > true_to_sigma_p_Sn + [rewrite > div_n_n + [rewrite > Ztimes_Zone_r. + rewrite < Zplus_z_OZ in \vdash (? ? ? %). + apply eq_f2 + [reflexivity + |apply (trans_eq ? ? (sigma_p (S n1) + (\lambda d:nat.divides_b d (S n1)) (\lambda d:nat.OZ))) + [apply eq_sigma_p1;intros + [reflexivity + |rewrite > is_one_OZ + [apply Ztimes_z_OZ + |unfold Not.intro. + apply (lt_to_not_le ? ? H1). + rewrite > (times_n_SO x). + rewrite > sym_times. + rewrite < H3. + rewrite > (div_mod ? x) in \vdash (? % ?) + [rewrite > divides_to_mod_O + [rewrite < plus_n_O. + apply le_n + |apply (divides_b_true_to_lt_O ? ? ? H2). + apply lt_O_S + |apply divides_b_true_to_divides. + assumption + ] + |apply (divides_b_true_to_lt_O ? ? ? H2). + apply lt_O_S + ] + ] + ] + |apply sigma_p_OZ + ] + ] + |apply lt_O_S + ] + |apply divides_to_divides_b_true + [apply lt_O_S + |apply divides_n_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. + +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. +unfold dirichlet_product. +apply (trans_eq ? ? + (sigma_p (S n) (\lambda d:nat.divides_b d n) + (\lambda d:nat.g (n/d) * f (n/(n/d))))) + [apply eq_sigma_p1;intros + [reflexivity + |rewrite > div_div + [apply sym_Ztimes. + |assumption + |apply divides_b_true_to_divides. + assumption + ] + ] + |apply (eq_sigma_p_gh ? (\lambda d.(n/d)) (\lambda d.(n/d))) + [intros. + apply divides_b_div_true;assumption + |intros. + apply div_div + [assumption + |apply divides_b_true_to_divides. + assumption + ] + |intros. + apply le_S_S. + apply le_div. + apply (divides_b_true_to_lt_O ? ? H H2) + |intros. + apply divides_b_div_true;assumption + |intros. + apply div_div + [assumption + |apply divides_b_true_to_divides. + assumption + ] + |intros. + apply le_S_S. + apply le_div. + apply (divides_b_true_to_lt_O ? ? H H2) + ] + ] +qed. + +theorem dirichlet_product_is_one_l: +\forall f:nat\to Z.\forall n:nat. +O < n \to dirichlet_product is_one f n = f n. +intros. +rewrite > commutative_dirichlet_product. +apply dirichlet_product_is_one_r. +assumption. +qed. + +theorem dirichlet_product_one_r: +\forall f:nat\to Z.\forall n:nat. O < n \to +dirichlet_product f (\lambda n.Zone) n = +sigma_p (S n) (\lambda d.divides_b d n) f. +intros. +unfold dirichlet_product. +apply eq_sigma_p;intros + [reflexivity + |simplify in \vdash (? ? (? ? %) ?). + apply Ztimes_Zone_r + ] +qed. + +theorem dirichlet_product_one_l: +\forall f:nat\to Z.\forall n:nat. O < n \to +dirichlet_product (\lambda n.Zone) f n = +sigma_p (S n) (\lambda d.divides_b d n) f. +intros. +rewrite > commutative_dirichlet_product + [apply dirichlet_product_one_r. + assumption + |assumption + ] +qed. diff --git a/helm/software/matita/library/Z/inversion.ma b/helm/software/matita/library/Z/inversion.ma new file mode 100644 index 000000000..d93a75268 --- /dev/null +++ b/helm/software/matita/library/Z/inversion.ma @@ -0,0 +1,101 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / Matita is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/Z/inversion". + +include "Z/dirichlet_product.ma". +include "Z/moebius.ma". + +definition sigma_div: (nat \to Z) \to nat \to Z \def +\lambda f.\lambda n. sigma_p (S n) (\lambda d.divides_b d n) f. + +theorem sigma_div_moebius: +\forall n:nat. O < n \to sigma_div moebius n = is_one n. +intros.elim H + [reflexivity + |rewrite > is_one_OZ + [unfold sigma_div. + apply sigma_p_moebius. + apply le_S_S. + assumption + |unfold Not.intro. + apply (lt_to_not_eq ? ? H1). + apply injective_S. + apply sym_eq. + assumption + ] + ] +qed. + +(* moebius inversion theorem *) +theorem inversion: \forall f:nat \to Z.\forall n:nat.O < n \to +dirichlet_product moebius (sigma_div f) n = f n. +intros. +rewrite > commutative_dirichlet_product + [apply (trans_eq ? ? (dirichlet_product (dirichlet_product f (\lambda n.Zone)) moebius n)) + [unfold dirichlet_product. + apply eq_sigma_p1;intros + [reflexivity + |apply eq_f2 + [apply sym_eq. + unfold sigma_div. + apply dirichlet_product_one_r. + apply (divides_b_true_to_lt_O ? ? H H2) + |reflexivity + ] + ] + |rewrite > associative_dirichlet_product + [apply (trans_eq ? ? (dirichlet_product f (sigma_div moebius) n)) + [unfold dirichlet_product. + apply eq_sigma_p1;intros + [reflexivity + |apply eq_f2 + [reflexivity + |unfold sigma_div. + apply dirichlet_product_one_l. + apply (lt_times_n_to_lt x) + [apply (divides_b_true_to_lt_O ? ? H H2) + |rewrite > divides_to_div + [assumption + |apply (divides_b_true_to_divides ? ? H2) + ] + ] + ] + ] + |apply (trans_eq ? ? (dirichlet_product f is_one n)) + [unfold dirichlet_product. + apply eq_sigma_p1;intros + [reflexivity + |apply eq_f2 + [reflexivity + |apply sigma_div_moebius. + apply (lt_times_n_to_lt x) + [apply (divides_b_true_to_lt_O ? ? H H2) + |rewrite > divides_to_div + [assumption + |apply (divides_b_true_to_divides ? ? H2) + ] + ] + ] + ] + |apply dirichlet_product_is_one_r + ] + ] + |assumption + ] + ] + |assumption + ] +qed. + \ No newline at end of file diff --git a/helm/software/matita/library/Z/moebius.ma b/helm/software/matita/library/Z/moebius.ma index e91bf8df9..98ffccd40 100644 --- a/helm/software/matita/library/Z/moebius.ma +++ b/helm/software/matita/library/Z/moebius.ma @@ -527,3 +527,6 @@ lapply (exp_ord (nth_prime (max_prime_factor n)) n) |apply lt_to_le.assumption ] qed. + + + diff --git a/helm/software/matita/library/Z/sigma_p.ma b/helm/software/matita/library/Z/sigma_p.ma index 27baf8db5..73b29a38c 100644 --- a/helm/software/matita/library/Z/sigma_p.ma +++ b/helm/software/matita/library/Z/sigma_p.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/Z/sigma_p.ma". -include "Z/plus.ma". +include "Z/times.ma". include "nat/primes.ma". include "nat/ord.ma". @@ -220,6 +220,68 @@ elim n ] qed. +(* a stronger, dependent version, required e.g. for dirichlet product *) +theorem sigma_p2' : +\forall n,m:nat. +\forall p1:nat \to bool. +\forall p2:nat \to nat \to bool. +\forall g: nat \to nat \to Z. +sigma_p (n*m) + (\lambda x.andb (p1 (div x m)) (p2 (div x m) (mod x m))) + (\lambda x.g (div x m) (mod x m)) = +sigma_p n p1 + (\lambda x.sigma_p m (p2 x) (g x)). +intros. +elim n + [simplify.reflexivity + |apply (bool_elim ? (p1 n1)) + [intro. + rewrite > (true_to_sigma_p_Sn ? ? ? H1). + simplify in \vdash (? ? (? % ? ?) ?); + rewrite > sigma_p_plus. + rewrite < H. + apply eq_f2 + [apply eq_sigma_p + [intros. + rewrite > sym_plus. + rewrite > (div_plus_times ? ? ? H2). + rewrite > (mod_plus_times ? ? ? H2). + rewrite > H1. + simplify.reflexivity + |intros. + rewrite > sym_plus. + rewrite > (div_plus_times ? ? ? H2). + rewrite > (mod_plus_times ? ? ? H2). + rewrite > H1. + simplify.reflexivity. + ] + |reflexivity + ] + |intro. + rewrite > (false_to_sigma_p_Sn ? ? ? H1). + simplify in \vdash (? ? (? % ? ?) ?); + rewrite > sigma_p_plus. + rewrite > H. + apply (trans_eq ? ? (O+(sigma_p n1 p1 (\lambda x:nat.sigma_p m (p2 x) (g x))))) + [apply eq_f2 + [rewrite > (eq_sigma_p ? (\lambda x.false) ? (\lambda x:nat.g ((x+n1*m)/m) ((x+n1*m)\mod m))) + [apply sigma_p_false + |intros. + rewrite > sym_plus. + rewrite > (div_plus_times ? ? ? H2). + rewrite > (mod_plus_times ? ? ? H2). + rewrite > H1. + simplify.reflexivity + |intros.reflexivity. + ] + |reflexivity + ] + |reflexivity + ] + ] + ] +qed. + lemma sigma_p_gi: \forall g: nat \to Z. \forall n,i.\forall p:nat \to bool.i < n \to p i = true \to sigma_p n p g = g i + sigma_p n (\lambda x. andb (p x) (notb (eqb x i))) g. @@ -431,45 +493,41 @@ elim n ] qed. -definition p_ord_times \def -\lambda p,m,x. - match p_ord x p with - [pair q r \Rightarrow r*m+q]. - -theorem eq_p_ord_times: \forall p,m,x. -p_ord_times p m x = (ord_rem x p)*m+(ord x p). -intros.unfold p_ord_times. unfold ord_rem. -unfold ord. -elim (p_ord x p). -reflexivity. -qed. - -theorem div_p_ord_times: -\forall p,m,x. ord x p < m \to p_ord_times p m x / m = ord_rem x p. -intros.rewrite > eq_p_ord_times. -apply div_plus_times. -assumption. -qed. - -theorem mod_p_ord_times: -\forall p,m,x. ord x p < m \to p_ord_times p m x \mod m = ord x p. -intros.rewrite > eq_p_ord_times. -apply mod_plus_times. -assumption. -qed. - -theorem times_O_to_O: \forall n,m:nat.n*m = O \to n = O \lor m= O. -apply nat_elim2;intros - [left.reflexivity - |right.reflexivity - |apply False_ind. - simplify in H1. - apply (not_eq_O_S ? (sym_eq ? ? ? H1)) +(* sigma_p and Ztimes *) +lemma Ztimes_sigma_pl: \forall z:Z.\forall n:nat.\forall p. \forall f. +z * (sigma_p n p f) = sigma_p n p (\lambda i.z*(f i)). +intros. +elim n + [rewrite > Ztimes_z_OZ.reflexivity + |apply (bool_elim ? (p n1)); intro + [rewrite > true_to_sigma_p_Sn + [rewrite > true_to_sigma_p_Sn + [rewrite < H. + apply distr_Ztimes_Zplus + |assumption + ] + |assumption + ] + |rewrite > false_to_sigma_p_Sn + [rewrite > false_to_sigma_p_Sn + [assumption + |assumption + ] + |assumption + ] + ] ] qed. -theorem prime_to_lt_O: \forall p. prime p \to O < p. -intros.elim H.apply lt_to_le.assumption. +lemma Ztimes_sigma_pr: \forall z:Z.\forall n:nat.\forall p. \forall f. +(sigma_p n p f) * z = sigma_p n p (\lambda i.(f i)*z). +intros. +rewrite < sym_Ztimes. +rewrite > Ztimes_sigma_pl. +apply eq_sigma_p + [intros.reflexivity + |intros.apply sym_Ztimes + ] qed. theorem divides_exp_to_lt_ord:\forall n,m,j,p. O < n \to prime p \to @@ -563,7 +621,7 @@ cut (O < p) (sigma_p (S n*S m) (\lambda x:nat.divides_b (x/S m) n) (\lambda x:nat.g (x/S m*(p)\sup(x\mod S m))))) [apply sym_eq. - apply (eq_sigma_p_gh g ? (p_ord_times p (S m))) + apply (eq_sigma_p_gh g ? (p_ord_inv p (S m))) [intros. lapply (divides_b_true_to_lt_O ? ? H H4). apply divides_to_divides_b_true @@ -584,7 +642,7 @@ cut (O < p) ] |intros. lapply (divides_b_true_to_lt_O ? ? H H4). - unfold p_ord_times. + unfold p_ord_inv. rewrite > (p_ord_exp1 p ? (i \mod (S m)) (i/S m)) [change with ((i/S m)*S m+i \mod S m=i). apply sym_eq. @@ -615,7 +673,7 @@ cut (O < p) ] |intros. cut (ord j p < S m) - [rewrite > div_p_ord_times + [rewrite > div_p_ord_inv [apply divides_to_divides_b_true [apply lt_O_ord_rem [elim H1.assumption @@ -636,8 +694,8 @@ cut (O < p) ] |intros. cut (ord j p < S m) - [rewrite > div_p_ord_times - [rewrite > mod_p_ord_times + [rewrite > div_p_ord_inv + [rewrite > mod_p_ord_inv [rewrite > sym_times. apply sym_eq. apply exp_ord @@ -658,7 +716,7 @@ cut (O < p) apply (divides_b_true_to_lt_O ? ? H4). ] |intros. - rewrite > eq_p_ord_times. + rewrite > eq_p_ord_inv. rewrite > sym_plus. apply (lt_to_le_to_lt ? (S m +ord_rem j p*S m)) [apply lt_plus_l. -- 2.39.2