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