1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / Matita is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/Z/moebius".
17 include "nat/factorization.ma".
18 include "Z/sigma_p.ma".
20 let rec moebius_aux p n : Z \def
24 match p_ord n (nth_prime p1) with
25 [ (pair q r) \Rightarrow
27 [ O \Rightarrow moebius_aux p1 r
30 [ O \Rightarrow Zopp (moebius_aux p1 r)
31 | (S q2) \Rightarrow OZ
38 definition moebius : nat \to Z \def
40 let p \def (max n (\lambda p:nat.eqb (n \mod (nth_prime p)) O)) in
44 theorem moebius_O : moebius O = pos O.
45 simplify. reflexivity.
48 theorem moebius_SO : moebius (S O) = pos O.
52 theorem moebius_SSO : moebius (S (S O)) = neg O.
56 theorem moebius_SSSO : moebius (S (S (S O))) = neg O.
60 theorem moebius_SSSSO : moebius (S (S (S (S O)))) = OZ.
65 theorem not_divides_to_p_ord_O: \forall n,i.
66 Not (divides (nth_prime i) n) \to p_ord n (nth_prime i) =
70 [apply lt_O_nth_prime_n
76 theorem p_ord_O_to_not_divides: \forall n,i,r.
78 p_ord n (nth_prime i) = pair nat nat O r
79 \to Not (divides (nth_prime i) n).
81 lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
82 [apply lt_SO_nth_prime_n
92 theorem not_divides_to_eq_moebius_aux: \forall n,p,p1.p \le p1 \to
93 (\forall i. p \le i \to i \le p1 \to Not (divides (nth_prime i) n))
94 \to moebius_aux p n = moebius_aux p1 n.
99 rewrite > not_divides_to_p_ord_O
100 [simplify.apply H2.intros.
101 apply H3[assumption|apply le_S.assumption]
102 |apply H3[assumption|apply le_n_Sn]
107 theorem eq_moebius_moebius_aux: \forall n,p.
108 max_prime_factor n < p \to p \le n \to
109 moebius n = moebius_aux p n.
113 (moebius_aux (S (max n (\lambda p:nat.eqb (n\mod nth_prime p) O))) n
115 apply not_divides_to_eq_moebius_aux
118 apply divides_b_false_to_not_divides.
120 apply (lt_max_to_false ? n i)
122 |apply (trans_le ? p)[assumption|assumption]
127 theorem moebius_aux_SO: \forall p.moebius_aux p (S O) = pos O.
130 [simplify.reflexivity
133 apply not_divides_to_eq_moebius_aux
135 |intros.unfold.intro.
136 absurd (nth_prime i \le S O)
138 [apply le_n|assumption]
140 apply lt_SO_nth_prime_n.
146 theorem p_ord_to_not_eq_O : \forall n,p,q,r.
148 p_ord n (nth_prime p) = pair nat nat q r \to
153 [lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
154 [apply lt_SO_nth_prime_n.
157 apply (lt_to_not_eq ? ? Hcut).
162 |apply (trans_lt ? (S O))[apply lt_O_S|assumption]
166 theorem max_prime_factor_to_not_p_ord_O : \forall n,p,r.
168 p = max_prime_factor n \to
169 p_ord n (nth_prime p) \neq pair nat nat O r.
170 intros.unfold Not.intro.
171 apply (p_ord_O_to_not_divides ? ? ? ? H2)
172 [apply (trans_lt ? (S O))[apply lt_O_S|assumption]
174 apply divides_max_prime_factor_n.
179 theorem p_ord_SO_SO_to_moebius : \forall n,p.
181 p = max_prime_factor n \to
182 p_ord n (nth_prime p) = pair nat nat (S O) (S O) \to
183 moebius n = Zopp (pos O).
186 (moebius_aux (S (max_prime_factor n)) n = neg O).
187 rewrite < H1.simplify.
188 rewrite > H2.simplify.
189 rewrite > moebius_aux_SO.
193 theorem p_ord_SO_r_to_moebius1 : \forall n,p,r.
195 p = max_prime_factor n \to
197 p_ord n (nth_prime p) = pair nat nat (S O) r \to
198 moebius n = Zopp (moebius r).
201 (moebius_aux (S (max_prime_factor n)) n = -(moebius r)).
202 rewrite < H1.simplify.
203 rewrite > H3.simplify.
207 (moebius_aux (S (max_prime_factor r)) r = moebius_aux p r).
208 apply not_divides_to_eq_moebius_aux
209 [apply (p_ord_to_lt_max_prime_factor n p (S O) ? ? H1)
210 [apply (trans_lt ? (S O))[apply lt_O_S|assumption]
211 |apply sym_eq. assumption
215 lapply (decidable_le i r).
217 [apply divides_b_false_to_not_divides.
218 apply (lt_max_to_false ? r i)[assumption|assumption]
219 |unfold.intro.apply H6.
220 apply (trans_le ? (nth_prime i))
222 apply lt_n_nth_prime_n
224 [apply (trans_lt ? (S O))[apply lt_O_S|assumption]
232 theorem p_ord_SO_r_to_moebius : \forall n,p,r.
234 p = max_prime_factor n \to
235 p_ord n (nth_prime p) = pair nat nat (S O) r \to
236 moebius n = Zopp (moebius r).
238 apply (nat_case r);intro
240 apply (p_ord_to_not_eq_O ? ? ? ? H H2).
242 |apply (nat_case m);intros
243 [simplify.apply (p_ord_SO_SO_to_moebius ? ? H H1 H2)
244 |apply (p_ord_SO_r_to_moebius1 ? ? ? H H1 ? H2).
245 apply le_S_S.apply le_S_S.apply le_O_n
250 theorem p_ord_SSq_r_to_moebius : \forall n,p,q,r.
252 p = max_prime_factor n \to
253 p_ord n (nth_prime p) = pair nat nat (S (S q)) r \to
257 (moebius_aux (S (max n (\lambda p:nat.eqb (n\mod nth_prime p) O))) n =OZ).
258 rewrite < H1.simplify.
259 rewrite > H2.simplify.
263 lemma eq_p_max: \forall n,p,r:nat. O < n \to
265 r = (S O) \lor (max r (\lambda p:nat.eqb (r \mod (nth_prime p)) O)) < p \to
266 p = max_prime_factor (r*(nth_prime p)\sup n).
269 unfold max_prime_factor.
270 apply max_spec_to_max.
273 [rewrite > times_n_SO in \vdash (? % ?).
278 apply (lt_to_le_to_lt ? (nth_prime p))
279 [apply lt_n_nth_prime_n
280 |rewrite > exp_n_SO in \vdash (? % ?).
282 [apply lt_O_nth_prime_n
287 |apply eq_to_eqb_true.
288 apply divides_to_mod_O
289 [apply lt_O_nth_prime_n
290 |apply (lt_O_n_elim ? H).
292 apply (witness ? ? (r*(nth_prime p \sup m))).
293 rewrite < assoc_times.
294 rewrite < sym_times in \vdash (? ? ? (? % ?)).
295 rewrite > exp_n_SO in \vdash (? ? ? (? (? ? %) ?)).
296 rewrite > assoc_times.
297 rewrite < exp_plus_times.
302 apply not_eq_to_eqb_false.
304 lapply (mod_O_to_divides ? ? ? H5)
305 [apply lt_O_nth_prime_n
306 |cut (Not (divides (nth_prime i) ((nth_prime p)\sup n)))
308 [rewrite > H6 in Hletin.
310 rewrite < plus_n_O in Hletin.
311 apply Hcut.assumption
312 |elim (divides_times_to_divides ? ? ? ? Hletin)
313 [apply (lt_to_not_le ? ? H3).
315 apply (le_to_lt_to_lt ? ? ? ? H6).
317 [apply (trans_le ? (nth_prime i))
319 apply lt_n_nth_prime_n
320 |apply divides_to_le[assumption|assumption]
322 |apply eq_to_eqb_true.
323 apply divides_to_mod_O
324 [apply lt_O_nth_prime_n|assumption]
326 |apply prime_nth_prime
327 |apply Hcut.assumption
331 apply (lt_to_not_eq ? ? H3).
333 elim (prime_nth_prime p).
334 apply injective_nth_prime.
336 [apply (divides_exp_to_divides ? ? ? ? H6).
337 apply prime_nth_prime.
338 |apply lt_SO_nth_prime_n
345 lemma lt_max_prime_factor_to_not_divides: \forall n,p:nat.
346 O < n \to n=S O \lor max_prime_factor n < p \to
347 (nth_prime p \ndivides n).
348 intros.unfold Not.intro.
351 apply (le_to_not_lt (nth_prime p) (S O))
352 [apply divides_to_le[apply le_n|assumption]
353 |apply lt_SO_nth_prime_n
355 |apply (not_le_Sn_n p).
357 apply (le_to_lt_to_lt ? ? ? ? H3).
358 unfold max_prime_factor.
360 [apply (trans_le ? (nth_prime p))
362 apply lt_n_nth_prime_n
363 |apply divides_to_le;assumption
365 |apply eq_to_eqb_true.
366 apply divides_to_mod_O
367 [apply lt_O_nth_prime_n|assumption]
372 theorem moebius_exp: \forall p,q,r:nat. O < r \to
373 r = (S O) \lor (max_prime_factor r) < p \to
374 (* r = (S O) \lor (max r (\lambda p:nat.eqb (r \mod (nth_prime p)) O)) < p \to *)
375 sigma_p (S (S q)) (\lambda y.true) (\lambda y.moebius (r*(exp (nth_prime p) y))) = O.
378 [rewrite > true_to_sigma_p_Sn
379 [rewrite > true_to_sigma_p_Sn
380 [rewrite > Zplus_z_OZ.
381 rewrite < times_n_SO.
382 rewrite > (p_ord_SO_r_to_moebius ? p r)
383 [rewrite > sym_Zplus.
384 rewrite > Zplus_Zopp.
388 rewrite > times_n_SO.
389 apply lt_to_le_to_lt_times
390 [apply lt_SO_nth_prime_n
395 [apply le_n|assumption|assumption]
397 [apply lt_O_nth_prime_n
398 |apply lt_max_prime_factor_to_not_divides;assumption
406 |rewrite > true_to_sigma_p_Sn
408 rewrite > Zplus_z_OZ.
409 apply (p_ord_SSq_r_to_moebius ? p n r)
410 [rewrite > times_n_SO.
411 rewrite > sym_times in \vdash (? ? %).
412 apply lt_to_le_to_lt_times
413 [apply (trans_lt ? (nth_prime p))
414 [apply lt_SO_nth_prime_n
415 |rewrite > exp_n_SO in \vdash (? % ?).
417 [apply lt_SO_nth_prime_n
418 |apply le_S_S.apply le_S_S.apply le_O_n
425 [apply le_S_S.apply le_O_n|assumption|assumption]
427 [apply lt_O_nth_prime_n
428 |apply lt_max_prime_factor_to_not_divides;assumption
437 theorem sigma_p_moebius1: \forall n,m,p:nat.O < n \to O < m \to
438 n = (S O) \lor max_prime_factor n < p \to
439 sigma_p (S (n*(exp (nth_prime p) m))) (\lambda y.divides_b y (n*(exp (nth_prime p) m))) moebius = O.
441 rewrite > sigma_p_divides_b
442 [apply (trans_eq ? ? (sigma_p (S n) (\lambda x:nat.divides_b x n) (\lambda x:nat.OZ)))
445 |apply (lt_O_n_elim m H1).
446 intros.apply moebius_exp
447 [apply (divides_b_true_to_lt_O ? ? ? H4).
450 [left.rewrite > H5 in H3.
451 elim (le_to_or_lt_eq ? ? (le_S_S_to_le ? ? H3))
453 apply (lt_to_not_le O x)
454 [apply (divides_b_true_to_lt_O n x H H4)
455 |apply le_S_S_to_le.assumption
460 apply (le_to_lt_to_lt ? ? ? ? H5).
461 apply (divides_to_max_prime_factor1 x n)
462 [apply (divides_b_true_to_lt_O ? ? H H4)
464 |apply divides_b_true_to_divides.
470 |generalize in match (\lambda x:nat.divides_b x n).
473 [simplify.elim (f O);reflexivity
474 |apply (bool_elim ? (f (S n1)))
476 rewrite > true_to_sigma_p_Sn
477 [rewrite > H3.reflexivity|assumption]
479 rewrite > false_to_sigma_p_Sn
480 [apply H3|assumption]
485 |apply prime_nth_prime
486 |apply lt_max_prime_factor_to_not_divides;assumption
490 theorem sigma_p_moebius: \forall n. (S O) < n \to
491 sigma_p (S n) (\lambda y.divides_b y n) moebius = O.
493 lapply (exp_ord (nth_prime (max_prime_factor n)) n)
494 [rewrite > sym_times in Hletin.
496 apply sigma_p_moebius1
498 [apply lt_SO_nth_prime_n
499 |apply lt_to_le.assumption
503 (fst ? ? (pair ? ? (S O) (S O)) \leq ord n (nth_prime (max_prime_factor n))).
504 rewrite < (p_ord_p (nth_prime (max_prime_factor n)))
505 [apply (divides_to_le_ord ? (nth_prime (max_prime_factor n)) n)
506 [apply lt_O_nth_prime_n
507 |apply lt_to_le.assumption
508 |apply prime_nth_prime
509 |apply divides_max_prime_factor_n.
512 |apply lt_SO_nth_prime_n
514 |lapply (lt_O_ord_rem (nth_prime (max_prime_factor n)) n)
515 [elim (le_to_or_lt_eq ? ? Hletin1)
517 apply (p_ord_to_lt_max_prime_factor1 n (max_prime_factor n)
518 (ord n (nth_prime (max_prime_factor n)))
519 (ord_rem n (nth_prime (max_prime_factor n))))
520 [apply lt_to_le.assumption
525 |left.apply sym_eq.assumption
527 |apply lt_SO_nth_prime_n
528 |apply lt_to_le.assumption
531 |apply lt_SO_nth_prime_n
532 |apply lt_to_le.assumption