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