X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fprimes.ma;h=dc5f627e43103119199d71747a837c60b8595cf4;hb=ab44166935d77276c04fcce50aa8281292776e29;hp=dddd9151657ed3b28764fa3a543fcacfcc648193;hpb=4efbd5e75ff51c4104be8c5f35dbabb65f51461f;p=helm.git

diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma
index dddd91516..dc5f627e4 100644
--- a/helm/matita/library/nat/primes.ma
+++ b/helm/matita/library/nat/primes.ma
@@ -59,7 +59,7 @@ apply witness n m (div m n).
 rewrite > plus_n_O (n*div m n).
 rewrite < H1.
 rewrite < sym_times.
-(* perche' hint non lo trova ?*)
+(* Andrea: perche' hint non lo trova ?*)
 apply div_mod.
 assumption.
 qed.
@@ -116,10 +116,11 @@ apply lt_O_n_elim n2 Hcut.intro.rewrite < sym_times.
 simplify.rewrite < sym_plus.
 apply le_plus_n.
 elim le_to_or_lt_eq O n2.
-assumption.apply le_O_n.
+assumption.
 absurd O<m.assumption.
 rewrite > H2.rewrite < H3.rewrite < times_n_O.
 apply not_le_Sn_n O.
+apply le_O_n.
 qed.
 
 theorem divides_to_lt_O : \forall n,m. O < m \to divides n m \to O < n.
@@ -136,7 +137,7 @@ definition divides_b : nat \to nat \to bool \def
 \lambda n,m :nat. (eqb (mod m n) O).
   
 theorem divides_b_to_Prop :
-\forall n,m:nat. O < n \to O < m \to
+\forall n,m:nat. O < n \to
 match divides_b n m with
 [ true \Rightarrow divides n m
 | false \Rightarrow \lnot (divides n m)].
@@ -147,31 +148,65 @@ match eqb (mod m n) O with
 | false \Rightarrow \lnot (divides n m)].
 apply eqb_elim.
 intro.simplify.apply mod_O_to_divides.assumption.assumption.
-intro.simplify.intro.apply H2.apply divides_to_mod_O.assumption.assumption.
+intro.simplify.intro.apply H1.apply divides_to_mod_O.assumption.assumption.
 qed.
 
 theorem divides_b_true_to_divides :
-\forall n,m:nat. O < n \to O < m \to
+\forall n,m:nat. O < n \to
 (divides_b n m = true ) \to divides n m.
 intros.
 change with 
 match true with
 [ true \Rightarrow divides n m
 | false \Rightarrow \lnot (divides n m)].
-rewrite < H2.apply divides_b_to_Prop.
-assumption.assumption.
+rewrite < H1.apply divides_b_to_Prop.
+assumption.
 qed.
 
 theorem divides_b_false_to_not_divides :
-\forall n,m:nat. O < n \to O < m \to
+\forall n,m:nat. O < n \to
 (divides_b n m = false ) \to \lnot (divides n m).
 intros.
 change with 
 match false with
 [ true \Rightarrow divides n m
 | false \Rightarrow \lnot (divides n m)].
-rewrite < H2.apply divides_b_to_Prop.
-assumption.assumption.
+rewrite < H1.apply divides_b_to_Prop.
+assumption.
+qed.
+
+theorem decidable_divides: \forall n,m:nat.O < n \to
+decidable (divides n m).
+intros.change with (divides n m) \lor \not (divides n m).
+cut 
+match divides_b n m with
+[ true \Rightarrow divides n m
+| false \Rightarrow \not (divides n m)] \to (divides n m) \lor \not (divides n m).
+apply Hcut.apply divides_b_to_Prop.assumption.
+elim (divides_b n m).left.apply H1.right.apply H1.
+qed.
+
+theorem divides_to_divides_b_true : \forall n,m:nat. O < n \to
+divides n m \to divides_b n m = true.
+intros.
+cut match (divides_b n m) with
+[ true \Rightarrow (divides n m)
+| false \Rightarrow \not (divides n m)] \to ((divides_b n m) = true).
+apply Hcut.apply divides_b_to_Prop.assumption.
+elim divides_b n m.reflexivity.
+absurd (divides n m).assumption.assumption.
+qed.
+
+theorem not_divides_to_divides_b_false: \forall n,m:nat. O < n \to
+\not(divides n m) \to (divides_b n m) = false.
+intros.
+cut match (divides_b n m) with
+[ true \Rightarrow (divides n m)
+| false \Rightarrow \not (divides n m)] \to ((divides_b n m) = false).
+apply Hcut.apply divides_b_to_Prop.assumption.
+elim divides_b n m.
+absurd (divides n m).assumption.assumption.
+reflexivity.
 qed.
 
 (* divides and pi *)
@@ -232,7 +267,6 @@ theorem not_divides_S_fact: \forall n,i:nat.
 intros.
 apply divides_b_false_to_not_divides.
 apply trans_lt O (S O).apply le_n (S O).assumption.
-simplify.apply le_S_S.apply le_O_n.
 change with (eqb (mod (S (fact n)) i) O) = false.
 rewrite > mod_S_fact.simplify.reflexivity.
 assumption.assumption.
@@ -274,8 +308,7 @@ theorem example3 : smallest_prime_factor (S(S(S(S(S(S(S O))))))) = (S(S(S(S(S(S(
 simplify.reflexivity.
 qed. *)
 
-(* not sure this is what we need *)
-theorem lt_S_O_smallest_factor: 
+theorem lt_SO_smallest_factor: 
 \forall n:nat. (S O) < n \to (S O) < (smallest_factor n).
 intro.
 apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S O) H.
@@ -292,15 +325,26 @@ apply sym_eq.apply plus_to_minus.apply le_S.apply le_n_Sn.
 rewrite < sym_plus.simplify.reflexivity.
 qed.
 
+theorem lt_O_smallest_factor: \forall n:nat. O < n \to O < (smallest_factor n).
+intro.
+apply nat_case n.intro.apply False_ind.apply not_le_Sn_n O H.
+intro.apply nat_case m.intro.
+simplify.apply le_n.
+intros.apply trans_lt ? (S O).
+simplify. apply le_n.
+apply lt_SO_smallest_factor.simplify. apply le_S_S.
+apply le_S_S.apply le_O_n.
+qed.
+
 theorem divides_smallest_factor_n : 
-\forall n:nat. (S O) < n \to divides (smallest_factor n) n.
+\forall n:nat. O < n \to divides (smallest_factor n) n.
 intro.
-apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S O) H.
-intro.apply nat_case m.intro. apply False_ind.apply not_le_Sn_n (S O) H.
+apply nat_case n.intro.apply False_ind.apply not_le_Sn_O O H.
+intro.apply nat_case m.intro. simplify.
+apply witness ? ? (S O). simplify.reflexivity.
 intros.
 apply divides_b_true_to_divides.
-apply trans_lt ? (S O).apply le_n (S O).apply lt_S_O_smallest_factor ? H.
-apply trans_lt ? (S O).apply le_n (S O).assumption.
+apply lt_O_smallest_factor ? H.
 change with 
 eqb (mod (S(S m1)) (min_aux m1 (S(S m1)) 
   (\lambda m.(eqb (mod (S(S m1)) m) O)))) O = true.
@@ -309,7 +353,8 @@ apply ex_intro nat ? (S(S m1)).
 split.split.
 apply le_minus_m.apply le_n.
 rewrite > mod_n_n.reflexivity.
-apply trans_lt ? (S O).apply le_n (S O).assumption.
+apply trans_lt ? (S O).apply le_n (S O).simplify.
+apply le_S_S.apply le_S_S.apply le_O_n.
 qed.
   
 theorem le_smallest_factor_n : 
@@ -319,7 +364,7 @@ intro.apply nat_case m.simplify.reflexivity.
 intro.apply divides_to_le.
 simplify.apply le_S_S.apply le_O_n.
 apply divides_smallest_factor_n.
-simplify.apply le_S_S.apply le_S_S. apply le_O_n.
+simplify.apply le_S_S.apply le_O_n.
 qed.
 
 theorem lt_smallest_factor_to_not_divides: \forall n,i:nat. 
@@ -330,7 +375,6 @@ intro.apply nat_case m.intro. apply False_ind.apply not_le_Sn_n (S O) H.
 intros.
 apply divides_b_false_to_not_divides.
 apply trans_lt O (S O).apply le_n (S O).assumption.
-apply trans_lt O (S O).apply le_n (S O).assumption.
 change with (eqb (mod (S(S m1)) i) O) = false.
 apply lt_min_aux_to_false 
 (\lambda i:nat.eqb (mod (S(S m1)) i) O) (S(S m1)) m1 i.
@@ -347,7 +391,7 @@ theorem prime_smallest_factor_n :
 intro. change with (S(S O)) \le n \to (S O) < (smallest_factor n) \land 
 (\forall m:nat. divides m (smallest_factor n) \to (S O) < m \to  m = (smallest_factor n)).
 intro.split.
-apply lt_S_O_smallest_factor.assumption.
+apply lt_SO_smallest_factor.assumption.
 intros.
 cut le m (smallest_factor n).
 elim le_to_or_lt_eq m (smallest_factor n) Hcut.
@@ -355,13 +399,13 @@ absurd divides m n.
 apply transitive_divides m (smallest_factor n).
 assumption.
 apply divides_smallest_factor_n.
-exact H.
+apply trans_lt ? (S O). simplify. apply le_n. exact H.
 apply lt_smallest_factor_to_not_divides.
 exact H.assumption.assumption.assumption.
 apply divides_to_le.
 apply trans_lt O (S O).
 apply le_n (S O).
-apply lt_S_O_smallest_factor.
+apply lt_SO_smallest_factor.
 exact H.
 assumption.
 qed.
@@ -377,8 +421,8 @@ change with
 smallest_factor (S(S m1)) = (S(S m1)).
 intro.elim H.apply H2.
 apply divides_smallest_factor_n.
-assumption.
-apply lt_S_O_smallest_factor.
+apply trans_lt ? (S O).simplify. apply le_n.assumption.
+apply lt_SO_smallest_factor.
 assumption.
 qed.
 
@@ -485,108 +529,3 @@ absurd (prime n).assumption.assumption.
 reflexivity.
 qed.
 
-(* upper bound by Bertrand's conjecture. *)
-(* Too difficult to prove.        
-let rec nth_prime n \def
-match n with
-  [ O \Rightarrow (S(S O))
-  | (S p) \Rightarrow
-    let previous_prime \def S (nth_prime p) in
-    min_aux previous_prime ((S(S O))*previous_prime) primeb].
-
-theorem example8 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
-normalize.reflexivity.
-qed.
-
-theorem example9 : nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))).
-normalize.reflexivity.
-qed.
-
-theorem example10 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
-normalize.reflexivity.
-qed. *)
-
-theorem smallest_factor_fact: \forall n:nat.
-n < smallest_factor (S (fact n)).
-intros.
-apply not_le_to_lt.
-change with smallest_factor (S (fact n)) \le n \to False.intro.
-apply not_divides_S_fact n (smallest_factor(S (fact n))) ? ?.
-apply divides_smallest_factor_n.
-simplify.apply le_S_S.apply le_SO_fact.
-apply lt_S_O_smallest_factor.
-simplify.apply le_S_S.apply le_SO_fact.
-assumption.
-qed.
-
-(* mi sembra che il problem sia ex *)
-theorem ex_prime: \forall n. (S O) \le n \to ex nat (\lambda m.
-n < m \land m \le (S (fact n)) \land (prime m)).
-intros.
-elim H.
-apply ex_intro nat ? (S(S O)).
-split.split.apply le_n (S(S O)).
-apply le_n (S(S O)).apply primeb_to_Prop (S(S O)).
-apply ex_intro nat ? (smallest_factor (S (fact (S n1)))).
-split.split.
-apply smallest_factor_fact.
-apply le_smallest_factor_n.
-(* ancora hint non lo trova *)
-apply prime_smallest_factor_n.
-change with (S(S O)) \le S (fact (S n1)).
-apply le_S.apply le_SSO_fact.
-simplify.apply le_S_S.assumption.
-qed.
-
-let rec nth_prime n \def
-match n with
-  [ O \Rightarrow (S(S O))
-  | (S p) \Rightarrow
-    let previous_prime \def (nth_prime p) in
-    let upper_bound \def S (fact previous_prime) in
-    min_aux (upper_bound - (S previous_prime)) upper_bound primeb].
-    
-(* it works, but nth_prime 4 takes already a few minutes -
-it must compute factorial of 7 ...
-
-theorem example11 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
-normalize.reflexivity.
-qed.
-
-theorem example12: nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))).
-normalize.reflexivity.
-qed.
-
-theorem example13 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
-normalize.reflexivity.
-*) 
-
-theorem prime_nth_prime : \forall n:nat.prime (nth_prime n).
-intro.
-apply nat_case n.
-change with prime (S(S O)).
-apply primeb_to_Prop (S(S O)).
-intro.
-(* ammirare la resa del letin !! *)
-change with
-let previous_prime \def (nth_prime m) in
-let upper_bound \def S (fact previous_prime) in
-prime (min_aux (upper_bound - (S previous_prime)) upper_bound primeb).
-apply primeb_true_to_prime.
-apply f_min_aux_true.
-apply ex_intro nat ? (smallest_factor (S (fact (nth_prime m)))).
-split.split.
-cut S (fact (nth_prime m))-(S (fact (nth_prime m)) - (S (nth_prime m))) = (S (nth_prime m)).
-rewrite > Hcut.exact smallest_factor_fact (nth_prime m).
-(* maybe we could factorize this proof *)
-apply plus_to_minus.
-apply le_minus_m.
-apply plus_minus_m_m.
-apply le_S_S.
-apply le_n_fact_n.
-apply le_smallest_factor_n.
-apply prime_to_primeb_true.
-apply prime_smallest_factor_n.
-change with (S(S O)) \le S (fact (nth_prime m)).
-apply le_S_S.apply le_SO_fact.
-qed.
\ No newline at end of file