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 leb n 1 then n else min n 2 (λm.(eqb (n \mod m) O)).
 251
 252 theorem smallest_factor_to_min : ∀n. 1 < n →
 253 smallest_factor n = (min n 2 (λm.(eqb (n \mod m) O))).
 254 #n #lt1n normalize >lt_to_leb_false //
 255 qed.
 256
 257 example example1 : smallest_factor 3 = 3.
 258 normalize //
 259 qed.
 260
 261 example example2: smallest_factor 4 = 2.
 262 normalize //
 263 qed.
 264
 265 example example3 : smallest_factor 7 = 7.
 266 normalize //
 267 qed.
 268
 269 theorem le_SO_smallest_factor: ∀n:nat.
 270   n ≤ 1 → smallest_factor n = n.
 271 #n #le1n normalize >le_to_leb_true //
 272 qed.
 273
 274 theorem lt_SO_smallest_factor: ∀n:nat.
 275   1 < n → 1 < smallest_factor n.
 276 #n #lt1n >smallest_factor_to_min //
 277 qed.
 278
 279 theorem lt_O_smallest_factor: ∀n:nat.
 280   O < n → O < (smallest_factor n).
 281 #n #posn (cases posn)
 282   [>le_SO_smallest_factor //
 283   |#m #posm @le_S_S_to_le @le_S @lt_SO_smallest_factor @le_S_S //
 284   ]
 285 qed.
 286
 287 theorem divides_smallest_factor_n : ∀n:nat. 0 < n →
 288   smallest_factor n ∣ n.
 289 #n #posn (cases (le_to_or_lt_eq … posn))
 290   [#lt1n @mod_O_to_divides [@lt_O_smallest_factor //]
 291    >smallest_factor_to_min // @eqb_true_to_eq @f_min_true
 292    @(ex_intro … n) % /2/
 293   |#H <H //
 294   ]
 295 qed.
 296
 297 theorem le_smallest_factor_n : ∀n.
 298   smallest_factor n ≤ n.
 299 #n (cases n) // #m @divides_to_le /2/
 300 qed.
 301
 302 theorem lt_smallest_factor_to_not_divides: ∀n,i:nat.
 303 1 < n → 1 < i → i < smallest_factor n → i ∤ n.
 304 #n #i #ltn #lti >smallest_factor_to_min // #ltmin
 305 @(not_to_not ? (n \mod i = 0))
 306   [#divin @divides_to_mod_O /2/
 307   |@eqb_false_to_not_eq @(lt_min_to_false … lti ltmin)
 308   ]
 309 qed.
 310
 311 theorem prime_smallest_factor_n : ∀n. 1 < n →
 312   prime (smallest_factor n).
 313 #n #lt1n (cut (0<n)) [/2/] #posn % (* bug? *) [/2/] #m #divmmin #lt1m
 314 @le_to_le_to_eq
 315   [@divides_to_le // @lt_O_smallest_factor //
 316   |>smallest_factor_to_min // @true_to_le_min //
 317    @eq_to_eqb_true @divides_to_mod_O /2/
 318    @(transitive_divides … divmmin) @divides_smallest_factor_n //
 319   ]
 320 qed.
 321
 322 theorem prime_to_smallest_factor: ∀n. prime n →
 323   smallest_factor n = n.
 324 #n * #lt1n #primen @primen
 325   [@divides_smallest_factor_n /2/
 326   |@lt_SO_smallest_factor //
 327   ]
 328 qed.
 329
 330 theorem smallest_factor_to_prime: ∀n. 1 < n →
 331   smallest_factor n = n → prime n.
 332 #n #lt1n #H <H /2/
 333 qed.
 334
 335 (* a number n > O is prime iff its smallest factor is n *)
 336 definition primeb ≝ λn:nat.
 337   (leb 2 n) ∧ (eqb (smallest_factor n) n).
 338
 339 (* it works! *)
 340 example example4 : primeb 3 = true.
 341 normalize // qed.
 342
 343 example example5 : primeb 6 = false.
 344 normalize // qed.
 345
 346 example example6 : primeb 11 = true.
 347 normalize // qed.
 348
 349 example example7 : primeb 17 = true.
 350 normalize // qed.
 351
 352 theorem primeb_true_to_prime : ∀n:nat.
 353   primeb n = true → prime n.
 354 #n #primebn @smallest_factor_to_prime
 355   [@leb_true_to_le @(andb_true_l … primebn)
 356   |@eqb_true_to_eq @( andb_true_r … primebn)
 357   ]
 358 qed.
 359
 360 theorem primeb_false_to_not_prime : ∀n:nat.
 361   primeb n = false → ¬ (prime n).
 362 #n #H cut ((leb 2 n ∧ (eqb (smallest_factor n) n)) = false) [@H]
 363 @leb_elim
 364   [#_ #H1 @(not_to_not … (prime_to_smallest_factor … ))
 365    @eqb_false_to_not_eq @H1
 366   |#len1 #_ @(not_to_not … len1) * //
 367   ]
 368 qed.
 369
 370 theorem decidable_prime : ∀n:nat.decidable (prime n).
 371 #n cases(true_or_false (primeb n)) #H
 372   [%1 /2/ |%2 /2/]
 373 qed.
 374
 375 theorem prime_to_primeb_true: ∀n:nat.
 376   prime n → primeb n = true.
 377 #n #primen (cases (true_or_false (primeb n))) //
 378 #H @False_ind @(absurd … primen) /2/
 379 qed.
 380
 381 theorem not_prime_to_primeb_false: ∀n:nat.
 382  ¬(prime n) → primeb n = false.
 383 #n #np (cases (true_or_false (primeb n))) //
 384 #p @False_ind @(absurd (prime n) (primeb_true_to_prime …) np) //
 385 qed.
 386
 387 (* enumeration of all primes *)
 388
 389 theorem divides_fact : ∀n,i:nat. O < i →
 390   i ≤ n → i ∣ n!.
 391 #n #i #ltOi (elim n)
 392   [#leiO @False_ind @(absurd … ltOi) /2/
 393   |#n #Hind #lei normalize cases(le_to_or_lt_eq … lei)
 394     [#ltiS @(transitive_divides ? n!) [@Hind /2/ | /2/]
 395     |#eqi >eqi /2/
 396     ]
 397   ]
 398 qed.
 399
 400 theorem mod_S_fact: ∀n,i:nat.
 401   1 < i → i ≤ n → (S n!) \mod i = 1.
 402 #n #i #lt1i #lein
 403 cut(O<i) [/2/] #posi
 404 cut (n! \mod i = O) [@divides_to_mod_O // @divides_fact //] #Hcut
 405 <Hcut @mod_S //
 406 qed.
 407
 408 theorem not_divides_S_fact: ∀n,i:nat.
 409   1 < i → i ≤ n → i ∤  S n!.
 410 #n #i #lt1i #lein @(not_to_not … (divides_to_mod_O i (S n!) ?)) /2/
 411 >mod_S_fact // @eqb_false_to_not_eq //
 412 qed.
 413
 414 theorem smallest_factor_fact: ∀n:nat.
 415   n < smallest_factor (S n!).
 416 #n @not_le_to_lt @(not_to_not ? ((smallest_factor (S n!)) ∤ (S n!)))
 417   [@not_divides_S_fact @lt_SO_smallest_factor @le_S_S //
 418   |% * #H @H @divides_smallest_factor_n @le_S_S //
 419   ]
 420 qed.
 421
 422 theorem ex_prime: ∀n. 1 ≤ n →∃m.
 423   n < m ∧ m ≤ S n! ∧ (prime m).
 424 #n #lein (cases lein)
 425   [@(ex_intro nat ? 2) % [/2/|@primeb_true_to_prime //]
 426   |#m #leim @(ex_intro nat ? (smallest_factor (S (S m)!)))
 427    % [% [@smallest_factor_fact |@le_smallest_factor_n ]
 428      |@prime_smallest_factor_n @le_S_S //
 429      ]
 430   ]
 431 qed.
 432
 433 let rec nth_prime n ≝ match n with
 434   [ O ⇒ 2
 435   | S p ⇒
 436     let previous_prime ≝ nth_prime p in
 437     let upper_bound ≝ S previous_prime! in
 438     min upper_bound (S previous_prime) primeb].
 439
 440 lemma nth_primeS: ∀n.nth_prime (S n) =
 441    (let previous_prime ≝ nth_prime n in
 442     let upper_bound ≝ S previous_prime! in
 443     min upper_bound (S previous_prime) primeb).
 444 // qed.
 445
 446 (* it works *)
 447 example example11 : nth_prime 2 = 5.
 448 normalize // qed.
 449
 450 example example12: nth_prime 3 = 7.
 451 normalize //
 452 qed.
 453
 454 example example13 : nth_prime 4 = 11.
 455 normalize // qed.
 456
 457 (* done in 13.1369330883s -- qualcosa non va: // lentissimo
 458 theorem example14 : nth_prime 18 = 67.
 459 normalize // (* @refl *)
 460 qed.
 461 *)
 462
 463 theorem prime_nth_prime : ∀n:nat.prime (nth_prime n).
 464 #n (cases n)
 465   [@primeb_true_to_prime //
 466   |#m >nth_primeS @primeb_true_to_prime @(f_min_true primeb)
 467    @(ex_intro nat ? (smallest_factor (S (nth_prime m)!)))
 468    % [% // @le_S_S @(transitive_le … (le_smallest_factor_n …))
 469       <plus_n_Sm @le_plus_n_r
 470      ]
 471    @prime_to_primeb_true @prime_smallest_factor_n @le_S_S //
 472   ]
 473 qed.
 474
 475 (* properties of nth_prime *)
 476 theorem increasing_nth_prime: ∀n. nth_prime n < nth_prime (S n).
 477 #n
 478 change with
 479 (let previous_prime ≝ (nth_prime n) in
 480  let upper_bound ≝ S previous_prime! in
 481  S previous_prime ≤ min upper_bound (S previous_prime) primeb)
 482 @le_min_l
 483 qed.
 484
 485 theorem lt_SO_nth_prime_n : ∀n:nat. 1 < nth_prime n.
 486 #n @prime_to_lt_SO //
 487 qed.
 488
 489 theorem lt_O_nth_prime_n : ∀n:nat. O < nth_prime n.
 490 #n @prime_to_lt_O //
 491 qed.
 492
 493 theorem lt_n_nth_prime_n : ∀n:nat. n < nth_prime n.
 494 #n (elim n)
 495   [@lt_O_nth_prime_n
 496   |#m #ltm @(le_to_lt_to_lt … ltm) //
 497   ]
 498 qed.
 499
 500 (*
 501 theorem ex_m_le_n_nth_prime_m:
 502 ∀n.nth_prime O ≤ n →
 503 ∃m. nth_prime m ≤ n ∧ n < nth_prime (S m).
 504 intros.
 505 apply increasing_to_le2.
 506 exact lt_nth_prime_n_nth_prime_Sn.assumption.
 507 qed. *)
 508
 509 theorem lt_nth_prime_to_not_prime: ∀n,m.
 510   nth_prime n < m → m < nth_prime (S n) → ¬ (prime m).
 511 #n #m #ltml >nth_primeS #ltmr @primeb_false_to_not_prime
 512 @(lt_min_to_false ? (S (nth_prime n)!) m (S (nth_prime n))) //
 513 qed.
 514
 515 (* nth_prime enumerates all primes *)
 516 theorem prime_to_nth_prime : ∀p:nat.
 517   prime p → ∃i.nth_prime i = p.
 518 #p #primep
 519 cut (∃m. nth_prime m ≤ p ∧ p < nth_prime (S m))
 520  [@(increasing_to_le2 nth_prime ?) // @prime_to_lt_SO //
 521  |* #n * #lepl #ltpr cases(le_to_or_lt_eq … lepl)
 522    [#ltpl @False_ind @(absurd … primep)
 523     @(lt_nth_prime_to_not_prime n p ltpl ltpr)
 524    |#eqp @(ex_intro … n) //
 525    ]
 526  ]
 527 qed.
 528