matita/library_auto/auto/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/library_auto/nat/nth_prime".
  16
  17 include "auto/nat/primes.ma".
  18 include "auto/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.
  45 unfold Not.
  46 intro.
  47 apply (not_divides_S_fact n (smallest_factor(S n!)))
  48 [ apply lt_SO_smallest_factor.
  49   auto
  50   (*unfold lt.
  51   apply le_S_S.
  52   apply le_SO_fact*)
  53 | assumption
  54 | auto
  55   (*apply divides_smallest_factor_n.
  56   unfold lt.
  57   apply le_S_S.
  58   apply le_O_n*)
  59 ]
  60 qed.
  61
  62 theorem ex_prime: \forall n. (S O) \le n \to \exists m.
  63 n < m \land m \le S n! \land (prime m).
  64 intros.
  65 elim H
  66 [ apply (ex_intro nat ? (S(S O))).
  67   split;auto
  68   (*[ split
  69     [ apply (le_n (S(S O)))
  70     | apply (le_n (S(S O)))
  71     ]
  72   | apply (primeb_to_Prop (S(S O)))
  73   ]*)
  74 | apply (ex_intro nat ? (smallest_factor (S (S n1)!))).
  75   split
  76   [ auto
  77     (*split
  78     [ apply smallest_factor_fact
  79     | apply le_smallest_factor_n
  80     ]*)
  81   | (* Andrea: ancora hint non lo trova *)
  82     apply prime_smallest_factor_n.
  83     auto
  84     (*unfold lt.
  85     apply le_S.
  86     apply le_SSO_fact.
  87     unfold lt.
  88     apply le_S_S.
  89     assumption*)
  90   ]
  91 ]
  92 qed.
  93
  94 let rec nth_prime n \def
  95 match n with
  96   [ O \Rightarrow (S(S O))
  97   | (S p) \Rightarrow
  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].
 101
 102 (* it works, but nth_prime 4 takes already a few minutes -
 103 it must compute factorial of 7 ...*)
 104
 105 theorem example11 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
 106 auto.
 107 (*normalize.reflexivity.*)
 108 qed.
 109
 110 theorem example12: nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))).
 111 auto.
 112 (*normalize.reflexivity.*)
 113 qed.
 114
 115 theorem example13 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
 116 auto.
 117 (*normalize.reflexivity.*)
 118 qed.
 119
 120 (*
 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.
 123 *)
 124
 125 theorem prime_nth_prime : \forall n:nat.prime (nth_prime n).
 126 intro.
 127 apply (nat_case n)
 128 [ auto
 129   (*simplify.
 130   apply (primeb_to_Prop (S(S O)))*)
 131 | intro.
 132   change with
 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)!))).
 139   split
 140   [ split
 141     [ cut (S (nth_prime m)!-(S (nth_prime m)! - (S (nth_prime m))) = (S (nth_prime m)))
 142       [ rewrite > Hcut.
 143         exact (smallest_factor_fact (nth_prime m))
 144       | (* maybe we could factorize this proof *)
 145         apply plus_to_minus.
 146         auto
 147         (*apply plus_minus_m_m.
 148         apply le_S_S.
 149         apply le_n_fact_n*)
 150       ]
 151     | apply le_smallest_factor_n
 152     ]
 153   | apply prime_to_primeb_true.
 154     apply prime_smallest_factor_n.
 155     auto
 156     (*unfold lt.
 157     apply le_S_S.
 158     apply le_SO_fact*)
 159   ]
 160 ]
 161 qed.
 162
 163 (* properties of nth_prime *)
 164 theorem increasing_nth_prime: increasing nth_prime.
 165 unfold increasing.
 166 intros.
 167 change with
 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).
 171 intros.
 172 cut (upper_bound - (upper_bound -(S previous_prime)) = (S previous_prime))
 173 [ rewrite < Hcut in \vdash (? % ?).
 174   apply le_min_aux
 175 | apply plus_to_minus.
 176   auto
 177   (*apply plus_minus_m_m.
 178   apply le_S_S.
 179   apply le_n_fact_n*)
 180 ]
 181 qed.
 182
 183 variant lt_nth_prime_n_nth_prime_Sn :\forall n:nat.
 184 (nth_prime n) < (nth_prime (S n)) \def increasing_nth_prime.
 185
 186 theorem injective_nth_prime: injective nat nat nth_prime.
 187 auto.
 188 (*apply increasing_to_injective.
 189 apply increasing_nth_prime.*)
 190 qed.
 191
 192 theorem lt_SO_nth_prime_n : \forall n:nat. (S O) \lt nth_prime n.
 193 intros.
 194 (*usando la tattica auto qui, dopo svariati minuti la computazione non era
 195  * ancora terminata
 196  *)
 197 elim n
 198 [ auto
 199   (*unfold lt.
 200   apply le_n*)
 201 | auto
 202   (*apply (trans_lt ? (nth_prime n1))
 203   [ assumption
 204   | apply lt_nth_prime_n_nth_prime_Sn
 205   ]*)
 206 ]
 207 qed.
 208
 209 theorem lt_O_nth_prime_n : \forall n:nat. O \lt nth_prime n.
 210 intros.
 211 auto.
 212 (*apply (trans_lt O (S O))
 213 [ unfold lt.
 214   apply le_n
 215 | apply lt_SO_nth_prime_n
 216 ]*)
 217 qed.
 218
 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).
 222 auto.
 223 (*intros.
 224 apply increasing_to_le2
 225 [ exact lt_nth_prime_n_nth_prime_Sn
 226 | assumption
 227 ]*)
 228 qed.
 229
 230 theorem lt_nth_prime_to_not_prime: \forall n,m. nth_prime n < m \to m < nth_prime (S n)
 231 \to \lnot (prime m).
 232 intros.
 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)))
 238   [ rewrite > Hcut.
 239     assumption
 240   | apply plus_to_minus.
 241     auto
 242     (*apply plus_minus_m_m.
 243     apply le_S_S.
 244     apply le_n_fact_n*)
 245   ]
 246 | assumption
 247 ]
 248 qed.
 249
 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.
 253 intros.
 254 cut (\exists m. nth_prime m \le p \land p < nth_prime (S m))
 255 [ elim Hcut.
 256   elim H1.
 257   cut (nth_prime a < p \lor nth_prime a = p)
 258   [ elim Hcut1
 259     [ absurd (prime p)
 260       [ assumption
 261       | auto
 262         (*apply (lt_nth_prime_to_not_prime a);assumption*)
 263       ]
 264     | auto
 265       (*apply (ex_intro nat ? a).
 266       assumption*)
 267     ]
 268   | auto
 269     (*apply le_to_or_lt_eq.
 270     assumption*)
 271   ]
 272 | apply ex_m_le_n_nth_prime_m.
 273   simplify.
 274   unfold prime in H.
 275   elim H.
 276   assumption
 277 ]
 278 qed.
 279