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 (**************************************************************************)
16 include "nat/primes.ma".
17 include "nat/lt_arith.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 n!).
43 apply not_le_to_lt.unfold Not.
45 apply (not_divides_S_fact n (smallest_factor(S n!))).
46 apply lt_SO_smallest_factor.
47 unfold lt.apply le_S_S.apply le_SO_fact.
49 apply divides_smallest_factor_n.
50 unfold lt.apply le_S_S.apply le_O_n.
53 theorem ex_prime: \forall n. (S O) \le n \to \exists m.
54 n < m \land m \le S n! \land (prime m).
57 apply (ex_intro nat ? (S(S O))).
58 split.split.apply (le_n (S(S O))).
59 apply (le_n (S(S O))).apply (primeb_to_Prop (S(S O))).
60 apply (ex_intro nat ? (smallest_factor (S (S n1)!))).
62 apply smallest_factor_fact.
63 apply le_smallest_factor_n.
64 (* Andrea: ancora hint non lo trova *)
65 apply prime_smallest_factor_n.unfold lt.
66 apply le_S.apply le_SSO_fact.
67 unfold lt.apply le_S_S.assumption.
70 let rec nth_prime n \def
72 [ O \Rightarrow (S(S O))
74 let previous_prime \def (nth_prime p) in
75 let upper_bound \def S previous_prime! in
76 min_aux upper_bound (S previous_prime) primeb].
79 theorem example11 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
80 normalize.reflexivity.
83 theorem example12: nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))).
84 normalize.reflexivity.
87 theorem example13 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
88 normalize.reflexivity.
91 alias num (instance 0) = "natural number".
92 theorem example14 : nth_prime 18 = 67.
93 normalize.reflexivity.
97 theorem prime_nth_prime : \forall n:nat.prime (nth_prime n).
99 apply (nat_case n).simplify.
100 apply (primeb_to_Prop (S(S O))).
103 (let previous_prime \def (nth_prime m) in
104 let upper_bound \def S previous_prime! in
105 prime (min_aux upper_bound (S previous_prime) primeb)).
106 apply primeb_true_to_prime.
107 apply f_min_aux_true.
108 apply (ex_intro nat ? (smallest_factor (S (nth_prime m)!))).
110 apply smallest_factor_fact.
112 [2: apply le_smallest_factor_n
114 | apply (le_plus_n_r (S (nth_prime m)) (S (fact (nth_prime m))))
116 apply prime_to_primeb_true.
117 apply prime_smallest_factor_n.unfold lt.
118 apply le_S_S.apply le_SO_fact.
121 (* properties of nth_prime *)
122 theorem increasing_nth_prime: increasing nth_prime.
126 (let previous_prime \def (nth_prime n) in
127 let upper_bound \def S previous_prime! in
128 (S previous_prime) \le min_aux upper_bound (S previous_prime) primeb).
133 variant lt_nth_prime_n_nth_prime_Sn :\forall n:nat.
134 (nth_prime n) < (nth_prime (S n)) \def increasing_nth_prime.
136 theorem injective_nth_prime: injective nat nat nth_prime.
137 apply increasing_to_injective.
138 apply increasing_nth_prime.
141 theorem lt_SO_nth_prime_n : \forall n:nat. (S O) \lt nth_prime n.
142 intros. elim n.unfold lt.apply le_n.
143 apply (trans_lt ? (nth_prime n1)).
144 assumption.apply lt_nth_prime_n_nth_prime_Sn.
147 theorem lt_O_nth_prime_n : \forall n:nat. O \lt nth_prime n.
148 intros.apply (trans_lt O (S O)).
149 unfold lt. apply le_n.apply lt_SO_nth_prime_n.
152 theorem lt_n_nth_prime_n : \forall n:nat. n \lt nth_prime n.
155 [apply lt_O_nth_prime_n
156 |apply (lt_to_le_to_lt ? (S (nth_prime n1)))
157 [unfold.apply le_S_S.assumption
158 |apply lt_nth_prime_n_nth_prime_Sn
163 theorem ex_m_le_n_nth_prime_m:
164 \forall n: nat. nth_prime O \le n \to
165 \exists 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 previous_prime!).
177 apply (lt_min_aux_to_false primeb (S previous_prime) upper_bound m).
180 apply (transitive_le (S m) (nth_prime (S n)) (min_aux (S (fact (nth_prime n))) (S (nth_prime n)) primeb) ? ?);
182 |apply (le_n (min_aux (S (fact (nth_prime n))) (S (nth_prime n)) primeb)).
186 (* nth_prime enumerates all primes *)
187 theorem prime_to_nth_prime : \forall p:nat. prime p \to
188 \exists i. nth_prime i = p.
190 cut (\exists m. nth_prime m \le p \land p < nth_prime (S m)).
192 cut (nth_prime a < p \lor nth_prime a = p).
196 apply (lt_nth_prime_to_not_prime a).assumption.assumption.
197 apply (ex_intro nat ? a).assumption.
198 apply le_to_or_lt_eq.assumption.
199 apply ex_m_le_n_nth_prime_m.
200 simplify.unfold prime in H.elim H.assumption.