helm/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 set "baseuri" "cic:/matita/nat/primes".
  16
  17 include "nat/div_and_mod.ma".
  18 include "nat/minimization.ma".
  19 include "nat/sigma_and_pi.ma".
  20 include "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/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/nat/primes/divides.ind#xpointer(1/1) n m)).
  28
  29 theorem reflexive_divides : reflexive nat divides.
  30 simplify.
  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 (div m n) O.
  37 intros.elim H1.rewrite > H2.
  38 constructor 1.assumption.
  39 apply lt_O_n_elim n H.intros.
  40 rewrite < plus_n_O.
  41 rewrite > div_times.apply sym_times.
  42 qed.
  43
  44 theorem div_mod_spec_to_div :
  45 \forall n,m,p. div_mod_spec m n p O \to n \divides m.
  46 intros.elim H.
  47 apply witness n m p.
  48 rewrite < sym_times.
  49 rewrite > plus_n_O (p*n).assumption.
  50 qed.
  51
  52 theorem divides_to_mod_O:
  53 \forall n,m. O < n \to n \divides m \to (mod m n) = O.
  54 intros.apply div_mod_spec_to_eq2 m n (div m n) (mod m n) (div m n) O.
  55 apply div_mod_spec_div_mod.assumption.
  56 apply divides_to_div_mod_spec.assumption.assumption.
  57 qed.
  58
  59 theorem mod_O_to_divides:
  60 \forall n,m. O< n \to (mod m n) = O \to  n \divides m.
  61 intros.
  62 apply witness n m (div m n).
  63 rewrite > plus_n_O (n*div m n).
  64 rewrite < H1.
  65 rewrite < sym_times.
  66 (* Andrea: perche' hint non lo trova ?*)
  67 apply div_mod.
  68 assumption.
  69 qed.
  70
  71 theorem divides_n_O: \forall n:nat. n \divides O.
  72 intro. apply witness n O O.apply times_n_O.
  73 qed.
  74
  75 theorem divides_SO_n: \forall n:nat. (S O) \divides n.
  76 intro. apply witness (S O) n n. simplify.apply plus_n_O.
  77 qed.
  78
  79 theorem divides_plus: \forall n,p,q:nat.
  80 n \divides p \to n \divides q \to n \divides p+q.
  81 intros.
  82 elim H.elim H1. apply witness n (p+q) (n2+n1).
  83 rewrite > H2.rewrite > H3.apply sym_eq.apply distr_times_plus.
  84 qed.
  85
  86 theorem divides_minus: \forall n,p,q:nat.
  87 divides n p \to divides n q \to divides n (p-q).
  88 intros.
  89 elim H.elim H1. apply witness n (p-q) (n2-n1).
  90 rewrite > H2.rewrite > H3.apply sym_eq.apply distr_times_minus.
  91 qed.
  92
  93 theorem divides_times: \forall n,m,p,q:nat.
  94 n \divides p \to m \divides q \to n*m \divides p*q.
  95 intros.
  96 elim H.elim H1. apply witness (n*m) (p*q) (n2*n1).
  97 rewrite > H2.rewrite > H3.
  98 apply trans_eq nat ? (n*(m*(n2*n1))).
  99 apply trans_eq nat ? (n*(n2*(m*n1))).
 100 apply assoc_times.
 101 apply eq_f.
 102 apply trans_eq nat ? ((n2*m)*n1).
 103 apply sym_eq. apply assoc_times.
 104 rewrite > sym_times n2 m.apply assoc_times.
 105 apply sym_eq. apply assoc_times.
 106 qed.
 107
 108 theorem transitive_divides: \forall n,m,p.
 109 n \divides m \to m \divides p \to n \divides p.
 110 intros.
 111 elim H.elim H1. apply witness n p (n2*n1).
 112 rewrite > H3.rewrite > H2.
 113 apply assoc_times.
 114 qed.
 115
 116 (* divides le *)
 117 theorem divides_to_le : \forall n,m. O < m \to n \divides m \to n \le m.
 118 intros. elim H1.rewrite > H2.cut O < n2.
 119 apply lt_O_n_elim n2 Hcut.intro.rewrite < sym_times.
 120 simplify.rewrite < sym_plus.
 121 apply le_plus_n.
 122 elim le_to_or_lt_eq O n2.
 123 assumption.
 124 absurd O<m.assumption.
 125 rewrite > H2.rewrite < H3.rewrite < times_n_O.
 126 apply not_le_Sn_n O.
 127 apply le_O_n.
 128 qed.
 129
 130 theorem divides_to_lt_O : \forall n,m. O < m \to n \divides m \to O < n.
 131 intros.elim H1.
 132 elim le_to_or_lt_eq O n (le_O_n n).
 133 assumption.
 134 rewrite < H3.absurd O < m.assumption.
 135 rewrite > H2.rewrite < H3.
 136 simplify.exact not_le_Sn_n O.
 137 qed.
 138
 139 (* boolean divides *)
 140 definition divides_b : nat \to nat \to bool \def
 141 \lambda n,m :nat. (eqb (mod m n) O).
 142
 143 theorem divides_b_to_Prop :
 144 \forall n,m:nat. O < n \to
 145 match divides_b n m with
 146 [ true \Rightarrow n \divides m
 147 | false \Rightarrow n \ndivides m].
 148 intros.
 149 change with
 150 match eqb (mod m n) O with
 151 [ true \Rightarrow n \divides m
 152 | false \Rightarrow n \ndivides m].
 153 apply eqb_elim.
 154 intro.simplify.apply mod_O_to_divides.assumption.assumption.
 155 intro.simplify.intro.apply H1.apply divides_to_mod_O.assumption.assumption.
 156 qed.
 157
 158 theorem divides_b_true_to_divides :
 159 \forall n,m:nat. O < n \to
 160 (divides_b n m = true ) \to n \divides m.
 161 intros.
 162 change with
 163 match true with
 164 [ true \Rightarrow n \divides m
 165 | false \Rightarrow n \ndivides m].
 166 rewrite < H1.apply divides_b_to_Prop.
 167 assumption.
 168 qed.
 169
 170 theorem divides_b_false_to_not_divides :
 171 \forall n,m:nat. O < n \to
 172 (divides_b n m = false ) \to n \ndivides m.
 173 intros.
 174 change with
 175 match false with
 176 [ true \Rightarrow n \divides m
 177 | false \Rightarrow n \ndivides m].
 178 rewrite < H1.apply divides_b_to_Prop.
 179 assumption.
 180 qed.
 181
 182 theorem decidable_divides: \forall n,m:nat.O < n \to
 183 decidable (n \divides m).
 184 intros.change with (n \divides m) \lor n \ndivides m.
 185 cut
 186 match divides_b n m with
 187 [ true \Rightarrow n \divides m
 188 | false \Rightarrow n \ndivides m] \to n \divides m \lor n \ndivides m.
 189 apply Hcut.apply divides_b_to_Prop.assumption.
 190 elim (divides_b n m).left.apply H1.right.apply H1.
 191 qed.
 192
 193 theorem divides_to_divides_b_true : \forall n,m:nat. O < n \to
 194 n \divides m \to divides_b n m = true.
 195 intros.
 196 cut match (divides_b n m) with
 197 [ true \Rightarrow n \divides m
 198 | false \Rightarrow n \ndivides m] \to ((divides_b n m) = true).
 199 apply Hcut.apply divides_b_to_Prop.assumption.
 200 elim divides_b n m.reflexivity.
 201 absurd (n \divides m).assumption.assumption.
 202 qed.
 203
 204 theorem not_divides_to_divides_b_false: \forall n,m:nat. O < n \to
 205 \lnot(n \divides m) \to (divides_b n m) = false.
 206 intros.
 207 cut match (divides_b n m) with
 208 [ true \Rightarrow n \divides m
 209 | false \Rightarrow n \ndivides m] \to ((divides_b n m) = false).
 210 apply Hcut.apply divides_b_to_Prop.assumption.
 211 elim divides_b n m.
 212 absurd (n \divides m).assumption.assumption.
 213 reflexivity.
 214 qed.
 215
 216 (* divides and pi *)
 217 theorem divides_f_pi_f : \forall f:nat \to nat.\forall n,i:nat.
 218 i < n \to f i \divides pi n f.
 219 intros 3.elim n.apply False_ind.apply not_le_Sn_O i H.
 220 simplify.
 221 apply le_n_Sm_elim (S i) n1 H1.
 222 intro.
 223 apply transitive_divides ? (pi n1 f).
 224 apply H.simplify.apply le_S_S_to_le. assumption.
 225 apply witness ? ? (f n1).apply sym_times.
 226 intro.cut i = n1.
 227 rewrite > Hcut.
 228 apply witness ? ? (pi n1 f).reflexivity.
 229 apply inj_S.assumption.
 230 qed.
 231
 232 theorem mod_S_pi: \forall f:nat \to nat.\forall n,i:nat.
 233 i < n \to (S O) < (f i) \to mod (S (pi n f)) (f i) = (S O).
 234 intros.cut mod (pi n f) (f i) = O.
 235 rewrite < Hcut.
 236 apply mod_S.apply trans_lt O (S O).apply le_n (S O).assumption.
 237 rewrite > Hcut.assumption.
 238 apply divides_to_mod_O.apply trans_lt O (S O).apply le_n (S O).assumption.
 239 apply divides_f_pi_f.assumption.
 240 qed.
 241
 242 (* divides and fact *)
 243 theorem divides_fact : \forall n,i:nat.
 244 O < i \to i \le n \to i \divides n!.
 245 intros 3.elim n.absurd O<i.assumption.apply le_n_O_elim i H1.
 246 apply not_le_Sn_O O.
 247 change with i \divides (S n1)*n1!.
 248 apply le_n_Sm_elim i n1 H2.
 249 intro.
 250 apply transitive_divides ? n1!.
 251 apply H1.apply le_S_S_to_le. assumption.
 252 apply witness ? ? (S n1).apply sym_times.
 253 intro.
 254 rewrite > H3.
 255 apply witness ? ? n1!.reflexivity.
 256 qed.
 257
 258 theorem mod_S_fact: \forall n,i:nat.
 259 (S O) < i \to i \le n \to mod (S n!) i = (S O).
 260 intros.cut mod n! i = O.
 261 rewrite < Hcut.
 262 apply mod_S.apply trans_lt O (S O).apply le_n (S O).assumption.
 263 rewrite > Hcut.assumption.
 264 apply divides_to_mod_O.apply trans_lt O (S O).apply le_n (S O).assumption.
 265 apply divides_fact.apply trans_lt O (S O).apply le_n (S O).assumption.
 266 assumption.
 267 qed.
 268
 269 theorem not_divides_S_fact: \forall n,i:nat.
 270 (S O) < i \to i \le n \to i \ndivides S n!.
 271 intros.
 272 apply divides_b_false_to_not_divides.
 273 apply trans_lt O (S O).apply le_n (S O).assumption.
 274 change with (eqb (mod (S n!) i) O) = false.
 275 rewrite > mod_S_fact.simplify.reflexivity.
 276 assumption.assumption.
 277 qed.
 278
 279 (* prime *)
 280 definition prime : nat \to  Prop \def
 281 \lambda n:nat. (S O) < n \land
 282 (\forall m:nat. m \divides n \to (S O) < m \to  m = n).
 283
 284 theorem not_prime_O: \lnot (prime O).
 285 simplify.intro.elim H.apply not_le_Sn_O (S O) H1.
 286 qed.
 287
 288 theorem not_prime_SO: \lnot (prime (S O)).
 289 simplify.intro.elim H.apply not_le_Sn_n (S O) H1.
 290 qed.
 291
 292 (* smallest factor *)
 293 definition smallest_factor : nat \to nat \def
 294 \lambda n:nat.
 295 match n with
 296 [ O \Rightarrow O
 297 | (S p) \Rightarrow
 298   match p with
 299   [ O \Rightarrow (S O)
 300   | (S q) \Rightarrow min_aux q (S(S q)) (\lambda m.(eqb (mod (S(S q)) m) O))]].
 301
 302 (* it works !
 303 theorem example1 : smallest_prime_factor (S(S(S O))) = (S(S(S O))).
 304 normalize.reflexivity.
 305 qed.
 306
 307 theorem example2: smallest_prime_factor (S(S(S(S O)))) = (S(S O)).
 308 normalize.reflexivity.
 309 qed.
 310
 311 theorem example3 : smallest_prime_factor (S(S(S(S(S(S(S O))))))) = (S(S(S(S(S(S(S O))))))).
 312 simplify.reflexivity.
 313 qed. *)
 314
 315 theorem lt_SO_smallest_factor:
 316 \forall n:nat. (S O) < n \to (S O) < (smallest_factor n).
 317 intro.
 318 apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S O) H.
 319 intro.apply nat_case m.intro. apply False_ind.apply not_le_Sn_n (S O) H.
 320 intros.
 321 change with
 322 S O < min_aux m1 (S(S m1)) (\lambda m.(eqb (mod (S(S m1)) m) O)).
 323 apply lt_to_le_to_lt ? (S (S O)).
 324 apply le_n (S(S O)).
 325 cut (S(S O)) = (S(S m1)) - m1.
 326 rewrite > Hcut.
 327 apply le_min_aux.
 328 apply sym_eq.apply plus_to_minus.apply le_S.apply le_n_Sn.
 329 rewrite < sym_plus.simplify.reflexivity.
 330 qed.
 331
 332 theorem lt_O_smallest_factor: \forall n:nat. O < n \to O < (smallest_factor n).
 333 intro.
 334 apply nat_case n.intro.apply False_ind.apply not_le_Sn_n O H.
 335 intro.apply nat_case m.intro.
 336 simplify.apply le_n.
 337 intros.apply trans_lt ? (S O).
 338 simplify. apply le_n.
 339 apply lt_SO_smallest_factor.simplify. apply le_S_S.
 340 apply le_S_S.apply le_O_n.
 341 qed.
 342
 343 theorem divides_smallest_factor_n :
 344 \forall n:nat. O < n \to smallest_factor n \divides n.
 345 intro.
 346 apply nat_case n.intro.apply False_ind.apply not_le_Sn_O O H.
 347 intro.apply nat_case m.intro. simplify.
 348 apply witness ? ? (S O). simplify.reflexivity.
 349 intros.
 350 apply divides_b_true_to_divides.
 351 apply lt_O_smallest_factor ? H.
 352 change with
 353 eqb (mod (S(S m1)) (min_aux m1 (S(S m1))
 354   (\lambda m.(eqb (mod (S(S m1)) m) O)))) O = true.
 355 apply f_min_aux_true.
 356 apply ex_intro nat ? (S(S m1)).
 357 split.split.
 358 apply le_minus_m.apply le_n.
 359 rewrite > mod_n_n.reflexivity.
 360 apply trans_lt ? (S O).apply le_n (S O).simplify.
 361 apply le_S_S.apply le_S_S.apply le_O_n.
 362 qed.
 363
 364 theorem le_smallest_factor_n :
 365 \forall n:nat. smallest_factor n \le n.
 366 intro.apply nat_case n.simplify.reflexivity.
 367 intro.apply nat_case m.simplify.reflexivity.
 368 intro.apply divides_to_le.
 369 simplify.apply le_S_S.apply le_O_n.
 370 apply divides_smallest_factor_n.
 371 simplify.apply le_S_S.apply le_O_n.
 372 qed.
 373
 374 theorem lt_smallest_factor_to_not_divides: \forall n,i:nat.
 375 (S O) < n \to (S O) < i \to i < (smallest_factor n) \to i \ndivides n.
 376 intros 2.
 377 apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S O) H.
 378 intro.apply nat_case m.intro. apply False_ind.apply not_le_Sn_n (S O) H.
 379 intros.
 380 apply divides_b_false_to_not_divides.
 381 apply trans_lt O (S O).apply le_n (S O).assumption.
 382 change with (eqb (mod (S(S m1)) i) O) = false.
 383 apply lt_min_aux_to_false
 384 (\lambda i:nat.eqb (mod (S(S m1)) i) O) (S(S m1)) m1 i.
 385 cut (S(S O)) = (S(S m1)-m1).
 386 rewrite < Hcut.exact H1.
 387 apply sym_eq. apply plus_to_minus.
 388 apply le_S.apply le_n_Sn.
 389 rewrite < sym_plus.simplify.reflexivity.
 390 exact H2.
 391 qed.
 392
 393 theorem prime_smallest_factor_n :
 394 \forall n:nat. (S O) < n \to prime (smallest_factor n).
 395 intro. change with (S(S O)) \le n \to (S O) < (smallest_factor n) \land
 396 (\forall m:nat. m \divides smallest_factor n \to (S O) < m \to  m = (smallest_factor n)).
 397 intro.split.
 398 apply lt_SO_smallest_factor.assumption.
 399 intros.
 400 cut le m (smallest_factor n).
 401 elim le_to_or_lt_eq m (smallest_factor n) Hcut.
 402 absurd m \divides n.
 403 apply transitive_divides m (smallest_factor n).
 404 assumption.
 405 apply divides_smallest_factor_n.
 406 apply trans_lt ? (S O). simplify. apply le_n. exact H.
 407 apply lt_smallest_factor_to_not_divides.
 408 exact H.assumption.assumption.assumption.
 409 apply divides_to_le.
 410 apply trans_lt O (S O).
 411 apply le_n (S O).
 412 apply lt_SO_smallest_factor.
 413 exact H.
 414 assumption.
 415 qed.
 416
 417 theorem prime_to_smallest_factor: \forall n. prime n \to
 418 smallest_factor n = n.
 419 intro.apply nat_case n.intro.apply False_ind.apply not_prime_O H.
 420 intro.apply nat_case m.intro.apply False_ind.apply not_prime_SO H.
 421 intro.
 422 change with
 423 (S O) < (S(S m1)) \land
 424 (\forall m:nat. m \divides S(S m1) \to (S O) < m \to  m = (S(S m1))) \to
 425 smallest_factor (S(S m1)) = (S(S m1)).
 426 intro.elim H.apply H2.
 427 apply divides_smallest_factor_n.
 428 apply trans_lt ? (S O).simplify. apply le_n.assumption.
 429 apply lt_SO_smallest_factor.
 430 assumption.
 431 qed.
 432
 433 (* a number n > O is prime iff its smallest factor is n *)
 434 definition primeb \def \lambda n:nat.
 435 match n with
 436 [ O \Rightarrow false
 437 | (S p) \Rightarrow
 438   match p with
 439   [ O \Rightarrow false
 440   | (S q) \Rightarrow eqb (smallest_factor (S(S q))) (S(S q))]].
 441
 442 (* it works!
 443 theorem example4 : primeb (S(S(S O))) = true.
 444 normalize.reflexivity.
 445 qed.
 446
 447 theorem example5 : primeb (S(S(S(S(S(S O)))))) = false.
 448 normalize.reflexivity.
 449 qed.
 450
 451 theorem example6 : primeb (S(S(S(S((S(S(S(S(S(S(S O)))))))))))) = true.
 452 normalize.reflexivity.
 453 qed.
 454
 455 theorem example7 : primeb (S(S(S(S(S(S((S(S(S(S((S(S(S(S(S(S(S O))))))))))))))))))) = true.
 456 normalize.reflexivity.
 457 qed. *)
 458
 459 theorem primeb_to_Prop: \forall n.
 460 match primeb n with
 461 [ true \Rightarrow prime n
 462 | false \Rightarrow \lnot (prime n)].
 463 intro.
 464 apply nat_case n.simplify.intro.elim H.apply not_le_Sn_O (S O) H1.
 465 intro.apply nat_case m.simplify.intro.elim H.apply not_le_Sn_n (S O) H1.
 466 intro.
 467 change with
 468 match eqb (smallest_factor (S(S m1))) (S(S m1)) with
 469 [ true \Rightarrow prime (S(S m1))
 470 | false \Rightarrow \lnot (prime (S(S m1)))].
 471 apply eqb_elim (smallest_factor (S(S m1))) (S(S m1)).
 472 intro.change with prime (S(S m1)).
 473 rewrite < H.
 474 apply prime_smallest_factor_n.
 475 simplify.apply le_S_S.apply le_S_S.apply le_O_n.
 476 intro.change with \lnot (prime (S(S m1))).
 477 change with prime (S(S m1)) \to False.
 478 intro.apply H.
 479 apply prime_to_smallest_factor.
 480 assumption.
 481 qed.
 482
 483 theorem primeb_true_to_prime : \forall n:nat.
 484 primeb n = true \to prime n.
 485 intros.change with
 486 match true with
 487 [ true \Rightarrow prime n
 488 | false \Rightarrow \lnot (prime n)].
 489 rewrite < H.
 490 apply primeb_to_Prop.
 491 qed.
 492
 493 theorem primeb_false_to_not_prime : \forall n:nat.
 494 primeb n = false \to \lnot (prime n).
 495 intros.change with
 496 match false with
 497 [ true \Rightarrow prime n
 498 | false \Rightarrow \lnot (prime n)].
 499 rewrite < H.
 500 apply primeb_to_Prop.
 501 qed.
 502
 503 theorem decidable_prime : \forall n:nat.decidable (prime n).
 504 intro.change with (prime n) \lor \lnot (prime n).
 505 cut
 506 match primeb n with
 507 [ true \Rightarrow prime n
 508 | false \Rightarrow \lnot (prime n)] \to (prime n) \lor \lnot (prime n).
 509 apply Hcut.apply primeb_to_Prop.
 510 elim (primeb n).left.apply H.right.apply H.
 511 qed.
 512
 513 theorem prime_to_primeb_true: \forall n:nat.
 514 prime n \to primeb n = true.
 515 intros.
 516 cut match (primeb n) with
 517 [ true \Rightarrow prime n
 518 | false \Rightarrow \lnot (prime n)] \to ((primeb n) = true).
 519 apply Hcut.apply primeb_to_Prop.
 520 elim primeb n.reflexivity.
 521 absurd (prime n).assumption.assumption.
 522 qed.
 523
 524 theorem not_prime_to_primeb_false: \forall n:nat.
 525 \lnot(prime n) \to primeb n = false.
 526 intros.
 527 cut match (primeb n) with
 528 [ true \Rightarrow prime n
 529 | false \Rightarrow \lnot (prime n)] \to ((primeb n) = false).
 530 apply Hcut.apply primeb_to_Prop.
 531 elim primeb n.
 532 absurd (prime n).assumption.assumption.
 533 reflexivity.
 534 qed.
 535