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 (*
  44 theorem moebius_O : moebius O = pos O.
  45 simplify. reflexivity.
  46 qed.
  47
  48 theorem moebius_SO : moebius (S O) = pos O.
  49 simplify.reflexivity.
  50 qed.
  51
  52 theorem moebius_SSO : moebius (S (S O)) = neg O.
  53 simplify.reflexivity.
  54 qed.
  55
  56 theorem moebius_SSSO : moebius (S (S (S O))) = neg O.
  57 simplify.reflexivity.
  58 qed.
  59
  60 theorem moebius_SSSSO : moebius (S (S (S (S O)))) = OZ.
  61 simplify.reflexivity.
  62 qed.
  63 *)
  64
  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) =
  67 pair nat nat O n.
  68 intros.
  69 apply p_ord_exp1
  70   [apply lt_O_nth_prime_n
  71   |assumption
  72   |autobatch
  73   ]
  74 qed.
  75
  76 theorem p_ord_O_to_not_divides: \forall n,i,r.
  77 O < n \to
  78 p_ord n (nth_prime i) = pair nat nat O r
  79 \to Not (divides (nth_prime i) n).
  80 intros.
  81 lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
  82   [apply lt_SO_nth_prime_n
  83   |assumption
  84   |elim Hletin.
  85    simplify in H3.
  86    rewrite > H3.
  87    rewrite < plus_n_O.
  88    assumption
  89   ]
  90 qed.
  91
  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.
  95 intros 4.
  96 elim H
  97   [reflexivity
  98   |simplify.
  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]
 103     ]
 104   ]
 105 qed.
 106
 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.
 110 intros.
 111 unfold moebius.
 112 change with
 113 (moebius_aux (S (max n (\lambda p:nat.eqb (n\mod nth_prime p) O))) n
 114 = moebius_aux p n).
 115 apply not_divides_to_eq_moebius_aux
 116   [assumption
 117   |intros.
 118    apply divides_b_false_to_not_divides.
 119    unfold divides_b.
 120    apply (lt_max_to_false ? n i)
 121     [assumption
 122     |apply (trans_le ? p)[assumption|assumption]
 123     ]
 124   ]
 125 qed.
 126
 127 theorem moebius_aux_SO: \forall p.moebius_aux p (S O) = pos O.
 128 intros.
 129 elim p
 130   [simplify.reflexivity
 131   |rewrite < H.
 132    apply sym_eq.
 133    apply not_divides_to_eq_moebius_aux
 134    [apply le_n_Sn
 135    |intros.unfold.intro.
 136     absurd (nth_prime i \le S O)
 137       [apply divides_to_le
 138         [apply le_n|assumption]
 139       |apply lt_to_not_le.
 140        apply lt_SO_nth_prime_n.
 141       ]
 142     ]
 143   ]
 144 qed.
 145
 146 theorem p_ord_to_not_eq_O : \forall n,p,q,r.
 147   (S O) < n \to
 148   p_ord n (nth_prime p) = pair nat nat q r \to
 149   Not (r=O).
 150 intros.
 151 unfold.intro.
 152 cut (O < n)
 153   [lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
 154     [apply lt_SO_nth_prime_n.
 155     |assumption
 156     |elim Hletin.
 157      apply (lt_to_not_eq ? ? Hcut).
 158      rewrite > H4.
 159      rewrite > H2.
 160      apply times_n_O
 161     ]
 162   |apply (trans_lt ? (S O))[apply lt_O_S|assumption]
 163   ]
 164 qed.
 165
 166 theorem max_prime_factor_to_not_p_ord_O : \forall n,p,r.
 167   (S O) < n \to
 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]
 173   |rewrite > H1.
 174    apply divides_max_prime_factor_n.
 175    assumption
 176   ]
 177 qed.
 178
 179 theorem p_ord_SO_SO_to_moebius : \forall n,p.
 180   (S O) < n \to
 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).
 184 intros.
 185 change with
 186   (moebius_aux (S (max_prime_factor n)) n = neg O).
 187 rewrite < H1.simplify.
 188 rewrite > H2.simplify.
 189 rewrite > moebius_aux_SO.
 190 reflexivity.
 191 qed.
 192
 193 theorem p_ord_SO_r_to_moebius1 : \forall n,p,r.
 194   (S O) < n \to
 195   p = max_prime_factor n \to
 196   (S O) < r \to
 197   p_ord n (nth_prime p) = pair nat nat (S O) r \to
 198   moebius n = Zopp (moebius r).
 199 intros.
 200 change with
 201   (moebius_aux (S (max_prime_factor n)) n = -(moebius r)).
 202 rewrite < H1.simplify.
 203 rewrite > H3.simplify.
 204 apply eq_f.
 205 apply sym_eq.
 206 change with
 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
 212     |assumption
 213     ]
 214   |intros.
 215    lapply (decidable_le i r).
 216    elim Hletin
 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))
 221       [apply lt_to_le.
 222        apply lt_n_nth_prime_n
 223       |apply divides_to_le
 224         [apply (trans_lt ? (S O))[apply lt_O_S|assumption]
 225         |assumption
 226         ]
 227       ]
 228     ]
 229   ]
 230 qed.
 231
 232 theorem p_ord_SO_r_to_moebius : \forall n,p,r.
 233   (S O) < n \to
 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).
 237 intros 5.
 238 apply (nat_case r);intro
 239   [apply False_ind.
 240    apply (p_ord_to_not_eq_O ? ? ? ? H H2).
 241    reflexivity
 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
 246     ]
 247   ]
 248 qed.
 249
 250 theorem p_ord_SSq_r_to_moebius : \forall n,p,q,r.
 251   (S O) < n \to
 252   p = max_prime_factor n \to
 253   p_ord n (nth_prime p) = pair nat nat (S (S q)) r \to
 254   moebius n = OZ.
 255 intros.
 256 change with
 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.
 260 reflexivity.
 261 qed.
 262
 263 lemma eq_p_max: \forall n,p,r:nat. O < n \to
 264 O < r \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).
 267 intros.
 268 apply sym_eq.
 269 unfold max_prime_factor.
 270 apply max_spec_to_max.
 271 split
 272   [split
 273     [rewrite > times_n_SO in \vdash (? % ?).
 274      rewrite > sym_times.
 275      apply le_times
 276       [assumption
 277       |apply lt_to_le.
 278        apply (lt_to_le_to_lt ? (nth_prime p))
 279         [apply lt_n_nth_prime_n
 280         |rewrite > exp_n_SO in \vdash (? % ?).
 281          apply le_exp
 282           [apply lt_O_nth_prime_n
 283           |assumption
 284           ]
 285         ]
 286       ]
 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).
 291        intro.
 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.
 298        reflexivity
 299       ]
 300     ]
 301   |intros.
 302    apply not_eq_to_eqb_false.
 303    unfold Not.intro.
 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)))
 307       [elim H2
 308         [rewrite > H6 in Hletin.
 309          simplify 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).
 314            apply lt_to_le.
 315            apply (le_to_lt_to_lt ? ? ? ? H6).
 316            apply f_m_to_le_max
 317             [apply (trans_le ? (nth_prime i))
 318               [apply lt_to_le.
 319                apply lt_n_nth_prime_n
 320               |apply divides_to_le[assumption|assumption]
 321               ]
 322             |apply eq_to_eqb_true.
 323              apply divides_to_mod_O
 324               [apply lt_O_nth_prime_n|assumption]
 325             ]
 326           |apply prime_nth_prime
 327           |apply Hcut.assumption
 328           ]
 329         ]
 330       |unfold Not.intro.
 331        apply (lt_to_not_eq ? ? H3).
 332        apply sym_eq.
 333        elim (prime_nth_prime p).
 334        apply injective_nth_prime.
 335        apply H8
 336         [apply (divides_exp_to_divides ? ? ? ? H6).
 337          apply prime_nth_prime.
 338         |apply lt_SO_nth_prime_n
 339         ]
 340       ]
 341     ]
 342   ]
 343 qed.
 344
 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.
 349 elim H1
 350   [rewrite > H3 in H2.
 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
 354     ]
 355   |apply (not_le_Sn_n p).
 356    change with (p < p).
 357    apply (le_to_lt_to_lt ? ? ? ? H3).
 358    unfold max_prime_factor.
 359    apply  f_m_to_le_max
 360     [apply (trans_le ? (nth_prime p))
 361       [apply lt_to_le.
 362        apply lt_n_nth_prime_n
 363       |apply divides_to_le;assumption
 364       ]
 365     |apply eq_to_eqb_true.
 366      apply divides_to_mod_O
 367       [apply lt_O_nth_prime_n|assumption]
 368     ]
 369   ]
 370 qed.
 371
 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.
 376 intros.
 377 elim q
 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.
 385          reflexivity
 386         |rewrite < exp_n_SO.
 387          rewrite > sym_times.
 388          rewrite > times_n_SO.
 389          apply lt_to_le_to_lt_times
 390           [apply lt_SO_nth_prime_n
 391           |assumption
 392           |assumption
 393           ]
 394         |apply eq_p_max
 395           [apply le_n|assumption|assumption]
 396         |apply p_ord_exp1
 397           [apply lt_O_nth_prime_n
 398           |apply lt_max_prime_factor_to_not_divides;assumption
 399           |apply sym_times
 400           ]
 401         ]
 402       |reflexivity
 403       ]
 404     |reflexivity
 405     ]
 406   |rewrite > true_to_sigma_p_Sn
 407     [rewrite > H2.
 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 (? % ?).
 416              apply lt_exp
 417               [apply lt_SO_nth_prime_n
 418               |apply le_S_S.apply le_S_S.apply le_O_n
 419               ]
 420             ]
 421           |assumption
 422           |assumption
 423           ]
 424         |apply eq_p_max
 425           [apply le_S_S.apply le_O_n|assumption|assumption]
 426         |apply p_ord_exp1
 427           [apply lt_O_nth_prime_n
 428           |apply lt_max_prime_factor_to_not_divides;assumption
 429           |apply sym_times
 430           ]
 431         ]
 432       |reflexivity
 433       ]
 434     ]
 435 qed.
 436
 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.
 440 intros.
 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)))
 443     [apply eq_sigma_p1
 444       [intros.reflexivity
 445       |apply (lt_O_n_elim m H1).
 446        intros.apply moebius_exp
 447         [apply (divides_b_true_to_lt_O ? ? ? H4).
 448          assumption
 449         |elim H2
 450           [left.rewrite > H5 in H3.
 451            elim (le_to_or_lt_eq ? ? (le_S_S_to_le ? ? H3))
 452             [apply False_ind.
 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
 456               ]
 457             |assumption
 458             ]
 459           |right.
 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)
 463             |assumption
 464             |apply divides_b_true_to_divides.
 465              assumption
 466             ]
 467           ]
 468         ]
 469       ]
 470     |generalize in match (\lambda x:nat.divides_b x n).
 471      intro.
 472      elim n
 473       [simplify.elim (f O);reflexivity
 474       |apply (bool_elim ? (f (S n1)))
 475         [intro.
 476          rewrite > true_to_sigma_p_Sn
 477           [rewrite > H3.reflexivity|assumption]
 478         |intro.
 479          rewrite > false_to_sigma_p_Sn
 480           [apply H3|assumption]
 481         ]
 482       ]
 483     ]
 484   |assumption
 485   |apply prime_nth_prime
 486   |apply lt_max_prime_factor_to_not_divides;assumption
 487   ]
 488 qed.
 489
 490 theorem sigma_p_moebius: \forall n. (S O) < n \to
 491 sigma_p (S n) (\lambda y.divides_b y n) moebius = O.
 492 intros.
 493 lapply (exp_ord (nth_prime (max_prime_factor n)) n)
 494   [rewrite > sym_times in Hletin.
 495    rewrite > Hletin.
 496    apply sigma_p_moebius1
 497     [apply lt_O_ord_rem
 498       [apply lt_SO_nth_prime_n
 499       |apply lt_to_le.assumption
 500       ]
 501     |unfold lt.
 502      change with
 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.
 510          assumption
 511         ]
 512       |apply lt_SO_nth_prime_n
 513       ]
 514     |lapply (lt_O_ord_rem (nth_prime (max_prime_factor n)) n)
 515       [elim (le_to_or_lt_eq ? ? Hletin1)
 516         [right.
 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
 521           |apply le_n
 522           |autobatch
 523           |assumption
 524           ]
 525         |left.apply sym_eq.assumption
 526         ]
 527       |apply lt_SO_nth_prime_n
 528       |apply lt_to_le.assumption
 529       ]
 530     ]
 531   |apply lt_SO_nth_prime_n
 532   |apply lt_to_le.assumption
 533   ]
 534 qed.
 535
 536
 537