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/library_auto/nat/nth_prime".
17 include "auto/nat/primes.ma".
18 include "auto/nat/lt_arith.ma".
20 (* upper bound by Bertrand's conjecture. *)
21 (* Too difficult to prove.
22 let rec nth_prime n \def
24 [ O \Rightarrow (S(S O))
26 let previous_prime \def S (nth_prime p) in
27 min_aux previous_prime ((S(S O))*previous_prime) primeb].
29 theorem example8 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
30 normalize.reflexivity.
33 theorem example9 : nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))).
34 normalize.reflexivity.
37 theorem example10 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
38 normalize.reflexivity.
41 theorem smallest_factor_fact: \forall n:nat.
42 n < smallest_factor (S n!).
47 apply (not_divides_S_fact n (smallest_factor(S n!)))
48 [ apply lt_SO_smallest_factor.
55 (*apply divides_smallest_factor_n.
62 theorem ex_prime: \forall n. (S O) \le n \to \exists m.
63 n < m \land m \le S n! \land (prime m).
66 [ apply (ex_intro nat ? (S(S O))).
69 [ apply (le_n (S(S O)))
70 | apply (le_n (S(S O)))
72 | apply (primeb_to_Prop (S(S O)))
74 | apply (ex_intro nat ? (smallest_factor (S (S n1)!))).
78 [ apply smallest_factor_fact
79 | apply le_smallest_factor_n
81 | (* Andrea: ancora hint non lo trova *)
82 apply prime_smallest_factor_n.
94 let rec nth_prime n \def
96 [ O \Rightarrow (S(S O))
98 let previous_prime \def (nth_prime p) in
99 let upper_bound \def S previous_prime! in
100 min_aux (upper_bound - (S previous_prime)) upper_bound primeb].
102 (* it works, but nth_prime 4 takes already a few minutes -
103 it must compute factorial of 7 ...*)
105 theorem example11 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
107 (*normalize.reflexivity.*)
110 theorem example12: nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))).
112 (*normalize.reflexivity.*)
115 theorem example13 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
117 (*normalize.reflexivity.*)
121 theorem example14 : nth_prime (S(S(S(S(S O))))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
122 normalize.reflexivity.
125 theorem prime_nth_prime : \forall n:nat.prime (nth_prime n).
130 apply (primeb_to_Prop (S(S O)))*)
133 (let previous_prime \def (nth_prime m) in
134 let upper_bound \def S previous_prime! in
135 prime (min_aux (upper_bound - (S previous_prime)) upper_bound primeb)).
136 apply primeb_true_to_prime.
137 apply f_min_aux_true.
138 apply (ex_intro nat ? (smallest_factor (S (nth_prime m)!))).
141 [ cut (S (nth_prime m)!-(S (nth_prime m)! - (S (nth_prime m))) = (S (nth_prime m)))
143 exact (smallest_factor_fact (nth_prime m))
144 | (* maybe we could factorize this proof *)
147 (*apply plus_minus_m_m.
151 | apply le_smallest_factor_n
153 | apply prime_to_primeb_true.
154 apply prime_smallest_factor_n.
163 (* properties of nth_prime *)
164 theorem increasing_nth_prime: increasing nth_prime.
168 (let previous_prime \def (nth_prime n) in
169 let upper_bound \def S previous_prime! in
170 (S previous_prime) \le min_aux (upper_bound - (S previous_prime)) upper_bound primeb).
172 cut (upper_bound - (upper_bound -(S previous_prime)) = (S previous_prime))
173 [ rewrite < Hcut in \vdash (? % ?).
175 | apply plus_to_minus.
177 (*apply plus_minus_m_m.
183 variant lt_nth_prime_n_nth_prime_Sn :\forall n:nat.
184 (nth_prime n) < (nth_prime (S n)) \def increasing_nth_prime.
186 theorem injective_nth_prime: injective nat nat nth_prime.
188 (*apply increasing_to_injective.
189 apply increasing_nth_prime.*)
192 theorem lt_SO_nth_prime_n : \forall n:nat. (S O) \lt nth_prime n.
194 (*usando la tattica auto qui, dopo svariati minuti la computazione non era
202 (*apply (trans_lt ? (nth_prime n1))
204 | apply lt_nth_prime_n_nth_prime_Sn
209 theorem lt_O_nth_prime_n : \forall n:nat. O \lt nth_prime n.
212 (*apply (trans_lt O (S O))
215 | apply lt_SO_nth_prime_n
219 theorem ex_m_le_n_nth_prime_m:
220 \forall n: nat. nth_prime O \le n \to
221 \exists m. nth_prime m \le n \land n < nth_prime (S m).
224 apply increasing_to_le2
225 [ exact lt_nth_prime_n_nth_prime_Sn
230 theorem lt_nth_prime_to_not_prime: \forall n,m. nth_prime n < m \to m < nth_prime (S n)
233 apply primeb_false_to_not_prime.
234 letin previous_prime \def (nth_prime n).
235 letin upper_bound \def (S previous_prime!).
236 apply (lt_min_aux_to_false primeb upper_bound (upper_bound - (S previous_prime)) m)
237 [ cut (S (nth_prime n)!-(S (nth_prime n)! - (S (nth_prime n))) = (S (nth_prime n)))
240 | apply plus_to_minus.
242 (*apply plus_minus_m_m.
250 (* nth_prime enumerates all primes *)
251 theorem prime_to_nth_prime : \forall p:nat. prime p \to
252 \exists i. nth_prime i = p.
254 cut (\exists m. nth_prime m \le p \land p < nth_prime (S m))
257 cut (nth_prime a < p \lor nth_prime a = p)
262 (*apply (lt_nth_prime_to_not_prime a);assumption*)
265 (*apply (ex_intro nat ? a).
269 (*apply le_to_or_lt_eq.
272 | apply ex_m_le_n_nth_prime_m.