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 = (cic:/matita/library_autobatch/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_autobatch/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   autobatch
  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 autobatch.
  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 [ autobatch
  67   (*apply div_mod_spec_div_mod.
  68   assumption*)
  69 | autobatch
  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 autobatch.
  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 autobatch.
  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 autobatch.
  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 autobatch.
 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 autobatch.
 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 autobatch.
 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     [ autobatch
 149       (*apply sym_eq.
 150       apply assoc_times*)
 151     | rewrite > (sym_times n2 m).
 152       apply assoc_times
 153     ]
 154   ]
 155 | autobatch
 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 autobatch.
 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     [ autobatch
 183       (*rewrite > Hcut1.
 184       apply (witness p O O).
 185       apply times_n_O*)
 186     | autobatch
 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       autobatch
 200       (*rewrite < div_mod
 201       [ reflexivity
 202       | assumption
 203       ]*)
 204     | apply sym_eq.
 205       apply plus_to_minus.
 206       rewrite > sym_plus.
 207       autobatch
 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     autobatch
 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       autobatch
 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       autobatch
 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   autobatch
 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     autobatch
 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   autobatch
 317   (*apply mod_O_to_divides;assumption*)
 318 | intro.
 319   simplify.
 320   unfold Not.
 321   intro.
 322   autobatch
 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 autobatch non chiude il goal, chiuso dalla sola apply H1*)
 368     apply H1
 369   | right.
 370     (*qui autobatch 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 autobatch 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 autobatch 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   [ autobatch
 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         autobatch
 437         (*apply le_S_S_to_le.
 438         assumption*)
 439       | autobatch
 440         (*apply (witness ? ? (f (S n1+m))).
 441         apply sym_times*)
 442       ]
 443     | autobatch
 444       (*rewrite > H3.
 445       apply (witness ? ? (pi n1 f m)).
 446       reflexivity*)
 447     ]
 448   | autobatch
 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   | autobatch
 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     [ autobatch
 483       (*apply H1.
 484       apply le_S_S_to_le.
 485       assumption*)
 486     | autobatch
 487       (*apply (witness ? ? (S n1)).
 488       apply sym_times*)
 489     ]
 490   | intro.
 491     autobatch
 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   [ autobatch
 506     (*apply (trans_lt O (S O))
 507     [ apply (le_n (S O))
 508     | assumption
 509     ]*)
 510   | rewrite > Hcut.
 511     assumption
 512   ]
 513 | autobatch(*
 514   apply divides_to_mod_O
 515   [ apply ltn_to_ltO [| apply H]
 516   | apply divides_fact
 517     [ apply ltn_to_ltO [| apply H]
 518     | assumption
 519     ]
 520   ]*)
 521 ]
 522 qed.
 523
 524 theorem not_divides_S_fact: \forall n,i:nat.
 525 (S O) < i \to i \le n \to i \ndivides S n!.
 526 intros.
 527 apply divides_b_false_to_not_divides
 528 [ autobatch
 529   (*apply (trans_lt O (S O))
 530   [ apply (le_n (S O))
 531   | assumption
 532   ]*)
 533 | unfold divides_b.
 534   rewrite > mod_S_fact;autobatch
 535   (*[ simplify.
 536     reflexivity
 537   | assumption
 538   | assumption
 539   ]*)
 540 ]
 541 qed.
 542
 543 (* prime *)
 544 definition prime : nat \to  Prop \def
 545 \lambda n:nat. (S O) < n \land
 546 (\forall m:nat. m \divides n \to (S O) < m \to  m = n).
 547
 548 theorem not_prime_O: \lnot (prime O).
 549 unfold Not.
 550 unfold prime.
 551 intro.
 552 elim H.
 553 apply (not_le_Sn_O (S O) H1).
 554 qed.
 555
 556 theorem not_prime_SO: \lnot (prime (S O)).
 557 unfold Not.
 558 unfold prime.
 559 intro.
 560 elim H.
 561 apply (not_le_Sn_n (S O) H1).
 562 qed.
 563
 564 (* smallest factor *)
 565 definition smallest_factor : nat \to nat \def
 566 \lambda n:nat.
 567 match n with
 568 [ O \Rightarrow O
 569 | (S p) \Rightarrow
 570   match p with
 571   [ O \Rightarrow (S O)
 572   | (S q) \Rightarrow min_aux q (S(S q)) (\lambda m.(eqb ((S(S q)) \mod m) O))]].
 573
 574 (* it works !
 575 theorem example1 : smallest_prime_factor (S(S(S O))) = (S(S(S O))).
 576 normalize.reflexivity.
 577 qed.
 578
 579 theorem example2: smallest_prime_factor (S(S(S(S O)))) = (S(S O)).
 580 normalize.reflexivity.
 581 qed.
 582
 583 theorem example3 : smallest_prime_factor (S(S(S(S(S(S(S O))))))) = (S(S(S(S(S(S(S O))))))).
 584 simplify.reflexivity.
 585 qed. *)
 586
 587 theorem lt_SO_smallest_factor:
 588 \forall n:nat. (S O) < n \to (S O) < (smallest_factor n).
 589 intro.
 590 apply (nat_case n)
 591 [ autobatch
 592   (*intro.
 593   apply False_ind.
 594   apply (not_le_Sn_O (S O) H)*)
 595 | intro.
 596   apply (nat_case m)
 597   [ autobatch
 598     (*intro. apply False_ind.
 599     apply (not_le_Sn_n (S O) H)*)
 600   | intros.
 601     change with
 602     (S O < min_aux m1 (S(S m1)) (\lambda m.(eqb ((S(S m1)) \mod m) O))).
 603     apply (lt_to_le_to_lt ? (S (S O)))
 604     [ apply (le_n (S(S O)))
 605     | cut ((S(S O)) = (S(S m1)) - m1)
 606       [ rewrite > Hcut.
 607         apply le_min_aux
 608       | apply sym_eq.
 609         apply plus_to_minus.
 610         autobatch
 611         (*rewrite < sym_plus.
 612         simplify.
 613         reflexivity*)
 614       ]
 615     ]
 616   ]
 617 ]
 618 qed.
 619
 620 theorem lt_O_smallest_factor: \forall n:nat. O < n \to O < (smallest_factor n).
 621 intro.
 622 apply (nat_case n)
 623 [ autobatch
 624   (*intro.
 625   apply False_ind.
 626   apply (not_le_Sn_n O H)*)
 627 | intro.
 628   apply (nat_case m)
 629   [ autobatch
 630     (*intro.
 631     simplify.
 632     unfold lt.
 633     apply le_n*)
 634   | intros.
 635     apply (trans_lt ? (S O))
 636     [ autobatch
 637       (*unfold lt.
 638       apply le_n*)
 639     | apply lt_SO_smallest_factor.
 640       unfold lt.autobatch
 641       (*apply le_S_S.
 642       apply le_S_S.
 643       apply le_O_n*)
 644     ]
 645   ]
 646 ]
 647 qed.
 648
 649 theorem divides_smallest_factor_n :
 650 \forall n:nat. O < n \to smallest_factor n \divides n.
 651 intro.
 652 apply (nat_case n)
 653 [ intro.
 654   autobatch
 655   (*apply False_ind.
 656   apply (not_le_Sn_O O H)*)
 657 | intro.
 658   apply (nat_case m)
 659   [ intro.
 660     autobatch
 661     (*simplify.
 662     apply (witness ? ? (S O)).
 663     simplify.
 664     reflexivity*)
 665   | intros.
 666     apply divides_b_true_to_divides
 667     [ apply (lt_O_smallest_factor ? H)
 668     | change with
 669        (eqb ((S(S m1)) \mod (min_aux m1 (S(S m1))
 670        (\lambda m.(eqb ((S(S m1)) \mod m) O)))) O = true).
 671       apply f_min_aux_true.
 672       apply (ex_intro nat ? (S(S m1))).
 673       split
 674       [ autobatch
 675         (*split
 676         [ apply le_minus_m
 677         | apply le_n
 678         ]*)
 679       | autobatch
 680         (*rewrite > mod_n_n
 681         [ reflexivity
 682         | apply (trans_lt ? (S O))
 683           [ apply (le_n (S O))
 684           | unfold lt.
 685             apply le_S_S.
 686             apply le_S_S.
 687             apply le_O_n
 688           ]
 689         ]*)
 690       ]
 691     ]
 692   ]
 693 ]
 694 qed.
 695
 696 theorem le_smallest_factor_n :
 697 \forall n:nat. smallest_factor n \le n.
 698 intro.
 699 apply (nat_case n)
 700 [ autobatch
 701   (*simplify.
 702   apply le_n*)
 703 | intro.
 704   autobatch
 705   (*apply (nat_case m)
 706   [ simplify.
 707     apply le_n
 708   | intro.
 709     apply divides_to_le
 710     [ unfold lt.
 711       apply le_S_S.
 712       apply le_O_n
 713     | apply divides_smallest_factor_n.
 714       unfold lt.
 715       apply le_S_S.
 716       apply le_O_n
 717     ]
 718   ]*)
 719 ]
 720 qed.
 721
 722 theorem lt_smallest_factor_to_not_divides: \forall n,i:nat.
 723 (S O) < n \to (S O) < i \to i < (smallest_factor n) \to i \ndivides n.
 724 intros 2.
 725 apply (nat_case n)
 726 [ intro.
 727   apply False_ind.
 728   apply (not_le_Sn_O (S O) H)
 729 | intro.
 730   apply (nat_case m)
 731   [ intro.
 732     apply False_ind.
 733     apply (not_le_Sn_n (S O) H)
 734   | intros.
 735     apply divides_b_false_to_not_divides
 736     [ autobatch
 737       (*apply (trans_lt O (S O))
 738       [ apply (le_n (S O))
 739       | assumption
 740       ]*)
 741     | unfold divides_b.
 742       apply (lt_min_aux_to_false
 743       (\lambda i:nat.eqb ((S(S m1)) \mod i) O) (S(S m1)) m1 i)
 744       [ cut ((S(S O)) = (S(S m1)-m1))
 745         [ rewrite < Hcut.
 746           exact H1
 747         | apply sym_eq.
 748           apply plus_to_minus.
 749           autobatch
 750           (*rewrite < sym_plus.
 751           simplify.
 752           reflexivity*)
 753         ]
 754       | exact H2
 755       ]
 756     ]
 757   ]
 758 ]
 759 qed.
 760
 761 theorem prime_smallest_factor_n :
 762 \forall n:nat. (S O) < n \to prime (smallest_factor n).
 763 intro.
 764 change with ((S(S O)) \le n \to (S O) < (smallest_factor n) \land
 765 (\forall m:nat. m \divides smallest_factor n \to (S O) < m \to  m = (smallest_factor n))).
 766 intro.
 767 split
 768 [ apply lt_SO_smallest_factor.
 769   assumption
 770 | intros.
 771   cut (le m (smallest_factor n))
 772   [ elim (le_to_or_lt_eq m (smallest_factor n) Hcut)
 773     [ absurd (m \divides n)
 774       [ apply (transitive_divides m (smallest_factor n))
 775         [ assumption
 776         | apply divides_smallest_factor_n.
 777           autobatch
 778           (*apply (trans_lt ? (S O))
 779           [ unfold lt.
 780             apply le_n
 781           | exact H
 782           ]*)
 783         ]
 784       | apply lt_smallest_factor_to_not_divides;autobatch
 785         (*[ exact H
 786         | assumption
 787         | assumption
 788         ]*)
 789       ]
 790     | assumption
 791     ]
 792   | apply divides_to_le
 793     [ apply (trans_lt O (S O))
 794       [ apply (le_n (S O))
 795       | apply lt_SO_smallest_factor.
 796         exact H
 797       ]
 798     | assumption
 799     ]
 800   ]
 801 ]
 802 qed.
 803
 804 theorem prime_to_smallest_factor: \forall n. prime n \to
 805 smallest_factor n = n.
 806 intro.
 807 apply (nat_case n)
 808 [ intro.
 809   autobatch
 810   (*apply False_ind.
 811   apply (not_prime_O H)*)
 812 | intro.
 813   apply (nat_case m)
 814   [ intro.
 815     autobatch
 816     (*apply False_ind.
 817     apply (not_prime_SO H)*)
 818   | intro.
 819     change with
 820      ((S O) < (S(S m1)) \land
 821      (\forall m:nat. m \divides S(S m1) \to (S O) < m \to  m = (S(S m1))) \to
 822     smallest_factor (S(S m1)) = (S(S m1))).
 823     intro.
 824     elim H.
 825     autobatch
 826     (*apply H2
 827     [ apply divides_smallest_factor_n.
 828       apply (trans_lt ? (S O))
 829       [ unfold lt.
 830         apply le_n
 831       | assumption
 832       ]
 833     | apply lt_SO_smallest_factor.
 834       assumption
 835     ]*)
 836   ]
 837 ]
 838 qed.
 839
 840 (* a number n > O is prime iff its smallest factor is n *)
 841 definition primeb \def \lambda n:nat.
 842 match n with
 843 [ O \Rightarrow false
 844 | (S p) \Rightarrow
 845   match p with
 846   [ O \Rightarrow false
 847   | (S q) \Rightarrow eqb (smallest_factor (S(S q))) (S(S q))]].
 848
 849 (* it works!
 850 theorem example4 : primeb (S(S(S O))) = true.
 851 normalize.reflexivity.
 852 qed.
 853
 854 theorem example5 : primeb (S(S(S(S(S(S O)))))) = false.
 855 normalize.reflexivity.
 856 qed.
 857
 858 theorem example6 : primeb (S(S(S(S((S(S(S(S(S(S(S O)))))))))))) = true.
 859 normalize.reflexivity.
 860 qed.
 861
 862 theorem example7 : primeb (S(S(S(S(S(S((S(S(S(S((S(S(S(S(S(S(S O))))))))))))))))))) = true.
 863 normalize.reflexivity.
 864 qed. *)
 865
 866 theorem primeb_to_Prop: \forall n.
 867 match primeb n with
 868 [ true \Rightarrow prime n
 869 | false \Rightarrow \lnot (prime n)].
 870 intro.
 871 apply (nat_case n)
 872 [ simplify.
 873   autobatch
 874   (*unfold Not.
 875   unfold prime.
 876   intro.
 877   elim H.
 878   apply (not_le_Sn_O (S O) H1)*)
 879 | intro.
 880   apply (nat_case m)
 881   [ simplify.
 882     autobatch
 883     (*unfold Not.
 884     unfold prime.
 885     intro.
 886     elim H.
 887     apply (not_le_Sn_n (S O) H1)*)
 888   | intro.
 889     change with
 890     match eqb (smallest_factor (S(S m1))) (S(S m1)) with
 891     [ true \Rightarrow prime (S(S m1))
 892     | false \Rightarrow \lnot (prime (S(S m1)))].
 893     apply (eqb_elim (smallest_factor (S(S m1))) (S(S m1)))
 894     [ intro.
 895       simplify.
 896       rewrite < H.
 897       apply prime_smallest_factor_n.
 898       unfold lt.autobatch
 899       (*apply le_S_S.
 900       apply le_S_S.
 901       apply le_O_n*)
 902     | intro.
 903       simplify.
 904       change with (prime (S(S m1)) \to False).
 905       intro.
 906       autobatch
 907       (*apply H.
 908       apply prime_to_smallest_factor.
 909       assumption*)
 910     ]
 911   ]
 912 ]
 913 qed.
 914
 915 theorem primeb_true_to_prime : \forall n:nat.
 916 primeb n = true \to prime n.
 917 intros.
 918 change with
 919 match true with
 920 [ true \Rightarrow prime n
 921 | false \Rightarrow \lnot (prime n)].
 922 rewrite < H.
 923 (*qui autobatch non chiude il goal*)
 924 apply primeb_to_Prop.
 925 qed.
 926
 927 theorem primeb_false_to_not_prime : \forall n:nat.
 928 primeb n = false \to \lnot (prime n).
 929 intros.
 930 change with
 931 match false with
 932 [ true \Rightarrow prime n
 933 | false \Rightarrow \lnot (prime n)].
 934 rewrite < H.
 935 (*qui autobatch non chiude il goal*)
 936 apply primeb_to_Prop.
 937 qed.
 938
 939 theorem decidable_prime : \forall n:nat.decidable (prime n).
 940 intro.
 941 unfold decidable.
 942 cut
 943 (match primeb n with
 944 [ true \Rightarrow prime n
 945 | false \Rightarrow \lnot (prime n)] \to (prime n) \lor \lnot (prime n))
 946 [ apply Hcut.
 947   (*qui autobatch non chiude il goal*)
 948   apply primeb_to_Prop
 949 | elim (primeb n)
 950   [ left.
 951     (*qui autobatch non chiude il goal*)
 952     apply H
 953   | right.
 954     (*qui autobatch non chiude il goal*)
 955     apply H
 956   ]
 957 ]
 958 qed.
 959
 960 theorem prime_to_primeb_true: \forall n:nat.
 961 prime n \to primeb n = true.
 962 intros.
 963 cut (match (primeb n) with
 964 [ true \Rightarrow prime n
 965 | false \Rightarrow \lnot (prime n)] \to ((primeb n) = true))
 966 [ apply Hcut.
 967   (*qui autobatch non chiude il goal*)
 968   apply primeb_to_Prop
 969 | elim (primeb n)
 970   [ reflexivity.
 971   | absurd (prime n)
 972     [ assumption
 973     | (*qui autobatch non chiude il goal*)
 974       assumption
 975     ]
 976   ]
 977 ]
 978 qed.
 979
 980 theorem not_prime_to_primeb_false: \forall n:nat.
 981 \lnot(prime n) \to primeb n = false.
 982 intros.
 983 cut (match (primeb n) with
 984 [ true \Rightarrow prime n
 985 | false \Rightarrow \lnot (prime n)] \to ((primeb n) = false))
 986 [ apply Hcut.
 987   (*qui autobatch non chiude il goal*)
 988   apply primeb_to_Prop
 989 | elim (primeb n)
 990   [ absurd (prime n)
 991     [ (*qui autobatch non chiude il goal*)
 992       assumption
 993     | assumption
 994     ]
 995   | reflexivity
 996   ]
 997 ]
 998 qed.
 999