matita/library/Z/moebius.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        Matita is distributed under the terms of the          *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/Z/moebius".
  16
  17 include "nat/factorization.ma".
  18 include "Z/sigma_p.ma".
  19
  20 let rec moebius_aux p n : Z \def
  21   match p with
  22   [ O \Rightarrow pos O
  23   | (S p1) \Rightarrow
  24     match p_ord n (nth_prime p1) with
  25     [ (pair q r) \Rightarrow
  26       match q with
  27       [ O \Rightarrow moebius_aux p1 r
  28       | (S q1) \Rightarrow
  29               match q1 with
  30               [ O \Rightarrow Zopp (moebius_aux p1 r)
  31         | (S q2) \Rightarrow OZ
  32         ]
  33       ]
  34     ]
  35   ]
  36 .
  37
  38 definition moebius : nat \to Z \def
  39 \lambda n.
  40   let p \def (max n (\lambda p:nat.eqb (n \mod (nth_prime p)) O)) in
  41   moebius_aux (S p) n.
  42
  43 theorem moebius_O : moebius O = pos O.
  44 simplify. reflexivity.
  45 qed.
  46
  47 theorem moebius_SO : moebius (S O) = pos O.
  48 simplify.reflexivity.
  49 qed.
  50
  51 theorem moebius_SSO : moebius (S (S O)) = neg O.
  52 simplify.reflexivity.
  53 qed.
  54
  55 theorem moebius_SSSO : moebius (S (S (S O))) = neg O.
  56 simplify.reflexivity.
  57 qed.
  58
  59
  60 theorem not_divides_to_p_ord_O: \forall n,i.
  61 Not (divides (nth_prime i) n) \to p_ord n (nth_prime i) =
  62 pair nat nat O n.
  63 intros.
  64 apply p_ord_exp1
  65   [apply lt_O_nth_prime_n
  66   |assumption
  67   |auto
  68   ]
  69 qed.
  70
  71 theorem p_ord_O_to_not_divides: \forall n,i,r.
  72 O < n \to
  73 p_ord n (nth_prime i) = pair nat nat O r
  74 \to Not (divides (nth_prime i) n).
  75 intros.
  76 lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
  77   [apply lt_SO_nth_prime_n
  78   |assumption
  79   |elim Hletin.
  80    simplify in H3.
  81    rewrite > H3.
  82    rewrite < plus_n_O.
  83    assumption
  84   ]
  85 qed.
  86
  87 theorem not_divides_to_eq_moebius_aux: \forall n,p,p1.p \le p1 \to
  88 (\forall i. p \le i \to i \le p1 \to Not (divides (nth_prime i) n))
  89 \to moebius_aux p n = moebius_aux p1 n.
  90 intros 4.
  91 elim H
  92   [reflexivity
  93   |simplify.
  94    rewrite > not_divides_to_p_ord_O
  95     [simplify.apply H2.intros.
  96      apply H3[assumption|apply le_S.assumption]
  97     |apply H3[assumption|apply le_n_Sn]
  98     ]
  99   ]
 100 qed.
 101
 102 theorem eq_moebius_moebius_aux: \forall n,p.
 103 max_prime_factor n < p \to p \le n \to
 104 moebius n = moebius_aux p n.
 105 intros.
 106 unfold moebius.
 107 change with
 108 (moebius_aux (S (max n (\lambda p:nat.eqb (n\mod nth_prime p) O))) n
 109 = moebius_aux p n).
 110 apply not_divides_to_eq_moebius_aux
 111   [assumption
 112   |intros.
 113    apply divides_b_false_to_not_divides.
 114    unfold divides_b.
 115    apply (lt_max_to_false ? n i)
 116     [assumption
 117     |apply (trans_le ? p)[assumption|assumption]
 118     ]
 119   ]
 120 qed.
 121
 122 theorem moebius_aux_SO: \forall p.moebius_aux p (S O) = pos O.
 123 intros.
 124 elim p
 125   [simplify.reflexivity
 126   |rewrite < H.
 127    apply sym_eq.
 128    apply not_divides_to_eq_moebius_aux
 129    [apply le_n_Sn
 130    |intros.unfold.intro.
 131     absurd (nth_prime i \le S O)
 132       [apply divides_to_le
 133         [apply le_n|assumption]
 134       |apply lt_to_not_le.
 135        apply lt_SO_nth_prime_n.
 136       ]
 137     ]
 138   ]
 139 qed.
 140
 141 theorem p_ord_to_not_eq_O : \forall n,p,q,r.
 142   (S O) < n \to
 143   p_ord n (nth_prime p) = pair nat nat q r \to
 144   Not (r=O).
 145 intros.
 146 unfold.intro.
 147 cut (O < n)
 148   [lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
 149     [apply lt_SO_nth_prime_n.
 150     |assumption
 151     |elim Hletin.
 152      apply (lt_to_not_eq ? ? Hcut).
 153      rewrite > H4.
 154      rewrite > H2.
 155      apply times_n_O
 156     ]
 157   |apply (trans_lt ? (S O))[apply lt_O_S|assumption]
 158   ]
 159 qed.
 160
 161 theorem max_prime_factor_to_not_p_ord_O : \forall n,p,r.
 162   (S O) < n \to
 163   p = max_prime_factor n \to
 164   p_ord n (nth_prime p) \neq pair nat nat O r.
 165 intros.unfold Not.intro.
 166 apply (p_ord_O_to_not_divides ? ? ? ? H2)
 167   [apply (trans_lt ? (S O))[apply lt_O_S|assumption]
 168   |rewrite > H1.
 169    apply divides_max_prime_factor_n.
 170    assumption
 171   ]
 172 qed.
 173
 174 theorem p_ord_SO_SO_to_moebius : \forall n,p.
 175   (S O) < n \to
 176   p = max_prime_factor n \to
 177   p_ord n (nth_prime p) = pair nat nat (S O) (S O) \to
 178   moebius n = Zopp (pos O).
 179 intros.
 180 change with
 181   (moebius_aux (S (max_prime_factor n)) n = neg O).
 182 rewrite < H1.simplify.
 183 rewrite > H2.simplify.
 184 rewrite > moebius_aux_SO.
 185 reflexivity.
 186 qed.
 187
 188 theorem p_ord_SO_r_to_moebius1 : \forall n,p,r.
 189   (S O) < n \to
 190   p = max_prime_factor n \to
 191   (S O) < r \to
 192   p_ord n (nth_prime p) = pair nat nat (S O) r \to
 193   moebius n = Zopp (moebius r).
 194 intros.
 195 change with
 196   (moebius_aux (S (max_prime_factor n)) n = -(moebius r)).
 197 rewrite < H1.simplify.
 198 rewrite > H3.simplify.
 199 apply eq_f.
 200 apply sym_eq.
 201 change with
 202  (moebius_aux (S (max_prime_factor r)) r = moebius_aux p r).
 203 apply not_divides_to_eq_moebius_aux
 204   [apply (p_ord_to_lt_max_prime_factor n p (S O) ? ? H1)
 205     [apply (trans_lt ? (S O))[apply lt_O_S|assumption]
 206     |apply sym_eq. assumption
 207     |assumption
 208     ]
 209   |intros.
 210    lapply (decidable_le i r).
 211    elim Hletin
 212     [apply divides_b_false_to_not_divides.
 213      apply (lt_max_to_false ? r i)[assumption|assumption]
 214     |unfold.intro.apply H6.
 215      apply (trans_le ? (nth_prime i))
 216       [apply lt_to_le.
 217        apply lt_n_nth_prime_n
 218       |apply divides_to_le
 219         [apply (trans_lt ? (S O))[apply lt_O_S|assumption]
 220         |assumption
 221         ]
 222       ]
 223     ]
 224   ]
 225 qed.
 226
 227 theorem p_ord_SO_r_to_moebius : \forall n,p,r.
 228   (S O) < n \to
 229   p = max_prime_factor n \to
 230   p_ord n (nth_prime p) = pair nat nat (S O) r \to
 231   moebius n = Zopp (moebius r).
 232 intros 5.
 233 apply (nat_case r);intro
 234   [apply False_ind.
 235    apply (p_ord_to_not_eq_O ? ? ? ? H H2).
 236    reflexivity
 237   |apply (nat_case m);intros
 238     [simplify.apply (p_ord_SO_SO_to_moebius ? ? H H1 H2)
 239     |apply (p_ord_SO_r_to_moebius1 ? ? ? H H1 ? H2).
 240      apply le_S_S.apply le_S_S.apply le_O_n
 241     ]
 242   ]
 243 qed.
 244
 245 theorem p_ord_SSq_r_to_moebius : \forall n,p,q,r.
 246   (S O) < n \to
 247   p = max_prime_factor n \to
 248   p_ord n (nth_prime p) = pair nat nat (S (S q)) r \to
 249   moebius n = OZ.
 250 intros.
 251 change with
 252   (moebius_aux (S (max n (\lambda p:nat.eqb (n\mod nth_prime p) O))) n =OZ).
 253 rewrite < H1.simplify.
 254 rewrite > H2.simplify.
 255 reflexivity.
 256 qed.
 257
 258 lemma eq_p_max: \forall n,p,r:nat. O < n \to
 259 O < r \to
 260 r = (S O) \lor (max r (\lambda p:nat.eqb (r \mod (nth_prime p)) O)) < p \to
 261 p = max_prime_factor (r*(nth_prime p)\sup n).
 262 intros.
 263 apply sym_eq.
 264 unfold max_prime_factor.
 265 apply max_spec_to_max.
 266 split
 267   [split
 268     [rewrite > times_n_SO in \vdash (? % ?).
 269      rewrite > sym_times.
 270      apply le_times
 271       [assumption
 272       |apply lt_to_le.
 273        apply (lt_to_le_to_lt ? (nth_prime p))
 274         [apply lt_n_nth_prime_n
 275         |rewrite > exp_n_SO in \vdash (? % ?).
 276          apply le_exp
 277           [apply lt_O_nth_prime_n
 278           |assumption
 279           ]
 280         ]
 281       ]
 282     |apply eq_to_eqb_true.
 283      apply divides_to_mod_O
 284       [apply lt_O_nth_prime_n
 285       |apply (lt_O_n_elim ? H).
 286        intro.
 287        apply (witness ? ? (r*(nth_prime p \sup m))).
 288        rewrite < assoc_times.
 289        rewrite < sym_times in \vdash (? ? ? (? % ?)).
 290        rewrite > exp_n_SO in \vdash (? ? ? (? (? ? %) ?)).
 291        rewrite > assoc_times.
 292        rewrite < exp_plus_times.
 293        reflexivity
 294       ]
 295     ]
 296   |intros.
 297    apply not_eq_to_eqb_false.
 298    unfold Not.intro.
 299    lapply (mod_O_to_divides ? ? ? H5)
 300     [apply lt_O_nth_prime_n
 301     |cut (Not (divides (nth_prime i) ((nth_prime p)\sup n)))
 302       [elim H2
 303         [rewrite > H6 in Hletin.
 304          simplify in Hletin.
 305          rewrite < plus_n_O in Hletin.
 306          apply Hcut.assumption
 307         |elim (divides_times_to_divides ? ? ? ? Hletin)
 308           [apply (lt_to_not_le ? ? H3).
 309            apply lt_to_le.
 310            apply (le_to_lt_to_lt ? ? ? ? H6).
 311            apply f_m_to_le_max
 312             [apply (trans_le ? (nth_prime i))
 313               [apply lt_to_le.
 314                apply lt_n_nth_prime_n
 315               |apply divides_to_le[assumption|assumption]
 316               ]
 317             |apply eq_to_eqb_true.
 318              apply divides_to_mod_O
 319               [apply lt_O_nth_prime_n|assumption]
 320             ]
 321           |apply prime_nth_prime
 322           |apply Hcut.assumption
 323           ]
 324         ]
 325       |unfold Not.intro.
 326        apply (lt_to_not_eq ? ? H3).
 327        apply sym_eq.
 328        elim (prime_nth_prime p).
 329        apply injective_nth_prime.
 330        apply H8
 331         [apply (divides_exp_to_divides ? ? ? ? H6).
 332          apply prime_nth_prime.
 333         |apply lt_SO_nth_prime_n
 334         ]
 335       ]
 336     ]
 337   ]
 338 qed.
 339
 340 lemma lt_max_prime_factor_to_not_divides: \forall n,p:nat.
 341 O < n \to n=S O \lor max_prime_factor n < p \to
 342 (nth_prime p \ndivides n).
 343 intros.unfold Not.intro.
 344 elim H1
 345   [rewrite > H3 in H2.
 346    apply (le_to_not_lt (nth_prime p) (S O))
 347     [apply divides_to_le[apply le_n|assumption]
 348     |apply lt_SO_nth_prime_n
 349     ]
 350   |apply (not_le_Sn_n p).
 351    change with (p < p).
 352    apply (le_to_lt_to_lt ? ? ? ? H3).
 353    unfold max_prime_factor.
 354    apply  f_m_to_le_max
 355     [apply (trans_le ? (nth_prime p))
 356       [apply lt_to_le.
 357        apply lt_n_nth_prime_n
 358       |apply divides_to_le;assumption
 359       ]
 360     |apply eq_to_eqb_true.
 361      apply divides_to_mod_O
 362       [apply lt_O_nth_prime_n|assumption]
 363     ]
 364   ]
 365 qed.
 366
 367 theorem moebius_exp: \forall p,q,r:nat. O < r \to
 368 r = (S O) \lor (max_prime_factor r) < p \to
 369 (* r = (S O) \lor (max r (\lambda p:nat.eqb (r \mod (nth_prime p)) O)) < p \to *)
 370 sigma_p (S (S q)) (\lambda y.true) (\lambda y.moebius (r*(exp (nth_prime p) y))) = O.
 371 intros.
 372 elim q
 373   [rewrite > true_to_sigma_p_Sn
 374     [rewrite > true_to_sigma_p_Sn
 375       [rewrite > Zplus_z_OZ.
 376        rewrite < times_n_SO.
 377        rewrite > (p_ord_SO_r_to_moebius ? p r)
 378         [rewrite > sym_Zplus.
 379          rewrite > Zplus_Zopp.
 380          reflexivity
 381         |rewrite < exp_n_SO.
 382          rewrite > sym_times.
 383          rewrite > times_n_SO.
 384          apply lt_to_le_to_lt_times
 385           [apply lt_SO_nth_prime_n
 386           |assumption
 387           |assumption
 388           ]
 389         |apply eq_p_max
 390           [apply le_n|assumption|assumption]
 391         |apply p_ord_exp1
 392           [apply lt_O_nth_prime_n
 393           |apply lt_max_prime_factor_to_not_divides;assumption
 394           |apply sym_times
 395           ]
 396         ]
 397       |reflexivity
 398       ]
 399     |reflexivity
 400     ]
 401   |rewrite > true_to_sigma_p_Sn
 402     [rewrite > H2.
 403      rewrite > Zplus_z_OZ.
 404      apply (p_ord_SSq_r_to_moebius ? p n r)
 405       [rewrite > times_n_SO.
 406        rewrite > sym_times in \vdash (? ? %).
 407        apply lt_to_le_to_lt_times
 408         [apply (trans_lt ? (nth_prime p))
 409           [apply lt_SO_nth_prime_n
 410             |rewrite > exp_n_SO in \vdash (? % ?).
 411              apply lt_exp
 412               [apply lt_SO_nth_prime_n
 413               |apply le_S_S.apply le_S_S.apply le_O_n
 414               ]
 415             ]
 416           |assumption
 417           |assumption
 418           ]
 419         |apply eq_p_max
 420           [apply le_S_S.apply le_O_n|assumption|assumption]
 421         |apply p_ord_exp1
 422           [apply lt_O_nth_prime_n
 423           |apply lt_max_prime_factor_to_not_divides;assumption
 424           |apply sym_times
 425           ]
 426         ]
 427       |reflexivity
 428       ]
 429     ]
 430 qed.
 431
 432 theorem sigma_p_moebius1: \forall n,m,p:nat.O < n \to O < m \to
 433 n = (S O) \lor max_prime_factor n < p \to
 434 sigma_p (S (n*(exp (nth_prime p) m))) (\lambda y.divides_b y (n*(exp (nth_prime p) m))) moebius = O.
 435 intros.
 436 rewrite > sigma_p_divides_b
 437   [apply (trans_eq ? ? (sigma_p (S n) (\lambda x:nat.divides_b x n) (\lambda x:nat.OZ)))
 438     [apply eq_sigma_p1
 439       [intros.reflexivity
 440       |apply (lt_O_n_elim m H1).
 441        intros.apply moebius_exp
 442         [apply (divides_b_true_to_lt_O ? ? ? H4).
 443          assumption
 444         |elim H2
 445           [left.rewrite > H5 in H3.
 446            elim (le_to_or_lt_eq ? ? (le_S_S_to_le ? ? H3))
 447             [apply False_ind.
 448              apply (lt_to_not_le O x)
 449               [apply (divides_b_true_to_lt_O n x H H4)
 450               |apply le_S_S_to_le.assumption
 451               ]
 452             |assumption
 453             ]
 454           |right.
 455            apply (le_to_lt_to_lt ? ? ? ? H5).
 456            apply (divides_to_max_prime_factor1 x n)
 457             [apply (divides_b_true_to_lt_O ? ? H H4)
 458             |assumption
 459             |apply divides_b_true_to_divides.
 460              assumption
 461             ]
 462           ]
 463         ]
 464       ]
 465     |generalize in match (\lambda x:nat.divides_b x n).
 466      intro.
 467      elim n
 468       [simplify.elim (f O);reflexivity
 469       |apply (bool_elim ? (f (S n1)))
 470         [intro.
 471          rewrite > true_to_sigma_p_Sn
 472           [rewrite > H3.reflexivity|assumption]
 473         |intro.
 474          rewrite > false_to_sigma_p_Sn
 475           [apply H3|assumption]
 476         ]
 477       ]
 478     ]
 479   |assumption
 480   |apply prime_nth_prime
 481   |apply lt_max_prime_factor_to_not_divides;assumption
 482   ]
 483 qed.
 484
 485 theorem sigma_p_moebius: \forall n. (S O) < n \to
 486 sigma_p (S n) (\lambda y.divides_b y n) moebius = O.
 487 intros.
 488 lapply (exp_ord (nth_prime (max_prime_factor n)) n)
 489   [rewrite > sym_times in Hletin.
 490    rewrite > Hletin.
 491    apply sigma_p_moebius1
 492     [apply lt_O_ord_rem
 493       [apply lt_SO_nth_prime_n
 494       |apply lt_to_le.assumption
 495       ]
 496     |unfold lt.
 497      change with
 498       (fst ? ? (pair ? ? (S O) (S O)) \leq ord n (nth_prime (max_prime_factor n))).
 499      rewrite < (p_ord_p (nth_prime (max_prime_factor n)))
 500       [apply (divides_to_le_ord ? (nth_prime (max_prime_factor n)) n)
 501         [apply lt_O_nth_prime_n
 502         |apply lt_to_le.assumption
 503         |apply prime_nth_prime
 504         |apply divides_max_prime_factor_n.
 505          assumption
 506         ]
 507       |apply lt_SO_nth_prime_n
 508       ]
 509     |lapply (lt_O_ord_rem (nth_prime (max_prime_factor n)) n)
 510       [elim (le_to_or_lt_eq ? ? Hletin1)
 511         [right.
 512          apply (p_ord_to_lt_max_prime_factor1 n (max_prime_factor n)
 513           (ord n (nth_prime (max_prime_factor n)))
 514           (ord_rem n (nth_prime (max_prime_factor n))))
 515           [apply lt_to_le.assumption
 516           |apply le_n
 517           |auto
 518           |assumption
 519           ]
 520         |left.apply sym_eq.assumption
 521         ]
 522       |apply lt_SO_nth_prime_n
 523       |apply lt_to_le.assumption
 524       ]
 525     ]
 526   |apply lt_SO_nth_prime_n
 527   |apply lt_to_le.assumption
 528   ]
 529 qed.
 530
 531
 532