helm/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 (fact n)).
  43 intros.
  44 apply not_le_to_lt.
  45 change with smallest_factor (S (fact n)) \le n \to False.intro.
  46 apply not_divides_S_fact n (smallest_factor(S (fact n))).
  47 apply lt_SO_smallest_factor.
  48 simplify.apply le_S_S.apply le_SO_fact.
  49 assumption.
  50 apply divides_smallest_factor_n.
  51 simplify.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 (fact 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 (fact (S n1)))).
  62 split.split.
  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.
  70 qed.
  71
  72 let rec nth_prime n \def
  73 match n with
  74   [ O \Rightarrow (S(S O))
  75   | (S p) \Rightarrow
  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].
  79
  80 (* it works, but nth_prime 4 takes already a few minutes -
  81 it must compute factorial of 7 ...
  82
  83 theorem example11 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
  84 normalize.reflexivity.
  85 qed.
  86
  87 theorem example12: nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))).
  88 normalize.reflexivity.
  89 qed.
  90
  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.
  93 *)
  94
  95 theorem prime_nth_prime : \forall n:nat.prime (nth_prime n).
  96 intro.
  97 apply nat_case n.
  98 change with prime (S(S O)).
  99 apply primeb_to_Prop (S(S O)).
 100 intro.
 101 (* ammirare la resa del letin !! *)
 102 change with
 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)))).
 109 split.split.
 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 *)
 113 apply plus_to_minus.
 114 apply le_minus_m.
 115 apply plus_minus_m_m.
 116 apply le_S_S.
 117 apply le_n_fact_n.
 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.
 123 qed.
 124
 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)).
 128 intros.
 129 change with
 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.
 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 le_minus_m.
 139 apply plus_minus_m_m.
 140 apply le_S_S.
 141 apply le_n_fact_n.
 142 qed.
 143
 144 variant lt_nth_prime_n_nth_prime_Sn :\forall n:nat.
 145 (nth_prime n) < (nth_prime (S n)) \def increasing_nth_prime.
 146
 147 theorem injective_nth_prime: injective nat nat nth_prime.
 148 apply increasing_to_injective.
 149 apply increasing_nth_prime.
 150 qed.
 151
 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.
 156 qed.
 157
 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.
 161 qed.
 162
 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).
 166 intros.
 167 apply increasing_to_le2.
 168 exact lt_nth_prime_n_nth_prime_Sn.assumption.
 169 qed.
 170
 171 theorem lt_nth_prime_to_not_prime: \forall n,m. nth_prime n < m \to m < nth_prime (S n)
 172 \to \not (prime m).
 173 intros.
 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.
 180 apply plus_to_minus.
 181 apply le_minus_m.
 182 apply plus_minus_m_m.
 183 apply le_S_S.
 184 apply le_n_fact_n.
 185 assumption.
 186 qed.
 187
 188 (* nth_prime enumerates all primes *)
 189 theorem prime_to_nth_prime : \forall p:nat. prime p \to
 190 \exists i. nth_prime i = p.
 191 intros.
 192 cut \exists m. nth_prime m \le p \land p < nth_prime (S m).
 193 elim Hcut.elim H1.
 194 cut nth_prime a < p \lor nth_prime a = p.
 195 elim Hcut1.
 196 absurd (prime p).
 197 assumption.
 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.
 203 qed.
 204