matita/matita/lib/arithmetics/primes.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "arithmetics/factorial.ma".
  13 include "arithmetics/minimization.ma".
  14
  15 inductive divides (n,m:nat) : Prop ≝
  16 quotient: ∀q:nat.m = times n q → divides n m.
  17
  18 interpretation "divides" 'divides n m = (divides n m).
  19 interpretation "not divides" 'ndivides n m = (Not (divides n m)).
  20
  21 theorem reflexive_divides : reflexive nat divides.
  22 /2/ qed.
  23
  24 theorem divides_to_div_mod_spec :
  25 ∀n,m. O < n → n ∣ m → div_mod_spec m n (m / n) O.
  26 #n #m #posn * #q #eqm % // >eqm
  27 >commutative_times >div_times //
  28 qed.
  29
  30 theorem div_mod_spec_to_divides :
  31 ∀n,m,q. div_mod_spec m n q O → n ∣ m.
  32 #n #m #q * #posn #eqm /2/
  33 qed.
  34
  35 theorem divides_to_mod_O:
  36 ∀n,m. O < n → n ∣ m → (m \mod n) = O.
  37 #n #m #posn #divnm
  38 @(div_mod_spec_to_eq2 m n (m / n) (m \mod n) (m / n) O) /2/
  39 qed.
  40
  41 theorem mod_O_to_divides:
  42 ∀n,m. O < n → (m \mod n) = O →  n ∣ m.
  43 /2/ qed.
  44
  45 theorem divides_n_O: ∀n:nat. n ∣ O.
  46 /2/ qed.
  47
  48 theorem divides_n_n: ∀n:nat. n ∣ n.
  49 /2/ qed.
  50
  51 theorem divides_SO_n: ∀n:nat. 1 ∣ n.
  52 /2/ qed.
  53
  54 theorem divides_plus: ∀n,p,q:nat.
  55 n ∣ p → n ∣ q → n ∣ p+q.
  56 #n #p #q * #d1 #H * #d2 #H1 @(quotient ?? (d1+d2))
  57 >H >H1 //
  58 qed.
  59
  60 theorem divides_minus: ∀n,p,q:nat.
  61 n ∣ p → n ∣ q → n ∣ (p-q).
  62 #n #p #q * #d1 #H * #d2 #H1 @(quotient ?? (d1-d2))
  63 >H >H1 //
  64 qed.
  65
  66 theorem divides_times: ∀n,m,p,q:nat.
  67 n ∣ p → m ∣ q → n*m ∣ p*q.
  68 #n #m #p #q * #d1 #H * #d2 #H1 @(quotient ?? (d1*d2))
  69 >H >associative_times >associative_times @eq_f //
  70 qed.
  71
  72 theorem transitive_divides: transitive ? divides.
  73 #a #b #c * #d1 #H * #d2 #H1 @(quotient ?? (d1*d2))
  74 >H1 >H //
  75 qed.
  76
  77 theorem eq_mod_to_divides: ∀n,m,q. O < q →
  78   mod n q = mod m q → q ∣ (n-m).
  79 #n #m #q #posq #eqmod @(leb_elim n m) #nm
  80   [cut (n-m=O) /2/
  81   |@(quotient ?? ((div n q)-(div m q)))
  82    >distributive_times_minus >commutative_times
  83    >(commutative_times q) cut((n/q)*q = n - (n \mod q)) [//] #H
  84    >H >minus_plus >eqmod >commutative_plus
  85    <div_mod //
  86   ]
  87 qed.
  88
  89 theorem divides_to_le : ∀n,m. O < m → n ∣ m → n ≤ m.
  90 #n #m #posm * #d (cases d)
  91   [#eqm @False_ind /2/ |#p #eqm >eqm // ]
  92 qed.
  93
  94 theorem antisymmetric_divides: ∀n,m. n ∣ m → m ∣ n → n = m.
  95 #n #m #divnm #divmn (cases (le_to_or_lt_eq … (le_O_n n))) #Hn
  96   [(cases (le_to_or_lt_eq … (le_O_n m))) #Hm
  97     [@le_to_le_to_eq @divides_to_le //
  98     |<Hm (cases divmn) //
  99     ]
 100   |<Hn (cases divnm) //
 101   ]
 102 qed.
 103
 104 theorem divides_to_lt_O : ∀n,m. O < m → n ∣ m → O < n.
 105 #n #m #posm (cases (le_to_or_lt_eq … (le_O_n n))) //
 106 #eqn0 * #d <eqn0 #eqm @False_ind @(absurd …posm)
 107 @le_to_not_lt > eqm //
 108 qed.
 109
 110 (*a variant of or_div_mod *)
 111 theorem or_div_mod1: ∀n,q. O < q →
 112   q ∣ S n ∧ S n = S (n/q) * q ∨
 113   q ∤ S n ∧ S n= (div n q) * q + S (n\mod q).
 114 #n #q #posq cases(or_div_mod n q posq) * #H1 #H2
 115   [%1 % /2/
 116   |%2 % // @(not_to_not ? ? (divides_to_mod_O … posq))
 117    cut (S n \mod q = S(n \mod q))
 118     [@(div_mod_spec_to_eq2 (S n) q (S n/q) (S n \mod q) (n/q) (S (n \mod q))) /2/]
 119    #Hcut >Hcut % /2/
 120   ]
 121 qed.
 122
 123 theorem divides_to_div: ∀n,m.n ∣m → m/n*n = m.
 124 #n #m #divnm (cases (le_to_or_lt_eq O n (le_O_n n))) #H
 125   [>(plus_n_O (m/n*n)) <(divides_to_mod_O ?? H divnm) //
 126   |(cases divnm) #d <H //
 127   ]
 128 qed.
 129
 130 theorem divides_div: ∀d,n. d ∣ n → n/d ∣ n.
 131 #d #n #divdn @(quotient ?? d) @sym_eq /2/
 132 qed.
 133
 134 theorem div_div: ∀n,d:nat. O < n → d ∣ n → n/(n/d) = d.
 135 #n #d #posn #divdn @(injective_times_l (n/d))
 136   [@(lt_times_n_to_lt_l d) >divides_to_div //
 137   |>divides_to_div
 138     [>commutative_times >divides_to_div //
 139     |@(quotient ? ? d) @sym_eq /2/
 140     ]
 141   ]
 142 qed.
 143
 144 theorem times_div: ∀a,b,c:nat.
 145   O < b → c ∣ b → a * (b /c) = (a*b)/c.
 146 #a #b #c #posb #divcb
 147 cut(O < c) [@(divides_to_lt_O … posb divcb)] #posc
 148 (cases divcb) #d #eqb >eqb
 149 >(commutative_times c d) >(div_times d c posc) <associative_times
 150 >(div_times (a * d) c posc) //
 151 qed.
 152
 153 theorem plus_div: ∀n,m,d. O < d →
 154   d ∣ n → d ∣ m → (n + m) / d = n/d + m/d.
 155 #n #m #d #posd #divdn #divdm
 156 (cases divdn) #a #eqn (cases divdm) #b #eqm
 157 >eqn >eqm <distributive_times_plus >commutative_times
 158 >div_times // >commutative_times >div_times //
 159 >commutative_times >div_times //
 160 qed.
 161
 162 (* boolean divides *)
 163 definition dividesb : nat → nat → bool ≝
 164 λn,m :nat. (eqb (m \mod n) O).
 165
 166 theorem dividesb_true_to_divides:
 167 ∀n,m:nat. dividesb n m = true → n ∣ m.
 168 #n #m (cases (le_to_or_lt_eq … (le_O_n n)))
 169   [#posn #divbnm @mod_O_to_divides // @eqb_true_to_eq @divbnm
 170   |#eqnO <eqnO normalize #eqbmO >(eqb_true_to_eq … eqbmO) //
 171   ]
 172 qed.
 173
 174 theorem dividesb_false_to_not_divides:
 175 ∀n,m:nat. dividesb n m = false → n ∤ m.
 176 #n #m (cases (le_to_or_lt_eq … (le_O_n n)))
 177   [#posn #ndivbnm @(not_to_not ?? (divides_to_mod_O … posn))
 178    @eqb_false_to_not_eq @ndivbnm
 179   |#eqnO <eqnO normalize
 180    @(nat_case m) [normalize /2/ |#a #_ #_ % * /2/]
 181   ]
 182 qed.
 183
 184 theorem decidable_divides: ∀n,m:nat. decidable (n ∣ m).
 185 #n #m cases(true_or_false (dividesb n m)) /3/
 186 qed.
 187
 188 theorem divides_to_dividesb_true : ∀n,m:nat. O < n →
 189   n ∣m → dividesb n m = true.
 190 #n #m #posn #divnm cases(true_or_false (dividesb n m)) //
 191 #ndivbnm @False_ind @(absurd … divnm) /2/
 192 qed.
 193
 194 theorem divides_to_dividesb_true1 : ∀n,m:nat.O < m →
 195   n ∣m → dividesb n m = true.
 196 #n #m #posn cases (le_to_or_lt_eq O n (le_O_n n)) /2/
 197 #eqn0 <eqn0 * #q #eqm @False_ind /2/
 198 qed.
 199
 200 theorem not_divides_to_dividesb_false: ∀n,m:nat. O < n →
 201   n ∤ m → dividesb n m = false.
 202 #n #m #posn cases(true_or_false (dividesb n m)) /2/
 203 #divbnm #ndivnm @False_ind @(absurd ?? ndivnm) /2/
 204 qed.
 205
 206 theorem dividesb_div_true:
 207 ∀d,n. O < n →
 208   dividesb d n = true → dividesb (n/d) n = true.
 209 #d #n #posn #divbdn @divides_to_dividesb_true1 //
 210 @divides_div /2/
 211 qed.
 212
 213 theorem dividesb_true_to_lt_O: ∀n,m.
 214   O < n → m ∣ n → O < m.
 215 #n #m #posn * #d cases (le_to_or_lt_eq ? ? (le_O_n m)) //
 216 qed.
 217
 218 (* divides and pi move away ??
 219 theorem divides_f_pi_f : ∀f:nat → nat.∀n,i:nat.
 220   i < n → f i ∣ \big[times,0]_{x < n | true}(f x).
 221 #f #n #i (elim n)
 222   [#ltiO @False_ind /2/
 223   |#n #Hind #lti >bigop_Strue //
 224    cases(le_to_or_lt_eq …(le_S_S_to_le … lti)) /3/
 225   ]
 226 *)
 227
 228 (* prime *)
 229 definition prime : nat → Prop ≝
 230 λn:nat. 1 < n ∧ (∀m:nat. m ∣ n → 1 < m → m = n).
 231
 232 theorem not_prime_O: ¬ (prime O).
 233 % * #lt10 /2/
 234 qed.
 235
 236 theorem not_prime_SO: ¬ (prime 1).
 237 % * #lt11 /2/
 238 qed.
 239
 240 theorem prime_to_lt_O: ∀p. prime p → O < p.
 241 #p * #lt1p /2/
 242 qed.
 243
 244 theorem prime_to_lt_SO: ∀p. prime p → 1 < p.
 245 #p * #lt1p /2/
 246 qed.
 247
 248 (* smallest factor *)
 249 definition smallest_factor : nat → nat ≝
 250 λn:nat. if_then_else ? (leb n 1) n
 251   (min n 2 (λm.(eqb (n \mod m) O))).
 252
 253 theorem smallest_factor_to_min : ∀n. 1 < n →
 254 smallest_factor n = (min n 2 (λm.(eqb (n \mod m) O))).
 255 #n #lt1n normalize >lt_to_leb_false //
 256 qed.
 257
 258 (* it works !
 259 theorem example1 : smallest_factor 3 = 3.
 260 normalize //
 261 qed.
 262
 263 theorem example2: smallest_factor 4 = 2.
 264 normalize //
 265 qed.
 266
 267 theorem example3 : smallest_factor 7 = 7.
 268 normalize //
 269 qed. *)
 270
 271 theorem le_SO_smallest_factor: ∀n:nat.
 272   n ≤ 1 → smallest_factor n = n.
 273 #n #le1n normalize >le_to_leb_true //
 274 qed.
 275
 276 theorem lt_SO_smallest_factor: ∀n:nat.
 277   1 < n → 1 < smallest_factor n.
 278 #n #lt1n >smallest_factor_to_min //
 279 qed.
 280
 281 theorem lt_O_smallest_factor: ∀n:nat.
 282   O < n → O < (smallest_factor n).
 283 #n #posn (cases posn)
 284   [>le_SO_smallest_factor //
 285   |#m #posm @le_S_S_to_le @le_S @lt_SO_smallest_factor @le_S_S //
 286   ]
 287 qed.
 288
 289 theorem divides_smallest_factor_n : ∀n:nat. 0 < n →
 290   smallest_factor n ∣ n.
 291 #n #posn (cases (le_to_or_lt_eq … posn))
 292   [#lt1n @mod_O_to_divides [@lt_O_smallest_factor //]
 293    >smallest_factor_to_min // @eqb_true_to_eq @f_min_true
 294    @(ex_intro … n) % /2/ @eq_to_eqb_true /2/
 295   |#H <H //
 296   ]
 297 qed.
 298
 299 theorem le_smallest_factor_n : ∀n.
 300   smallest_factor n ≤ n.
 301 #n (cases n) // #m @divides_to_le /2/
 302 qed.
 303
 304 theorem lt_smallest_factor_to_not_divides: ∀n,i:nat.
 305 1 < n → 1 < i → i < smallest_factor n → i ∤ n.
 306 #n #i #ltn #lti >smallest_factor_to_min // #ltmin
 307 @(not_to_not ? (n \mod i = 0))
 308   [#divin @divides_to_mod_O /2/
 309   |@eqb_false_to_not_eq @(lt_min_to_false … lti ltmin)
 310   ]
 311 qed.
 312
 313 theorem prime_smallest_factor_n : ∀n. 1 < n →
 314   prime (smallest_factor n).
 315 #n #lt1n (cut (0<n)) [/2/] #posn % /2/ #m #divmmin #lt1m
 316 @le_to_le_to_eq
 317   [@divides_to_le // @lt_O_smallest_factor //
 318   |>smallest_factor_to_min // @true_to_le_min //
 319    @eq_to_eqb_true @divides_to_mod_O /2/
 320    @(transitive_divides … divmmin) @divides_smallest_factor_n //
 321   ]
 322 qed.
 323
 324 theorem prime_to_smallest_factor: ∀n. prime n →
 325   smallest_factor n = n.
 326 #n * #lt1n #primen @primen
 327   [@divides_smallest_factor_n /2/
 328   |@lt_SO_smallest_factor //
 329   ]
 330 qed.
 331
 332 theorem smallest_factor_to_prime: ∀n. 1 < n →
 333   smallest_factor n = n → prime n.
 334 #n #lt1n #H <H /2/
 335 qed.
 336
 337 (* a number n > O is prime iff its smallest factor is n *)
 338 definition primeb ≝ λn:nat.
 339   (leb 2 n) ∧ (eqb (smallest_factor n) n).
 340
 341 (* it works! *)
 342 theorem example4 : primeb 3 = true.
 343 normalize // qed.
 344
 345 theorem example5 : primeb 6 = false.
 346 normalize // qed.
 347
 348 theorem example6 : primeb 11 = true.
 349 normalize // qed.
 350
 351 theorem example7 : primeb 17 = true.
 352 normalize // qed.
 353
 354 theorem primeb_true_to_prime : ∀n:nat.
 355   primeb n = true → prime n.
 356 #n #primebn @smallest_factor_to_prime
 357   [@leb_true_to_le @(andb_true_l … primebn)
 358   |@eqb_true_to_eq @( andb_true_r … primebn)
 359   ]
 360 qed.
 361
 362 theorem primeb_false_to_not_prime : ∀n:nat.
 363   primeb n = false → ¬ (prime n).
 364 #n #H cut ((leb 2 n ∧ (eqb (smallest_factor n) n)) = false) [@H]
 365 @leb_elim
 366   [#_ #H1 @(not_to_not … (prime_to_smallest_factor … ))
 367    @eqb_false_to_not_eq @H1
 368   |#len1 #_ @(not_to_not … len1) * //
 369   ]
 370 qed.
 371
 372 theorem decidable_prime : ∀n:nat.decidable (prime n).
 373 #n cases(true_or_false (primeb n)) #H
 374   [%1 /2/ |%2 /2/]
 375 qed.
 376
 377 theorem prime_to_primeb_true: ∀n:nat.
 378   prime n → primeb n = true.
 379 #n #primen (cases (true_or_false (primeb n))) //
 380 #H @False_ind @(absurd … primen) /2/
 381 qed.
 382
 383 theorem not_prime_to_primeb_false: ∀n:nat.
 384  ¬(prime n) → primeb n = false.
 385 #n #np (cases (true_or_false (primeb n))) //
 386 #p @False_ind @(absurd (prime n) (primeb_true_to_prime …) np) //
 387 qed.
 388
 389 (* enumeration of all primes *)
 390
 391 theorem divides_fact : ∀n,i:nat. O < i →
 392   i ≤ n → i ∣ n!.
 393 #n #i #ltOi (elim n)
 394   [#leiO @False_ind @(absurd … ltOi) /2/
 395   |#n #Hind #lei normalize cases(le_to_or_lt_eq … lei)
 396     [#ltiS @(transitive_divides ? n!) [@Hind /2/ | /2/]
 397     |#eqi >eqi /2/
 398     ]
 399   ]
 400 qed.
 401
 402 theorem mod_S_fact: ∀n,i:nat.
 403   1 < i → i ≤ n → (S n!) \mod i = 1.
 404 #n #i #lt1i #lein
 405 cut(O<i) [/2/] #posi
 406 cut (n! \mod i = O) [@divides_to_mod_O // @divides_fact //] #Hcut
 407 <Hcut @mod_S //
 408 qed.
 409
 410 theorem not_divides_S_fact: ∀n,i:nat.
 411   1 < i → i ≤ n → i ∤  S n!.
 412 #n #i #lt1i #lein @(not_to_not … (divides_to_mod_O i (S n!) ?)) /2/
 413 >mod_S_fact // @eqb_false_to_not_eq //
 414 qed.
 415
 416 theorem smallest_factor_fact: ∀n:nat.
 417   n < smallest_factor (S n!).
 418 #n @not_le_to_lt @(not_to_not ? ((smallest_factor (S n!)) ∤ (S n!)))
 419   [@not_divides_S_fact @lt_SO_smallest_factor @le_S_S //
 420   |% * #H @H @divides_smallest_factor_n @le_S_S //
 421   ]
 422 qed.
 423
 424 theorem ex_prime: ∀n. 1 ≤ n →∃m.
 425   n < m ∧ m ≤ S n! ∧ (prime m).
 426 #n #lein (cases lein)
 427   [@(ex_intro nat ? 2) % [/2/|@primeb_true_to_prime //]
 428   |#m #leim @(ex_intro nat ? (smallest_factor (S (S m)!)))
 429    % [% [@smallest_factor_fact |@le_smallest_factor_n ]
 430      |@prime_smallest_factor_n @le_S_S //
 431      ]
 432   ]
 433 qed.
 434
 435 let rec nth_prime n ≝ match n with
 436   [ O ⇒ 2
 437   | S p ⇒
 438     let previous_prime ≝ nth_prime p in
 439     let upper_bound ≝ S previous_prime! in
 440     min upper_bound (S previous_prime) primeb].
 441
 442 lemma nth_primeS: ∀n.nth_prime (S n) =
 443   let previous_prime ≝ nth_prime n in
 444     let upper_bound ≝ S previous_prime! in
 445     min upper_bound (S previous_prime) primeb.
 446 // qed.
 447
 448 (* it works *)
 449 theorem example11 : nth_prime 2 = 5.
 450 normalize // qed.
 451
 452 theorem example12: nth_prime 3 = 7.
 453 normalize //
 454 qed.
 455
 456 theorem example13 : nth_prime 4 = 11.
 457 normalize // qed.
 458
 459 (* done in 13.1369330883s -- qualcosa non va: // lentissimo
 460 theorem example14 : nth_prime 18 = 67.
 461 normalize // (* @refl *)
 462 qed.
 463 *)
 464
 465 theorem prime_nth_prime : ∀n:nat.prime (nth_prime n).
 466 #n (cases n)
 467   [@primeb_true_to_prime //
 468   |#m >nth_primeS @primeb_true_to_prime check f_min_true @(f_min_true primeb)
 469    @(ex_intro nat ? (smallest_factor (S (nth_prime m)!)))
 470    % [% // @le_S_S @(transitive_le … (le_smallest_factor_n …))
 471       <plus_n_Sm @le_plus_n_r
 472      ]
 473    @prime_to_primeb_true @prime_smallest_factor_n @le_S_S //
 474   ]
 475 qed.
 476
 477 (* properties of nth_prime *)
 478 theorem increasing_nth_prime: ∀n. nth_prime n < nth_prime (S n).
 479 #n
 480 change with
 481 (let previous_prime ≝ (nth_prime n) in
 482  let upper_bound ≝ S previous_prime! in
 483  S previous_prime ≤ min upper_bound (S previous_prime) primeb)
 484 apply le_min_l
 485 qed.
 486
 487 theorem lt_SO_nth_prime_n : ∀n:nat. 1 < nth_prime n.
 488 #n @prime_to_lt_SO //
 489 qed.
 490
 491 theorem lt_O_nth_prime_n : ∀n:nat. O < nth_prime n.
 492 #n @prime_to_lt_O //
 493 qed.
 494
 495 theorem lt_n_nth_prime_n : ∀n:nat. n < nth_prime n.
 496 #n (elim n)
 497   [@lt_O_nth_prime_n
 498   |#m #ltm @(le_to_lt_to_lt … ltm) //
 499   ]
 500 qed.
 501
 502 (*
 503 theorem ex_m_le_n_nth_prime_m:
 504 ∀n.nth_prime O ≤ n →
 505 ∃m. nth_prime m ≤ n ∧ n < nth_prime (S m).
 506 intros.
 507 apply increasing_to_le2.
 508 exact lt_nth_prime_n_nth_prime_Sn.assumption.
 509 qed. *)
 510
 511 theorem lt_nth_prime_to_not_prime: ∀n,m.
 512   nth_prime n < m → m < nth_prime (S n) → ¬ (prime m).
 513 #n #m #ltml >nth_primeS #ltmr @primeb_false_to_not_prime
 514 @(lt_min_to_false ? (S (nth_prime n)!) m (S (nth_prime n))) //
 515 qed.
 516
 517 (* nth_prime enumerates all primes *)
 518 theorem prime_to_nth_prime : ∀p:nat.
 519   prime p → ∃i.nth_prime i = p.
 520 #p #primep
 521 cut (∃m. nth_prime m ≤ p ∧ p < nth_prime (S m))
 522  [@(increasing_to_le2 nth_prime ?) // @prime_to_lt_SO //
 523  |* #n * #lepl #ltpr cases(le_to_or_lt_eq … lepl)
 524    [#ltpl @False_ind @(absurd … primep)
 525     @(lt_nth_prime_to_not_prime n p ltpl ltpr)
 526    |#eqp @(ex_intro … n) //
 527    ]
 528  ]
 529 qed.
 530