]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/nth_prime.ma
examples of applyS
[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 set "baseuri" "cic:/matita/nat/nth_prime".
16
17 include "nat/primes.ma".
18 include "nat/lt_arith.ma".
19
20 (* upper bound by Bertrand's conjecture. *)
21 (* Too difficult to prove.        
22 let rec nth_prime n \def
23 match n with
24   [ O \Rightarrow (S(S O))
25   | (S p) \Rightarrow
26     let previous_prime \def S (nth_prime p) in
27     min_aux previous_prime ((S(S O))*previous_prime) primeb].
28
29 theorem example8 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
30 normalize.reflexivity.
31 qed.
32
33 theorem example9 : nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))).
34 normalize.reflexivity.
35 qed.
36
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.
39 qed. *)
40
41 theorem smallest_factor_fact: \forall n:nat.
42 n < smallest_factor (S n!).
43 intros.
44 apply not_le_to_lt.unfold Not.
45 intro.
46 apply (not_divides_S_fact n (smallest_factor(S n!))).
47 apply lt_SO_smallest_factor.
48 unfold lt.apply le_S_S.apply le_SO_fact.
49 assumption.
50 apply divides_smallest_factor_n.
51 unfold lt.apply le_S_S.apply le_O_n.
52 qed.
53
54 theorem ex_prime: \forall n. (S O) \le n \to \exists m.
55 n < m \land m \le S n! \land (prime m).
56 intros.
57 elim H.
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 (S n1)!))).
62 split.split.
63 apply smallest_factor_fact.
64 apply le_smallest_factor_n.
65 (* Andrea: ancora hint non lo trova *)
66 apply prime_smallest_factor_n.unfold lt.
67 apply le_S.apply le_SSO_fact.
68 unfold lt.apply le_S_S.assumption.
69 qed.
70
71 let rec nth_prime n \def
72 match n with
73   [ O \Rightarrow (S(S O))
74   | (S p) \Rightarrow
75     let previous_prime \def (nth_prime p) in
76     let upper_bound \def S previous_prime! in
77     min_aux (upper_bound - (S previous_prime)) upper_bound primeb].
78     
79 (* it works, but nth_prime 4 takes already a few minutes -
80 it must compute factorial of 7 ...*)
81
82 theorem example11 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
83 normalize.reflexivity.
84 qed.
85
86 theorem example12: nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))).
87 normalize.reflexivity.
88 qed.
89
90 theorem example13 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
91 normalize.reflexivity.
92 qed.
93
94 (*
95 theorem example14 : nth_prime (S(S(S(S(S O))))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
96 normalize.reflexivity.
97 *) 
98
99 theorem prime_nth_prime : \forall n:nat.prime (nth_prime n).
100 intro.
101 apply (nat_case n).simplify.
102 apply (primeb_to_Prop (S(S O))).
103 intro.
104 change with
105 (let previous_prime \def (nth_prime m) in
106 let upper_bound \def S previous_prime! in
107 prime (min_aux (upper_bound - (S previous_prime)) upper_bound primeb)).
108 apply primeb_true_to_prime.
109 apply f_min_aux_true.
110 apply (ex_intro nat ? (smallest_factor (S (nth_prime m)!))).
111 split.split.
112 cut (S (nth_prime m)!-(S (nth_prime m)! - (S (nth_prime m))) = (S (nth_prime m))).
113 rewrite > Hcut.exact (smallest_factor_fact (nth_prime m)).
114 (* maybe we could factorize this proof *)
115 apply plus_to_minus.
116 apply plus_minus_m_m.
117 apply le_S_S.
118 apply le_n_fact_n.
119 apply le_smallest_factor_n.
120 apply prime_to_primeb_true.
121 apply prime_smallest_factor_n.unfold lt.
122 apply le_S_S.apply le_SO_fact.
123 qed.
124
125 (* properties of nth_prime *)
126 theorem increasing_nth_prime: increasing nth_prime.
127 unfold increasing.
128 intros.
129 change with
130 (let previous_prime \def (nth_prime n) in
131 let upper_bound \def S previous_prime! in
132 (S previous_prime) \le min_aux (upper_bound - (S previous_prime)) upper_bound primeb).
133 intros.
134 cut (upper_bound - (upper_bound -(S previous_prime)) = (S previous_prime)).
135 rewrite < Hcut in \vdash (? % ?).
136 apply le_min_aux.
137 apply plus_to_minus.
138 apply plus_minus_m_m.
139 apply le_S_S.
140 apply le_n_fact_n.
141 qed.
142
143 variant lt_nth_prime_n_nth_prime_Sn :\forall n:nat. 
144 (nth_prime n) < (nth_prime (S n)) \def increasing_nth_prime.
145
146 theorem injective_nth_prime: injective nat nat nth_prime.
147 apply increasing_to_injective.
148 apply increasing_nth_prime.
149 qed.
150
151 theorem lt_SO_nth_prime_n : \forall n:nat. (S O) \lt nth_prime n.
152 intros. elim n.unfold lt.apply le_n.
153 apply (trans_lt ? (nth_prime n1)).
154 assumption.apply lt_nth_prime_n_nth_prime_Sn.
155 qed.
156
157 theorem lt_O_nth_prime_n : \forall n:nat. O \lt nth_prime n.
158 intros.apply (trans_lt O (S O)).
159 unfold lt. apply le_n.apply lt_SO_nth_prime_n.
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 upper_bound (upper_bound - (S previous_prime)) m).
177 cut (S (nth_prime n)!-(S (nth_prime n)! - (S (nth_prime n))) = (S (nth_prime n))).
178 rewrite > Hcut.assumption.
179 apply plus_to_minus.
180 apply plus_minus_m_m.
181 apply le_S_S.
182 apply le_n_fact_n.
183 assumption.
184 qed.
185
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.
189 intros.
190 cut (\exists m. nth_prime m \le p \land p < nth_prime (S m)).
191 elim Hcut.elim H1.
192 cut (nth_prime a < p \lor nth_prime a = p).
193 elim Hcut1.
194 absurd (prime p).
195 assumption.
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.
201 qed.
202