]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/nth_prime.ma
...
[helm.git] / helm / software / matita / library / nat / nth_prime.ma
1 (**************************************************************************)
2 (*       ___                                                                *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        Matita is distributed under the terms of the          *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "nat/primes.ma".
16 include "nat/lt_arith.ma".
17
18 (* upper bound by Bertrand's conjecture. *)
19 (* Too difficult to prove.        
20 let rec nth_prime n \def
21 match n with
22   [ O \Rightarrow (S(S O))
23   | (S p) \Rightarrow
24     let previous_prime \def S (nth_prime p) in
25     min_aux previous_prime ((S(S O))*previous_prime) primeb].
26
27 theorem example8 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
28 normalize.reflexivity.
29 qed.
30
31 theorem example9 : nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))).
32 normalize.reflexivity.
33 qed.
34
35 theorem example10 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
36 normalize.reflexivity.
37 qed. *)
38
39 theorem smallest_factor_fact: \forall n:nat.
40 n < smallest_factor (S n!).
41 intros.
42 apply not_le_to_lt.unfold Not.
43 intro.
44 apply (not_divides_S_fact n (smallest_factor(S n!))).
45 apply lt_SO_smallest_factor.
46 unfold lt.apply le_S_S.apply le_SO_fact.
47 assumption.
48 apply divides_smallest_factor_n.
49 unfold lt.apply le_S_S.apply le_O_n.
50 qed.
51
52 theorem ex_prime: \forall n. (S O) \le n \to \exists m.
53 n < m \land m \le S n! \land (prime m).
54 intros.
55 elim H.
56 apply (ex_intro nat ? (S(S O))).
57 split.split.apply (le_n (S(S O))).
58 apply (le_n (S(S O))).apply (primeb_to_Prop (S(S O))).
59 apply (ex_intro nat ? (smallest_factor (S (S n1)!))).
60 split.split.
61 apply smallest_factor_fact.
62 apply le_smallest_factor_n.
63 (* Andrea: ancora hint non lo trova *)
64 apply prime_smallest_factor_n.unfold lt.
65 apply le_S.apply le_SSO_fact.
66 unfold lt.apply le_S_S.assumption.
67 qed.
68
69 let rec nth_prime n \def
70 match n with
71   [ O \Rightarrow (S(S O))
72   | (S p) \Rightarrow
73     let previous_prime \def (nth_prime p) in
74     let upper_bound \def S previous_prime! in
75     min_aux upper_bound (S previous_prime) primeb].
76     
77 (* it works
78 theorem example11 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
79 normalize.reflexivity.
80 qed.
81
82 theorem example12: nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))).
83 normalize.reflexivity.
84 qed.
85
86 theorem example13 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
87 normalize.reflexivity.
88 qed.
89
90 alias num (instance 0) = "natural number".
91 theorem example14 : nth_prime 18 = 67.
92 normalize.reflexivity.
93 qed.
94 *)
95
96 theorem prime_nth_prime : \forall n:nat.prime (nth_prime n).
97 intro.
98 apply (nat_case n).simplify.
99 apply (primeb_to_Prop (S(S O))).
100 intro.
101 change with
102 (let previous_prime \def (nth_prime m) in
103 let upper_bound \def S previous_prime! in
104 prime (min_aux upper_bound (S previous_prime) primeb)).
105 apply primeb_true_to_prime.
106 apply f_min_aux_true.
107 apply (ex_intro nat ? (smallest_factor (S (nth_prime m)!))).
108 split.split.
109 apply smallest_factor_fact.
110 apply transitive_le;
111  [2: apply le_smallest_factor_n
112  | skip
113  | apply (le_plus_n_r (S (nth_prime m)) (S (fact (nth_prime m))))
114  ].
115 apply prime_to_primeb_true.
116 apply prime_smallest_factor_n.unfold lt.
117 apply le_S_S.apply le_SO_fact.
118 qed.
119
120 (* properties of nth_prime *)
121 theorem increasing_nth_prime: increasing nth_prime.
122 unfold increasing.
123 intros.
124 change with
125 (let previous_prime \def (nth_prime n) in
126 let upper_bound \def S previous_prime! in
127 (S previous_prime) \le min_aux upper_bound (S previous_prime) primeb).
128 intros.
129 apply le_min_aux.
130 qed.
131
132 variant lt_nth_prime_n_nth_prime_Sn :\forall n:nat. 
133 (nth_prime n) < (nth_prime (S n)) \def increasing_nth_prime.
134
135 theorem injective_nth_prime: injective nat nat nth_prime.
136 apply increasing_to_injective.
137 apply increasing_nth_prime.
138 qed.
139
140 theorem lt_SO_nth_prime_n : \forall n:nat. (S O) \lt nth_prime n.
141 intros. elim n.unfold lt.apply le_n.
142 apply (trans_lt ? (nth_prime n1)).
143 assumption.apply lt_nth_prime_n_nth_prime_Sn.
144 qed.
145
146 theorem lt_O_nth_prime_n : \forall n:nat. O \lt nth_prime n.
147 intros.apply (trans_lt O (S O)).
148 unfold lt. apply le_n.apply lt_SO_nth_prime_n.
149 qed.
150
151 theorem lt_n_nth_prime_n : \forall n:nat. n \lt nth_prime n.
152 intro.
153 elim n
154   [apply lt_O_nth_prime_n
155   |apply (lt_to_le_to_lt ? (S (nth_prime n1)))
156     [unfold.apply le_S_S.assumption
157     |apply lt_nth_prime_n_nth_prime_Sn
158     ]
159   ]
160 qed.
161
162 theorem ex_m_le_n_nth_prime_m: 
163 \forall n: nat. nth_prime O \le n \to 
164 \exists m. nth_prime m \le n \land n < nth_prime (S m).
165 intros.
166 apply increasing_to_le2.
167 exact lt_nth_prime_n_nth_prime_Sn.assumption.
168 qed.
169
170 theorem lt_nth_prime_to_not_prime: \forall n,m. nth_prime n < m \to m < nth_prime (S n) 
171 \to \lnot (prime m).
172 intros.
173 apply primeb_false_to_not_prime.
174 letin previous_prime \def (nth_prime n).
175 letin upper_bound \def (S previous_prime!).
176 apply (lt_min_aux_to_false primeb (S previous_prime) upper_bound m).
177 assumption.
178 unfold lt.
179 apply (transitive_le (S m) (nth_prime (S n)) (min_aux (S (fact (nth_prime n))) (S (nth_prime n)) primeb) ? ?);
180   [apply (H1).
181   |apply (le_n (min_aux (S (fact (nth_prime n))) (S (nth_prime n)) primeb)).
182   ]
183 qed.
184
185 (* nth_prime enumerates all primes *)
186 theorem prime_to_nth_prime : \forall p:nat. prime p \to
187 \exists i. nth_prime i = p.
188 intros.
189 cut (\exists m. nth_prime m \le p \land p < nth_prime (S m)).
190 elim Hcut.elim H1.
191 cut (nth_prime a < p \lor nth_prime a = p).
192 elim Hcut1.
193 absurd (prime p).
194 assumption.
195 apply (lt_nth_prime_to_not_prime a).assumption.assumption.
196 apply (ex_intro nat ? a).assumption.
197 apply le_to_or_lt_eq.assumption.
198 apply ex_m_le_n_nth_prime_m.
199 simplify.unfold prime in H.elim H.assumption.
200 qed.
201