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