X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fnth_prime.ma;h=5330f52adbb923ddd84fc91ac1a876b373751ccc;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=ee21195dc10bd823f4a96b8998a87ad99f6bb562;hpb=78044035b4419e569df0d7f6a7f96fa32d21a19d;p=helm.git

diff --git a/helm/matita/library/nat/nth_prime.ma b/helm/matita/library/nat/nth_prime.ma
index ee21195dc..5330f52ad 100644
--- a/helm/matita/library/nat/nth_prime.ma
+++ b/helm/matita/library/nat/nth_prime.ma
@@ -15,6 +15,7 @@
 set "baseuri" "cic:/matita/nat/nth_prime".
 
 include "nat/primes.ma".
+include "nat/lt_arith.ma".
 
 (* upper bound by Bertrand's conjecture. *)
 (* Too difficult to prove.        
@@ -38,35 +39,34 @@ normalize.reflexivity.
 qed. *)
 
 theorem smallest_factor_fact: \forall n:nat.
-n < smallest_factor (S (fact n)).
+n < smallest_factor (S 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))) ? ?.
+change with (smallest_factor (S n!) \le n \to False).intro.
+apply (not_divides_S_fact n (smallest_factor(S n!))).
 apply lt_SO_smallest_factor.
-simplify.apply le_S_S.apply le_SO_fact.
+unfold lt.apply le_S_S.apply le_SO_fact.
 assumption.
 apply divides_smallest_factor_n.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 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)).
+theorem ex_prime: \forall n. (S O) \le n \to \exists m.
+n < m \land m \le S 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)))).
+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 (S n1)!))).
 split.split.
 apply smallest_factor_fact.
 apply le_smallest_factor_n.
-(* ancora hint non lo trova *)
+(* Andrea: ancora hint non lo trova *)
 apply prime_smallest_factor_n.
-change with (S(S O)) \le S (fact (S n1)).
+change with ((S(S O)) \le S (S n1)!).
 apply le_S.apply le_SSO_fact.
-simplify.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
 qed.
 
 let rec nth_prime n \def
@@ -74,7 +74,7 @@ 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
+    let upper_bound \def S previous_prime! in
     min_aux (upper_bound - (S previous_prime)) upper_bound primeb].
     
 (* it works, but nth_prime 4 takes already a few minutes -
@@ -94,48 +94,45 @@ 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)).
+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).
+(let previous_prime \def (nth_prime m) in
+let upper_bound \def S 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)))).
+apply (ex_intro nat ? (smallest_factor (S (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).
+cut (S (nth_prime m)!-(S (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)).
+change with ((S(S O)) \le S (nth_prime m)!).
 apply le_S_S.apply le_SO_fact.
 qed.
 
 (* properties of nth_prime *)
 theorem increasing_nth_prime: increasing nth_prime.
-change with \forall n:nat. (nth_prime n) < (nth_prime (S n)).
+change with (\forall n:nat. (nth_prime n) < (nth_prime (S n))).
 intros.
 change with
-let previous_prime \def (nth_prime n) in
-let upper_bound \def S (fact previous_prime) in
-(S previous_prime) \le min_aux (upper_bound - (S previous_prime)) upper_bound primeb.
+(let previous_prime \def (nth_prime n) in
+let upper_bound \def S previous_prime! in
+(S previous_prime) \le min_aux (upper_bound - (S previous_prime)) upper_bound primeb).
 intros.
-cut upper_bound - (upper_bound -(S previous_prime)) = (S previous_prime).
+cut (upper_bound - (upper_bound -(S previous_prime)) = (S previous_prime)).
 rewrite < Hcut in \vdash (? % ?).
 apply le_min_aux.
 apply plus_to_minus.
-apply le_minus_m.
 apply plus_minus_m_m.
 apply le_S_S.
 apply le_n_fact_n.
@@ -150,35 +147,34 @@ apply increasing_nth_prime.
 qed.
 
 theorem lt_SO_nth_prime_n : \forall n:nat. (S O) \lt nth_prime n.
-intros. elim n.simplify.apply le_n.
-apply trans_lt ? (nth_prime n1).
+intros. elim n.unfold lt.apply le_n.
+apply (trans_lt ? (nth_prime n1)).
 assumption.apply lt_nth_prime_n_nth_prime_Sn.
 qed.
 
 theorem lt_O_nth_prime_n : \forall n:nat. O \lt nth_prime n.
-intros.apply trans_lt O (S O).
-simplify. apply le_n.apply lt_SO_nth_prime_n.
+intros.apply (trans_lt O (S O)).
+unfold lt. apply le_n.apply lt_SO_nth_prime_n.
 qed.
 
 theorem ex_m_le_n_nth_prime_m: 
 \forall n: nat. nth_prime O \le n \to 
-ex nat (\lambda m. nth_prime m \le n \land n < nth_prime (S m)).
+\exists m. nth_prime m \le n \land n < nth_prime (S m).
 intros.
 apply increasing_to_le2.
 exact lt_nth_prime_n_nth_prime_Sn.assumption.
 qed.
 
 theorem lt_nth_prime_to_not_prime: \forall n,m. nth_prime n < m \to m < nth_prime (S n) 
-\to \not (prime m).
+\to \lnot (prime m).
 intros.
 apply primeb_false_to_not_prime.
-letin previous_prime \def nth_prime n.
-letin upper_bound \def S (fact previous_prime).
-apply lt_min_aux_to_false primeb upper_bound (upper_bound - (S previous_prime)) m.
-cut S (fact (nth_prime n))-(S (fact (nth_prime n)) - (S (nth_prime n))) = (S (nth_prime n)).
+letin previous_prime \def (nth_prime n).
+letin upper_bound \def (S previous_prime!).
+apply (lt_min_aux_to_false primeb upper_bound (upper_bound - (S previous_prime)) m).
+cut (S (nth_prime n)!-(S (nth_prime n)! - (S (nth_prime n))) = (S (nth_prime n))).
 rewrite > Hcut.assumption.
 apply plus_to_minus.
-apply le_minus_m.
 apply plus_minus_m_m.
 apply le_S_S.
 apply le_n_fact_n.
@@ -187,18 +183,18 @@ qed.
 
 (* nth_prime enumerates all primes *)
 theorem prime_to_nth_prime : \forall p:nat. prime p \to
-ex nat (\lambda i:nat. nth_prime i = p).
+\exists i. nth_prime i = p.
 intros.
-cut ex nat (\lambda m. nth_prime m \le p \land p < nth_prime (S m)).
+cut (\exists m. nth_prime m \le p \land p < nth_prime (S m)).
 elim Hcut.elim H1.
-cut nth_prime a < p \lor nth_prime a = p.
+cut (nth_prime a < p \lor nth_prime a = p).
 elim Hcut1.
 absurd (prime p).
 assumption.
-apply lt_nth_prime_to_not_prime a.assumption.assumption.
-apply ex_intro nat ? a.assumption.
+apply (lt_nth_prime_to_not_prime a).assumption.assumption.
+apply (ex_intro nat ? a).assumption.
 apply le_to_or_lt_eq.assumption.
 apply ex_m_le_n_nth_prime_m.
-simplify.simplify in H.elim H.assumption.
+simplify.unfold prime in H.elim H.assumption.
 qed.