helm/software/matita/library/nat/chebyshev.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/nat/chebishev".
  16
  17 include "nat/log.ma".
  18 include "nat/pi_p.ma".
  19 include "nat/factorization.ma".
  20 include "nat/factorial2.ma".
  21
  22 definition prim: nat \to nat \def
  23 \lambda n. sigma_p (S n) primeb (\lambda p.(S O)).
  24
  25 definition A: nat \to nat \def
  26 \lambda n. pi_p (S n) primeb (\lambda p.exp p (log p n)).
  27
  28 theorem le_Al1: \forall n.
  29 A n \le pi_p (S n) primeb (\lambda p.n).
  30 intro.unfold A.
  31 cases n
  32   [simplify.apply le_n
  33   |apply le_pi_p.
  34    intros.
  35    apply le_exp_log.
  36    apply lt_O_S
  37   ]
  38 qed.
  39
  40 theorem le_Al: \forall n.
  41 A n \le exp n (prim n).
  42 intro.unfold prim.
  43 rewrite < exp_sigma_p.
  44 apply le_Al1.
  45 qed.
  46
  47 theorem leA_r2: \forall n.
  48 exp n (prim n) \le A n * A n.
  49 intro.unfold prim.
  50 elim (le_to_or_lt_eq ? ? (le_O_n n))
  51   [rewrite < (exp_sigma_p (S n) n primeb).
  52    unfold A.
  53    rewrite < times_pi_p.
  54    apply le_pi_p.
  55    intros.
  56    rewrite < exp_plus_times.
  57    apply (trans_le ? (exp i (S(log i n))))
  58     [apply lt_to_le.
  59      apply lt_exp_log.
  60      apply prime_to_lt_SO.
  61      apply primeb_true_to_prime.
  62      assumption
  63     |apply le_exp
  64       [apply prime_to_lt_O.
  65        apply primeb_true_to_prime.
  66        assumption
  67       |rewrite > plus_n_O.
  68        simplify.
  69        rewrite > plus_n_Sm.
  70        apply le_plus_r.
  71        apply lt_O_log
  72         [assumption
  73         |apply le_S_S_to_le.
  74          apply H1
  75         ]
  76       ]
  77     ]
  78   |rewrite < H. apply le_n
  79   ]
  80 qed.
  81
  82 definition A': nat \to nat \def
  83 \lambda n. pi_p (S n) primeb
  84   (\lambda p.(pi_p (log p n) (\lambda i.true) (\lambda i.p))).
  85
  86 theorem eq_A_A': \forall n.A n = A' n.
  87 intro.unfold A.unfold A'.
  88 apply eq_pi_p
  89   [intros.reflexivity
  90   |intros.
  91    apply (trans_eq ? ? (exp x (sigma_p (log x n) (λi:nat.true) (λi:nat.(S O)))))
  92     [apply eq_f.apply sym_eq.apply sigma_p_true
  93     |apply sym_eq.apply exp_sigma_p
  94     ]
  95   ]
  96 qed.
  97
  98 theorem eq_pi_p_primeb_divides_b: \forall n,m.
  99 pi_p n (\lambda p.primeb p \land divides_b p m) (\lambda p.exp p (ord m p))
 100 = pi_p n primeb (\lambda p.exp p (ord m p)).
 101 intro.
 102 elim n
 103   [reflexivity
 104   |apply (bool_elim ? (primeb n1));intro
 105     [rewrite > true_to_pi_p_Sn in ⊢ (? ? ? %)
 106       [apply (bool_elim ? (divides_b n1 m));intro
 107         [rewrite > true_to_pi_p_Sn
 108           [apply eq_f.
 109            apply H
 110           |apply true_to_true_to_andb_true;assumption
 111           ]
 112         |rewrite > false_to_pi_p_Sn
 113           [rewrite > not_divides_to_ord_O
 114             [simplify in ⊢ (? ? ? (? % ?)).
 115              rewrite > sym_times.
 116              rewrite < times_n_SO.
 117              apply H
 118             |apply primeb_true_to_prime.assumption
 119             |apply divides_b_false_to_not_divides.
 120              assumption
 121             ]
 122           |rewrite > H1.rewrite > H2.reflexivity
 123           ]
 124         ]
 125       |assumption
 126       ]
 127     |rewrite > false_to_pi_p_Sn
 128       [rewrite > false_to_pi_p_Sn
 129         [apply H
 130         |assumption
 131         ]
 132       |rewrite > H1.reflexivity
 133       ]
 134     ]
 135   ]
 136 qed.
 137
 138 theorem lt_max_to_pi_p_primeb: \forall q,m. O < m \to max m (\lambda i.primeb i \land divides_b i m) < q \to
 139 m = pi_p q (\lambda i.primeb i \land divides_b i m) (\lambda p.exp p (ord m p)).
 140 intro.elim q
 141   [apply False_ind.
 142    apply (not_le_Sn_O ? H1)
 143   |apply (bool_elim ? (primeb n∧divides_b n m));intro
 144     [rewrite > true_to_pi_p_Sn
 145       [rewrite > (exp_ord n m) in ⊢ (? ? % ?)
 146         [apply eq_f.
 147          rewrite > (H (ord_rem m n))
 148           [apply eq_pi_p1
 149             [intros.
 150              apply (bool_elim ? (primeb x));intro
 151               [simplify.
 152                apply (bool_elim ? (divides_b x (ord_rem m n)));intro
 153                 [apply sym_eq.
 154                  apply divides_to_divides_b_true
 155                   [apply prime_to_lt_O.
 156                    apply primeb_true_to_prime.
 157                    assumption
 158                   |apply (trans_divides ? (ord_rem m n))
 159                     [apply divides_b_true_to_divides.
 160                      assumption
 161                     |apply divides_ord_rem
 162                       [apply (trans_lt ? x)
 163                         [apply prime_to_lt_SO.
 164                          apply primeb_true_to_prime.
 165                          assumption
 166                         |assumption
 167                         ]
 168                       |assumption
 169                       ]
 170                     ]
 171                   ]
 172                 |apply sym_eq.
 173                  apply not_divides_to_divides_b_false
 174                   [apply prime_to_lt_O.
 175                    apply primeb_true_to_prime.
 176                    assumption
 177                   |apply ord_O_to_not_divides
 178                     [assumption
 179                     |apply primeb_true_to_prime.
 180                      assumption
 181                     |rewrite < (ord_ord_rem n)
 182                       [apply not_divides_to_ord_O
 183                         [apply primeb_true_to_prime.
 184                          assumption
 185                         |apply divides_b_false_to_not_divides.
 186                          assumption
 187                         ]
 188                       |assumption
 189                       |apply primeb_true_to_prime.
 190                        apply (andb_true_true ? ? H3)
 191                       |apply primeb_true_to_prime.
 192                        assumption
 193                       |assumption
 194                       ]
 195                     ]
 196                   ]
 197                 ]
 198               |reflexivity
 199               ]
 200             |intros.
 201              apply eq_f.
 202              apply ord_ord_rem
 203               [assumption
 204               |apply primeb_true_to_prime.
 205                apply (andb_true_true ? ? H3)
 206               |apply primeb_true_to_prime.
 207                apply (andb_true_true ? ? H5)
 208               |assumption
 209               ]
 210             ]
 211           |apply lt_O_ord_rem
 212             [apply prime_to_lt_SO.
 213              apply primeb_true_to_prime.
 214              apply (andb_true_true ? ? H3)
 215             |assumption
 216             ]
 217           |apply not_eq_to_le_to_lt
 218             [elim (exists_max_forall_false (λi:nat.primeb i∧divides_b i (ord_rem m n)) (ord_rem m n))
 219               [elim H4.
 220                intro.rewrite > H7 in H6.simplify in H6.
 221                apply (not_divides_ord_rem m n)
 222                 [assumption
 223                 |apply prime_to_lt_SO.
 224                  apply primeb_true_to_prime.
 225                  apply (andb_true_true ? ? H3)
 226                 |apply divides_b_true_to_divides.
 227                  apply (andb_true_true_r ? ? H6)
 228                 ]
 229               |elim H4.rewrite > H6.
 230                apply lt_to_not_eq.
 231                apply prime_to_lt_O.
 232                apply primeb_true_to_prime.
 233                apply (andb_true_true ? ? H3)
 234               ]
 235             |apply (trans_le ? (max m (λi:nat.primeb i∧divides_b i (ord_rem m n))))
 236               [apply le_to_le_max.
 237                apply divides_to_le
 238                 [assumption
 239                 |apply divides_ord_rem
 240                   [apply prime_to_lt_SO.
 241                    apply primeb_true_to_prime.
 242                    apply (andb_true_true ? ? H3)
 243                   |assumption
 244                   ]
 245                 ]
 246               |apply (trans_le ? (max m (λi:nat.primeb i∧divides_b i m)))
 247                 [apply le_max_f_max_g.
 248                  intros.
 249                  apply (bool_elim ? (primeb i));intro
 250                   [simplify.
 251                    apply divides_to_divides_b_true
 252                     [apply prime_to_lt_O.
 253                      apply primeb_true_to_prime.
 254                      assumption
 255                     |apply (trans_divides ? (ord_rem m n))
 256                       [apply divides_b_true_to_divides.
 257                        apply (andb_true_true_r ? ? H5)
 258                       |apply divides_ord_rem
 259                         [apply prime_to_lt_SO.
 260                          apply primeb_true_to_prime.
 261                          apply (andb_true_true ? ? H3)
 262                         |assumption
 263                         ]
 264                       ]
 265                     ]
 266                   |rewrite > H6 in H5.
 267                    assumption
 268                   ]
 269                 |apply le_S_S_to_le.
 270                  assumption
 271                 ]
 272               ]
 273             ]
 274           ]
 275         |apply prime_to_lt_SO.
 276          apply primeb_true_to_prime.
 277          apply (andb_true_true ? ? H3)
 278         |assumption
 279         ]
 280       |assumption
 281       ]
 282     |elim (le_to_or_lt_eq ? ? H1)
 283       [rewrite > false_to_pi_p_Sn
 284         [apply H
 285           [assumption
 286           |apply false_to_lt_max
 287             [apply (lt_to_le_to_lt ? (max m (λi:nat.primeb i∧divides_b i m)))
 288               [apply lt_to_le.
 289                apply lt_SO_max_prime.
 290                assumption
 291               |apply le_S_S_to_le.
 292                assumption
 293               ]
 294             |assumption
 295             |apply le_S_S_to_le.
 296              assumption
 297             ]
 298           ]
 299         |assumption
 300         ]
 301       |rewrite < H4.
 302        rewrite < (pi_p_false (λp:nat.p\sup(ord (S O) p)) (S n) ) in ⊢ (? ? % ?).
 303        apply eq_pi_p
 304         [intros.
 305          apply (bool_elim ? (primeb x));intro
 306           [apply sym_eq.
 307            change with (divides_b x (S O) =false).
 308            apply not_divides_to_divides_b_false
 309             [apply prime_to_lt_O.
 310              apply primeb_true_to_prime.
 311              assumption
 312             |intro.
 313              apply (le_to_not_lt x (S O))
 314               [apply divides_to_le
 315                 [apply lt_O_S.assumption
 316                 |assumption
 317                 ]
 318               |elim (primeb_true_to_prime ? H6).
 319                assumption
 320               ]
 321             ]
 322           |reflexivity
 323           ]
 324         |intros.reflexivity
 325         ]
 326       ]
 327     ]
 328   ]
 329 qed.
 330
 331 theorem pi_p_primeb_divides_b: \forall n. O < n \to
 332 n = pi_p (S n) (\lambda i.primeb i \land divides_b i n) (\lambda p.exp p (ord n p)).
 333 intros.
 334 apply lt_max_to_pi_p_primeb
 335   [assumption
 336   |apply le_S_S.
 337    apply le_max_n
 338   ]
 339 qed.
 340
 341 theorem pi_p_primeb: \forall n. O < n \to
 342 n = pi_p (S n) primeb (\lambda p.exp p (ord n p)).
 343 intros.
 344 rewrite < eq_pi_p_primeb_divides_b.
 345 apply pi_p_primeb_divides_b.
 346 assumption.
 347 qed.
 348
 349 theorem le_ord_log: \forall n,p. O < n \to S O < p \to
 350 ord n p \le log p n.
 351 intros.
 352 rewrite > (exp_ord p) in ⊢ (? ? (? ? %))
 353   [rewrite > log_exp
 354     [apply le_plus_n_r
 355     |assumption
 356     |apply lt_O_ord_rem;assumption
 357     ]
 358   |assumption
 359   |assumption
 360   ]
 361 qed.
 362
 363 theorem sigma_p_divides_b:
 364 \forall m,n,p. O < n \to prime p \to \lnot divides p n \to
 365 m = sigma_p m (λi:nat.divides_b (p\sup (S i)) ((exp p m)*n)) (λx:nat.S O).
 366 intro.elim m
 367   [reflexivity
 368   |simplify in ⊢ (? ? ? (? % ? ?)).
 369    rewrite > true_to_sigma_p_Sn
 370     [rewrite > sym_plus.rewrite < plus_n_SO.
 371      apply eq_f.
 372      rewrite > (H n1 p H1 H2 H3) in ⊢ (? ? % ?).
 373      apply eq_sigma_p1
 374       [intros.
 375        apply (bool_elim ? (divides_b (p\sup(S x)) (p\sup n*n1)));intro
 376         [apply sym_eq.
 377          apply divides_to_divides_b_true
 378           [apply lt_O_exp.
 379            apply prime_to_lt_O.
 380            assumption
 381           |apply (witness ? ? ((exp p (n - x))*n1)).
 382            rewrite < assoc_times.
 383            rewrite < exp_plus_times.
 384            apply eq_f2
 385             [apply eq_f.simplify.
 386              apply eq_f.
 387              rewrite > sym_plus.
 388              apply plus_minus_m_m.
 389              apply lt_to_le.assumption
 390             |reflexivity
 391             ]
 392           ]
 393         |apply sym_eq.
 394          apply False_ind.
 395          apply (divides_b_false_to_not_divides ? ? H5).
 396          apply (witness ? ? ((exp p (n - S x))*n1)).
 397          rewrite < assoc_times.
 398          rewrite < exp_plus_times.
 399          apply eq_f2
 400           [apply eq_f.
 401            rewrite > sym_plus.
 402            apply plus_minus_m_m.
 403            assumption
 404           |reflexivity
 405           ]
 406         ]
 407       |intros.reflexivity
 408       ]
 409     |apply divides_to_divides_b_true
 410       [apply lt_O_exp.
 411        apply prime_to_lt_O.assumption
 412       |apply (witness ? ? n1).reflexivity
 413       ]
 414     ]
 415   ]
 416 qed.
 417
 418 theorem sigma_p_divides_b1:
 419 \forall m,n,p,k. O < n \to prime p \to \lnot divides p n \to m \le k \to
 420 m = sigma_p k (λi:nat.divides_b (p\sup (S i)) ((exp p m)*n)) (λx:nat.S O).
 421 intros.
 422 lapply (prime_to_lt_SO ? H1) as H4.
 423 lapply (prime_to_lt_O ? H1) as H5.
 424 rewrite > (false_to_eq_sigma_p m k)
 425   [apply sigma_p_divides_b;assumption
 426   |assumption
 427   |intros.
 428    apply not_divides_to_divides_b_false
 429     [apply lt_O_exp.assumption
 430     |intro.apply (le_to_not_lt ? ? H6).
 431      unfold lt.
 432      rewrite < (ord_exp p)
 433       [rewrite > (plus_n_O m).
 434        rewrite < (not_divides_to_ord_O ? ? H1 H2).
 435        rewrite < (ord_exp p ? H4) in ⊢ (? ? (? % ?)).
 436        rewrite < ord_times
 437         [apply divides_to_le_ord
 438           [apply lt_O_exp.assumption
 439           |rewrite > (times_n_O O).
 440            apply lt_times
 441             [apply lt_O_exp.assumption
 442             |assumption
 443             ]
 444           |assumption
 445           |assumption
 446           ]
 447         |apply lt_O_exp.assumption
 448         |assumption
 449         |assumption
 450         ]
 451       |assumption
 452       ]
 453     ]
 454   ]
 455 qed.
 456
 457 theorem eq_ord_sigma_p:
 458 \forall n,m,x. O < n \to prime x \to
 459 exp x m \le n \to n < exp x (S m) \to
 460 ord n x=sigma_p m (λi:nat.divides_b (x\sup (S i)) n) (λx:nat.S O).
 461 intros.
 462 lapply (prime_to_lt_SO ? H1).
 463 rewrite > (exp_ord x n) in ⊢ (? ? ? (? ? (λi:?.? ? %) ?))
 464   [apply sigma_p_divides_b1
 465     [apply lt_O_ord_rem;assumption
 466     |assumption
 467     |apply not_divides_ord_rem;assumption
 468     |apply lt_S_to_le.
 469      apply (le_to_lt_to_lt ? (log x n))
 470       [apply le_ord_log;assumption
 471       |apply (lt_exp_to_lt x)
 472         [assumption
 473         |apply (le_to_lt_to_lt ? n ? ? H3).
 474          apply le_exp_log.
 475          assumption
 476         ]
 477       ]
 478     ]
 479   |assumption
 480   |assumption
 481   ]
 482 qed.
 483
 484 theorem pi_p_primeb1: \forall n. O < n \to
 485 n = pi_p (S n) primeb
 486   (\lambda p.(pi_p (log p n)
 487     (\lambda i.divides_b (exp p (S i)) n) (\lambda i.p))).
 488 intros.
 489 rewrite > (pi_p_primeb n H) in ⊢ (? ? % ?).
 490 apply eq_pi_p1
 491   [intros.reflexivity
 492   |intros.
 493    rewrite > exp_sigma_p.
 494    apply eq_f.
 495    apply eq_ord_sigma_p
 496     [assumption
 497     |apply primeb_true_to_prime.
 498      assumption
 499     |apply le_exp_log.assumption
 500     |apply lt_exp_log.
 501      apply prime_to_lt_SO.
 502      apply primeb_true_to_prime.
 503      assumption
 504     ]
 505   ]
 506 qed.
 507
 508 theorem eq_fact_pi_p:\forall n. fact n =
 509 pi_p (S n) (\lambda i.leb (S O) i) (\lambda i.i).
 510 intro.elim n
 511   [reflexivity
 512   |change with ((S n1)*n1! = pi_p (S (S n1)) (λi:nat.leb (S O) i) (λi:nat.i)).
 513    rewrite > true_to_pi_p_Sn
 514     [apply eq_f.assumption
 515     |reflexivity
 516     ]
 517   ]
 518 qed.
 519
 520 theorem eq_sigma_p_div: \forall n,q.O < q \to
 521 sigma_p (S n) (λm:nat.leb (S O) m∧divides_b q m) (λx:nat.S O)
 522 =n/q.
 523 intros.
 524 apply (div_mod_spec_to_eq n q ? (n \mod q) ? (n \mod q))
 525   [apply div_mod_spec_intro
 526     [apply lt_mod_m_m.assumption
 527     |elim n
 528       [simplify.elim q;reflexivity
 529       |elim (or_div_mod1 n1 q)
 530         [elim H2.clear H2.
 531          rewrite > divides_to_mod_O
 532           [rewrite < plus_n_O.
 533            rewrite > true_to_sigma_p_Sn
 534             [rewrite > H4 in ⊢ (? ? % ?).
 535              apply eq_f2
 536               [rewrite < sym_plus.
 537                rewrite < plus_n_SO.
 538                apply eq_f.
 539                apply (div_mod_spec_to_eq n1 q (div n1 q) (mod n1 q) ? (mod n1 q))
 540                 [apply div_mod_spec_div_mod.
 541                  assumption
 542                 |apply div_mod_spec_intro
 543                   [apply lt_mod_m_m.assumption
 544                   |assumption
 545                   ]
 546                 ]
 547               |reflexivity
 548               ]
 549             |apply true_to_true_to_andb_true
 550               [reflexivity
 551               |apply divides_to_divides_b_true;assumption
 552               ]
 553             ]
 554           |assumption
 555           |assumption
 556           ]
 557         |elim H2.clear H2.
 558          rewrite > false_to_sigma_p_Sn
 559           [rewrite > mod_S
 560             [rewrite < plus_n_Sm.
 561              apply eq_f.
 562              assumption
 563             |assumption
 564             |elim (le_to_or_lt_eq (S (mod n1 q)) q)
 565               [assumption
 566               |apply False_ind.
 567                apply H3.
 568                apply (witness ? ? (S(div n1 q))).
 569                rewrite < times_n_Sm.
 570                rewrite < sym_plus.
 571                rewrite < H2 in ⊢ (? ? ? (? ? %)).
 572                rewrite > sym_times.
 573                assumption
 574               |apply lt_mod_m_m.
 575                assumption
 576               ]
 577             ]
 578           |rewrite > not_divides_to_divides_b_false
 579             [rewrite < andb_sym in ⊢ (? ? % ?).reflexivity
 580             |assumption
 581             |assumption
 582             ]
 583           ]
 584         |assumption
 585         ]
 586       ]
 587     ]
 588   |apply div_mod_spec_div_mod.
 589    assumption
 590   ]
 591 qed.
 592
 593 theorem fact_pi_p: \forall n. fact n =
 594 pi_p (S n) primeb
 595   (\lambda p.(pi_p (log p n)
 596     (\lambda i.true) (\lambda i.(exp p (n /(exp p (S i))))))).
 597 intros.
 598 rewrite > eq_fact_pi_p.
 599 apply (trans_eq ? ?
 600   (pi_p (S n) (λi:nat.leb (S O) i)
 601    (λn.pi_p (S n) primeb
 602     (\lambda p.(pi_p (log p n)
 603      (\lambda i.divides_b (exp p (S i)) n) (\lambda i.p))))))
 604   [apply eq_pi_p1;intros
 605     [reflexivity
 606     |apply pi_p_primeb1.
 607      apply leb_true_to_le.assumption
 608     ]
 609   |apply (trans_eq ? ?
 610     (pi_p (S n) (λi:nat.leb (S O) i)
 611      (λn:nat
 612       .pi_p (S n) (\lambda p.primeb p\land leb p n)
 613        (λp:nat.pi_p (log p n) (λi:nat.divides_b ((p)\sup(S i)) n) (λi:nat.p)))))
 614     [apply eq_pi_p1
 615       [intros.reflexivity
 616       |intros.apply eq_pi_p1
 617         [intros.elim (primeb x1)
 618           [simplify.apply sym_eq.
 619            apply le_to_leb_true.
 620            apply le_S_S_to_le.
 621            assumption
 622           |reflexivity
 623           ]
 624         |intros.reflexivity
 625         ]
 626       ]
 627     |apply (trans_eq ? ?
 628       (pi_p (S n) (λi:nat.leb (S O) i)
 629        (λm:nat
 630         .pi_p (S n) (λp:nat.primeb p∧leb p m)
 631          (λp:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p)))))
 632       [apply eq_pi_p1
 633         [intros.reflexivity
 634         |intros.
 635          apply sym_eq.
 636          apply false_to_eq_pi_p
 637           [assumption
 638           |intros.rewrite > lt_to_leb_false
 639             [elim primeb;reflexivity|assumption]
 640           ]
 641         ]
 642       |(* make a general theorem *)
 643        apply (trans_eq ? ?
 644         (pi_p (S n) primeb
 645          (λp:nat
 646           .pi_p (S n) (λm.leb p m)
 647            (λm:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p)))
 648         ))
 649         [apply pi_p_pi_p1.
 650          intros.
 651          apply (bool_elim ? (primeb y \land leb y x));intros
 652           [rewrite > (le_to_leb_true (S O) x)
 653             [reflexivity
 654             |apply (trans_le ? y)
 655               [apply prime_to_lt_O.
 656                apply primeb_true_to_prime.
 657                apply (andb_true_true ? ? H2)
 658               |apply leb_true_to_le.
 659                apply (andb_true_true_r ? ? H2)
 660               ]
 661             ]
 662           |elim (leb (S O) x);reflexivity
 663           ]
 664         |apply eq_pi_p1
 665           [intros.reflexivity
 666           |intros.
 667            apply (trans_eq ? ?
 668             (pi_p (S n) (λm:nat.leb x m)
 669              (λm:nat.pi_p (log x n) (λi:nat.divides_b (x\sup(S i)) m) (λi:nat.x))))
 670             [apply eq_pi_p1
 671               [intros.reflexivity
 672               |intros.
 673                apply sym_eq.
 674                apply false_to_eq_pi_p
 675                 [apply le_log
 676                   [apply prime_to_lt_SO.
 677                    apply primeb_true_to_prime.
 678                    assumption
 679                   |apply (lt_to_le_to_lt ? x)
 680                     [apply prime_to_lt_O.
 681                      apply primeb_true_to_prime.
 682                      assumption
 683                     |apply leb_true_to_le.
 684                      assumption
 685                     ]
 686                   |apply le_S_S_to_le.
 687                    assumption
 688                   ]
 689                 |intros.
 690                  apply not_divides_to_divides_b_false
 691                   [apply lt_O_exp.
 692                    apply prime_to_lt_O.
 693                    apply primeb_true_to_prime.
 694                    assumption
 695                   |intro.
 696                    apply (lt_to_not_le x1 (exp x (S i)))
 697                     [apply (lt_to_le_to_lt ? (exp x (S(log x x1))))
 698                       [apply lt_exp_log.
 699                        apply prime_to_lt_SO.
 700                        apply primeb_true_to_prime.
 701                        assumption
 702                       |apply le_exp
 703                         [apply prime_to_lt_O.
 704                          apply primeb_true_to_prime.
 705                          assumption
 706                         |apply le_S_S.
 707                          assumption
 708                         ]
 709                       ]
 710                     |apply divides_to_le
 711                       [apply (lt_to_le_to_lt ? x)
 712                         [apply prime_to_lt_O.
 713                          apply primeb_true_to_prime.
 714                          assumption
 715                         |apply leb_true_to_le.
 716                          assumption
 717                         ]
 718                       |assumption
 719                       ]
 720                     ]
 721                   ]
 722                 ]
 723               ]
 724             |apply
 725              (trans_eq ? ?
 726               (pi_p (log x n) (λi:nat.true)
 727                (λi:nat.pi_p (S n) (λm:nat.leb x m \land divides_b (x\sup(S i)) m) (λm:nat.x))))
 728               [apply (pi_p_pi_p1 (\lambda m,i.x)).
 729                intros.
 730                reflexivity
 731               |apply eq_pi_p1
 732                 [intros.reflexivity
 733                 |intros.
 734                  rewrite > exp_sigma_p.
 735                  apply eq_f.
 736                  apply (trans_eq ? ?
 737                   (sigma_p (S n) (λm:nat.leb (S O) m∧divides_b (x\sup(S x1)) m) (λx:nat.S O)))
 738                   [apply eq_sigma_p1
 739                     [intros.
 740                      apply (bool_elim ? (divides_b (x\sup(S x1)) x2));intro
 741                       [apply (bool_elim ? (leb x x2));intro
 742                         [rewrite > le_to_leb_true
 743                           [reflexivity
 744                           |apply (trans_le ? x)
 745                             [apply prime_to_lt_O.
 746                              apply primeb_true_to_prime.
 747                              assumption
 748                             |apply leb_true_to_le.
 749                              assumption
 750                             ]
 751                           ]
 752                         |rewrite > lt_to_leb_false
 753                           [reflexivity
 754                           |apply not_le_to_lt.intro.
 755                            apply (leb_false_to_not_le ? ? H6).
 756                            apply (trans_le ? (exp x (S x1)))
 757                             [rewrite > times_n_SO in ⊢ (? % ?).
 758                              change with (exp x (S O) \le exp x (S x1)).
 759                              apply le_exp
 760                               [apply prime_to_lt_O.
 761                                apply primeb_true_to_prime.
 762                                assumption
 763                               |apply le_S_S.apply le_O_n.
 764                               ]
 765                             |apply divides_to_le
 766                               [assumption
 767                               |apply divides_b_true_to_divides.
 768                                assumption
 769                               ]
 770                             ]
 771                           ]
 772                         ]
 773                       |rewrite < andb_sym.
 774                        rewrite < andb_sym in ⊢ (? ? ? %).
 775                        reflexivity
 776                       ]
 777                     |intros.reflexivity
 778                     ]
 779                   |apply eq_sigma_p_div.
 780                    apply lt_O_exp.
 781                    apply prime_to_lt_O.
 782                    apply primeb_true_to_prime.
 783                    assumption
 784                   ]
 785                 ]
 786               ]
 787             ]
 788           ]
 789         ]
 790       ]
 791     ]
 792   ]
 793 qed.
 794
 795 (* odd n is just mod n (S(S O))
 796 let rec odd n \def
 797   match n with
 798   [ O \Rightarrow O
 799   | S m \Rightarrow (S O) - odd m
 800   ].
 801
 802 theorem le_odd_SO: \forall n. odd n \le S O.
 803 intro.elim n
 804   [apply le_O_n
 805   |simplify.cases (odd n1)
 806     [simplify.apply le_n.
 807     |apply le_O_n
 808     ]
 809   ]
 810 qed.
 811
 812 theorem SSO_odd: \forall n. n = (n/(S(S O)))*(S(S O)) + odd n.
 813 intro.elim n
 814   [apply (lt_O_n_elim ? H).
 815    intro.simplify.reflexivity
 816   |
 817 *)
 818
 819 theorem fact_pi_p2: \forall n. fact ((S(S O))*n) =
 820 pi_p (S ((S(S O))*n)) primeb
 821   (\lambda p.(pi_p (log p ((S(S O))*n))
 822     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))*(exp p (mod ((S(S O))*n /(exp p (S i))) (S(S O)))))))).
 823 intros.rewrite > fact_pi_p.
 824 apply eq_pi_p1
 825   [intros.reflexivity
 826   |intros.apply eq_pi_p
 827     [intros.reflexivity
 828     |intros.
 829      rewrite < exp_plus_times.
 830      apply eq_f.
 831      rewrite > sym_times in ⊢ (? ? ? (? % ?)).
 832      apply SSO_mod.
 833      apply lt_O_exp.
 834      apply prime_to_lt_O.
 835      apply primeb_true_to_prime.
 836      assumption
 837     ]
 838   ]
 839 qed.
 840
 841 theorem fact_pi_p3: \forall n. fact ((S(S O))*n) =
 842 pi_p (S ((S(S O))*n)) primeb
 843   (\lambda p.(pi_p (log p ((S(S O))*n))
 844     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))*
 845 pi_p (S ((S(S O))*n)) primeb
 846   (\lambda p.(pi_p (log p ((S(S O))*n))
 847     (\lambda i.true) (\lambda i.(exp p (mod ((S(S O))*n /(exp p (S i))) (S(S O))))))).
 848 intros.
 849 rewrite < times_pi_p.
 850 rewrite > fact_pi_p2.
 851 apply eq_pi_p;intros
 852   [reflexivity
 853   |apply times_pi_p
 854   ]
 855 qed.
 856
 857 theorem pi_p_primeb4: \forall n. S O < n \to
 858 pi_p (S ((S(S O))*n)) primeb
 859   (\lambda p.(pi_p (log p ((S(S O))*n))
 860     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))
 861 =
 862 pi_p (S n) primeb
 863   (\lambda p.(pi_p (log p (S(S O)*n))
 864     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
 865 intros.
 866 apply or_false_eq_SO_to_eq_pi_p
 867   [apply le_S_S.
 868    apply le_times_n.
 869    apply lt_O_S
 870   |intros.
 871    right.
 872    rewrite > log_i_SSOn
 873     [change with (i\sup((S(S O))*(n/i\sup(S O)))*(S O) = S O).
 874      rewrite < times_n_SO.
 875      rewrite > eq_div_O
 876       [reflexivity
 877       |simplify.rewrite < times_n_SO.assumption
 878       ]
 879     |assumption
 880     |assumption
 881     |apply le_S_S_to_le.assumption
 882     ]
 883   ]
 884 qed.
 885
 886 theorem pi_p_primeb5: \forall n. S O < n \to
 887 pi_p (S ((S(S O))*n)) primeb
 888   (\lambda p.(pi_p (log p ((S(S O))*n))
 889     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))
 890 =
 891 pi_p (S n) primeb
 892   (\lambda p.(pi_p (log p n)
 893     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
 894 intros.
 895 rewrite > (pi_p_primeb4 ? H).
 896 apply eq_pi_p1;intros
 897   [reflexivity
 898   |apply or_false_eq_SO_to_eq_pi_p
 899     [apply le_log
 900       [apply prime_to_lt_SO.
 901        apply primeb_true_to_prime.
 902        assumption
 903       |apply lt_to_le.assumption
 904       |apply le_times_n.
 905        apply lt_O_S
 906       ]
 907     |intros.right.
 908      rewrite > eq_div_O
 909       [simplify.reflexivity
 910       |apply (lt_to_le_to_lt ? (exp x (S(log x n))))
 911         [apply lt_exp_log.
 912          apply prime_to_lt_SO.
 913          apply primeb_true_to_prime.
 914          assumption
 915         |apply le_exp
 916           [apply prime_to_lt_O.
 917            apply primeb_true_to_prime.
 918            assumption
 919           |apply le_S_S.
 920            assumption
 921           ]
 922         ]
 923       ]
 924     ]
 925   ]
 926 qed.
 927
 928 theorem exp_fact_SSO: \forall n.
 929 exp (fact n) (S(S O))
 930 =
 931 pi_p (S n) primeb
 932   (\lambda p.(pi_p (log p n)
 933     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
 934 intros.
 935 rewrite > fact_pi_p.
 936 rewrite < exp_pi_p.
 937 apply eq_pi_p;intros
 938   [reflexivity
 939   |apply sym_eq.
 940    apply exp_times_pi_p
 941   ]
 942 qed.
 943
 944 definition B \def
 945 \lambda n.
 946 pi_p (S n) primeb
 947   (\lambda p.(pi_p (log p n)
 948     (\lambda i.true) (\lambda i.(exp p (mod (n /(exp p (S i))) (S(S O))))))).
 949
 950 theorem eq_fact_B:\forall n.S O < n \to
 951 fact ((S(S O))*n) = exp (fact n) (S(S O)) * B((S(S O))*n).
 952 intros. unfold B.
 953 rewrite > fact_pi_p3.
 954 apply eq_f2
 955   [apply sym_eq.
 956    rewrite > pi_p_primeb5
 957     [apply exp_fact_SSO
 958     |assumption
 959     ]
 960   |reflexivity
 961   ]
 962 qed.
 963
 964 theorem le_B_A: \forall n. B n \le A n.
 965 intro.unfold B.
 966 rewrite > eq_A_A'.
 967 unfold A'.
 968 apply le_pi_p.intros.
 969 apply le_pi_p.intros.
 970 rewrite > exp_n_SO in ⊢ (? ? %).
 971 apply le_exp
 972   [apply prime_to_lt_O.
 973    apply primeb_true_to_prime.
 974    assumption
 975   |apply le_S_S_to_le.
 976    apply lt_mod_m_m.
 977    apply lt_O_S
 978   ]
 979 qed.
 980
 981 theorem le_fact_A:\forall n.S O < n \to
 982 fact ((S(S O))*n) \le exp (fact n) (S(S O)) * A ((S(S O))*n).
 983 intros.
 984 rewrite > eq_fact_B
 985   [apply le_times_r.
 986    apply le_B_A
 987   |assumption
 988   ]
 989 qed.
 990
 991 theorem lt_SO_to_le_B_exp: \forall n.S O < n \to
 992 B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
 993 intros.
 994 apply (le_times_to_le (exp (fact n) (S(S O))))
 995   [apply lt_O_exp.
 996    apply lt_O_fact
 997   |rewrite < eq_fact_B
 998     [rewrite < sym_times in ⊢ (? ? %).
 999      rewrite > exp_SSO.
1000      rewrite < assoc_times.
1001      apply fact1
1002     |assumption
1003     ]
1004   ]
1005 qed.
1006
1007 theorem le_B_exp: \forall n.
1008 B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
1009 intro.cases n
1010   [apply le_n
1011   |cases n1
1012     [simplify.apply le_S.apply le_S.apply le_n
1013     |apply lt_SO_to_le_B_exp.
1014      apply le_S_S.apply lt_O_S.
1015     ]
1016   ]
1017 qed.
1018
1019 theorem eq_A_SSO_n: \forall n.O < n \to
1020 A((S(S O))*n) =
1021  pi_p (S ((S(S O))*n)) primeb
1022   (\lambda p.(pi_p (log p ((S(S O))*n) )
1023     (\lambda i.true) (\lambda i.(exp p (bool_to_nat (leb (S n) (exp p (S i))))))))
1024  *A n.
1025 intro.
1026 rewrite > eq_A_A'.rewrite > eq_A_A'.
1027 unfold A'.intros.
1028 cut (
1029  pi_p (S n) primeb (λp:nat.pi_p (log p n) (λi:nat.true) (λi:nat.p))
1030  = pi_p (S ((S(S O))*n)) primeb
1031     (λp:nat.pi_p (log p ((S(S O))*n)) (λi:nat.true) (λi:nat.(p)\sup(bool_to_nat (\lnot (leb (S n) (exp p (S i))))))))
1032   [rewrite > Hcut.
1033    rewrite < times_pi_p.
1034    apply eq_pi_p1;intros
1035     [reflexivity
1036     |rewrite < times_pi_p.
1037      apply eq_pi_p;intros
1038       [reflexivity
1039       |apply (bool_elim ? (leb (S n) (exp x (S x1))));intro
1040         [simplify.rewrite < times_n_SO.apply times_n_SO
1041         |simplify.rewrite < plus_n_O.apply times_n_SO
1042         ]
1043       ]
1044     ]
1045   |apply (trans_eq ? ? (pi_p (S n) primeb
1046     (\lambda p:nat.pi_p (log p n) (\lambda i:nat.true) (\lambda i:nat.(p)\sup(bool_to_nat (¬leb (S n) (exp p (S i))))))))
1047     [apply eq_pi_p1;intros
1048       [reflexivity
1049       |apply eq_pi_p1;intros
1050         [reflexivity
1051         |rewrite > lt_to_leb_false
1052           [simplify.apply times_n_SO
1053           |apply le_S_S.
1054            apply (trans_le ? (exp x (log x n)))
1055             [apply le_exp
1056               [apply prime_to_lt_O.
1057                apply primeb_true_to_prime.
1058                assumption
1059               |assumption
1060               ]
1061             |apply le_exp_log.
1062              assumption
1063             ]
1064           ]
1065         ]
1066       ]
1067     |apply (trans_eq ? ?
1068       (pi_p (S ((S(S O))*n)) primeb
1069        (λp:nat.pi_p (log p n) (λi:nat.true)
1070         (λi:nat.(p)\sup(bool_to_nat (¬leb (S n) ((p)\sup(S i))))))))
1071       [apply sym_eq.
1072        apply or_false_eq_SO_to_eq_pi_p
1073         [apply le_S_S.
1074          simplify.
1075          apply le_plus_n_r
1076         |intros.right.
1077          rewrite > lt_to_log_O
1078           [reflexivity
1079           |assumption
1080           |assumption
1081           ]
1082         ]
1083       |apply eq_pi_p1;intros
1084         [reflexivity
1085         |apply sym_eq.
1086          apply or_false_eq_SO_to_eq_pi_p
1087           [apply le_log
1088             [apply prime_to_lt_SO.
1089              apply primeb_true_to_prime.
1090              assumption
1091             |assumption
1092             |simplify.
1093              apply le_plus_n_r
1094             ]
1095           |intros.right.
1096            rewrite > le_to_leb_true
1097             [simplify.reflexivity
1098             |apply (lt_to_le_to_lt ? (exp x (S (log x n))))
1099               [apply lt_exp_log.
1100                apply prime_to_lt_SO.
1101                apply primeb_true_to_prime.
1102                assumption
1103               |apply le_exp
1104                 [apply prime_to_lt_O.
1105                  apply primeb_true_to_prime.
1106                  assumption
1107                 |apply le_S_S.assumption
1108                 ]
1109               ]
1110             ]
1111           ]
1112         ]
1113       ]
1114     ]
1115   ]
1116 qed.
1117
1118 theorem le_A_BA1: \forall n. O < n \to
1119 A((S(S O))*n) \le B((S(S O))*n)*A n.
1120 intros.
1121 rewrite > eq_A_SSO_n
1122   [apply le_times_l.
1123    unfold B.
1124    apply le_pi_p.intros.
1125    apply le_pi_p.intros.
1126    apply le_exp
1127     [apply prime_to_lt_O.
1128      apply primeb_true_to_prime.
1129      assumption
1130     |apply (bool_elim ? (leb (S n) (exp i (S i1))));intro
1131       [simplify in ⊢ (? % ?).
1132        cut ((S(S O))*n/i\sup(S i1) = S O)
1133         [rewrite > Hcut.apply le_n
1134         |apply (div_mod_spec_to_eq
1135           ((S(S O))*n) (exp i (S i1))
1136            ? (mod ((S(S O))*n) (exp i (S i1)))
1137            ? (minus ((S(S O))*n) (exp i (S i1))) )
1138           [apply div_mod_spec_div_mod.
1139            apply lt_O_exp.
1140            apply prime_to_lt_O.
1141            apply primeb_true_to_prime.
1142            assumption
1143           |cut (i\sup(S i1)≤(S(S O))*n)
1144             [apply div_mod_spec_intro
1145               [alias id "lt_plus_to_lt_minus" = "cic:/matita/nat/map_iter_p.ma/lt_plus_to_lt_minus.con".
1146                apply lt_plus_to_lt_minus
1147                 [assumption
1148                 |simplify in ⊢ (? % ?).
1149                  rewrite < plus_n_O.
1150                  apply lt_plus
1151                   [apply leb_true_to_le.assumption
1152                   |apply leb_true_to_le.assumption
1153                   ]
1154                 ]
1155               |rewrite > sym_plus.
1156                rewrite > sym_times in ⊢ (? ? ? (? ? %)).
1157                rewrite < times_n_SO.
1158                apply plus_minus_m_m.
1159                assumption
1160               ]
1161             |apply (trans_le ? (exp i (log i ((S(S O))*n))))
1162               [apply le_exp
1163                 [apply prime_to_lt_O.
1164                  apply primeb_true_to_prime.
1165                  assumption
1166                 |assumption
1167                 ]
1168               |apply le_exp_log.
1169                rewrite > (times_n_O O) in ⊢ (? % ?).
1170                apply lt_times
1171                 [apply lt_O_S
1172                 |assumption
1173                 ]
1174               ]
1175             ]
1176           ]
1177         ]
1178       |apply le_O_n
1179       ]
1180     ]
1181   |assumption
1182   ]
1183 qed.
1184
1185 theorem le_A_BA: \forall n. A((S(S O))*n) \le B((S(S O))*n)*A n.
1186 intros.cases n
1187   [apply le_n
1188   |apply le_A_BA1.apply lt_O_S
1189   ]
1190 qed.
1191
1192 theorem le_A_exp: \forall n.
1193 A((S(S O))*n) \le (exp (S(S O)) ((S(S O)*n)))*A n.
1194 intro.
1195 apply (trans_le ? (B((S(S O))*n)*A n))
1196   [apply le_A_BA
1197   |apply le_times_l.
1198    apply le_B_exp
1199   ]
1200 qed.
1201
1202 theorem le_A_exp1: \forall n.
1203 A(exp (S(S O)) n) \le (exp (S(S O)) ((S(S O))*(exp (S(S O)) n))).
1204 intro.elim n
1205   [simplify.apply le_S_S.apply le_O_n
1206   |change with (A ((S(S O))*((S(S O)))\sup n1)≤ ((S(S O)))\sup((S(S O))*((S(S O))\sup(S n1)))).
1207    apply (trans_le ? ((exp (S(S O)) ((S(S O)*(exp (S(S O)) n1))))*A (exp (S(S O)) n1)))
1208     [apply le_A_exp
1209     |apply (trans_le ? ((S(S O))\sup((S(S O))*((S(S O)))\sup(n1))*(S(S O))\sup((S(S O))*((S(S O)))\sup(n1))))
1210       [apply le_times_r.
1211        assumption
1212       |rewrite < exp_plus_times.
1213        simplify.rewrite < plus_n_O in ⊢ (? ? (? ? (? ? %))).
1214        apply le_n
1215       ]
1216     ]
1217   ]
1218 qed.
1219
1220 theorem monotonic_A: monotonic nat le A.
1221 unfold.intros.
1222 elim H
1223   [apply le_n
1224   |apply (trans_le ? (A n1))
1225     [assumption
1226     |unfold A.
1227      cut (pi_p (S n1) primeb (λp:nat.(p)\sup(log p n1))
1228           ≤pi_p (S n1) primeb (λp:nat.(p)\sup(log p (S n1))))
1229       [apply (bool_elim ? (primeb (S n1)));intro
1230         [rewrite > (true_to_pi_p_Sn ? ? ? H3).
1231          rewrite > times_n_SO in ⊢ (? % ?).
1232          rewrite > sym_times.
1233          apply le_times
1234           [apply lt_O_exp.apply lt_O_S
1235           |assumption
1236           ]
1237         |rewrite > (false_to_pi_p_Sn ? ? ? H3).
1238          assumption
1239         ]
1240       |apply le_pi_p.intros.
1241        apply le_exp
1242         [apply prime_to_lt_O.
1243          apply primeb_true_to_prime.
1244          assumption
1245         |apply le_log
1246           [apply prime_to_lt_SO.
1247            apply primeb_true_to_prime.
1248            assumption
1249           |apply (lt_to_le_to_lt ? i)
1250             [apply prime_to_lt_O.
1251              apply primeb_true_to_prime.
1252              assumption
1253             |apply le_S_S_to_le.
1254              assumption
1255             ]
1256           |apply le_S.apply le_n
1257           ]
1258         ]
1259       ]
1260     ]
1261   ]
1262 qed.
1263
1264 theorem le_A_exp2: \forall n. O < n \to
1265 A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)).
1266 intros.
1267 apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n)))))
1268   [apply monotonic_A.
1269    apply lt_to_le.
1270    apply lt_exp_log.
1271    apply le_n
1272   |apply (trans_le ? ((exp (S(S O)) ((S(S O))*(exp (S(S O)) (S(log (S(S O)) n)))))))
1273     [apply le_A_exp1
1274     |apply le_exp
1275       [apply lt_O_S
1276       |rewrite > assoc_times.apply le_times_r.
1277        change with ((S(S O))*((S(S O))\sup(log (S(S O)) n))≤(S(S O))*n).
1278        apply le_times_r.
1279        apply le_exp_log.
1280        assumption
1281       ]
1282     ]
1283   ]
1284 qed.
1285
1286 (* example *)
1287 theorem A_SO: A (S O) = S O.
1288 reflexivity.
1289 qed.
1290
1291 theorem A_SSO: A (S(S O)) = S (S O).
1292 reflexivity.
1293 qed.
1294
1295 theorem A_SSSO: A (S(S(S O))) = S(S(S(S(S(S O))))).
1296 reflexivity.
1297 qed.
1298
1299 theorem A_SSSSO: A (S(S(S(S O)))) = S(S(S(S(S(S(S(S(S(S(S(S O))))))))))).
1300 reflexivity.
1301 qed.
1302
1303 (* da spostare *)
1304 theorem or_eq_eq_S: \forall n.\exists m.
1305 n = (S(S O))*m \lor n = S ((S(S O))*m).
1306 intro.elim n
1307   [apply (ex_intro ? ? O).
1308    left.reflexivity
1309   |elim H.elim H1
1310     [apply (ex_intro ? ? a).
1311      right.apply eq_f.assumption
1312     |apply (ex_intro ? ? (S a)).
1313      left.rewrite > H2.
1314      apply sym_eq.
1315      apply times_SSO
1316     ]
1317   ]
1318 qed.
1319
1320 theorem times_exp:
1321 \forall n,m,p. exp n p * exp m p = exp (n*m) p.
1322 intros.elim p
1323   [simplify.reflexivity
1324   |simplify.
1325    rewrite > assoc_times.
1326    rewrite < assoc_times in ⊢ (? ? (? ? %) ?).
1327    rewrite < sym_times in ⊢ (? ? (? ? (? % ?)) ?).
1328    rewrite > assoc_times in ⊢ (? ? (? ? %) ?).
1329    rewrite < assoc_times.
1330    rewrite < H.
1331    reflexivity
1332   ]
1333 qed.
1334
1335 theorem monotonic_exp1: \forall n.
1336 monotonic nat le (\lambda x.(exp x n)).
1337 unfold monotonic. intros.
1338 simplify.elim n
1339   [apply le_n
1340   |simplify.
1341    apply le_times;assumption
1342   ]
1343 qed.
1344
1345 (* a better result *)
1346 theorem le_A_exp3: \forall n. S O < n \to
1347 A(n) \le exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * n)).
1348 intro.
1349 apply (nat_elim1 n).
1350 intros.
1351 elim (or_eq_eq_S m).
1352 elim H2
1353   [elim (le_to_or_lt_eq (S O) a)
1354     [rewrite > H3 in ⊢ (? % ?).
1355      apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a))
1356       [apply le_A_exp
1357       |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)*
1358          ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*a))))
1359         [apply le_times_r.
1360          apply H
1361           [rewrite > H3.
1362            rewrite > times_n_SO in ⊢ (? % ?).
1363            rewrite > sym_times.
1364            apply lt_times_l1
1365             [apply lt_to_le.assumption
1366             |apply le_n
1367             ]
1368           |assumption
1369           ]
1370         |rewrite > sym_times.
1371          rewrite > assoc_times.
1372          rewrite < exp_plus_times.
1373          apply (trans_le ?
1374           (pred a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1375           [rewrite > assoc_times.
1376            apply le_times_r.
1377            rewrite < exp_plus_times.
1378            apply le_exp
1379             [apply lt_O_S
1380             |rewrite < H3.
1381              simplify.
1382              rewrite < plus_n_O.
1383              apply le_S.apply le_S.
1384              apply le_n
1385             ]
1386           |apply le_times_l.
1387            rewrite > times_exp.
1388            apply monotonic_exp1.
1389            rewrite > H3.
1390            rewrite > sym_times.
1391            cases a
1392             [apply le_n
1393             |simplify.
1394              rewrite < plus_n_Sm.
1395              apply le_S.
1396              apply le_n
1397             ]
1398           ]
1399         ]
1400       ]
1401     |rewrite < H4 in H3.
1402      simplify in H3.
1403      rewrite > H3.
1404      simplify.
1405      apply le_S_S.apply le_S_S.apply le_O_n
1406     |apply not_lt_to_le.intro.
1407      apply (lt_to_not_le ? ? H1).
1408      rewrite > H3.
1409      apply (le_n_O_elim a)
1410       [apply le_S_S_to_le.assumption
1411       |apply le_O_n
1412       ]
1413     ]
1414   |elim (le_to_or_lt_eq O a (le_O_n ?))
1415     [apply (trans_le ? (A ((S(S O))*(S a))))
1416       [apply monotonic_A.
1417        rewrite > H3.
1418        rewrite > times_SSO.
1419        apply le_n_Sn
1420       |apply (trans_le ? ((exp (S(S O)) ((S(S O)*(S a))))*A (S a)))
1421         [apply le_A_exp
1422         |apply (trans_le ? (((S(S O)))\sup((S(S O))*S a)*
1423            (a\sup((S(S O)))*((S(S O)))\sup((S(S O))*(S a)))))
1424           [apply le_times_r.
1425            apply H
1426             [rewrite > H3.
1427              apply le_S_S.
1428              simplify.
1429              rewrite > plus_n_SO.
1430              apply le_plus_r.
1431              rewrite < plus_n_O.
1432              assumption
1433             |apply le_S_S.assumption
1434             ]
1435           |rewrite > sym_times.
1436            rewrite > assoc_times.
1437            rewrite < exp_plus_times.
1438            apply (trans_le ?
1439             (a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1440             [rewrite > assoc_times.
1441              apply le_times_r.
1442              rewrite < exp_plus_times.
1443              apply le_exp
1444               [apply lt_O_S
1445               |rewrite > times_SSO.
1446                rewrite < H3.
1447                simplify.
1448                rewrite < plus_n_Sm.
1449                rewrite < plus_n_O.
1450                apply le_n
1451               ]
1452             |apply le_times_l.
1453              rewrite > times_exp.
1454              apply monotonic_exp1.
1455              rewrite > H3.
1456              rewrite > sym_times.
1457              apply le_n
1458             ]
1459           ]
1460         ]
1461       ]
1462     |rewrite < H4 in H3.simplify in H3.
1463      apply False_ind.
1464      apply (lt_to_not_le ? ? H1).
1465      rewrite > H3.
1466      apply le_n
1467     ]
1468   ]
1469 qed.
1470
1471
1472
1473 (* da spostare *)
1474 theorem times_exp: \forall n,m,p.exp n p * exp m p = exp (n*m) p.
1475 intros.elim p
1476   [reflexivity
1477   |simplify.autobatch
1478   ]
1479 qed.
1480
1481 theorem le_exp_log: \forall p,n. O < n \to
1482 exp p (
1483 log n) \le n.
1484 intros.
1485 apply leb_true_to_le.
1486 unfold log.
1487 apply (f_max_true (\lambda x.leb (exp p x) n)).
1488 apply (ex_intro ? ? O).
1489 split
1490   [apply le_O_n
1491   |apply le_to_leb_true.simplify.assumption
1492   ]
1493 qed.
1494
1495 theorem lt_log_n_n: \forall n. O < n \to log n < n.
1496 intros.
1497 cut (log n \le n)
1498   [elim (le_to_or_lt_eq ? ? Hcut)
1499     [assumption
1500     |absurd (exp (S(S O)) n \le n)
1501       [rewrite < H1 in ⊢ (? (? ? %) ?).
1502        apply le_exp_log.
1503        assumption
1504       |apply lt_to_not_le.
1505        apply lt_m_exp_nm.
1506        apply le_n
1507       ]
1508     ]
1509   |unfold log.apply le_max_n
1510   ]
1511 qed.
1512
1513 theorem le_log_n_n: \forall n. log n \le n.
1514 intro.
1515 cases n
1516   [apply le_n
1517   |apply lt_to_le.
1518    apply lt_log_n_n.
1519    apply lt_O_S
1520   ]
1521 qed.
1522
1523 theorem lt_exp_log: \forall n. n < exp (S(S O)) (S (log n)).
1524 intro.cases n
1525   [simplify.apply le_S.apply le_n
1526   |apply not_le_to_lt.
1527    apply leb_false_to_not_le.
1528    apply (lt_max_to_false ? (S n1) (S (log (S n1))))
1529     [apply le_S_S.apply le_n
1530     |apply lt_log_n_n.apply lt_O_S
1531     ]
1532   ]
1533 qed.
1534
1535 theorem f_false_to_le_max: \forall f,n,p. (∃i:nat.i≤n∧f i=true) \to
1536 (\forall m. p < m \to f m = false)
1537 \to max n f \le p.
1538 intros.
1539 apply not_lt_to_le.intro.
1540 apply not_eq_true_false.
1541 rewrite < (H1 ? H2).
1542 apply sym_eq.
1543 apply f_max_true.
1544 assumption.
1545 qed.
1546
1547 theorem log_times1: \forall n,m. O < n \to O < m \to
1548 log (n*m) \le S(log n+log m).
1549 intros.
1550 unfold in ⊢ (? (% ?) ?).
1551 apply f_false_to_le_max
1552   [apply (ex_intro ? ? O).
1553    split
1554     [apply le_O_n
1555     |apply le_to_leb_true.
1556      simplify.
1557      rewrite > times_n_SO.
1558      apply le_times;assumption
1559     ]
1560   |intros.
1561    apply lt_to_leb_false.
1562    apply (lt_to_le_to_lt ? ((exp (S(S O)) (S(log n)))*(exp (S(S O)) (S(log m)))))
1563     [apply lt_times;apply lt_exp_log
1564     |rewrite < exp_plus_times.
1565      apply le_exp
1566       [apply lt_O_S
1567       |simplify.
1568        rewrite < plus_n_Sm.
1569        assumption
1570       ]
1571     ]
1572   ]
1573 qed.
1574
1575 theorem log_times: \forall n,m.log (n*m) \le S(log n+log m).
1576 intros.
1577 cases n
1578   [apply le_O_n
1579   |cases m
1580     [rewrite < times_n_O.
1581      apply le_O_n
1582     |apply log_times1;apply lt_O_S
1583     ]
1584   ]
1585 qed.
1586
1587 theorem log_exp: \forall n,m.O < m \to
1588 log ((exp (S(S O)) n)*m)=n+log m.
1589 intros.
1590 unfold log in ⊢ (? ? (% ?) ?).
1591 apply max_spec_to_max.
1592 unfold max_spec.
1593 split
1594   [split
1595     [elim n
1596       [simplify.
1597        rewrite < plus_n_O.
1598        apply le_log_n_n
1599       |simplify.
1600        rewrite < plus_n_O.
1601        rewrite > times_plus_l.
1602        apply (trans_le ? (S((S(S O))\sup(n1)*m)))
1603         [apply le_S_S.assumption
1604         |apply (lt_O_n_elim ((S(S O))\sup(n1)*m))
1605           [rewrite > (times_n_O O) in ⊢ (? % ?).
1606            apply lt_times
1607             [apply lt_O_exp.
1608              apply lt_O_S
1609             |assumption
1610             ]
1611           |intro.simplify.apply le_S_S.
1612            apply le_plus_n
1613           ]
1614         ]
1615       ]
1616     |simplify.
1617      apply le_to_leb_true.
1618      rewrite > exp_plus_times.
1619      apply le_times_r.
1620      apply le_exp_log.
1621      assumption
1622     ]
1623   |intros.
1624    simplify.
1625    apply lt_to_leb_false.
1626    apply (lt_to_le_to_lt ? ((exp (S(S O)) n)*(exp (S(S O)) (S(log m)))))
1627     [apply lt_times_r1
1628       [apply lt_O_exp.apply lt_O_S
1629       |apply lt_exp_log.
1630       ]
1631     |rewrite < exp_plus_times.
1632      apply le_exp
1633       [apply lt_O_S
1634       |rewrite < plus_n_Sm.
1635        assumption
1636       ]
1637     ]
1638   ]
1639 qed.
1640
1641 theorem log_SSO: \forall n. O < n \to
1642 log ((S(S O))*n) = S (log n).
1643 intros.
1644 change with (log ((exp (S(S O)) (S O))*n)=S (log n)).
1645 rewrite > log_exp.reflexivity.assumption.
1646 qed.
1647
1648 theorem or_eq_S: \forall n.\exists m.
1649 (n = (S(S O))*m) \lor (n = S((S(S O))*m)).
1650 intro.
1651 elim n
1652   [apply (ex_intro ? ? O).left.apply times_n_O
1653   |elim H.elim H1
1654     [apply (ex_intro ? ? a).right.apply eq_f.assumption
1655     |apply (ex_intro ? ? (S a)).left.
1656      rewrite > H2.simplify.
1657      rewrite < plus_n_O.
1658      rewrite < plus_n_Sm.
1659      reflexivity
1660     ]
1661   ]
1662 qed.
1663
1664 theorem lt_O_to_or_eq_S: \forall n.O < n \to \exists m.m < n \land
1665 ((n = (S(S O))*m) \lor (n = S((S(S O))*m))).
1666 intros.
1667 elim (or_eq_S n).
1668 elim H1
1669   [apply (ex_intro ? ? a).split
1670     [rewrite > H2.
1671      rewrite > times_n_SO in ⊢ (? % ?).
1672      rewrite > sym_times.
1673      apply lt_times_l1
1674       [apply (divides_to_lt_O a n ? ?)
1675         [assumption
1676         |apply (witness a n (S (S O))).
1677          rewrite > sym_times.
1678          assumption
1679         ]
1680       |apply le_n
1681       ]
1682     |left.assumption
1683     ]
1684   |apply (ex_intro ? ? a).split
1685     [rewrite > H2.
1686      apply (le_to_lt_to_lt ? ((S(S O))*a))
1687       [rewrite > times_n_SO in ⊢ (? % ?).
1688        rewrite > sym_times.
1689        apply le_times_l.
1690        apply le_n_Sn
1691       |apply le_n
1692       ]
1693     |right.assumption
1694     ]
1695   ]
1696 qed.
1697
1698 theorem factS: \forall n. fact (S n) = (S n)*(fact n).
1699 intro.simplify.reflexivity.
1700 qed.
1701
1702 theorem exp_S: \forall n,m. exp m (S n) = m*exp m n.
1703 intros.reflexivity.
1704 qed.
1705
1706 lemma times_SSO: \forall n.(S(S O))*(S n) = S(S((S(S O))*n)).
1707 intro.simplify.rewrite < plus_n_Sm.reflexivity.
1708 qed.
1709
1710 theorem fact1: \forall n.
1711 fact ((S(S O))*n) \le (exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n).
1712 intro.elim n
1713   [rewrite < times_n_O.apply le_n
1714   |rewrite > times_SSO.
1715    rewrite > factS.
1716    rewrite > factS.
1717    rewrite < assoc_times.
1718    rewrite > factS.
1719    apply (trans_le ? (((S(S O))*(S n1))*((S(S O))*(S n1))*(fact (((S(S O))*n1)))))
1720     [apply le_times_l.
1721      rewrite > times_SSO.
1722      apply le_times_r.
1723      apply le_n_Sn
1724     |rewrite > assoc_times.
1725      rewrite > assoc_times.
1726      rewrite > assoc_times in ⊢ (? ? %).
1727      rewrite > exp_S.
1728      rewrite > assoc_times in ⊢ (? ? %).
1729      apply le_times_r.
1730      rewrite < assoc_times.
1731      rewrite < assoc_times.
1732      rewrite < sym_times in ⊢ (? (? (? % ?) ?) ?).
1733      rewrite > assoc_times.
1734      rewrite > assoc_times.
1735      rewrite > exp_S.
1736      rewrite > assoc_times in ⊢ (? ? %).
1737      apply le_times_r.
1738      rewrite > sym_times in ⊢ (? ? %).
1739      rewrite > assoc_times in ⊢ (? ? %).
1740      rewrite > assoc_times in ⊢ (? ? %).
1741      apply le_times_r.
1742      rewrite < assoc_times in ⊢ (? ? %).
1743      rewrite < assoc_times in ⊢ (? ? %).
1744      rewrite < sym_times in ⊢ (? ? (? (? % ?) ?)).
1745      rewrite > assoc_times in ⊢ (? ? %).
1746      rewrite > assoc_times in ⊢ (? ? %).
1747      apply le_times_r.
1748      rewrite > sym_times in ⊢ (? ? (? ? %)).
1749      rewrite > sym_times in ⊢ (? ? %).
1750      assumption
1751     ]
1752   ]
1753 qed.
1754
1755 theorem monotonic_log: monotonic nat le log.
1756 unfold monotonic.intros.
1757 elim (le_to_or_lt_eq ? ? H) 0
1758   [cases x;intro
1759     [apply le_O_n
1760     |apply lt_S_to_le.
1761      apply (lt_exp_to_lt (S(S O)))
1762       [apply le_n
1763       |apply (le_to_lt_to_lt ? (S n))
1764         [apply le_exp_log.
1765          apply lt_O_S
1766         |apply (trans_lt ? y)
1767           [assumption
1768           |apply lt_exp_log
1769           ]
1770         ]
1771       ]
1772     ]
1773   |intro.rewrite < H1.apply le_n
1774   ]
1775 qed.
1776
1777 theorem lt_O_fact: \forall n. O < fact n.
1778 intro.elim n
1779   [simplify.apply lt_O_S
1780   |rewrite > factS.
1781    rewrite > (times_n_O O).
1782    apply lt_times
1783     [apply lt_O_S
1784     |assumption
1785     ]
1786   ]
1787 qed.
1788
1789 theorem fact2: \forall n.O < n \to
1790 (exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n) < fact (S((S(S O))*n)).
1791 intros.elim H
1792   [simplify.apply le_S.apply le_n
1793   |rewrite > times_SSO.
1794    rewrite > factS.
1795    rewrite > factS.
1796    rewrite < assoc_times.
1797    rewrite > factS.
1798    rewrite < times_SSO in ⊢ (? ? %).
1799    apply (trans_lt ? (((S(S O))*S n1)*((S(S O))*S n1*(S ((S(S O))*n1))!)))
1800     [rewrite > assoc_times in ⊢ (? ? %).
1801      rewrite > exp_S.
1802      rewrite > assoc_times.
1803      rewrite > assoc_times.
1804      rewrite > assoc_times.
1805      apply lt_times_r.
1806      rewrite > exp_S.
1807      rewrite > assoc_times.
1808      rewrite > sym_times in ⊢ (? ? %).
1809      rewrite > assoc_times in ⊢ (? ? %).
1810      rewrite > assoc_times in ⊢ (? ? %).
1811      apply lt_times_r.
1812      rewrite > sym_times.
1813      rewrite > assoc_times.
1814      rewrite > assoc_times.
1815      apply lt_times_r.
1816      rewrite < assoc_times.
1817      rewrite < assoc_times.
1818      rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
1819      rewrite > assoc_times.
1820      rewrite > assoc_times.
1821      rewrite > sym_times in ⊢ (? ? %).
1822      apply lt_times_r.
1823      rewrite < assoc_times.
1824      rewrite < sym_times.
1825      rewrite < assoc_times.
1826      assumption
1827     |apply lt_times_l1
1828       [rewrite > (times_n_O O) in ⊢ (? % ?).
1829        apply lt_times
1830         [rewrite > (times_n_O O) in ⊢ (? % ?).
1831          apply lt_times
1832           [apply lt_O_S
1833           |apply lt_O_S
1834           ]
1835         |apply lt_O_fact
1836         ]
1837       |apply le_n
1838       ]
1839     ]
1840   ]
1841 qed.
1842
1843 theorem lt_O_log: \forall n. S O < n \to O < log n.
1844 intros.elim H
1845   [simplify.apply lt_O_S
1846   |apply (lt_to_le_to_lt ? (log n1))
1847     [assumption
1848     |apply monotonic_log.
1849      apply le_n_Sn
1850     ]
1851   ]
1852 qed.
1853
1854 theorem log_fact_SSSO: log (fact (S(S(S O)))) = S (S O).
1855 reflexivity.
1856 qed.
1857
1858 lemma exp_SSO_SSO: exp (S(S O)) (S(S O)) = S(S(S(S O))).
1859 reflexivity.
1860 qed.
1861 (*
1862 theorem log_fact_SSSSO: log (fact (S(S(S(S O))))) = S(S(S(S O))).
1863 reflexivity.
1864 qed.
1865 *)
1866 theorem log_fact_SSSSSO: log (fact (S(S(S(S(S O)))))) = S(S(S(S O))).
1867 reflexivity.
1868 qed.
1869
1870 theorem bof_bof: \forall n.(S(S(S(S O)))) < n \to
1871 n \le (S(S(S(S(S(S(S(S O)))))))) \to log (fact n) < n*log n - n.
1872 intros.
1873 elim H
1874   [rewrite > factS in ⊢ (? (? %) ?).
1875    rewrite > factS in ⊢ (? (? (? ? %)) ?).
1876    rewrite < assoc_times in ⊢ (? (? %) ?).
1877    rewrite < sym_times in ⊢ (? (? (? % ?)) ?).
1878    rewrite > assoc_times in ⊢ (? (? %) ?).
1879    change with (exp (S(S O)) (S(S O))) in ⊢ (? (? (? % ?)) ?).
1880
1881 theorem bof: \forall n.(S(S(S(S O))))) < n \to log (fact n) < n*log n - n.
1882 intro.apply (nat_elim1 n).
1883 intros.
1884 elim (lt_O_to_or_eq_S m)
1885   [elim H2.clear H2.
1886    elim H4.clear H4.
1887    rewrite > H2.
1888    apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
1889     [apply monotonic_log.
1890      apply fact1
1891     |rewrite > assoc_times in ⊢ (? (? %) ?).
1892      rewrite > log_exp.
1893      apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
1894       [apply le_plus_r.
1895        apply log_times
1896       |rewrite > plus_n_Sm.
1897        rewrite > log_SSO.
1898        rewrite < times_n_Sm.
1899        apply (le_to_lt_to_lt ? ((S(S O))*a+(log a!+(a*log a-a))))
1900         [apply le_plus_r.
1901          apply le_plus_r.
1902          apply H.assumption
1903         |apply (lt_to_le_to_lt ? ((S(S O))*a+((a*log a-a)+(a*log a-a))))
1904           [apply lt_plus_r.
1905            apply lt_plus_l.
1906            apply H.
1907            assumption.
1908           |rewrite > times_SSO_n.
1909            rewrite > distr_times_minus.
1910            rewrite > sym_plus.
1911            rewrite > plus_minus
1912             [rewrite > sym_plus.
1913              rewrite < assoc_times.
1914              apply le_n
1915             |rewrite < assoc_times.
1916              rewrite > times_n_SO in ⊢ (? % ?).
1917              apply le_times
1918               [apply le_n
1919               |apply lt_O_log.
1920                apply (lt_times_n_to_lt_r (S(S O)))
1921                 [apply lt_O_S
1922                 |rewrite < times_n_SO.
1923                  rewrite < H2.
1924                  assumption
1925                 ]
1926               ]
1927             ]
1928           ]
1929
1930              .
1931           ]
1932         |
1933            rewrite < eq_plus_minus_minus_plus.
1934
1935        rewrite > assoc_plus.
1936        apply lt_plus_r.
1937        rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
1938        change with
1939         (S((S(S O))*a+((S(S O))*log a!)) < (S(S O))*a*log ((S(S O))*a)-(S(S O))*a+k*log ((S(S O))*a)).
1940        apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))
1941         [apply le_S_S.
1942          apply lt_plus_r.
1943          apply lt_times_r.
1944          apply H.
1945          assumption
1946         |
1947
1948 theorem stirling: \forall n,k.k \le n \to
1949 log (fact n) < n*log n - n + k*log n.
1950 intro.
1951 apply (nat_elim1 n).
1952 intros.
1953 elim (lt_O_to_or_eq_S m)
1954   [elim H2.clear H2.
1955    elim H4.clear H4.
1956    rewrite > H2.
1957    apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
1958     [apply monotonic_log.
1959      apply fact1
1960     |rewrite > assoc_times in ⊢ (? (? %) ?).
1961      rewrite > log_exp.
1962      apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
1963       [apply le_plus_r.
1964        apply log_times
1965       |rewrite < plus_n_Sm.
1966        rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
1967        change with
1968         (S((S(S O))*a+((S(S O))*log a!)) < (S(S O))*a*log ((S(S O))*a)-(S(S O))*a+k*log ((S(S O))*a)).
1969        apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))
1970         [apply le_S_S.
1971          apply lt_plus_r.
1972          apply lt_times_r.
1973          apply H.
1974          assumption
1975         |
1976
1977           [
1978
1979        a*log a-a+k*log a
1980
1981 *)