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