1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / Matita is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/nth_prime".
17 include "nat/primes.ma".
19 (* upper bound by Bertrand's conjecture. *)
20 (* Too difficult to prove.
21 let rec nth_prime n \def
23 [ O \Rightarrow (S(S O))
25 let previous_prime \def S (nth_prime p) in
26 min_aux previous_prime ((S(S O))*previous_prime) primeb].
28 theorem example8 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
29 normalize.reflexivity.
32 theorem example9 : nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))).
33 normalize.reflexivity.
36 theorem example10 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
37 normalize.reflexivity.
40 theorem smallest_factor_fact: \forall n:nat.
41 n < smallest_factor (S (fact n)).
44 change with smallest_factor (S (fact n)) \le n \to False.intro.
45 apply not_divides_S_fact n (smallest_factor(S (fact n))) ? ?.
46 apply divides_smallest_factor_n.
47 simplify.apply le_S_S.apply le_O_n.
48 apply lt_SO_smallest_factor.
49 simplify.apply le_S_S.apply le_SO_fact.
53 (* mi sembra che il problem sia ex *)
54 theorem ex_prime: \forall n. (S O) \le n \to ex nat (\lambda m.
55 n < m \land m \le (S (fact n)) \land (prime m)).
58 apply ex_intro nat ? (S(S O)).
59 split.split.apply le_n (S(S O)).
60 apply le_n (S(S O)).apply primeb_to_Prop (S(S O)).
61 apply ex_intro nat ? (smallest_factor (S (fact (S n1)))).
63 apply smallest_factor_fact.
64 apply le_smallest_factor_n.
65 (* ancora hint non lo trova *)
66 apply prime_smallest_factor_n.
67 change with (S(S O)) \le S (fact (S n1)).
68 apply le_S.apply le_SSO_fact.
69 simplify.apply le_S_S.assumption.
72 let rec nth_prime n \def
74 [ O \Rightarrow (S(S O))
76 let previous_prime \def (nth_prime p) in
77 let upper_bound \def S (fact previous_prime) in
78 min_aux (upper_bound - (S previous_prime)) upper_bound primeb].
80 (* it works, but nth_prime 4 takes already a few minutes -
81 it must compute factorial of 7 ...
83 theorem example11 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
84 normalize.reflexivity.
87 theorem example12: nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))).
88 normalize.reflexivity.
91 theorem example13 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
92 normalize.reflexivity.
95 theorem prime_nth_prime : \forall n:nat.prime (nth_prime n).
98 change with prime (S(S O)).
99 apply primeb_to_Prop (S(S O)).
101 (* ammirare la resa del letin !! *)
103 let previous_prime \def (nth_prime m) in
104 let upper_bound \def S (fact previous_prime) in
105 prime (min_aux (upper_bound - (S previous_prime)) upper_bound primeb).
106 apply primeb_true_to_prime.
107 apply f_min_aux_true.
108 apply ex_intro nat ? (smallest_factor (S (fact (nth_prime m)))).
110 cut S (fact (nth_prime m))-(S (fact (nth_prime m)) - (S (nth_prime m))) = (S (nth_prime m)).
111 rewrite > Hcut.exact smallest_factor_fact (nth_prime m).
112 (* maybe we could factorize this proof *)
115 apply plus_minus_m_m.
118 apply le_smallest_factor_n.
119 apply prime_to_primeb_true.
120 apply prime_smallest_factor_n.
121 change with (S(S O)) \le S (fact (nth_prime m)).
122 apply le_S_S.apply le_SO_fact.
125 (* properties of nth_prime *)
126 theorem increasing_nth_prime: increasing nth_prime.
127 change with \forall n:nat. (nth_prime n) < (nth_prime (S n)).
130 let previous_prime \def (nth_prime n) in
131 let upper_bound \def S (fact previous_prime) in
132 (S previous_prime) \le min_aux (upper_bound - (S previous_prime)) upper_bound primeb.
134 cut upper_bound - (upper_bound -(S previous_prime)) = (S previous_prime).
135 rewrite < Hcut in \vdash (? % ?).
139 apply plus_minus_m_m.
144 variant lt_nth_prime_n_nth_prime_Sn :\forall n:nat.
145 (nth_prime n) < (nth_prime (S n)) \def increasing_nth_prime.
147 theorem injective_nth_prime: injective nat nat nth_prime.
148 apply increasing_to_injective.
149 apply increasing_nth_prime.
152 theorem lt_SO_nth_prime_n : \forall n:nat. (S O) \lt nth_prime n.
153 intros. elim n.simplify.apply le_n.
154 apply trans_lt ? (nth_prime n1).
155 assumption.apply lt_nth_prime_n_nth_prime_Sn.
158 theorem lt_O_nth_prime_n : \forall n:nat. O \lt nth_prime n.
159 intros.apply trans_lt O (S O).
160 simplify. apply le_n.apply lt_SO_nth_prime_n.
163 theorem ex_m_le_n_nth_prime_m:
164 \forall n: nat. nth_prime O \le n \to
165 ex nat (\lambda m. nth_prime m \le n \land n < nth_prime (S m)).
167 apply increasing_to_le2.
168 exact lt_nth_prime_n_nth_prime_Sn.assumption.
171 theorem lt_nth_prime_to_not_prime: \forall n,m. nth_prime n < m \to m < nth_prime (S n)
174 apply primeb_false_to_not_prime.
175 letin previous_prime \def nth_prime n.
176 letin upper_bound \def S (fact previous_prime).
177 apply lt_min_aux_to_false primeb upper_bound (upper_bound - (S previous_prime)) m.
178 cut S (fact (nth_prime n))-(S (fact (nth_prime n)) - (S (nth_prime n))) = (S (nth_prime n)).
179 rewrite > Hcut.assumption.
182 apply plus_minus_m_m.
188 (* nth_prime enumerates all primes *)
189 theorem prime_to_nth_prime : \forall p:nat. prime p \to
190 ex nat (\lambda i:nat. nth_prime i = p).
192 cut ex nat (\lambda m. nth_prime m \le p \land p < nth_prime (S m)).
194 cut nth_prime a < p \lor nth_prime a = p.
198 apply lt_nth_prime_to_not_prime a.assumption.assumption.
199 apply ex_intro nat ? a.assumption.
200 apply le_to_or_lt_eq.assumption.
201 apply ex_m_le_n_nth_prime_m.
202 simplify.simplify in H.elim H.assumption.