(* smallest factor *)
definition smallest_factor : nat → nat ≝
-λn:nat. if_then_else ? (leb n 1) n
- (min n 2 (λm.(eqb (n \mod m) O))).
+λn:nat. if leb n 1 then n else min n 2 (λm.(eqb (n \mod m) O)).
theorem smallest_factor_to_min : ∀n. 1 < n →
smallest_factor n = (min n 2 (λm.(eqb (n \mod m) O))).
#n #lt1n normalize >lt_to_leb_false //
qed.
-(* it works !
-theorem example1 : smallest_factor 3 = 3.
+example example1 : smallest_factor 3 = 3.
normalize //
qed.
-theorem example2: smallest_factor 4 = 2.
+example example2: smallest_factor 4 = 2.
normalize //
qed.
-theorem example3 : smallest_factor 7 = 7.
+example example3 : smallest_factor 7 = 7.
normalize //
-qed. *)
+qed.
theorem le_SO_smallest_factor: ∀n:nat.
n ≤ 1 → smallest_factor n = n.
#n #posn (cases (le_to_or_lt_eq … posn))
[#lt1n @mod_O_to_divides [@lt_O_smallest_factor //]
>smallest_factor_to_min // @eqb_true_to_eq @f_min_true
- @(ex_intro … n) % /2/ @eq_to_eqb_true /2/
+ @(ex_intro … n) % /2/
|#H <H //
]
qed.
(leb 2 n) ∧ (eqb (smallest_factor n) n).
(* it works! *)
-theorem example4 : primeb 3 = true.
+example example4 : primeb 3 = true.
normalize // qed.
-theorem example5 : primeb 6 = false.
+example example5 : primeb 6 = false.
normalize // qed.
-theorem example6 : primeb 11 = true.
+example example6 : primeb 11 = true.
normalize // qed.
-theorem example7 : primeb 17 = true.
+example example7 : primeb 17 = true.
normalize // qed.
theorem primeb_true_to_prime : ∀n:nat.
min upper_bound (S previous_prime) primeb].
lemma nth_primeS: ∀n.nth_prime (S n) =
- let previous_prime ≝ nth_prime n in
+ (let previous_prime ≝ nth_prime n in
let upper_bound ≝ S previous_prime! in
- min upper_bound (S previous_prime) primeb.
+ min upper_bound (S previous_prime) primeb).
// qed.
(* it works *)
-theorem example11 : nth_prime 2 = 5.
+example example11 : nth_prime 2 = 5.
normalize // qed.
-theorem example12: nth_prime 3 = 7.
+example example12: nth_prime 3 = 7.
normalize //
qed.
-theorem example13 : nth_prime 4 = 11.
+example example13 : nth_prime 4 = 11.
normalize // qed.
(* done in 13.1369330883s -- qualcosa non va: // lentissimo
theorem prime_nth_prime : ∀n:nat.prime (nth_prime n).
#n (cases n)
[@primeb_true_to_prime //
- |#m >nth_primeS @primeb_true_to_prime check f_min_true @(f_min_true primeb)
+ |#m >nth_primeS @primeb_true_to_prime @(f_min_true primeb)
@(ex_intro nat ? (smallest_factor (S (nth_prime m)!)))
% [% // @le_S_S @(transitive_le … (le_smallest_factor_n …))
<plus_n_Sm @le_plus_n_r
(let previous_prime ≝ (nth_prime n) in
let upper_bound ≝ S previous_prime! in
S previous_prime ≤ min upper_bound (S previous_prime) primeb)
-apply le_min_l
+@le_min_l
qed.
theorem lt_SO_nth_prime_n : ∀n:nat. 1 < nth_prime n.