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