From: Andrea Asperti Date: Fri, 16 Mar 2007 08:05:44 +0000 (+0000) Subject: New contrib moebius.ma. X-Git-Tag: make_still_working~6422 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0ec069491a2e870c95e095e15d8c54c76a17bc80;p=helm.git New contrib moebius.ma. --- diff --git a/helm/software/matita/library/Z/moebius.ma b/helm/software/matita/library/Z/moebius.ma new file mode 100644 index 000000000..e91bf8df9 --- /dev/null +++ b/helm/software/matita/library/Z/moebius.ma @@ -0,0 +1,529 @@ +(**************************************************************************) +(* ___ *) +(* ||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/moebius". + +include "nat/factorization.ma". +include "Z/sigma_p.ma". + +let rec moebius_aux p n : Z \def + match p with + [ O \Rightarrow pos O + | (S p1) \Rightarrow + match p_ord n (nth_prime p1) with + [ (pair q r) \Rightarrow + match q with + [ O \Rightarrow moebius_aux p1 r + | (S q1) \Rightarrow + match q1 with + [ O \Rightarrow Zopp (moebius_aux p1 r) + | (S q2) \Rightarrow OZ + ] + ] + ] + ] +. + +definition moebius : nat \to Z \def +\lambda n. + 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. + +theorem moebius_SO : moebius (S O) = pos O. +simplify.reflexivity. +qed. + +theorem moebius_SSO : moebius (S (S O)) = neg O. +simplify.reflexivity. +qed. + +theorem moebius_SSSO : moebius (S (S (S O))) = neg O. +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) = +pair nat nat O n. +intros. +apply p_ord_exp1 + [apply lt_O_nth_prime_n + |assumption + |auto + ] +qed. + +theorem p_ord_O_to_not_divides: \forall n,i,r. +O < n \to +p_ord n (nth_prime i) = pair nat nat O r +\to Not (divides (nth_prime i) n). +intros. +lapply (p_ord_to_exp1 ? ? ? ? ? ? H1) + [apply lt_SO_nth_prime_n + |assumption + |elim Hletin. + simplify in H3. + rewrite > H3. + rewrite < plus_n_O. + assumption + ] +qed. + +theorem not_divides_to_eq_moebius_aux: \forall n,p,p1.p \le p1 \to +(\forall i. p \le i \to i \le p1 \to Not (divides (nth_prime i) n)) +\to moebius_aux p n = moebius_aux p1 n. +intros 4. +elim H + [reflexivity + |simplify. + rewrite > not_divides_to_p_ord_O + [simplify.apply H2.intros. + apply H3[assumption|apply le_S.assumption] + |apply H3[assumption|apply le_n_Sn] + ] + ] +qed. + +theorem eq_moebius_moebius_aux: \forall n,p. +max_prime_factor n < p \to p \le n \to +moebius n = moebius_aux p n. +intros. +unfold moebius. +change with +(moebius_aux (S (max n (\lambda p:nat.eqb (n\mod nth_prime p) O))) n += moebius_aux p n). +apply not_divides_to_eq_moebius_aux + [assumption + |intros. + apply divides_b_false_to_not_divides. + unfold divides_b. + apply (lt_max_to_false ? n i) + [assumption + |apply (trans_le ? p)[assumption|assumption] + ] + ] +qed. + +theorem moebius_aux_SO: \forall p.moebius_aux p (S O) = pos O. +intros. +elim p + [simplify.reflexivity + |rewrite < H. + apply sym_eq. + apply not_divides_to_eq_moebius_aux + [apply le_n_Sn + |intros.unfold.intro. + absurd (nth_prime i \le S O) + [apply divides_to_le + [apply le_n|assumption] + |apply lt_to_not_le. + apply lt_SO_nth_prime_n. + ] + ] + ] +qed. + +theorem p_ord_to_not_eq_O : \forall n,p,q,r. + (S O) < n \to + p_ord n (nth_prime p) = pair nat nat q r \to + Not (r=O). +intros. +unfold.intro. +cut (O < n) + [lapply (p_ord_to_exp1 ? ? ? ? ? ? H1) + [apply lt_SO_nth_prime_n. + |assumption + |elim Hletin. + apply (lt_to_not_eq ? ? Hcut). + rewrite > H4. + rewrite > H2. + apply times_n_O + ] + |apply (trans_lt ? (S O))[apply lt_O_S|assumption] + ] +qed. + +theorem max_prime_factor_to_not_p_ord_O : \forall n,p,r. + (S O) < n \to + p = max_prime_factor n \to + p_ord n (nth_prime p) \neq pair nat nat O r. +intros.unfold Not.intro. +apply (p_ord_O_to_not_divides ? ? ? ? H2) + [apply (trans_lt ? (S O))[apply lt_O_S|assumption] + |rewrite > H1. + apply divides_max_prime_factor_n. + assumption + ] +qed. + +theorem p_ord_SO_SO_to_moebius : \forall n,p. + (S O) < n \to + p = max_prime_factor n \to + p_ord n (nth_prime p) = pair nat nat (S O) (S O) \to + moebius n = Zopp (pos O). +intros. +change with + (moebius_aux (S (max_prime_factor n)) n = neg O). +rewrite < H1.simplify. +rewrite > H2.simplify. +rewrite > moebius_aux_SO. +reflexivity. +qed. + +theorem p_ord_SO_r_to_moebius1 : \forall n,p,r. + (S O) < n \to + p = max_prime_factor n \to + (S O) < r \to + p_ord n (nth_prime p) = pair nat nat (S O) r \to + moebius n = Zopp (moebius r). +intros. +change with + (moebius_aux (S (max_prime_factor n)) n = -(moebius r)). +rewrite < H1.simplify. +rewrite > H3.simplify. +apply eq_f. +apply sym_eq. +change with + (moebius_aux (S (max_prime_factor r)) r = moebius_aux p r). +apply not_divides_to_eq_moebius_aux + [apply (p_ord_to_lt_max_prime_factor n p (S O) ? ? H1) + [apply (trans_lt ? (S O))[apply lt_O_S|assumption] + |apply sym_eq. assumption + |assumption + ] + |intros. + lapply (decidable_le i r). + elim Hletin + [apply divides_b_false_to_not_divides. + apply (lt_max_to_false ? r i)[assumption|assumption] + |unfold.intro.apply H6. + apply (trans_le ? (nth_prime i)) + [apply lt_to_le. + apply lt_n_nth_prime_n + |apply divides_to_le + [apply (trans_lt ? (S O))[apply lt_O_S|assumption] + |assumption + ] + ] + ] + ] +qed. + +theorem p_ord_SO_r_to_moebius : \forall n,p,r. + (S O) < n \to + p = max_prime_factor n \to + p_ord n (nth_prime p) = pair nat nat (S O) r \to + moebius n = Zopp (moebius r). +intros 5. +apply (nat_case r);intro + [apply False_ind. + apply (p_ord_to_not_eq_O ? ? ? ? H H2). + reflexivity + |apply (nat_case m);intros + [simplify.apply (p_ord_SO_SO_to_moebius ? ? H H1 H2) + |apply (p_ord_SO_r_to_moebius1 ? ? ? H H1 ? H2). + apply le_S_S.apply le_S_S.apply le_O_n + ] + ] +qed. + +theorem p_ord_SSq_r_to_moebius : \forall n,p,q,r. + (S O) < n \to + p = max_prime_factor n \to + p_ord n (nth_prime p) = pair nat nat (S (S q)) r \to + moebius n = OZ. +intros. +change with + (moebius_aux (S (max n (\lambda p:nat.eqb (n\mod nth_prime p) O))) n =OZ). +rewrite < H1.simplify. +rewrite > H2.simplify. +reflexivity. +qed. + +lemma eq_p_max: \forall n,p,r:nat. O < n \to +O < r \to +r = (S O) \lor (max r (\lambda p:nat.eqb (r \mod (nth_prime p)) O)) < p \to +p = max_prime_factor (r*(nth_prime p)\sup n). +intros. +apply sym_eq. +unfold max_prime_factor. +apply max_spec_to_max. +split + [split + [rewrite > times_n_SO in \vdash (? % ?). + rewrite > sym_times. + apply le_times + [assumption + |apply lt_to_le. + apply (lt_to_le_to_lt ? (nth_prime p)) + [apply lt_n_nth_prime_n + |rewrite > exp_n_SO in \vdash (? % ?). + apply le_exp + [apply lt_O_nth_prime_n + |assumption + ] + ] + ] + |apply eq_to_eqb_true. + apply divides_to_mod_O + [apply lt_O_nth_prime_n + |apply (lt_O_n_elim ? H). + intro. + apply (witness ? ? (r*(nth_prime p \sup m))). + rewrite < assoc_times. + rewrite < sym_times in \vdash (? ? ? (? % ?)). + rewrite > exp_n_SO in \vdash (? ? ? (? (? ? %) ?)). + rewrite > assoc_times. + rewrite < exp_plus_times. + reflexivity + ] + ] + |intros. + apply not_eq_to_eqb_false. + unfold Not.intro. + lapply (mod_O_to_divides ? ? ? H5) + [apply lt_O_nth_prime_n + |cut (Not (divides (nth_prime i) ((nth_prime p)\sup n))) + [elim H2 + [rewrite > H6 in Hletin. + simplify in Hletin. + rewrite < plus_n_O in Hletin. + apply Hcut.assumption + |elim (divides_times_to_divides ? ? ? ? Hletin) + [apply (lt_to_not_le ? ? H3). + apply lt_to_le. + apply (le_to_lt_to_lt ? ? ? ? H6). + apply f_m_to_le_max + [apply (trans_le ? (nth_prime i)) + [apply lt_to_le. + apply lt_n_nth_prime_n + |apply divides_to_le[assumption|assumption] + ] + |apply eq_to_eqb_true. + apply divides_to_mod_O + [apply lt_O_nth_prime_n|assumption] + ] + |apply prime_nth_prime + |apply Hcut.assumption + ] + ] + |unfold Not.intro. + apply (lt_to_not_eq ? ? H3). + apply sym_eq. + elim (prime_nth_prime p). + apply injective_nth_prime. + apply H8 + [apply (divides_exp_to_divides ? ? ? ? H6). + apply prime_nth_prime. + |apply lt_SO_nth_prime_n + ] + ] + ] + ] +qed. + +lemma lt_max_prime_factor_to_not_divides: \forall n,p:nat. +O < n \to n=S O \lor max_prime_factor n < p \to +(nth_prime p \ndivides n). +intros.unfold Not.intro. +elim H1 + [rewrite > H3 in H2. + apply (le_to_not_lt (nth_prime p) (S O)) + [apply divides_to_le[apply le_n|assumption] + |apply lt_SO_nth_prime_n + ] + |apply (not_le_Sn_n p). + change with (p < p). + apply (le_to_lt_to_lt ? ? ? ? H3). + unfold max_prime_factor. + apply f_m_to_le_max + [apply (trans_le ? (nth_prime p)) + [apply lt_to_le. + apply lt_n_nth_prime_n + |apply divides_to_le;assumption + ] + |apply eq_to_eqb_true. + apply divides_to_mod_O + [apply lt_O_nth_prime_n|assumption] + ] + ] +qed. + +theorem moebius_exp: \forall p,q,r:nat. O < r \to +r = (S O) \lor (max_prime_factor r) < p \to +(* r = (S O) \lor (max r (\lambda p:nat.eqb (r \mod (nth_prime p)) O)) < p \to *) +sigma_p (S (S q)) (\lambda y.true) (\lambda y.moebius (r*(exp (nth_prime p) y))) = O. +intros. +elim q + [rewrite > true_to_sigma_p_Sn + [rewrite > true_to_sigma_p_Sn + [rewrite > Zplus_z_OZ. + rewrite < times_n_SO. + rewrite > (p_ord_SO_r_to_moebius ? p r) + [rewrite > sym_Zplus. + rewrite > Zplus_Zopp. + reflexivity + |rewrite < exp_n_SO. + rewrite > sym_times. + rewrite > times_n_SO. + apply lt_to_le_to_lt_times + [apply lt_SO_nth_prime_n + |assumption + |assumption + ] + |apply eq_p_max + [apply le_n|assumption|assumption] + |apply p_ord_exp1 + [apply lt_O_nth_prime_n + |apply lt_max_prime_factor_to_not_divides;assumption + |apply sym_times + ] + ] + |reflexivity + ] + |reflexivity + ] + |rewrite > true_to_sigma_p_Sn + [rewrite > H2. + rewrite > Zplus_z_OZ. + apply (p_ord_SSq_r_to_moebius ? p n r) + [rewrite > times_n_SO. + rewrite > sym_times in \vdash (? ? %). + apply lt_to_le_to_lt_times + [apply (trans_lt ? (nth_prime p)) + [apply lt_SO_nth_prime_n + |rewrite > exp_n_SO in \vdash (? % ?). + apply lt_exp + [apply lt_SO_nth_prime_n + |apply le_S_S.apply le_S_S.apply le_O_n + ] + ] + |assumption + |assumption + ] + |apply eq_p_max + [apply le_S_S.apply le_O_n|assumption|assumption] + |apply p_ord_exp1 + [apply lt_O_nth_prime_n + |apply lt_max_prime_factor_to_not_divides;assumption + |apply sym_times + ] + ] + |reflexivity + ] + ] +qed. + +theorem sigma_p_moebius1: \forall n,m,p:nat.O < n \to O < m \to +n = (S O) \lor max_prime_factor n < p \to +sigma_p (S (n*(exp (nth_prime p) m))) (\lambda y.divides_b y (n*(exp (nth_prime p) m))) moebius = O. +intros. +rewrite > sigma_p_divides_b + [apply (trans_eq ? ? (sigma_p (S n) (\lambda x:nat.divides_b x n) (\lambda x:nat.OZ))) + [apply eq_sigma_p1 + [intros.reflexivity + |apply (lt_O_n_elim m H1). + intros.apply moebius_exp + [apply (divides_b_true_to_lt_O ? ? ? H4). + assumption + |elim H2 + [left.rewrite > H5 in H3. + elim (le_to_or_lt_eq ? ? (le_S_S_to_le ? ? H3)) + [apply False_ind. + apply (lt_to_not_le O x) + [apply (divides_b_true_to_lt_O n x H H4) + |apply le_S_S_to_le.assumption + ] + |assumption + ] + |right. + apply (le_to_lt_to_lt ? ? ? ? H5). + apply (divides_to_max_prime_factor1 x n) + [apply (divides_b_true_to_lt_O ? ? H H4) + |assumption + |apply divides_b_true_to_divides. + assumption + ] + ] + ] + ] + |generalize in match (\lambda x:nat.divides_b x n). + intro. + elim n + [simplify.elim (f O);reflexivity + |apply (bool_elim ? (f (S n1))) + [intro. + rewrite > true_to_sigma_p_Sn + [rewrite > H3.reflexivity|assumption] + |intro. + rewrite > false_to_sigma_p_Sn + [apply H3|assumption] + ] + ] + ] + |assumption + |apply prime_nth_prime + |apply lt_max_prime_factor_to_not_divides;assumption + ] +qed. + +theorem sigma_p_moebius: \forall n. (S O) < n \to +sigma_p (S n) (\lambda y.divides_b y n) moebius = O. +intros. +lapply (exp_ord (nth_prime (max_prime_factor n)) n) + [rewrite > sym_times in Hletin. + rewrite > Hletin. + apply sigma_p_moebius1 + [apply lt_O_ord_rem + [apply lt_SO_nth_prime_n + |apply lt_to_le.assumption + ] + |unfold lt. + change with + (fst ? ? (pair ? ? (S O) (S O)) \leq ord n (nth_prime (max_prime_factor n))). + rewrite < (p_ord_p (nth_prime (max_prime_factor n))) + [apply (divides_to_le_ord ? (nth_prime (max_prime_factor n)) n) + [apply lt_O_nth_prime_n + |apply lt_to_le.assumption + |apply prime_nth_prime + |apply divides_max_prime_factor_n. + assumption + ] + |apply lt_SO_nth_prime_n + ] + |lapply (lt_O_ord_rem (nth_prime (max_prime_factor n)) n) + [elim (le_to_or_lt_eq ? ? Hletin1) + [right. + apply (p_ord_to_lt_max_prime_factor1 n (max_prime_factor n) + (ord n (nth_prime (max_prime_factor n))) + (ord_rem n (nth_prime (max_prime_factor n)))) + [apply lt_to_le.assumption + |apply le_n + |auto + |assumption + ] + |left.apply sym_eq.assumption + ] + |apply lt_SO_nth_prime_n + |apply lt_to_le.assumption + ] + ] + |apply lt_SO_nth_prime_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 new file mode 100644 index 000000000..27baf8db5 --- /dev/null +++ b/helm/software/matita/library/Z/sigma_p.ma @@ -0,0 +1,709 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/Z/sigma_p.ma". + +include "Z/plus.ma". +include "nat/primes.ma". +include "nat/ord.ma". + +let rec sigma_p n p (g:nat \to Z) \def + match n with + [ O \Rightarrow OZ + | (S k) \Rightarrow + match p k with + [true \Rightarrow (g k)+(sigma_p k p g) + |false \Rightarrow sigma_p k p g] + ]. + +theorem true_to_sigma_p_Sn: +\forall n:nat. \forall p:nat \to bool. \forall g:nat \to Z. +p n = true \to sigma_p (S n) p g = +(g n)+(sigma_p n p g). +intros.simplify. +rewrite > H.reflexivity. +qed. + +theorem false_to_sigma_p_Sn: +\forall n:nat. \forall p:nat \to bool. \forall g:nat \to Z. +p n = false \to sigma_p (S n) p g = sigma_p n p g. +intros.simplify. +rewrite > H.reflexivity. +qed. + +theorem eq_sigma_p: \forall p1,p2:nat \to bool. +\forall g1,g2: nat \to Z.\forall n. +(\forall x. x < n \to p1 x = p2 x) \to +(\forall x. x < n \to g1 x = g2 x) \to +sigma_p n p1 g1 = sigma_p n p2 g2. +intros 5.elim n + [reflexivity + |apply (bool_elim ? (p1 n1)) + [intro. + rewrite > (true_to_sigma_p_Sn ? ? ? H3). + rewrite > true_to_sigma_p_Sn + [apply eq_f2 + [apply H2.apply le_n. + |apply H + [intros.apply H1.apply le_S.assumption + |intros.apply H2.apply le_S.assumption + ] + ] + |rewrite < H3.apply sym_eq.apply H1.apply le_n + ] + |intro. + rewrite > (false_to_sigma_p_Sn ? ? ? H3). + rewrite > false_to_sigma_p_Sn + [apply H + [intros.apply H1.apply le_S.assumption + |intros.apply H2.apply le_S.assumption + ] + |rewrite < H3.apply sym_eq.apply H1.apply le_n + ] + ] + ] +qed. + +theorem eq_sigma_p1: \forall p1,p2:nat \to bool. +\forall g1,g2: nat \to Z.\forall n. +(\forall x. x < n \to p1 x = p2 x) \to +(\forall x. x < n \to p1 x = true \to g1 x = g2 x) \to +sigma_p n p1 g1 = sigma_p n p2 g2. +intros 5. +elim n + [reflexivity + |apply (bool_elim ? (p1 n1)) + [intro. + rewrite > (true_to_sigma_p_Sn ? ? ? H3). + rewrite > true_to_sigma_p_Sn + [apply eq_f2 + [apply H2 + [apply le_n|assumption] + |apply H + [intros.apply H1.apply le_S.assumption + |intros.apply H2 + [apply le_S.assumption|assumption] + ] + ] + |rewrite < H3.apply sym_eq.apply H1.apply le_n + ] + |intro. + rewrite > (false_to_sigma_p_Sn ? ? ? H3). + rewrite > false_to_sigma_p_Sn + [apply H + [intros.apply H1.apply le_S.assumption + |intros.apply H2 + [apply le_S.assumption|assumption] + ] + |rewrite < H3.apply sym_eq.apply H1.apply le_n + ] + ] + ] +qed. + +theorem sigma_p_false: +\forall g: nat \to Z.\forall n.sigma_p n (\lambda x.false) g = O. +intros. +elim n[reflexivity|simplify.assumption] +qed. + +theorem sigma_p_plus: \forall n,k:nat.\forall p:nat \to bool. +\forall g: nat \to Z. +sigma_p (k+n) p g += sigma_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) + sigma_p n p g. +intros. +elim k + [reflexivity + |apply (bool_elim ? (p (n1+n))) + [intro. + simplify in \vdash (? ? (? % ? ?) ?). + rewrite > (true_to_sigma_p_Sn ? ? ? H1). + rewrite > (true_to_sigma_p_Sn n1 (\lambda x.p (x+n)) ? H1). + rewrite > assoc_Zplus. + rewrite < H.reflexivity + |intro. + simplify in \vdash (? ? (? % ? ?) ?). + rewrite > (false_to_sigma_p_Sn ? ? ? H1). + rewrite > (false_to_sigma_p_Sn n1 (\lambda x.p (x+n)) ? H1). + assumption. + ] + ] +qed. + +theorem false_to_eq_sigma_p: \forall n,m:nat.n \le m \to +\forall p:nat \to bool. +\forall g: nat \to Z. (\forall i:nat. n \le i \to i < m \to +p i = false) \to sigma_p m p g = sigma_p n p g. +intros 5. +elim H + [reflexivity + |simplify. + rewrite > H3 + [simplify. + apply H2. + intros. + apply H3[apply H4|apply le_S.assumption] + |assumption + |apply le_n + ] + ] +qed. + +theorem sigma_p2 : +\forall n,m:nat. +\forall p1,p2:nat \to bool. +\forall g: nat \to nat \to Z. +sigma_p (n*m) + (\lambda x.andb (p1 (div x m)) (p2 (mod x m))) + (\lambda x.g (div x m) (mod x m)) = +sigma_p n p1 + (\lambda x.sigma_p m p2 (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 (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. +intros 2. +elim n + [apply False_ind. + apply (not_le_Sn_O i). + assumption + |apply (bool_elim ? (p n1));intro + [elim (le_to_or_lt_eq i n1) + [rewrite > true_to_sigma_p_Sn + [rewrite > true_to_sigma_p_Sn + [rewrite < assoc_Zplus. + rewrite < sym_Zplus in \vdash (? ? ? (? % ?)). + rewrite > assoc_Zplus. + apply eq_f2 + [reflexivity + |apply H[assumption|assumption] + ] + |rewrite > H3.simplify. + change with (notb (eqb n1 i) = notb false). + apply eq_f. + apply not_eq_to_eqb_false. + unfold Not.intro. + apply (lt_to_not_eq ? ? H4). + apply sym_eq.assumption + ] + |assumption + ] + |rewrite > true_to_sigma_p_Sn + [rewrite > H4. + apply eq_f2 + [reflexivity + |rewrite > false_to_sigma_p_Sn + [apply eq_sigma_p + [intros. + elim (p x) + [simplify. + change with (notb false = notb (eqb x n1)). + apply eq_f. + apply sym_eq. + apply not_eq_to_eqb_false. + apply (lt_to_not_eq ? ? H5) + |reflexivity + ] + |intros.reflexivity + ] + |rewrite > H3. + rewrite > (eq_to_eqb_true ? ? (refl_eq ? n1)). + reflexivity + ] + ] + |assumption + ] + |apply le_S_S_to_le.assumption + ] + |rewrite > false_to_sigma_p_Sn + [elim (le_to_or_lt_eq i n1) + [rewrite > false_to_sigma_p_Sn + [apply H[assumption|assumption] + |rewrite > H3.reflexivity + ] + |apply False_ind. + apply not_eq_true_false. + rewrite < H2. + rewrite > H4. + assumption + |apply le_S_S_to_le.assumption + ] + |assumption + ] + ] + ] +qed. + +theorem eq_sigma_p_gh: +\forall g: nat \to Z. +\forall h,h1: nat \to nat.\forall n,n1. +\forall p1,p2:nat \to bool. +(\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to +(\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to +(\forall i. i < n \to p1 i = true \to h i < n1) \to +(\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to +(\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to +(\forall j. j < n1 \to p2 j = true \to h1 j < n) \to +sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 (\lambda x.p2 x) g. +intros 4. +elim n + [generalize in match H5. + elim n1 + [reflexivity + |apply (bool_elim ? (p2 n2));intro + [apply False_ind. + apply (not_le_Sn_O (h1 n2)). + apply H7 + [apply le_n|assumption] + |rewrite > false_to_sigma_p_Sn + [apply H6. + intros. + apply H7[apply le_S.apply H9|assumption] + |assumption + ] + ] + ] + |apply (bool_elim ? (p1 n1));intro + [rewrite > true_to_sigma_p_Sn + [rewrite > (sigma_p_gi g n2 (h n1)) + [apply eq_f2 + [reflexivity + |apply H + [intros. + rewrite > H1 + [simplify. + change with ((\not eqb (h i) (h n1))= \not false). + apply eq_f. + apply not_eq_to_eqb_false. + unfold Not.intro. + apply (lt_to_not_eq ? ? H8). + rewrite < H2 + [rewrite < (H2 n1) + [apply eq_f.assumption|apply le_n|assumption] + |apply le_S.assumption + |assumption + ] + |apply le_S.assumption + |assumption + ] + |intros. + apply H2[apply le_S.assumption|assumption] + |intros. + apply H3[apply le_S.assumption|assumption] + |intros. + apply H4 + [assumption + |generalize in match H9. + elim (p2 j) + [reflexivity|assumption] + ] + |intros. + apply H5 + [assumption + |generalize in match H9. + elim (p2 j) + [reflexivity|assumption] + ] + |intros. + elim (le_to_or_lt_eq (h1 j) n1) + [assumption + |generalize in match H9. + elim (p2 j) + [simplify in H11. + absurd (j = (h n1)) + [rewrite < H10. + rewrite > H5 + [reflexivity|assumption|auto] + |apply eqb_false_to_not_eq. + generalize in match H11. + elim (eqb j (h n1)) + [apply sym_eq.assumption|reflexivity] + ] + |simplify in H11. + apply False_ind. + apply not_eq_true_false. + apply sym_eq.assumption + ] + |apply le_S_S_to_le. + apply H6 + [assumption + |generalize in match H9. + elim (p2 j) + [reflexivity|assumption] + ] + ] + ] + ] + |apply H3[apply le_n|assumption] + |apply H1[apply le_n|assumption] + ] + |assumption + ] + |rewrite > false_to_sigma_p_Sn + [apply H + [intros.apply H1[apply le_S.assumption|assumption] + |intros.apply H2[apply le_S.assumption|assumption] + |intros.apply H3[apply le_S.assumption|assumption] + |intros.apply H4[assumption|assumption] + |intros.apply H5[assumption|assumption] + |intros. + elim (le_to_or_lt_eq (h1 j) n1) + [assumption + |absurd (j = (h n1)) + [rewrite < H10. + rewrite > H5 + [reflexivity|assumption|assumption] + |unfold Not.intro. + apply not_eq_true_false. + rewrite < H7. + rewrite < H10. + rewrite > H4 + [reflexivity|assumption|assumption] + ] + |apply le_S_S_to_le. + apply H6[assumption|assumption] + ] + ] + |assumption + ] + ] + ] +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)) + ] +qed. + +theorem prime_to_lt_O: \forall p. prime p \to O < p. +intros.elim H.apply lt_to_le.assumption. +qed. + +theorem divides_exp_to_lt_ord:\forall n,m,j,p. O < n \to prime p \to +p \ndivides n \to j \divides n*(exp p m) \to ord j p < S m. +intros. +cut (m = ord (n*(exp p m)) p) + [apply le_S_S. + rewrite > Hcut. + apply divides_to_le_ord + [elim (le_to_or_lt_eq ? ? (le_O_n j)) + [assumption + |apply False_ind. + apply (lt_to_not_eq ? ? H). + elim H3. + rewrite < H4 in H5.simplify in H5. + elim (times_O_to_O ? ? H5) + [apply sym_eq.assumption + |apply False_ind. + apply (not_le_Sn_n O). + rewrite < H6 in \vdash (? ? %). + apply lt_O_exp. + elim H1.apply lt_to_le.assumption + ] + ] + |rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.apply (prime_to_lt_O ? H1)] + |assumption + |assumption + ] + |unfold ord. + rewrite > (p_ord_exp1 p ? m n) + [reflexivity + |apply (prime_to_lt_O ? H1) + |assumption + |apply sym_times + ] + ] +qed. + +theorem divides_exp_to_divides_ord_rem:\forall n,m,j,p. O < n \to prime p \to +p \ndivides n \to j \divides n*(exp p m) \to ord_rem j p \divides n. +intros. +cut (O < j) + [cut (n = ord_rem (n*(exp p m)) p) + [rewrite > Hcut1. + apply divides_to_divides_ord_rem + [assumption + |rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.apply (prime_to_lt_O ? H1)] + |assumption + |assumption + ] + |unfold ord_rem. + rewrite > (p_ord_exp1 p ? m n) + [reflexivity + |apply (prime_to_lt_O ? H1) + |assumption + |apply sym_times + ] + ] + |elim (le_to_or_lt_eq ? ? (le_O_n j)) + [assumption + |apply False_ind. + apply (lt_to_not_eq ? ? H). + elim H3. + rewrite < H4 in H5.simplify in H5. + elim (times_O_to_O ? ? H5) + [apply sym_eq.assumption + |apply False_ind. + apply (not_le_Sn_n O). + rewrite < H6 in \vdash (? ? %). + apply lt_O_exp. + elim H1.apply lt_to_le.assumption + ] + ] + ] +qed. + +theorem sigma_p_divides_b: +\forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to +\forall g: nat \to Z. +sigma_p (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) g = +sigma_p (S n) (\lambda x.divides_b x n) + (\lambda x.sigma_p (S m) (\lambda y.true) (\lambda y.g (x*(exp p y)))). +intros. +cut (O < p) + [rewrite < sigma_p2. + apply (trans_eq ? ? + (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))) + [intros. + lapply (divides_b_true_to_lt_O ? ? H H4). + apply divides_to_divides_b_true + [rewrite > (times_n_O O). + apply lt_times + [assumption + |apply lt_O_exp.assumption + ] + |apply divides_times + [apply divides_b_true_to_divides.assumption + |apply (witness ? ? (p \sup (m-i \mod (S m)))). + rewrite < exp_plus_times. + apply eq_f. + rewrite > sym_plus. + apply plus_minus_m_m. + auto + ] + ] + |intros. + lapply (divides_b_true_to_lt_O ? ? H H4). + unfold p_ord_times. + 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. + apply div_mod. + apply lt_O_S + |assumption + |unfold Not.intro. + apply H2. + apply (trans_divides ? (i/ S m)) + [assumption| + apply divides_b_true_to_divides;assumption] + |apply sym_times. + ] + |intros. + apply le_S_S. + apply le_times + [apply le_S_S_to_le. + change with ((i/S m) < S n). + apply (lt_times_to_lt_l m). + apply (le_to_lt_to_lt ? i) + [auto|assumption] + |apply le_exp + [assumption + |apply le_S_S_to_le. + apply lt_mod_m_m. + apply lt_O_S + ] + ] + |intros. + cut (ord j p < S m) + [rewrite > div_p_ord_times + [apply divides_to_divides_b_true + [apply lt_O_ord_rem + [elim H1.assumption + |apply (divides_b_true_to_lt_O ? ? ? H4). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + ] + |apply (divides_exp_to_divides_ord_rem ? m ? ? H H1 H2). + apply divides_b_true_to_divides. + assumption + ] + |assumption + ] + |apply (divides_exp_to_lt_ord ? ? ? ? H H1 H2). + apply (divides_b_true_to_divides ? ? H4). + apply (divides_b_true_to_lt_O ? ? H4) + ] + |intros. + cut (ord j p < S m) + [rewrite > div_p_ord_times + [rewrite > mod_p_ord_times + [rewrite > sym_times. + apply sym_eq. + apply exp_ord + [elim H1.assumption + |apply (divides_b_true_to_lt_O ? ? ? H4). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + ] + |apply (divides_exp_to_lt_ord ? ? ? ? H H1 H2). + apply (divides_b_true_to_divides ? ? H4). + apply (divides_b_true_to_lt_O ? ? H4) + ] + |assumption + ] + |apply (divides_exp_to_lt_ord ? ? ? ? H H1 H2). + apply (divides_b_true_to_divides ? ? H4). + apply (divides_b_true_to_lt_O ? ? H4). + ] + |intros. + rewrite > eq_p_ord_times. + rewrite > sym_plus. + apply (lt_to_le_to_lt ? (S m +ord_rem j p*S m)) + [apply lt_plus_l. + apply le_S_S. + cut (m = ord (n*(p \sup m)) p) + [rewrite > Hcut1. + apply divides_to_le_ord + [apply (divides_b_true_to_lt_O ? ? ? H4). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |assumption + |apply divides_b_true_to_divides. + assumption + ] + |unfold ord. + rewrite > sym_times. + rewrite > (p_ord_exp1 p ? m n) + [reflexivity + |assumption + |assumption + |reflexivity + ] + ] + |change with (S (ord_rem j p)*S m \le S n*S m). + apply le_times_l. + apply le_S_S. + apply divides_to_le + [assumption + |apply (divides_exp_to_divides_ord_rem ? m ? ? H H1 H2). + apply divides_b_true_to_divides. + assumption + ] + ] + ] + |apply eq_sigma_p + [intros. + elim (divides_b (x/S m) n);reflexivity + |intros.reflexivity + ] + ] + |elim H1.apply lt_to_le.assumption + ] +qed. +