matita/matita/lib/arithmetics/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 (* To be ported
  16 include "nat/primes.ma".
  17 include "nat/lt_arith.ma".
  18
  19 (* upper bound by Bertrand's conjecture. *)
  20 (* Too difficult to prove.
  21 let rec nth_prime n \def
  22 match n with
  23   [ O \Rightarrow (S(S O))
  24   | (S p) \Rightarrow
  25     let previous_prime \def S (nth_prime p) in
  26     min_aux previous_prime ((S(S O))*previous_prime) primeb].
  27
  28 theorem example8 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
  29 normalize.reflexivity.
  30 qed.
  31
  32 theorem example9 : nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))).
  33 normalize.reflexivity.
  34 qed.
  35
  36 theorem example10 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
  37 normalize.reflexivity.
  38 qed. *)
  39
  40 theorem smallest_factor_fact: \forall n:nat.
  41 n < smallest_factor (S n!).
  42 intros.
  43 apply not_le_to_lt.unfold Not.
  44 intro.
  45 apply (not_divides_S_fact n (smallest_factor(S n!))).
  46 apply lt_SO_smallest_factor.
  47 unfold lt.apply le_S_S.apply le_SO_fact.
  48 assumption.
  49 apply divides_smallest_factor_n.
  50 unfold lt.apply le_S_S.apply le_O_n.
  51 qed.
  52
  53 theorem ex_prime: \forall n. (S O) \le n \to \exists m.
  54 n < m \land m \le S n! \land (prime m).
  55 intros.
  56 elim H.
  57 apply (ex_intro nat ? (S(S O))).
  58 split.split.apply (le_n (S(S O))).
  59 apply (le_n (S(S O))).apply (primeb_to_Prop (S(S O))).
  60 apply (ex_intro nat ? (smallest_factor (S (S n1)!))).
  61 split.split.
  62 apply smallest_factor_fact.
  63 apply le_smallest_factor_n.
  64 (* Andrea: ancora hint non lo trova *)
  65 apply prime_smallest_factor_n.unfold lt.
  66 apply le_S.apply le_SSO_fact.
  67 unfold lt.apply le_S_S.assumption.
  68 qed.
  69
  70 let rec nth_prime n \def
  71 match n with
  72   [ O \Rightarrow (S(S O))
  73   | (S p) \Rightarrow
  74     let previous_prime \def (nth_prime p) in
  75     let upper_bound \def S previous_prime! in
  76     min_aux upper_bound (S previous_prime) primeb].
  77
  78 (* it works
  79 theorem example11 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
  80 normalize.reflexivity.
  81 qed.
  82
  83 theorem example12: nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))).
  84 normalize.reflexivity.
  85 qed.
  86
  87 theorem example13 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
  88 normalize.reflexivity.
  89 qed.
  90
  91 alias num (instance 0) = "natural number".
  92 theorem example14 : nth_prime 18 = 67.
  93 normalize.reflexivity.
  94 qed.
  95 *)
  96
  97 theorem prime_nth_prime : \forall n:nat.prime (nth_prime n).
  98 intro.
  99 apply (nat_case n).simplify.
 100 apply (primeb_to_Prop (S(S O))).
 101 intro.
 102 change with
 103 (let previous_prime \def (nth_prime m) in
 104 let upper_bound \def S previous_prime! in
 105 prime (min_aux upper_bound (S previous_prime) primeb)).
 106 apply primeb_true_to_prime.
 107 apply f_min_aux_true.
 108 apply (ex_intro nat ? (smallest_factor (S (nth_prime m)!))).
 109 split.split.
 110 apply smallest_factor_fact.
 111 apply transitive_le;
 112  [2: apply le_smallest_factor_n
 113  | skip
 114  | apply (le_plus_n_r (S (nth_prime m)) (S (fact (nth_prime m))))
 115  ].
 116 apply prime_to_primeb_true.
 117 apply prime_smallest_factor_n.unfold lt.
 118 apply le_S_S.apply le_SO_fact.
 119 qed.
 120
 121 (* properties of nth_prime *)
 122 theorem increasing_nth_prime: increasing nth_prime.
 123 unfold increasing.
 124 intros.
 125 change with
 126 (let previous_prime \def (nth_prime n) in
 127 let upper_bound \def S previous_prime! in
 128 (S previous_prime) \le min_aux upper_bound (S previous_prime) primeb).
 129 intros.
 130 apply le_min_aux.
 131 qed.
 132
 133 variant lt_nth_prime_n_nth_prime_Sn :\forall n:nat.
 134 (nth_prime n) < (nth_prime (S n)) \def increasing_nth_prime.
 135
 136 theorem injective_nth_prime: injective nat nat nth_prime.
 137 apply increasing_to_injective.
 138 apply increasing_nth_prime.
 139 qed.
 140
 141 theorem lt_SO_nth_prime_n : \forall n:nat. (S O) \lt nth_prime n.
 142 intros. elim n.unfold lt.apply le_n.
 143 apply (trans_lt ? (nth_prime n1)).
 144 assumption.apply lt_nth_prime_n_nth_prime_Sn.
 145 qed.
 146
 147 theorem lt_O_nth_prime_n : \forall n:nat. O \lt nth_prime n.
 148 intros.apply (trans_lt O (S O)).
 149 unfold lt. apply le_n.apply lt_SO_nth_prime_n.
 150 qed.
 151
 152 theorem lt_n_nth_prime_n : \forall n:nat. n \lt nth_prime n.
 153 intro.
 154 elim n
 155   [apply lt_O_nth_prime_n
 156   |apply (lt_to_le_to_lt ? (S (nth_prime n1)))
 157     [unfold.apply le_S_S.assumption
 158     |apply lt_nth_prime_n_nth_prime_Sn
 159     ]
 160   ]
 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 \lnot (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 previous_prime!).
 177 apply (lt_min_aux_to_false primeb (S previous_prime) upper_bound m).
 178 assumption.
 179 unfold lt.
 180 apply (transitive_le (S m) (nth_prime (S n)) (min_aux (S (fact (nth_prime n))) (S (nth_prime n)) primeb) ? ?);
 181   [apply (H1).
 182   |apply (le_n (min_aux (S (fact (nth_prime n))) (S (nth_prime n)) primeb)).
 183   ]
 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 *)