helm/software/matita/library/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 include "nat/div_and_mod.ma".
  16 include "nat/minimization.ma".
  17 include "nat/sigma_and_pi.ma".
  18 include "nat/factorial.ma".
  19
  20 inductive divides (n,m:nat) : Prop \def
  21 witness : \forall p:nat.m = times n p \to divides n m.
  22
  23 interpretation "divides" 'divides n m = (cic:/matita/nat/primes/divides.ind#xpointer(1/1) n m).
  24 interpretation "not divides" 'ndivides n m =
  25  (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/primes/divides.ind#xpointer(1/1) n m)).
  26
  27 theorem reflexive_divides : reflexive nat divides.
  28 unfold reflexive.
  29 intros.
  30 exact (witness x x (S O) (times_n_SO x)).
  31 qed.
  32
  33 theorem divides_to_div_mod_spec :
  34 \forall n,m. O < n \to n \divides m \to div_mod_spec m n (m / n) O.
  35 intros.elim H1.rewrite > H2.
  36 constructor 1.assumption.
  37 apply (lt_O_n_elim n H).intros.
  38 rewrite < plus_n_O.
  39 rewrite > div_times.apply sym_times.
  40 qed.
  41
  42 theorem div_mod_spec_to_divides :
  43 \forall n,m,p. div_mod_spec m n p O \to n \divides m.
  44 intros.elim H.
  45 apply (witness n m p).
  46 rewrite < sym_times.
  47 rewrite > (plus_n_O (p*n)).assumption.
  48 qed.
  49
  50 theorem divides_to_mod_O:
  51 \forall n,m. O < n \to n \divides m \to (m \mod n) = O.
  52 intros.apply (div_mod_spec_to_eq2 m n (m / n) (m \mod n) (m / n) O).
  53 apply div_mod_spec_div_mod.assumption.
  54 apply divides_to_div_mod_spec.assumption.assumption.
  55 qed.
  56
  57 theorem mod_O_to_divides:
  58 \forall n,m. O< n \to (m \mod n) = O \to  n \divides m.
  59 intros.
  60 apply (witness n m (m / n)).
  61 rewrite > (plus_n_O (n * (m / n))).
  62 rewrite < H1.
  63 rewrite < sym_times.
  64 (* Andrea: perche' hint non lo trova ?*)
  65 apply div_mod.
  66 assumption.
  67 qed.
  68
  69 theorem divides_n_O: \forall n:nat. n \divides O.
  70 intro. apply (witness n O O).apply times_n_O.
  71 qed.
  72
  73 theorem divides_n_n: \forall n:nat. n \divides n.
  74 intro. apply (witness n n (S O)).apply times_n_SO.
  75 qed.
  76
  77 theorem divides_SO_n: \forall n:nat. (S O) \divides n.
  78 intro. apply (witness (S O) n n). simplify.apply plus_n_O.
  79 qed.
  80
  81 theorem divides_plus: \forall n,p,q:nat.
  82 n \divides p \to n \divides q \to n \divides p+q.
  83 intros.
  84 elim H.elim H1. apply (witness n (p+q) (n2+n1)).
  85 rewrite > H2.rewrite > H3.apply sym_eq.apply distr_times_plus.
  86 qed.
  87
  88 theorem divides_minus: \forall n,p,q:nat.
  89 divides n p \to divides n q \to divides n (p-q).
  90 intros.
  91 elim H.elim H1. apply (witness n (p-q) (n2-n1)).
  92 rewrite > H2.rewrite > H3.apply sym_eq.apply distr_times_minus.
  93 qed.
  94
  95 theorem divides_times: \forall n,m,p,q:nat.
  96 n \divides p \to m \divides q \to n*m \divides p*q.
  97 intros.
  98 elim H.elim H1. apply (witness (n*m) (p*q) (n2*n1)).
  99 rewrite > H2.rewrite > H3.
 100 apply (trans_eq nat ? (n*(m*(n2*n1)))).
 101 apply (trans_eq nat ? (n*(n2*(m*n1)))).
 102 apply assoc_times.
 103 apply eq_f.
 104 apply (trans_eq nat ? ((n2*m)*n1)).
 105 apply sym_eq. apply assoc_times.
 106 rewrite > (sym_times n2 m).apply assoc_times.
 107 apply sym_eq. apply assoc_times.
 108 qed.
 109
 110 theorem transitive_divides: transitive ? divides.
 111 unfold.
 112 intros.
 113 elim H.elim H1. apply (witness x z (n2*n)).
 114 rewrite > H3.rewrite > H2.
 115 apply assoc_times.
 116 qed.
 117
 118 variant trans_divides: \forall n,m,p.
 119  n \divides m \to m \divides p \to n \divides p \def transitive_divides.
 120
 121 theorem eq_mod_to_divides:\forall n,m,p. O< p \to
 122 mod n p = mod m p \to divides p (n-m).
 123 intros.
 124 cut (n \le m \or \not n \le m).
 125 elim Hcut.
 126 cut (n-m=O).
 127 rewrite > Hcut1.
 128 apply (witness p O O).
 129 apply times_n_O.
 130 apply eq_minus_n_m_O.
 131 assumption.
 132 apply (witness p (n-m) ((div n p)-(div m p))).
 133 rewrite > distr_times_minus.
 134 rewrite > sym_times.
 135 rewrite > (sym_times p).
 136 cut ((div n p)*p = n - (mod n p)).
 137 rewrite > Hcut1.
 138 rewrite > eq_minus_minus_minus_plus.
 139 rewrite > sym_plus.
 140 rewrite > H1.
 141 rewrite < div_mod.reflexivity.
 142 assumption.
 143 apply sym_eq.
 144 apply plus_to_minus.
 145 rewrite > sym_plus.
 146 apply div_mod.
 147 assumption.
 148 apply (decidable_le n m).
 149 qed.
 150
 151 theorem antisymmetric_divides: antisymmetric nat divides.
 152 unfold antisymmetric.intros.elim H. elim H1.
 153 apply (nat_case1 n2).intro.
 154 rewrite > H3.rewrite > H2.rewrite > H4.
 155 rewrite < times_n_O.reflexivity.
 156 intros.
 157 apply (nat_case1 n).intro.
 158 rewrite > H2.rewrite > H3.rewrite > H5.
 159 rewrite < times_n_O.reflexivity.
 160 intros.
 161 apply antisymmetric_le.
 162 rewrite > H2.rewrite > times_n_SO in \vdash (? % ?).
 163 apply le_times_r.rewrite > H4.apply le_S_S.apply le_O_n.
 164 rewrite > H3.rewrite > times_n_SO in \vdash (? % ?).
 165 apply le_times_r.rewrite > H5.apply le_S_S.apply le_O_n.
 166 qed.
 167
 168 (* divides le *)
 169 theorem divides_to_le : \forall n,m. O < m \to n \divides m \to n \le m.
 170 intros. elim H1.rewrite > H2.cut (O < n2).
 171 apply (lt_O_n_elim n2 Hcut).intro.rewrite < sym_times.
 172 simplify.rewrite < sym_plus.
 173 apply le_plus_n.
 174 elim (le_to_or_lt_eq O n2).
 175 assumption.
 176 absurd (O<m).assumption.
 177 rewrite > H2.rewrite < H3.rewrite < times_n_O.
 178 apply (not_le_Sn_n O).
 179 apply le_O_n.
 180 qed.
 181
 182 theorem divides_to_lt_O : \forall n,m. O < m \to n \divides m \to O < n.
 183 intros.elim H1.
 184 elim (le_to_or_lt_eq O n (le_O_n n)).
 185 assumption.
 186 rewrite < H3.absurd (O < m).assumption.
 187 rewrite > H2.rewrite < H3.
 188 simplify.exact (not_le_Sn_n O).
 189 qed.
 190
 191 (*a variant of or_div_mod *)
 192 theorem or_div_mod1: \forall n,q. O < q \to
 193 (divides q (S n)) \land S n = (S (div n q)) * q \lor
 194 (\lnot (divides q (S n)) \land S n= (div n q) * q + S (n\mod q)).
 195 intros.elim (or_div_mod n q H);elim H1
 196   [left.split
 197     [apply (witness ? ? (S (n/q))).
 198      rewrite > sym_times.assumption
 199     |assumption
 200     ]
 201   |right.split
 202     [intro.
 203      apply (not_eq_O_S (n \mod q)).
 204      (* come faccio a fare unfold nelleipotesi ? *)
 205      cut ((S n) \mod q = O)
 206       [rewrite < Hcut.
 207        apply (div_mod_spec_to_eq2 (S n) q (div (S n) q) (mod (S n) q) (div n q) (S (mod n q)))
 208         [apply div_mod_spec_div_mod.
 209          assumption
 210         |apply div_mod_spec_intro;assumption
 211         ]
 212       |apply divides_to_mod_O;assumption
 213       ]
 214     |assumption
 215     ]
 216   ]
 217 qed.
 218
 219 theorem divides_to_div: \forall n,m.divides n m \to m/n*n = m.
 220 intro.
 221 elim (le_to_or_lt_eq O n (le_O_n n))
 222   [rewrite > plus_n_O.
 223    rewrite < (divides_to_mod_O ? ? H H1).
 224    apply sym_eq.
 225    apply div_mod.
 226    assumption
 227   |elim H1.
 228    generalize in match H2.
 229    rewrite < H.
 230    simplify.
 231    intro.
 232    rewrite > H3.
 233    reflexivity
 234   ]
 235 qed.
 236
 237 theorem divides_div: \forall d,n. divides d n \to divides (n/d) n.
 238 intros.
 239 apply (witness ? ? d).
 240 apply sym_eq.
 241 apply divides_to_div.
 242 assumption.
 243 qed.
 244
 245 theorem div_div: \forall n,d:nat. O < n \to divides d n \to
 246 n/(n/d) = d.
 247 intros.
 248 apply (inj_times_l1 (n/d))
 249   [apply (lt_times_n_to_lt d)
 250     [apply (divides_to_lt_O ? ? H H1).
 251     |rewrite > divides_to_div;assumption
 252     ]
 253   |rewrite > divides_to_div
 254     [rewrite > sym_times.
 255      rewrite > divides_to_div
 256       [reflexivity
 257       |assumption
 258       ]
 259     |apply (witness ? ? d).
 260      apply sym_eq.
 261      apply divides_to_div.
 262      assumption
 263     ]
 264   ]
 265 qed.
 266
 267 theorem divides_to_eq_times_div_div_times: \forall a,b,c:nat.
 268 O \lt b \to c \divides b \to a * (b /c) = (a*b)/c.
 269 intros.
 270 elim H1.
 271 rewrite > H2.
 272 rewrite > (sym_times c n2).
 273 cut(O \lt c)
 274 [ rewrite > (lt_O_to_div_times n2 c)
 275   [ rewrite < assoc_times.
 276     rewrite > (lt_O_to_div_times (a *n2) c)
 277     [ reflexivity
 278     | assumption
 279     ]
 280   | assumption
 281   ]
 282 | apply (divides_to_lt_O c b);
 283     assumption.
 284 ]
 285 qed.
 286
 287 theorem eq_div_plus: \forall n,m,d. O < d \to
 288 divides d n \to divides d m \to
 289 (n + m ) / d = n/d + m/d.
 290 intros.
 291 elim H1.
 292 elim H2.
 293 rewrite > H3.rewrite > H4.
 294 rewrite < distr_times_plus.
 295 rewrite > sym_times.
 296 rewrite > sym_times in ⊢ (? ? ? (? (? % ?) ?)).
 297 rewrite > sym_times in ⊢ (? ? ? (? ? (? % ?))).
 298 rewrite > lt_O_to_div_times
 299   [rewrite > lt_O_to_div_times
 300     [rewrite > lt_O_to_div_times
 301       [reflexivity
 302       |assumption
 303       ]
 304     |assumption
 305     ]
 306   |assumption
 307   ]
 308 qed.
 309
 310 (* boolean divides *)
 311 definition divides_b : nat \to nat \to bool \def
 312 \lambda n,m :nat. (eqb (m \mod n) O).
 313
 314 theorem divides_b_to_Prop :
 315 \forall n,m:nat. O < n \to
 316 match divides_b n m with
 317 [ true \Rightarrow n \divides m
 318 | false \Rightarrow n \ndivides m].
 319 intros.unfold divides_b.
 320 apply eqb_elim.
 321 intro.simplify.apply mod_O_to_divides.assumption.assumption.
 322 intro.simplify.unfold Not.intro.apply H1.apply divides_to_mod_O.assumption.assumption.
 323 qed.
 324
 325 theorem divides_b_true_to_divides1:
 326 \forall n,m:nat. O < n \to
 327 (divides_b n m = true ) \to n \divides m.
 328 intros.
 329 change with
 330 match true with
 331 [ true \Rightarrow n \divides m
 332 | false \Rightarrow n \ndivides m].
 333 rewrite < H1.apply divides_b_to_Prop.
 334 assumption.
 335 qed.
 336
 337 theorem divides_b_true_to_divides:
 338 \forall n,m:nat. divides_b n m = true \to n \divides m.
 339 intros 2.apply (nat_case n)
 340   [apply (nat_case m)
 341     [intro.apply divides_n_n
 342     |simplify.intros.apply False_ind.
 343      apply not_eq_true_false.apply sym_eq.
 344      assumption
 345     ]
 346   |intros.
 347    apply divides_b_true_to_divides1
 348     [apply lt_O_S|assumption]
 349   ]
 350 qed.
 351
 352 theorem divides_b_false_to_not_divides1:
 353 \forall n,m:nat. O < n \to
 354 (divides_b n m = false ) \to n \ndivides m.
 355 intros.
 356 change with
 357 match false with
 358 [ true \Rightarrow n \divides m
 359 | false \Rightarrow n \ndivides m].
 360 rewrite < H1.apply divides_b_to_Prop.
 361 assumption.
 362 qed.
 363
 364 theorem divides_b_false_to_not_divides:
 365 \forall n,m:nat. divides_b n m = false \to n \ndivides m.
 366 intros 2.apply (nat_case n)
 367   [apply (nat_case m)
 368     [simplify.unfold Not.intros.
 369      apply not_eq_true_false.assumption
 370     |unfold Not.intros.elim H1.
 371      apply (not_eq_O_S m1).apply sym_eq.
 372      assumption
 373     ]
 374   |intros.
 375    apply divides_b_false_to_not_divides1
 376     [apply lt_O_S|assumption]
 377   ]
 378 qed.
 379
 380 theorem decidable_divides: \forall n,m:nat.O < n \to
 381 decidable (n \divides m).
 382 intros.unfold decidable.
 383 cut
 384 (match divides_b n m with
 385 [ true \Rightarrow n \divides m
 386 | false \Rightarrow n \ndivides m] \to n \divides m \lor n \ndivides m).
 387 apply Hcut.apply divides_b_to_Prop.assumption.
 388 elim (divides_b n m).left.apply H1.right.apply H1.
 389 qed.
 390
 391 theorem divides_to_divides_b_true : \forall n,m:nat. O < n \to
 392 n \divides m \to divides_b n m = true.
 393 intros.
 394 cut (match (divides_b n m) with
 395 [ true \Rightarrow n \divides m
 396 | false \Rightarrow n \ndivides m] \to ((divides_b n m) = true)).
 397 apply Hcut.apply divides_b_to_Prop.assumption.
 398 elim (divides_b n m).reflexivity.
 399 absurd (n \divides m).assumption.assumption.
 400 qed.
 401
 402 theorem divides_to_divides_b_true1 : \forall n,m:nat.
 403 O < m \to n \divides m \to divides_b n m = true.
 404 intro.
 405 elim (le_to_or_lt_eq O n (le_O_n n))
 406   [apply divides_to_divides_b_true
 407     [assumption|assumption]
 408   |apply False_ind.
 409    rewrite < H in H2.
 410    elim H2.
 411    simplify in H3.
 412    apply (not_le_Sn_O O).
 413    rewrite > H3 in H1.
 414    assumption
 415   ]
 416 qed.
 417
 418 theorem not_divides_to_divides_b_false: \forall n,m:nat. O < n \to
 419 \lnot(n \divides m) \to (divides_b n m) = false.
 420 intros.
 421 cut (match (divides_b n m) with
 422 [ true \Rightarrow n \divides m
 423 | false \Rightarrow n \ndivides m] \to ((divides_b n m) = false)).
 424 apply Hcut.apply divides_b_to_Prop.assumption.
 425 elim (divides_b n m).
 426 absurd (n \divides m).assumption.assumption.
 427 reflexivity.
 428 qed.
 429
 430 theorem divides_b_div_true:
 431 \forall d,n. O < n \to
 432   divides_b d n = true \to divides_b (n/d) n = true.
 433 intros.
 434 apply divides_to_divides_b_true1
 435   [assumption
 436   |apply divides_div.
 437    apply divides_b_true_to_divides.
 438    assumption
 439   ]
 440 qed.
 441
 442 theorem divides_b_true_to_lt_O: \forall n,m. O < n \to divides_b m n = true \to O < m.
 443 intros.
 444 elim (le_to_or_lt_eq ? ? (le_O_n m))
 445   [assumption
 446   |apply False_ind.
 447    elim H1.
 448    rewrite < H2 in H1.
 449    simplify in H1.
 450    apply (lt_to_not_eq O n H).
 451    apply sym_eq.
 452    apply eqb_true_to_eq.
 453    assumption
 454   ]
 455 qed.
 456
 457 (* divides and pi *)
 458 theorem divides_f_pi_f : \forall f:nat \to nat.\forall n,m,i:nat.
 459 m \le i \to i \le n+m \to f i \divides pi n f m.
 460 intros 5.elim n.simplify.
 461 cut (i = m).rewrite < Hcut.apply divides_n_n.
 462 apply antisymmetric_le.assumption.assumption.
 463 simplify.
 464 cut (i < S n1+m \lor i = S n1 + m).
 465 elim Hcut.
 466 apply (transitive_divides ? (pi n1 f m)).
 467 apply H1.apply le_S_S_to_le. assumption.
 468 apply (witness ? ? (f (S n1+m))).apply sym_times.
 469 rewrite > H3.
 470 apply (witness ? ? (pi n1 f m)).reflexivity.
 471 apply le_to_or_lt_eq.assumption.
 472 qed.
 473
 474 (*
 475 theorem mod_S_pi: \forall f:nat \to nat.\forall n,i:nat.
 476 i < n \to (S O) < (f i) \to (S (pi n f)) \mod (f i) = (S O).
 477 intros.cut (pi n f) \mod (f i) = O.
 478 rewrite < Hcut.
 479 apply mod_S.apply trans_lt O (S O).apply le_n (S O).assumption.
 480 rewrite > Hcut.assumption.
 481 apply divides_to_mod_O.apply trans_lt O (S O).apply le_n (S O).assumption.
 482 apply divides_f_pi_f.assumption.
 483 qed.
 484 *)
 485
 486 (* divides and fact *)
 487 theorem divides_fact : \forall n,i:nat.
 488 O < i \to i \le n \to i \divides n!.
 489 intros 3.elim n.absurd (O<i).assumption.apply (le_n_O_elim i H1).
 490 apply (not_le_Sn_O O).
 491 change with (i \divides (S n1)*n1!).
 492 apply (le_n_Sm_elim i n1 H2).
 493 intro.
 494 apply (transitive_divides ? n1!).
 495 apply H1.apply le_S_S_to_le. assumption.
 496 apply (witness ? ? (S n1)).apply sym_times.
 497 intro.
 498 rewrite > H3.
 499 apply (witness ? ? n1!).reflexivity.
 500 qed.
 501
 502 theorem mod_S_fact: \forall n,i:nat.
 503 (S O) < i \to i \le n \to (S n!) \mod i = (S O).
 504 intros.cut (n! \mod i = O).
 505 rewrite < Hcut.
 506 apply mod_S.apply (trans_lt O (S O)).apply (le_n (S O)).assumption.
 507 rewrite > Hcut.assumption.
 508 apply divides_to_mod_O.apply (trans_lt O (S O)).apply (le_n (S O)).assumption.
 509 apply divides_fact.apply (trans_lt O (S O)).apply (le_n (S O)).assumption.
 510 assumption.
 511 qed.
 512
 513 theorem not_divides_S_fact: \forall n,i:nat.
 514 (S O) < i \to i \le n \to i \ndivides S n!.
 515 intros.
 516 apply divides_b_false_to_not_divides.
 517 unfold divides_b.
 518 rewrite > mod_S_fact[simplify.reflexivity|assumption|assumption].
 519 qed.
 520
 521 (* prime *)
 522 definition prime : nat \to  Prop \def
 523 \lambda n:nat. (S O) < n \land
 524 (\forall m:nat. m \divides n \to (S O) < m \to  m = n).
 525
 526 theorem not_prime_O: \lnot (prime O).
 527 unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_O (S O) H1).
 528 qed.
 529
 530 theorem not_prime_SO: \lnot (prime (S O)).
 531 unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_n (S O) H1).
 532 qed.
 533
 534 theorem prime_to_lt_O: \forall p. prime p \to O < p.
 535 intros.elim H.apply lt_to_le.assumption.
 536 qed.
 537
 538 theorem prime_to_lt_SO: \forall p. prime p \to S O < p.
 539 intros.elim H.
 540 assumption.
 541 qed.
 542
 543 (* smallest factor *)
 544 definition smallest_factor : nat \to nat \def
 545 \lambda n:nat.
 546 match n with
 547 [ O \Rightarrow O
 548 | (S p) \Rightarrow
 549   match p with
 550   [ O \Rightarrow (S O)
 551   | (S q) \Rightarrow min_aux q (S (S O)) (\lambda m.(eqb ((S(S q)) \mod m) O))]].
 552
 553 (* it works !
 554 theorem example1 : smallest_factor (S(S(S O))) = (S(S(S O))).
 555 normalize.reflexivity.
 556 qed.
 557
 558 theorem example2: smallest_factor (S(S(S(S O)))) = (S(S O)).
 559 normalize.reflexivity.
 560 qed.
 561
 562 theorem example3 : smallest_factor (S(S(S(S(S(S(S O))))))) = (S(S(S(S(S(S(S O))))))).
 563 simplify.reflexivity.
 564 qed. *)
 565
 566 theorem lt_SO_smallest_factor:
 567 \forall n:nat. (S O) < n \to (S O) < (smallest_factor n).
 568 intro.
 569 apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O (S O) H).
 570 intro.apply (nat_case m).intro. apply False_ind.apply (not_le_Sn_n (S O) H).
 571 intros.
 572 change with
 573 (S O < min_aux m1 (S (S O)) (\lambda m.(eqb ((S(S m1)) \mod m) O))).
 574 apply (lt_to_le_to_lt ? (S (S O))).
 575 apply (le_n (S(S O))).
 576 cut ((S(S O)) = (S(S m1)) - m1).
 577 rewrite > Hcut.
 578 apply le_min_aux.
 579 apply sym_eq.apply plus_to_minus.
 580 rewrite < sym_plus.simplify.reflexivity.
 581 qed.
 582
 583 theorem lt_O_smallest_factor: \forall n:nat. O < n \to O < (smallest_factor n).
 584 intro.
 585 apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_n O H).
 586 intro.apply (nat_case m).intro.
 587 simplify.unfold lt.apply le_n.
 588 intros.apply (trans_lt ? (S O)).
 589 unfold lt.apply le_n.
 590 apply lt_SO_smallest_factor.unfold lt. apply le_S_S.
 591 apply le_S_S.apply le_O_n.
 592 qed.
 593
 594 theorem divides_smallest_factor_n :
 595 \forall n:nat. O < n \to smallest_factor n \divides n.
 596 intro.
 597 apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O O H).
 598 intro.apply (nat_case m).intro. simplify.
 599 apply (witness ? ? (S O)). simplify.reflexivity.
 600 intros.
 601 apply divides_b_true_to_divides.
 602 change with
 603 (eqb ((S(S m1)) \mod (min_aux m1 (S (S O))
 604   (\lambda m.(eqb ((S(S m1)) \mod m) O)))) O = true).
 605 apply f_min_aux_true.
 606 apply (ex_intro nat ? (S(S m1))).
 607 split.split.
 608 apply (le_S_S_to_le (S (S O)) (S (S m1)) ?).
 609 apply (minus_le_O_to_le (S (S (S O))) (S (S (S m1))) ?).
 610 apply (le_n O).
 611 rewrite < sym_plus. simplify. apply le_n.
 612 apply (eq_to_eqb_true (mod (S (S m1)) (S (S m1))) O ?).
 613 apply (mod_n_n (S (S m1)) ?).
 614 apply (H).
 615 qed.
 616
 617 theorem le_smallest_factor_n :
 618 \forall n:nat. smallest_factor n \le n.
 619 intro.apply (nat_case n).simplify.apply le_n.
 620 intro.apply (nat_case m).simplify.apply le_n.
 621 intro.apply divides_to_le.
 622 unfold lt.apply le_S_S.apply le_O_n.
 623 apply divides_smallest_factor_n.
 624 unfold lt.apply le_S_S.apply le_O_n.
 625 qed.
 626
 627 theorem lt_smallest_factor_to_not_divides: \forall n,i:nat.
 628 (S O) < n \to (S O) < i \to i < (smallest_factor n) \to i \ndivides n.
 629 intros 2.
 630 apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O (S O) H).
 631 intro.apply (nat_case m).intro. apply False_ind.apply (not_le_Sn_n (S O) H).
 632 intros.
 633 apply divides_b_false_to_not_divides.
 634 apply (lt_min_aux_to_false
 635 (\lambda i:nat.eqb ((S(S m1)) \mod i) O) (S (S O)) m1 i).
 636 assumption.
 637 assumption.
 638 qed.
 639
 640 theorem prime_smallest_factor_n :
 641 \forall n:nat. (S O) < n \to prime (smallest_factor n).
 642 intro.change with ((S(S O)) \le n \to (S O) < (smallest_factor n) \land
 643 (\forall m:nat. m \divides smallest_factor n \to (S O) < m \to  m = (smallest_factor n))).
 644 intro.split.
 645 apply lt_SO_smallest_factor.assumption.
 646 intros.
 647 cut (le m (smallest_factor n)).
 648 elim (le_to_or_lt_eq m (smallest_factor n) Hcut).
 649 absurd (m \divides n).
 650 apply (transitive_divides m (smallest_factor n)).
 651 assumption.
 652 apply divides_smallest_factor_n.
 653 apply (trans_lt ? (S O)). unfold lt. apply le_n. exact H.
 654 apply lt_smallest_factor_to_not_divides.
 655 exact H.assumption.assumption.assumption.
 656 apply divides_to_le.
 657 apply (trans_lt O (S O)).
 658 apply (le_n (S O)).
 659 apply lt_SO_smallest_factor.
 660 exact H.
 661 assumption.
 662 qed.
 663
 664 theorem prime_to_smallest_factor: \forall n. prime n \to
 665 smallest_factor n = n.
 666 intro.apply (nat_case n).intro.apply False_ind.apply (not_prime_O H).
 667 intro.apply (nat_case m).intro.apply False_ind.apply (not_prime_SO H).
 668 intro.
 669 change with
 670 ((S O) < (S(S m1)) \land
 671 (\forall m:nat. m \divides S(S m1) \to (S O) < m \to  m = (S(S m1))) \to
 672 smallest_factor (S(S m1)) = (S(S m1))).
 673 intro.elim H.apply H2.
 674 apply divides_smallest_factor_n.
 675 apply (trans_lt ? (S O)).unfold lt. apply le_n.assumption.
 676 apply lt_SO_smallest_factor.
 677 assumption.
 678 qed.
 679
 680 (* a number n > O is prime iff its smallest factor is n *)
 681 definition primeb \def \lambda n:nat.
 682 match n with
 683 [ O \Rightarrow false
 684 | (S p) \Rightarrow
 685   match p with
 686   [ O \Rightarrow false
 687   | (S q) \Rightarrow eqb (smallest_factor (S(S q))) (S(S q))]].
 688
 689 (* it works!
 690 theorem example4 : primeb (S(S(S O))) = true.
 691 normalize.reflexivity.
 692 qed.
 693
 694 theorem example5 : primeb (S(S(S(S(S(S O)))))) = false.
 695 normalize.reflexivity.
 696 qed.
 697
 698 theorem example6 : primeb (S(S(S(S((S(S(S(S(S(S(S O)))))))))))) = true.
 699 normalize.reflexivity.
 700 qed.
 701
 702 theorem example7 : primeb (S(S(S(S(S(S((S(S(S(S((S(S(S(S(S(S(S O))))))))))))))))))) = true.
 703 normalize.reflexivity.
 704 qed. *)
 705
 706 theorem primeb_to_Prop: \forall n.
 707 match primeb n with
 708 [ true \Rightarrow prime n
 709 | false \Rightarrow \lnot (prime n)].
 710 intro.
 711 apply (nat_case n).simplify.unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_O (S O) H1).
 712 intro.apply (nat_case m).simplify.unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_n (S O) H1).
 713 intro.
 714 change with
 715 match eqb (smallest_factor (S(S m1))) (S(S m1)) with
 716 [ true \Rightarrow prime (S(S m1))
 717 | false \Rightarrow \lnot (prime (S(S m1)))].
 718 apply (eqb_elim (smallest_factor (S(S m1))) (S(S m1))).
 719 intro.simplify.
 720 rewrite < H.
 721 apply prime_smallest_factor_n.
 722 unfold lt.apply le_S_S.apply le_S_S.apply le_O_n.
 723 intro.simplify.
 724 change with (prime (S(S m1)) \to False).
 725 intro.apply H.
 726 apply prime_to_smallest_factor.
 727 assumption.
 728 qed.
 729
 730 theorem primeb_true_to_prime : \forall n:nat.
 731 primeb n = true \to prime n.
 732 intros.change with
 733 match true with
 734 [ true \Rightarrow prime n
 735 | false \Rightarrow \lnot (prime n)].
 736 rewrite < H.
 737 apply primeb_to_Prop.
 738 qed.
 739
 740 theorem primeb_false_to_not_prime : \forall n:nat.
 741 primeb n = false \to \lnot (prime n).
 742 intros.change with
 743 match false with
 744 [ true \Rightarrow prime n
 745 | false \Rightarrow \lnot (prime n)].
 746 rewrite < H.
 747 apply primeb_to_Prop.
 748 qed.
 749
 750 theorem decidable_prime : \forall n:nat.decidable (prime n).
 751 intro.unfold decidable.
 752 cut
 753 (match primeb n with
 754 [ true \Rightarrow prime n
 755 | false \Rightarrow \lnot (prime n)] \to (prime n) \lor \lnot (prime n)).
 756 apply Hcut.apply primeb_to_Prop.
 757 elim (primeb n).left.apply H.right.apply H.
 758 qed.
 759
 760 theorem prime_to_primeb_true: \forall n:nat.
 761 prime n \to primeb n = true.
 762 intros.
 763 cut (match (primeb n) with
 764 [ true \Rightarrow prime n
 765 | false \Rightarrow \lnot (prime n)] \to ((primeb n) = true)).
 766 apply Hcut.apply primeb_to_Prop.
 767 elim (primeb n).reflexivity.
 768 absurd (prime n).assumption.assumption.
 769 qed.
 770
 771 theorem not_prime_to_primeb_false: \forall n:nat.
 772 \lnot(prime n) \to primeb n = false.
 773 intros.
 774 cut (match (primeb n) with
 775 [ true \Rightarrow prime n
 776 | false \Rightarrow \lnot (prime n)] \to ((primeb n) = false)).
 777 apply Hcut.apply primeb_to_Prop.
 778 elim (primeb n).
 779 absurd (prime n).assumption.assumption.
 780 reflexivity.
 781 qed.
 782