helm/software/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 include "nat/primes.ma".
  16 include "Z/sigma_p.ma".
  17 include "Z/times.ma".
  18
  19 definition dirichlet_product : (nat \to Z) \to (nat \to Z) \to nat \to Z \def
  20 \lambda f,g.\lambda n.
  21 sigma_p (S n)
  22  (\lambda d.divides_b d n) (\lambda d. (f d)*(g (div n d))).
  23
  24 (* dirichlet_product is associative only up to extensional equality *)
  25 theorem associative_dirichlet_product:
  26 \forall f,g,h:nat\to Z.\forall n:nat.O < n \to
  27 dirichlet_product (dirichlet_product f g) h n
  28  = dirichlet_product f (dirichlet_product g h) n.
  29 intros.
  30 unfold dirichlet_product.
  31 unfold dirichlet_product.
  32 apply (trans_eq ? ?
  33 (sigma_p (S n) (\lambda d:nat.divides_b d n)
  34 (\lambda d:nat
  35  .sigma_p (S n) (\lambda d1:nat.divides_b d1 d) (\lambda d1:nat.f d1*g (d/d1)*h (n/d)))))
  36   [apply eq_sigma_p1
  37     [intros.reflexivity
  38     |intros.
  39      apply (trans_eq ? ?
  40      (sigma_p (S x) (\lambda d1:nat.divides_b d1 x) (\lambda d1:nat.f d1*g (x/d1)*h (n/x))))
  41       [apply Ztimes_sigma_pr
  42       |(* hint solleva unification uncertain ?? *)
  43        apply sym_eq.
  44        apply false_to_eq_sigma_p
  45         [assumption
  46         |intros.
  47          apply not_divides_to_divides_b_false
  48           [apply (lt_to_le_to_lt ? (S x))
  49             [apply lt_O_S|assumption]
  50           |unfold Not. intro.
  51            apply (lt_to_not_le ? ? H3).
  52            apply divides_to_le
  53             [apply (divides_b_true_to_lt_O ? ? H H2).
  54             |assumption
  55             ]
  56           ]
  57         ]
  58       ]
  59     ]
  60   |apply (trans_eq ? ?
  61    (sigma_p (S n) (\lambda d:nat.divides_b d n)
  62     (\lambda d:nat
  63       .sigma_p (S n) (\lambda d1:nat.divides_b d1 (n/d))
  64       (\lambda d1:nat.f d*g d1*h ((n/d)/d1)))))
  65     [apply (trans_eq ? ?
  66       (sigma_p (S n) (\lambda d:nat.divides_b d n)
  67        (\lambda d:nat
  68         .sigma_p (S n) (\lambda d1:nat.divides_b d1 (n/d))
  69         (\lambda d1:nat.f d*g ((times d d1)/d)*h ((n/times d d1))))))
  70       [apply (sigma_p2_eq
  71         (\lambda d,d1.f d1*g (d/d1)*h (n/d))
  72         (\lambda d,d1:nat.times d d1)
  73         (\lambda d,d1:nat.d)
  74         (\lambda d,d1:nat.d1)
  75         (\lambda d,d1:nat.d/d1)
  76         (S n)
  77         (S n)
  78         (S n)
  79         (S n)
  80         ?
  81         ?
  82         (\lambda d,d1:nat.divides_b d1 d)
  83         (\lambda d,d1:nat.divides_b d1 (n/d))
  84         )
  85         [intros.
  86          split
  87           [split
  88             [split
  89               [split
  90                 [split
  91                   [apply divides_to_divides_b_true1
  92                     [assumption
  93                     |apply (witness ? ? ((n/i)/j)).
  94                      rewrite > assoc_times.
  95                      rewrite > sym_times in \vdash (? ? ? (? ? %)).
  96                      rewrite > divides_to_div
  97                       [rewrite > sym_times.
  98                        rewrite > divides_to_div
  99                         [reflexivity
 100                         |apply divides_b_true_to_divides.
 101                          assumption
 102                         ]
 103                       |apply divides_b_true_to_divides.
 104                        assumption
 105                       ]
 106                     ]
 107                   |apply divides_to_divides_b_true
 108                     [apply (divides_b_true_to_lt_O ? ? H H3)
 109                     |apply (witness ? ? j).
 110                      reflexivity
 111                     ]
 112                   ]
 113                 |reflexivity
 114                 ]
 115               |rewrite < sym_times.
 116                rewrite > (plus_n_O (j*i)).
 117                apply div_plus_times.
 118                apply (divides_b_true_to_lt_O ? ? H H3)
 119               ]
 120             |apply (le_to_lt_to_lt ? (i*(n/i)))
 121               [apply le_times
 122                 [apply le_n
 123                 |apply divides_to_le
 124                   [elim (le_to_or_lt_eq ? ? (le_O_n (n/i)))
 125                     [assumption
 126                     |apply False_ind.
 127                      apply (lt_to_not_le ? ? H).
 128                      rewrite < (divides_to_div i n)
 129                       [rewrite < H5.
 130                        apply le_n
 131                       |apply divides_b_true_to_divides.
 132                        assumption
 133                       ]
 134                     ]
 135                   |apply divides_b_true_to_divides.
 136                    assumption
 137                   ]
 138                 ]
 139               |rewrite < sym_times.
 140                rewrite > divides_to_div
 141                 [apply le_n
 142                 |apply divides_b_true_to_divides.
 143                  assumption
 144                 ]
 145               ]
 146             ]
 147           |assumption
 148           ]
 149         |intros.
 150          split
 151           [split
 152             [split
 153               [split
 154                 [split
 155                   [apply divides_to_divides_b_true1
 156                     [assumption
 157                     |apply (transitive_divides ? i)
 158                       [apply divides_b_true_to_divides.
 159                        assumption
 160                       |apply divides_b_true_to_divides.
 161                        assumption
 162                       ]
 163                     ]
 164                   |apply divides_to_divides_b_true
 165                     [apply (divides_b_true_to_lt_O i (i/j))
 166                       [apply (divides_b_true_to_lt_O ? ? ? H3).
 167                        assumption
 168                       |apply divides_to_divides_b_true1
 169                         [apply (divides_b_true_to_lt_O ? ? ? H3).
 170                          assumption
 171                         |apply (witness ? ? j).
 172                          apply sym_eq.
 173                          apply divides_to_div.
 174                          apply divides_b_true_to_divides.
 175                          assumption
 176                         ]
 177                       ]
 178                     |apply (witness ? ? (n/i)).
 179                      apply (inj_times_l1 j)
 180                       [apply (divides_b_true_to_lt_O ? ? ? H4).
 181                        apply (divides_b_true_to_lt_O ? ? ? H3).
 182                        assumption
 183                       |rewrite > divides_to_div
 184                         [rewrite > sym_times in \vdash (? ? ? (? % ?)).
 185                          rewrite > assoc_times.
 186                          rewrite > divides_to_div
 187                           [rewrite > divides_to_div
 188                             [reflexivity
 189                             |apply divides_b_true_to_divides.
 190                              assumption
 191                             ]
 192                           |apply divides_b_true_to_divides.
 193                            assumption
 194                           ]
 195                         |apply (transitive_divides ? i)
 196                           [apply divides_b_true_to_divides.
 197                            assumption
 198                           |apply divides_b_true_to_divides.
 199                            assumption
 200                           ]
 201                         ]
 202                       ]
 203                     ]
 204                   ]
 205                 |rewrite < sym_times.
 206                  apply divides_to_div.
 207                  apply divides_b_true_to_divides.
 208                  assumption
 209                 ]
 210               |reflexivity
 211               ]
 212             |assumption
 213             ]
 214           |apply (le_to_lt_to_lt ? i)
 215             [apply le_div.
 216              apply (divides_b_true_to_lt_O ? ? ? H4).
 217              apply (divides_b_true_to_lt_O ? ? ? H3).
 218              assumption
 219             |assumption
 220             ]
 221           ]
 222         ]
 223       |apply eq_sigma_p1
 224         [intros.reflexivity
 225         |intros.
 226          apply eq_sigma_p1
 227           [intros.reflexivity
 228           |intros.
 229            apply eq_f2
 230             [apply eq_f2
 231               [reflexivity
 232               |apply eq_f.
 233                rewrite > sym_times.
 234                rewrite > (plus_n_O (x1*x)).
 235                apply div_plus_times.
 236                apply (divides_b_true_to_lt_O ? ? ? H2).
 237                assumption
 238               ]
 239             |apply eq_f.
 240              cut (O < x)
 241               [cut (O < x1)
 242                 [apply (inj_times_l1 (x*x1))
 243                   [rewrite > (times_n_O O).
 244                    apply lt_times;assumption
 245                   |rewrite > divides_to_div
 246                     [rewrite > sym_times in \vdash (? ? ? (? ? %)).
 247                      rewrite < assoc_times.
 248                      rewrite > divides_to_div
 249                       [rewrite > divides_to_div
 250                         [reflexivity
 251                         |apply divides_b_true_to_divides.
 252                          assumption
 253                         ]
 254                       |apply divides_b_true_to_divides.
 255                        assumption
 256                       ]
 257                     |elim (divides_b_true_to_divides ? ? H4).
 258                      apply (witness ? ? n1).
 259                      rewrite > assoc_times.
 260                      rewrite < H5.
 261                      rewrite < sym_times.
 262                      apply sym_eq.
 263                      apply divides_to_div.
 264                      apply divides_b_true_to_divides.
 265                      assumption
 266                     ]
 267                   ]
 268                 |apply (divides_b_true_to_lt_O ? ? ? H4).
 269                  apply (lt_times_n_to_lt x)
 270                   [assumption
 271                   |simplify.
 272                    rewrite > divides_to_div
 273                     [assumption
 274                     |apply (divides_b_true_to_divides ? ? H2).
 275                      assumption
 276                     ]
 277                   ]
 278                 ]
 279               |apply (divides_b_true_to_lt_O ? ? ? H2).
 280                assumption
 281               ]
 282             ]
 283           ]
 284         ]
 285       ]
 286     |apply eq_sigma_p1
 287       [intros.reflexivity
 288       |intros.
 289        apply (trans_eq ? ?
 290        (sigma_p (S n) (\lambda d1:nat.divides_b d1 (n/x)) (\lambda d1:nat.f x*(g d1*h (n/x/d1)))))
 291         [apply eq_sigma_p
 292           [intros.reflexivity
 293           |intros.apply assoc_Ztimes
 294           ]
 295         |apply (trans_eq ? ?
 296           (sigma_p (S (n/x)) (\lambda d1:nat.divides_b d1 (n/x)) (\lambda d1:nat.f x*(g d1*h (n/x/d1)))))
 297           [apply false_to_eq_sigma_p
 298             [apply le_S_S.
 299              cut (O < x)
 300               [apply (le_times_to_le x)
 301                 [assumption
 302                 |rewrite > sym_times.
 303                  rewrite > divides_to_div
 304                   [apply le_times_n.
 305                    assumption
 306                   |apply divides_b_true_to_divides.
 307                    assumption
 308                   ]
 309                 ]
 310               |apply (divides_b_true_to_lt_O ? ? ? H2).
 311                assumption
 312               ]
 313             |intros.
 314              apply not_divides_to_divides_b_false
 315               [apply (trans_le ? ? ? ? H3).
 316                apply le_S_S.
 317                apply le_O_n
 318               |unfold Not.intro.
 319                apply (le_to_not_lt ? ? H3).
 320                apply le_S_S.
 321                apply divides_to_le
 322                 [apply (lt_times_n_to_lt x)
 323                   [apply (divides_b_true_to_lt_O ? ? ? H2).
 324                    assumption
 325                   |simplify.
 326                    rewrite > divides_to_div
 327                     [assumption
 328                     |apply (divides_b_true_to_divides ? ? H2).
 329                      assumption
 330                     ]
 331                   ]
 332                 |assumption
 333                 ]
 334               ]
 335             ]
 336           |apply sym_eq.
 337            apply Ztimes_sigma_pl
 338           ]
 339         ]
 340       ]
 341     ]
 342   ]
 343 qed.
 344
 345 definition is_one: nat \to Z \def
 346 \lambda n.
 347   match n with
 348   [O \Rightarrow OZ
 349   | (S p) \Rightarrow
 350     match p with
 351     [ O \Rightarrow pos O
 352     | (S q) \Rightarrow OZ]]
 353 .
 354
 355 theorem is_one_OZ: \forall n. n \neq S O \to is_one n = OZ.
 356 intro.apply (nat_case n)
 357   [intro.reflexivity
 358   |intro. apply (nat_case m)
 359     [intro.apply False_ind.apply H.reflexivity
 360     |intros.reflexivity
 361     ]
 362   ]
 363 qed.
 364
 365 theorem sigma_p_OZ:
 366 \forall p: nat \to bool.\forall n.sigma_p n p (\lambda m.OZ) = OZ.
 367 intros.elim n
 368   [reflexivity
 369   |apply (bool_elim ? (p n1));intro
 370     [rewrite > true_to_sigma_p_Sn
 371       [rewrite > sym_Zplus.
 372        rewrite > Zplus_z_OZ.
 373        assumption
 374       |assumption
 375       ]
 376     |rewrite > false_to_sigma_p_Sn
 377       [assumption
 378       |assumption
 379       ]
 380     ]
 381   ]
 382 qed.
 383
 384 theorem dirichlet_product_is_one_r:
 385 \forall f:nat\to Z.\forall n:nat.
 386   dirichlet_product f is_one n = f n.
 387 intros.
 388 elim n
 389   [unfold dirichlet_product.
 390    rewrite > true_to_sigma_p_Sn
 391     [rewrite > Ztimes_Zone_r.
 392      rewrite > Zplus_z_OZ.
 393      reflexivity
 394     |reflexivity
 395     ]
 396   |unfold dirichlet_product.
 397    rewrite > true_to_sigma_p_Sn
 398     [rewrite > div_n_n
 399       [rewrite > Ztimes_Zone_r.
 400        rewrite < Zplus_z_OZ in \vdash (? ? ? %).
 401        apply eq_f2
 402         [reflexivity
 403         |apply (trans_eq ? ? (sigma_p (S n1)
 404           (\lambda d:nat.divides_b d (S n1)) (\lambda d:nat.OZ)))
 405           [apply eq_sigma_p1;intros
 406             [reflexivity
 407             |rewrite > is_one_OZ
 408               [apply Ztimes_z_OZ
 409               |unfold Not.intro.
 410                apply (lt_to_not_le ? ? H1).
 411                rewrite > (times_n_SO x).
 412                rewrite > sym_times.
 413                rewrite < H3.
 414                rewrite > (div_mod ? x) in \vdash (? % ?)
 415                 [rewrite > divides_to_mod_O
 416                   [rewrite < plus_n_O.
 417                    apply le_n
 418                   |apply (divides_b_true_to_lt_O ? ? ? H2).
 419                    apply lt_O_S
 420                   |apply divides_b_true_to_divides.
 421                    assumption
 422                   ]
 423                 |apply (divides_b_true_to_lt_O ? ? ? H2).
 424                  apply lt_O_S
 425                 ]
 426               ]
 427             ]
 428           |apply sigma_p_OZ
 429           ]
 430         ]
 431       |apply lt_O_S
 432       ]
 433     |apply divides_to_divides_b_true
 434       [apply lt_O_S
 435       |apply divides_n_n
 436       ]
 437     ]
 438   ]
 439 qed.
 440
 441 theorem commutative_dirichlet_product: \forall f,g:nat \to Z.\forall n. O < n \to
 442 dirichlet_product f g n = dirichlet_product g f n.
 443 intros.
 444 unfold dirichlet_product.
 445 apply (trans_eq ? ?
 446   (sigma_p (S n) (\lambda d:nat.divides_b d n)
 447   (\lambda d:nat.g (n/d) * f (n/(n/d)))))
 448   [apply eq_sigma_p1;intros
 449     [reflexivity
 450     |rewrite > div_div
 451       [apply sym_Ztimes.
 452       |assumption
 453       |apply divides_b_true_to_divides.
 454        assumption
 455       ]
 456     ]
 457   |apply (eq_sigma_p_gh ? (\lambda d.(n/d)) (\lambda d.(n/d)))
 458     [intros.
 459      apply divides_b_div_true;assumption
 460     |intros.
 461      apply div_div
 462       [assumption
 463       |apply divides_b_true_to_divides.
 464        assumption
 465       ]
 466     |intros.
 467      apply le_S_S.
 468      apply le_div.
 469      apply (divides_b_true_to_lt_O ? ? H H2)
 470     |intros.
 471      apply divides_b_div_true;assumption
 472     |intros.
 473      apply div_div
 474       [assumption
 475       |apply divides_b_true_to_divides.
 476        assumption
 477       ]
 478     |intros.
 479      apply le_S_S.
 480      apply le_div.
 481      apply (divides_b_true_to_lt_O ? ? H H2)
 482     ]
 483   ]
 484 qed.
 485
 486 theorem dirichlet_product_is_one_l:
 487 \forall f:nat\to Z.\forall n:nat.
 488 O < n \to dirichlet_product is_one f n = f n.
 489 intros.
 490 rewrite > commutative_dirichlet_product.
 491 apply dirichlet_product_is_one_r.
 492 assumption.
 493 qed.
 494
 495 theorem dirichlet_product_one_r:
 496 \forall f:nat\to Z.\forall n:nat. O < n \to
 497 dirichlet_product f (\lambda n.Zone) n =
 498 sigma_p (S n) (\lambda d.divides_b d n) f.
 499 intros.
 500 unfold dirichlet_product.
 501 apply eq_sigma_p;intros
 502   [reflexivity
 503   |simplify in \vdash (? ? (? ? %) ?).
 504    apply Ztimes_Zone_r
 505   ]
 506 qed.
 507
 508 theorem dirichlet_product_one_l:
 509 \forall f:nat\to Z.\forall n:nat. O < n \to
 510 dirichlet_product (\lambda n.Zone) f n =
 511 sigma_p (S n) (\lambda d.divides_b d n) f.
 512 intros.
 513 rewrite > commutative_dirichlet_product
 514   [apply dirichlet_product_one_r.
 515    assumption
 516   |assumption
 517   ]
 518 qed.