matita/library/Z/dirichlet_product.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/dirichlet_product".
  16
  17 include "nat/primes.ma".
  18 include "Z/sigma_p.ma".
  19 include "Z/times.ma".
  20
  21 definition dirichlet_product : (nat \to Z) \to (nat \to Z) \to nat \to Z \def
  22 \lambda f,g.\lambda n.
  23 sigma_p (S n)
  24  (\lambda d.divides_b d n) (\lambda d. (f d)*(g (div n d))).
  25
  26 (* da spostare *)
  27
  28 (* spostati in div_and_mod.ma
  29 theorem mod_SO: \forall n:nat. mod n (S O) = O.
  30 intro.
  31 apply sym_eq.
  32 apply le_n_O_to_eq.
  33 apply le_S_S_to_le.
  34 apply lt_mod_m_m.
  35 apply le_n.
  36 qed.
  37 theorem div_SO: \forall n:nat. div n (S O) = n.
  38 intro.
  39 rewrite > (div_mod ? (S O)) in \vdash (? ? ? %)
  40   [rewrite > mod_SO.
  41    rewrite < plus_n_O.
  42    apply times_n_SO
  43   |apply le_n
  44   ]
  45 qed.*)
  46
  47 theorem and_true: \forall a,b:bool.
  48 andb a b =true \to a =true \land b= true.
  49 intro.elim a
  50   [split
  51     [reflexivity|assumption]
  52   |apply False_ind.
  53    apply not_eq_true_false.
  54    apply sym_eq.
  55    assumption
  56   ]
  57 qed.
  58
  59 theorem lt_times_plus_times: \forall a,b,n,m:nat.
  60 a < n \to b < m \to a*m + b < n*m.
  61 intros 3.
  62 apply (nat_case n)
  63   [intros.apply False_ind.apply (not_le_Sn_O ? H)
  64   |intros.simplify.
  65    rewrite < sym_plus.
  66    unfold.
  67    change with (S b+a*m1 \leq m1+m*m1).
  68    apply le_plus
  69     [assumption
  70     |apply le_times
  71       [apply le_S_S_to_le.assumption
  72       |apply le_n
  73       ]
  74     ]
  75   ]
  76 qed.
  77
  78 theorem divides_to_divides_b_true1 : \forall n,m:nat.
  79 O < m \to n \divides m \to divides_b n m = true.
  80 intro.
  81 elim (le_to_or_lt_eq O n (le_O_n n))
  82   [apply divides_to_divides_b_true
  83     [assumption|assumption]
  84   |apply False_ind.
  85    rewrite < H in H2.
  86    elim H2.
  87    simplify in H3.
  88    apply (not_le_Sn_O O).
  89    rewrite > H3 in H1.
  90    assumption
  91   ]
  92 qed.
  93 (* spostato in primes.ma
  94 theorem divides_to_div: \forall n,m.divides n m \to m/n*n = m.
  95 intro.
  96 elim (le_to_or_lt_eq O n (le_O_n n))
  97   [rewrite > plus_n_O.
  98    rewrite < (divides_to_mod_O ? ? H H1).
  99    apply sym_eq.
 100    apply div_mod.
 101    assumption
 102   |elim H1.
 103    generalize in match H2.
 104    rewrite < H.
 105    simplify.
 106    intro.
 107    rewrite > H3.
 108    reflexivity
 109   ]
 110 qed.*)
 111 (* spostato in div_and_mod.ma
 112 theorem le_div: \forall n,m. O < n \to m/n \le m.
 113 intros.
 114 rewrite > (div_mod m n) in \vdash (? ? %)
 115   [apply (trans_le ? (m/n*n))
 116     [rewrite > times_n_SO in \vdash (? % ?).
 117      apply le_times
 118       [apply le_n|assumption]
 119     |apply le_plus_n_r
 120     ]
 121   |assumption
 122   ]
 123 qed.*)
 124
 125 theorem sigma_p2_eq:
 126 \forall g: nat \to nat \to Z.
 127 \forall h11,h12,h21,h22: nat \to nat \to nat.
 128 \forall n,m.
 129 \forall p11,p21:nat \to bool.
 130 \forall p12,p22:nat \to nat \to bool.
 131 (\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to
 132 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
 133 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
 134 \land h11 i j < n \land h12 i j < m) \to
 135 (\forall i,j. i < n \to j < m \to p11 i = true \to p12 i j = true \to
 136 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
 137 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
 138 \land (h21 i j) < n \land (h22 i j) < m) \to
 139 sigma_p n p11 (\lambda x:nat .sigma_p m (p12 x) (\lambda y. g x y)) =
 140 sigma_p n p21 (\lambda x:nat .sigma_p m (p22 x) (\lambda y. g (h11 x y) (h12 x y))).
 141 intros.
 142 rewrite < sigma_p2'.
 143 rewrite < sigma_p2'.
 144 apply sym_eq.
 145 letin h := (\lambda x.(h11 (x/m) (x\mod m))*m + (h12 (x/m) (x\mod m))).
 146 letin h1 := (\lambda x.(h21 (x/m) (x\mod m))*m + (h22 (x/m) (x\mod m))).
 147 apply (trans_eq ? ?
 148   (sigma_p (n*m) (\lambda x:nat.p21 (x/m)\land p22 (x/m) (x\mod m))
 149   (\lambda x:nat.g ((h x)/m) ((h x)\mod m))))
 150   [clear h.clear h1.
 151    apply eq_sigma_p1
 152     [intros.reflexivity
 153     |intros.
 154      cut (O < m)
 155       [cut (x/m < n)
 156         [cut (x \mod m < m)
 157           [elim (and_true ? ? H3).
 158            elim (H ? ? Hcut1 Hcut2 H4 H5).
 159            elim H6.clear H6.
 160            elim H8.clear H8.
 161            elim H6.clear H6.
 162            elim H8.clear H8.
 163            apply eq_f2
 164             [apply sym_eq.
 165              apply div_plus_times.
 166              assumption
 167             |autobatch
 168             ]
 169           |apply lt_mod_m_m.
 170            assumption
 171           ]
 172         |apply (lt_times_n_to_lt m)
 173           [assumption
 174           |apply (le_to_lt_to_lt ? x)
 175             [apply (eq_plus_to_le ? ? (x \mod m)).
 176              apply div_mod.
 177              assumption
 178             |assumption
 179             ]
 180           ]
 181         ]
 182       |apply not_le_to_lt.unfold.intro.
 183        generalize in match H2.
 184        apply (le_n_O_elim ? H4).
 185        rewrite < times_n_O.
 186        apply le_to_not_lt.
 187        apply le_O_n
 188       ]
 189     ]
 190   |apply (eq_sigma_p_gh ? h h1);intros
 191     [cut (O < m)
 192       [cut (i/m < n)
 193         [cut (i \mod m < m)
 194           [elim (and_true ? ? H3).
 195            elim (H ? ? Hcut1 Hcut2 H4 H5).
 196            elim H6.clear H6.
 197            elim H8.clear H8.
 198            elim H6.clear H6.
 199            elim H8.clear H8.
 200            cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))/m =
 201                  h11 (i/m) (i\mod m))
 202             [cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))\mod m =
 203                   h12 (i/m) (i\mod m))
 204               [rewrite > Hcut3.
 205                rewrite > Hcut4.
 206                rewrite > H6.
 207                rewrite > H12.
 208                reflexivity
 209               |apply mod_plus_times.
 210                assumption
 211               ]
 212             |apply div_plus_times.
 213              assumption
 214             ]
 215           |apply lt_mod_m_m.
 216            assumption
 217           ]
 218         |apply (lt_times_n_to_lt m)
 219           [assumption
 220           |apply (le_to_lt_to_lt ? i)
 221             [apply (eq_plus_to_le ? ? (i \mod m)).
 222              apply div_mod.
 223              assumption
 224             |assumption
 225             ]
 226           ]
 227         ]
 228       |apply not_le_to_lt.unfold.intro.
 229        generalize in match H2.
 230        apply (le_n_O_elim ? H4).
 231        rewrite < times_n_O.
 232        apply le_to_not_lt.
 233        apply le_O_n
 234       ]
 235     |cut (O < m)
 236       [cut (i/m < n)
 237         [cut (i \mod m < m)
 238           [elim (and_true ? ? H3).
 239            elim (H ? ? Hcut1 Hcut2 H4 H5).
 240            elim H6.clear H6.
 241            elim H8.clear H8.
 242            elim H6.clear H6.
 243            elim H8.clear H8.
 244            cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))/m =
 245                  h11 (i/m) (i\mod m))
 246             [cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))\mod m =
 247                   h12 (i/m) (i\mod m))
 248               [rewrite > Hcut3.
 249                rewrite > Hcut4.
 250                rewrite > H10.
 251                rewrite > H11.
 252                apply sym_eq.
 253                apply div_mod.
 254                assumption
 255               |apply mod_plus_times.
 256                assumption
 257               ]
 258             |apply div_plus_times.
 259              assumption
 260             ]
 261           |apply lt_mod_m_m.
 262            assumption
 263           ]
 264         |apply (lt_times_n_to_lt m)
 265           [assumption
 266           |apply (le_to_lt_to_lt ? i)
 267             [apply (eq_plus_to_le ? ? (i \mod m)).
 268              apply div_mod.
 269              assumption
 270             |assumption
 271             ]
 272           ]
 273         ]
 274       |apply not_le_to_lt.unfold.intro.
 275        generalize in match H2.
 276        apply (le_n_O_elim ? H4).
 277        rewrite < times_n_O.
 278        apply le_to_not_lt.
 279        apply le_O_n
 280       ]
 281     |cut (O < m)
 282       [cut (i/m < n)
 283         [cut (i \mod m < m)
 284           [elim (and_true ? ? H3).
 285            elim (H ? ? Hcut1 Hcut2 H4 H5).
 286            elim H6.clear H6.
 287            elim H8.clear H8.
 288            elim H6.clear H6.
 289            elim H8.clear H8.
 290            apply lt_times_plus_times
 291             [assumption|assumption]
 292           |apply lt_mod_m_m.
 293            assumption
 294           ]
 295         |apply (lt_times_n_to_lt m)
 296           [assumption
 297           |apply (le_to_lt_to_lt ? i)
 298             [apply (eq_plus_to_le ? ? (i \mod m)).
 299              apply div_mod.
 300              assumption
 301             |assumption
 302             ]
 303           ]
 304         ]
 305       |apply not_le_to_lt.unfold.intro.
 306        generalize in match H2.
 307        apply (le_n_O_elim ? H4).
 308        rewrite < times_n_O.
 309        apply le_to_not_lt.
 310        apply le_O_n
 311       ]
 312     |cut (O < m)
 313       [cut (j/m < n)
 314         [cut (j \mod m < m)
 315           [elim (and_true ? ? H3).
 316            elim (H1 ? ? Hcut1 Hcut2 H4 H5).
 317            elim H6.clear H6.
 318            elim H8.clear H8.
 319            elim H6.clear H6.
 320            elim H8.clear H8.
 321            cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))/m =
 322                  h21 (j/m) (j\mod m))
 323             [cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))\mod m =
 324                   h22 (j/m) (j\mod m))
 325               [rewrite > Hcut3.
 326                rewrite > Hcut4.
 327                rewrite > H6.
 328                rewrite > H12.
 329                reflexivity
 330               |apply mod_plus_times.
 331                assumption
 332               ]
 333             |apply div_plus_times.
 334              assumption
 335             ]
 336           |apply lt_mod_m_m.
 337            assumption
 338           ]
 339         |apply (lt_times_n_to_lt m)
 340           [assumption
 341           |apply (le_to_lt_to_lt ? j)
 342             [apply (eq_plus_to_le ? ? (j \mod m)).
 343              apply div_mod.
 344              assumption
 345             |assumption
 346             ]
 347           ]
 348         ]
 349       |apply not_le_to_lt.unfold.intro.
 350        generalize in match H2.
 351        apply (le_n_O_elim ? H4).
 352        rewrite < times_n_O.
 353        apply le_to_not_lt.
 354        apply le_O_n
 355       ]
 356     |cut (O < m)
 357       [cut (j/m < n)
 358         [cut (j \mod m < m)
 359           [elim (and_true ? ? H3).
 360            elim (H1 ? ? Hcut1 Hcut2 H4 H5).
 361            elim H6.clear H6.
 362            elim H8.clear H8.
 363            elim H6.clear H6.
 364            elim H8.clear H8.
 365            cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))/m =
 366                  h21 (j/m) (j\mod m))
 367             [cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))\mod m =
 368                   h22 (j/m) (j\mod m))
 369               [rewrite > Hcut3.
 370                rewrite > Hcut4.
 371                rewrite > H10.
 372                rewrite > H11.
 373                apply sym_eq.
 374                apply div_mod.
 375                assumption
 376               |apply mod_plus_times.
 377                assumption
 378               ]
 379             |apply div_plus_times.
 380              assumption
 381             ]
 382           |apply lt_mod_m_m.
 383            assumption
 384           ]
 385         |apply (lt_times_n_to_lt m)
 386           [assumption
 387           |apply (le_to_lt_to_lt ? j)
 388             [apply (eq_plus_to_le ? ? (j \mod m)).
 389              apply div_mod.
 390              assumption
 391             |assumption
 392             ]
 393           ]
 394         ]
 395       |apply not_le_to_lt.unfold.intro.
 396        generalize in match H2.
 397        apply (le_n_O_elim ? H4).
 398        rewrite < times_n_O.
 399        apply le_to_not_lt.
 400        apply le_O_n
 401       ]
 402     |cut (O < m)
 403       [cut (j/m < n)
 404         [cut (j \mod m < m)
 405           [elim (and_true ? ? H3).
 406            elim (H1 ? ? Hcut1 Hcut2 H4 H5).
 407            elim H6.clear H6.
 408            elim H8.clear H8.
 409            elim H6.clear H6.
 410            elim H8.clear H8.
 411            apply (lt_times_plus_times ? ? ? m)
 412             [assumption|assumption]
 413           |apply lt_mod_m_m.
 414            assumption
 415           ]
 416         |apply (lt_times_n_to_lt m)
 417           [assumption
 418           |apply (le_to_lt_to_lt ? j)
 419             [apply (eq_plus_to_le ? ? (j \mod m)).
 420              apply div_mod.
 421              assumption
 422             |assumption
 423             ]
 424           ]
 425         ]
 426       |apply not_le_to_lt.unfold.intro.
 427        generalize in match H2.
 428        apply (le_n_O_elim ? H4).
 429        rewrite < times_n_O.
 430        apply le_to_not_lt.
 431        apply le_O_n
 432       ]
 433     ]
 434   ]
 435 qed.
 436
 437 (* dirichlet_product is associative only up to extensional equality *)
 438 theorem associative_dirichlet_product:
 439 \forall f,g,h:nat\to Z.\forall n:nat.O < n \to
 440 dirichlet_product (dirichlet_product f g) h n
 441  = dirichlet_product f (dirichlet_product g h) n.
 442 intros.
 443 unfold dirichlet_product.
 444 unfold dirichlet_product.
 445 apply (trans_eq ? ?
 446 (sigma_p (S n) (\lambda d:nat.divides_b d n)
 447 (\lambda d:nat
 448  .sigma_p (S n) (\lambda d1:nat.divides_b d1 d) (\lambda d1:nat.f d1*g (d/d1)*h (n/d)))))
 449   [apply eq_sigma_p1
 450     [intros.reflexivity
 451     |intros.
 452      apply (trans_eq ? ?
 453      (sigma_p (S x) (\lambda d1:nat.divides_b d1 x) (\lambda d1:nat.f d1*g (x/d1)*h (n/x))))
 454       [apply Ztimes_sigma_pr
 455       |(* hint solleva unification uncertain ?? *)
 456        apply sym_eq.
 457        apply false_to_eq_sigma_p
 458         [assumption
 459         |intros.
 460          apply not_divides_to_divides_b_false
 461           [apply (lt_to_le_to_lt ? (S x))
 462             [apply lt_O_S|assumption]
 463           |unfold Not. intro.
 464            apply (lt_to_not_le ? ? H3).
 465            apply divides_to_le
 466             [apply (divides_b_true_to_lt_O ? ? H H2).
 467             |assumption
 468             ]
 469           ]
 470         ]
 471       ]
 472     ]
 473   |apply (trans_eq ? ?
 474    (sigma_p (S n) (\lambda d:nat.divides_b d n)
 475     (\lambda d:nat
 476       .sigma_p (S n) (\lambda d1:nat.divides_b d1 (n/d))
 477       (\lambda d1:nat.f d*g d1*h ((n/d)/d1)))))
 478     [apply (trans_eq ? ?
 479       (sigma_p (S n) (\lambda d:nat.divides_b d n)
 480        (\lambda d:nat
 481         .sigma_p (S n) (\lambda d1:nat.divides_b d1 (n/d))
 482         (\lambda d1:nat.f d*g ((times d d1)/d)*h ((n/times d d1))))))
 483       [apply (sigma_p2_eq
 484         (\lambda d,d1.f d1*g (d/d1)*h (n/d))
 485         (\lambda d,d1:nat.times d d1)
 486         (\lambda d,d1:nat.d)
 487         (\lambda d,d1:nat.d1)
 488         (\lambda d,d1:nat.d/d1)
 489         (S n)
 490         (S n)
 491         ?
 492         ?
 493         (\lambda d,d1:nat.divides_b d1 d)
 494         (\lambda d,d1:nat.divides_b d1 (n/d))
 495         )
 496         [intros.
 497          split
 498           [split
 499             [split
 500               [split
 501                 [split
 502                   [apply divides_to_divides_b_true1
 503                     [assumption
 504                     |apply (witness ? ? ((n/i)/j)).
 505                      rewrite > assoc_times.
 506                      rewrite > sym_times in \vdash (? ? ? (? ? %)).
 507                      rewrite > divides_to_div
 508                       [rewrite > sym_times.
 509                        rewrite > divides_to_div
 510                         [reflexivity
 511                         |apply divides_b_true_to_divides.
 512                          assumption
 513                         ]
 514                       |apply divides_b_true_to_divides.
 515                        assumption
 516                       ]
 517                     ]
 518                   |apply divides_to_divides_b_true
 519                     [apply (divides_b_true_to_lt_O ? ? H H3)
 520                     |apply (witness ? ? j).
 521                      reflexivity
 522                     ]
 523                   ]
 524                 |reflexivity
 525                 ]
 526               |rewrite < sym_times.
 527                rewrite > (plus_n_O (j*i)).
 528                apply div_plus_times.
 529                apply (divides_b_true_to_lt_O ? ? H H3)
 530               ]
 531             |apply (le_to_lt_to_lt ? (i*(n/i)))
 532               [apply le_times
 533                 [apply le_n
 534                 |apply divides_to_le
 535                   [elim (le_to_or_lt_eq ? ? (le_O_n (n/i)))
 536                     [assumption
 537                     |apply False_ind.
 538                      apply (lt_to_not_le ? ? H).
 539                      rewrite < (divides_to_div i n)
 540                       [rewrite < H5.
 541                        apply le_n
 542                       |apply divides_b_true_to_divides.
 543                        assumption
 544                       ]
 545                     ]
 546                   |apply divides_b_true_to_divides.
 547                    assumption
 548                   ]
 549                 ]
 550               |rewrite < sym_times.
 551                rewrite > divides_to_div
 552                 [apply le_n
 553                 |apply divides_b_true_to_divides.
 554                  assumption
 555                 ]
 556               ]
 557             ]
 558           |assumption
 559           ]
 560         |intros.
 561          split
 562           [split
 563             [split
 564               [split
 565                 [split
 566                   [apply divides_to_divides_b_true1
 567                     [assumption
 568                     |apply (transitive_divides ? i)
 569                       [apply divides_b_true_to_divides.
 570                        assumption
 571                       |apply divides_b_true_to_divides.
 572                        assumption
 573                       ]
 574                     ]
 575                   |apply divides_to_divides_b_true
 576                     [apply (divides_b_true_to_lt_O i (i/j))
 577                       [apply (divides_b_true_to_lt_O ? ? ? H3).
 578                        assumption
 579                       |apply divides_to_divides_b_true1
 580                         [apply (divides_b_true_to_lt_O ? ? ? H3).
 581                          assumption
 582                         |apply (witness ? ? j).
 583                          apply sym_eq.
 584                          apply divides_to_div.
 585                          apply divides_b_true_to_divides.
 586                          assumption
 587                         ]
 588                       ]
 589                     |apply (witness ? ? (n/i)).
 590                      apply (inj_times_l1 j)
 591                       [apply (divides_b_true_to_lt_O ? ? ? H4).
 592                        apply (divides_b_true_to_lt_O ? ? ? H3).
 593                        assumption
 594                       |rewrite > divides_to_div
 595                         [rewrite > sym_times in \vdash (? ? ? (? % ?)).
 596                          rewrite > assoc_times.
 597                          rewrite > divides_to_div
 598                           [rewrite > divides_to_div
 599                             [reflexivity
 600                             |apply divides_b_true_to_divides.
 601                              assumption
 602                             ]
 603                           |apply divides_b_true_to_divides.
 604                            assumption
 605                           ]
 606                         |apply (transitive_divides ? i)
 607                           [apply divides_b_true_to_divides.
 608                            assumption
 609                           |apply divides_b_true_to_divides.
 610                            assumption
 611                           ]
 612                         ]
 613                       ]
 614                     ]
 615                   ]
 616                 |rewrite < sym_times.
 617                  apply divides_to_div.
 618                  apply divides_b_true_to_divides.
 619                  assumption
 620                 ]
 621               |reflexivity
 622               ]
 623             |assumption
 624             ]
 625           |apply (le_to_lt_to_lt ? i)
 626             [apply le_div.
 627              apply (divides_b_true_to_lt_O ? ? ? H4).
 628              apply (divides_b_true_to_lt_O ? ? ? H3).
 629              assumption
 630             |assumption
 631             ]
 632           ]
 633         ]
 634       |apply eq_sigma_p1
 635         [intros.reflexivity
 636         |intros.
 637          apply eq_sigma_p1
 638           [intros.reflexivity
 639           |intros.
 640            apply eq_f2
 641             [apply eq_f2
 642               [reflexivity
 643               |apply eq_f.
 644                rewrite > sym_times.
 645                rewrite > (plus_n_O (x1*x)).
 646                apply div_plus_times.
 647                apply (divides_b_true_to_lt_O ? ? ? H2).
 648                assumption
 649               ]
 650             |apply eq_f.
 651              cut (O < x)
 652               [cut (O < x1)
 653                 [apply (inj_times_l1 (x*x1))
 654                   [rewrite > (times_n_O O).
 655                    apply lt_times;assumption
 656                   |rewrite > divides_to_div
 657                     [rewrite > sym_times in \vdash (? ? ? (? ? %)).
 658                      rewrite < assoc_times.
 659                      rewrite > divides_to_div
 660                       [rewrite > divides_to_div
 661                         [reflexivity
 662                         |apply divides_b_true_to_divides.
 663                          assumption
 664                         ]
 665                       |apply divides_b_true_to_divides.
 666                        assumption
 667                       ]
 668                     |elim (divides_b_true_to_divides ? ? H4).
 669                      apply (witness ? ? n2).
 670                      rewrite > assoc_times.
 671                      rewrite < H5.
 672                      rewrite < sym_times.
 673                      apply sym_eq.
 674                      apply divides_to_div.
 675                      apply divides_b_true_to_divides.
 676                      assumption
 677                     ]
 678                   ]
 679                 |apply (divides_b_true_to_lt_O ? ? ? H4).
 680                  apply (lt_times_n_to_lt x)
 681                   [assumption
 682                   |simplify.
 683                    rewrite > divides_to_div
 684                     [assumption
 685                     |apply (divides_b_true_to_divides ? ? H2).
 686                      assumption
 687                     ]
 688                   ]
 689                 ]
 690               |apply (divides_b_true_to_lt_O ? ? ? H2).
 691                assumption
 692               ]
 693             ]
 694           ]
 695         ]
 696       ]
 697     |apply eq_sigma_p1
 698       [intros.reflexivity
 699       |intros.
 700        apply (trans_eq ? ?
 701        (sigma_p (S n) (\lambda d1:nat.divides_b d1 (n/x)) (\lambda d1:nat.f x*(g d1*h (n/x/d1)))))
 702         [apply eq_sigma_p
 703           [intros.reflexivity
 704           |intros.apply assoc_Ztimes
 705           ]
 706         |apply (trans_eq ? ?
 707           (sigma_p (S (n/x)) (\lambda d1:nat.divides_b d1 (n/x)) (\lambda d1:nat.f x*(g d1*h (n/x/d1)))))
 708           [apply false_to_eq_sigma_p
 709             [apply le_S_S.
 710              cut (O < x)
 711               [apply (le_times_to_le x)
 712                 [assumption
 713                 |rewrite > sym_times.
 714                  rewrite > divides_to_div
 715                   [apply le_times_n.
 716                    assumption
 717                   |apply divides_b_true_to_divides.
 718                    assumption
 719                   ]
 720                 ]
 721               |apply (divides_b_true_to_lt_O ? ? ? H2).
 722                assumption
 723               ]
 724             |intros.
 725              apply not_divides_to_divides_b_false
 726               [apply (trans_le ? ? ? ? H3).
 727                apply le_S_S.
 728                apply le_O_n
 729               |unfold Not.intro.
 730                apply (le_to_not_lt ? ? H3).
 731                apply le_S_S.
 732                apply divides_to_le
 733                 [apply (lt_times_n_to_lt x)
 734                   [apply (divides_b_true_to_lt_O ? ? ? H2).
 735                    assumption
 736                   |simplify.
 737                    rewrite > divides_to_div
 738                     [assumption
 739                     |apply (divides_b_true_to_divides ? ? H2).
 740                      assumption
 741                     ]
 742                   ]
 743                 |assumption
 744                 ]
 745               ]
 746             ]
 747           |apply sym_eq.
 748            apply Ztimes_sigma_pl
 749           ]
 750         ]
 751       ]
 752     ]
 753   ]
 754 qed.
 755
 756 definition is_one: nat \to Z \def
 757 \lambda n.
 758   match n with
 759   [O \Rightarrow OZ
 760   | (S p) \Rightarrow
 761     match p with
 762     [ O \Rightarrow pos O
 763     | (S q) \Rightarrow OZ]]
 764 .
 765
 766 theorem is_one_OZ: \forall n. n \neq S O \to is_one n = OZ.
 767 intro.apply (nat_case n)
 768   [intro.reflexivity
 769   |intro. apply (nat_case m)
 770     [intro.apply False_ind.apply H.reflexivity
 771     |intros.reflexivity
 772     ]
 773   ]
 774 qed.
 775
 776 (* da spostare in times *)
 777 definition Zone \def pos O.
 778
 779 theorem Ztimes_Zone_l: \forall z:Z. Ztimes Zone z = z.
 780 intro.unfold Zone.simplify.
 781 elim z;simplify
 782   [reflexivity
 783   |rewrite < plus_n_O.reflexivity
 784   |rewrite < plus_n_O.reflexivity
 785   ]
 786 qed.
 787
 788 theorem Ztimes_Zone_r: \forall z:Z. Ztimes z Zone = z.
 789 intro.
 790 rewrite < sym_Ztimes.
 791 apply Ztimes_Zone_l.
 792 qed.
 793
 794 theorem injective_Zplus_l: \forall x:Z.injective Z Z (\lambda y.y+x).
 795 intro.simplify.intros (z y).
 796 rewrite < Zplus_z_OZ.
 797 rewrite < (Zplus_z_OZ y).
 798 rewrite < (Zplus_Zopp x).
 799 rewrite < (Zplus_Zopp x).
 800 rewrite < assoc_Zplus.
 801 rewrite < assoc_Zplus.
 802 apply eq_f2
 803   [assumption|reflexivity]
 804 qed.
 805
 806 theorem injective_Zplus_r: \forall x:Z.injective Z Z (\lambda y.x+y).
 807 intro.simplify.intros (z y).
 808 apply (injective_Zplus_l x).
 809 rewrite < sym_Zplus.
 810 rewrite > H.
 811 apply sym_Zplus.
 812 qed.
 813
 814 theorem sigma_p_OZ:
 815 \forall p: nat \to bool.\forall n.sigma_p n p (\lambda m.OZ) = OZ.
 816 intros.elim n
 817   [reflexivity
 818   |apply (bool_elim ? (p n1));intro
 819     [rewrite > true_to_sigma_p_Sn
 820       [rewrite > sym_Zplus.
 821        rewrite > Zplus_z_OZ.
 822        assumption
 823       |assumption
 824       ]
 825     |rewrite > false_to_sigma_p_Sn
 826       [assumption
 827       |assumption
 828       ]
 829     ]
 830   ]
 831 qed.
 832
 833 theorem dirichlet_product_is_one_r:
 834 \forall f:nat\to Z.\forall n:nat.
 835   dirichlet_product f is_one n = f n.
 836 intros.
 837 elim n
 838   [unfold dirichlet_product.
 839    rewrite > true_to_sigma_p_Sn
 840     [rewrite > Ztimes_Zone_r.
 841      rewrite > Zplus_z_OZ.
 842      reflexivity
 843     |reflexivity
 844     ]
 845   |unfold dirichlet_product.
 846    rewrite > true_to_sigma_p_Sn
 847     [rewrite > div_n_n
 848       [rewrite > Ztimes_Zone_r.
 849        rewrite < Zplus_z_OZ in \vdash (? ? ? %).
 850        apply eq_f2
 851         [reflexivity
 852         |apply (trans_eq ? ? (sigma_p (S n1)
 853           (\lambda d:nat.divides_b d (S n1)) (\lambda d:nat.OZ)))
 854           [apply eq_sigma_p1;intros
 855             [reflexivity
 856             |rewrite > is_one_OZ
 857               [apply Ztimes_z_OZ
 858               |unfold Not.intro.
 859                apply (lt_to_not_le ? ? H1).
 860                rewrite > (times_n_SO x).
 861                rewrite > sym_times.
 862                rewrite < H3.
 863                rewrite > (div_mod ? x) in \vdash (? % ?)
 864                 [rewrite > divides_to_mod_O
 865                   [rewrite < plus_n_O.
 866                    apply le_n
 867                   |apply (divides_b_true_to_lt_O ? ? ? H2).
 868                    apply lt_O_S
 869                   |apply divides_b_true_to_divides.
 870                    assumption
 871                   ]
 872                 |apply (divides_b_true_to_lt_O ? ? ? H2).
 873                  apply lt_O_S
 874                 ]
 875               ]
 876             ]
 877           |apply sigma_p_OZ
 878           ]
 879         ]
 880       |apply lt_O_S
 881       ]
 882     |apply divides_to_divides_b_true
 883       [apply lt_O_S
 884       |apply divides_n_n
 885       ]
 886     ]
 887   ]
 888 qed.
 889
 890 (* da spostare *)
 891 theorem notb_notb: \forall b:bool. notb (notb b) = b.
 892 intros.
 893 elim b;reflexivity.
 894 qed.
 895
 896 theorem injective_notb: injective bool bool notb.
 897 unfold injective.
 898 intros.
 899 rewrite < notb_notb.
 900 rewrite < (notb_notb y).
 901 apply eq_f.
 902 assumption.
 903 qed.
 904
 905 theorem divides_div: \forall d,n. divides d n \to divides (n/d) n.
 906 intros.
 907 apply (witness ? ? d).
 908 apply sym_eq.
 909 apply divides_to_div.
 910 assumption.
 911 qed.
 912
 913 theorem divides_b_div_true:
 914 \forall d,n. O < n \to
 915   divides_b d n = true \to divides_b (n/d) n = true.
 916 intros.
 917 apply divides_to_divides_b_true1
 918   [assumption
 919   |apply divides_div.
 920    apply divides_b_true_to_divides.
 921    assumption
 922   ]
 923 qed.
 924
 925 (* spostato in primes.ma (non in div_and_mod.ma perche' serve il predicato divides)
 926 theorem div_div: \forall n,d:nat. O < n \to divides d n \to
 927 n/(n/d) = d.
 928 intros.
 929 apply (inj_times_l1 (n/d))
 930   [apply (lt_times_n_to_lt d)
 931     [apply (divides_to_lt_O ? ? H H1).
 932     |rewrite > divides_to_div;assumption
 933     ]
 934   |rewrite > divides_to_div
 935     [rewrite > sym_times.
 936      rewrite > divides_to_div
 937       [reflexivity
 938       |assumption
 939       ]
 940     |apply (witness ? ? d).
 941      apply sym_eq.
 942      apply divides_to_div.
 943      assumption
 944     ]
 945   ]
 946 qed.
 947 *)
 948 theorem commutative_dirichlet_product: \forall f,g:nat \to Z.\forall n. O < n \to
 949 dirichlet_product f g n = dirichlet_product g f n.
 950 intros.
 951 unfold dirichlet_product.
 952 apply (trans_eq ? ?
 953   (sigma_p (S n) (\lambda d:nat.divides_b d n)
 954   (\lambda d:nat.g (n/d) * f (n/(n/d)))))
 955   [apply eq_sigma_p1;intros
 956     [reflexivity
 957     |rewrite > div_div
 958       [apply sym_Ztimes.
 959       |assumption
 960       |apply divides_b_true_to_divides.
 961        assumption
 962       ]
 963     ]
 964   |apply (eq_sigma_p_gh ? (\lambda d.(n/d)) (\lambda d.(n/d)))
 965     [intros.
 966      apply divides_b_div_true;assumption
 967     |intros.
 968      apply div_div
 969       [assumption
 970       |apply divides_b_true_to_divides.
 971        assumption
 972       ]
 973     |intros.
 974      apply le_S_S.
 975      apply le_div.
 976      apply (divides_b_true_to_lt_O ? ? H H2)
 977     |intros.
 978      apply divides_b_div_true;assumption
 979     |intros.
 980      apply div_div
 981       [assumption
 982       |apply divides_b_true_to_divides.
 983        assumption
 984       ]
 985     |intros.
 986      apply le_S_S.
 987      apply le_div.
 988      apply (divides_b_true_to_lt_O ? ? H H2)
 989     ]
 990   ]
 991 qed.
 992
 993 theorem dirichlet_product_is_one_l:
 994 \forall f:nat\to Z.\forall n:nat.
 995 O < n \to dirichlet_product is_one f n = f n.
 996 intros.
 997 rewrite > commutative_dirichlet_product.
 998 apply dirichlet_product_is_one_r.
 999 assumption.
1000 qed.
1001
1002 theorem dirichlet_product_one_r:
1003 \forall f:nat\to Z.\forall n:nat. O < n \to
1004 dirichlet_product f (\lambda n.Zone) n =
1005 sigma_p (S n) (\lambda d.divides_b d n) f.
1006 intros.
1007 unfold dirichlet_product.
1008 apply eq_sigma_p;intros
1009   [reflexivity
1010   |simplify in \vdash (? ? (? ? %) ?).
1011    apply Ztimes_Zone_r
1012   ]
1013 qed.
1014
1015 theorem dirichlet_product_one_l:
1016 \forall f:nat\to Z.\forall n:nat. O < n \to
1017 dirichlet_product (\lambda n.Zone) f n =
1018 sigma_p (S n) (\lambda d.divides_b d n) f.
1019 intros.
1020 rewrite > commutative_dirichlet_product
1021   [apply dirichlet_product_one_r.
1022    assumption
1023   |assumption
1024   ]
1025 qed.