X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fprimes.ma;h=62c0a0081af5ecadfade0e7b0bbaa1ff4a3b216a;hb=143c97a8fe657eb7b041dec2747b0e67b5899762;hp=71e372f96722f893ebd3889a0b78eaf59f37d1fb;hpb=7ad16d18416a08382d62747fce4a0ac18ee557e0;p=helm.git

diff --git a/matita/matita/lib/arithmetics/primes.ma b/matita/matita/lib/arithmetics/primes.ma
index 71e372f96..62c0a0081 100644
--- a/matita/matita/lib/arithmetics/primes.ma
+++ b/matita/matita/lib/arithmetics/primes.ma
@@ -247,26 +247,24 @@ qed.
 
 (* 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.
@@ -291,7 +289,7 @@ theorem divides_smallest_factor_n : ∀n:nat. 0 < 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.
@@ -312,7 +310,7 @@ qed.
 
 theorem prime_smallest_factor_n : ∀n. 1 < n → 
   prime (smallest_factor n).
-#n #lt1n (cut (0<n)) [/2/] #posn % /2/ #m #divmmin #lt1m
+#n #lt1n (cut (0<n)) [/2/] #posn % (* bug? *) [/2/] #m #divmmin #lt1m
 @le_to_le_to_eq
   [@divides_to_le // @lt_O_smallest_factor //
   |>smallest_factor_to_min // @true_to_le_min //
@@ -339,16 +337,16 @@ definition primeb ≝ λn:nat.
   (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.
@@ -361,7 +359,7 @@ qed.
 
 theorem primeb_false_to_not_prime : ∀n:nat.
   primeb n = false → ¬ (prime n).
-#n #H cut ((leb 2 n ∧ (eqb (smallest_factor n) n)) = false) [>H //] 
+#n #H cut ((leb 2 n ∧ (eqb (smallest_factor n) n)) = false) [@H] 
 @leb_elim 
   [#_ #H1 @(not_to_not … (prime_to_smallest_factor … ))
    @eqb_false_to_not_eq @H1
@@ -440,20 +438,20 @@ let rec nth_prime n ≝ match n with
     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 
@@ -465,7 +463,7 @@ qed.
 theorem prime_nth_prime : ∀n:nat.prime (nth_prime n).
 #n (cases n) 
   [@primeb_true_to_prime //
-  |#m >nth_primeS @primeb_true_to_prime @f_min_true
+  |#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
@@ -481,7 +479,7 @@ change with
 (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.