helm/software/matita/library/nat/sieve.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 include "nat/primes.ma".
  16 include "list/sort.ma".
  17
  18 let rec list_n_aux n k \def
  19     match n with
  20     [ O => nil nat
  21     | S n1 => k::list_n_aux n1 (S k) ].
  22
  23 definition list_n : nat \to list nat \def
  24   \lambda n.list_n_aux (pred n) 2.
  25
  26 let rec sieve_aux l1 l2 t on t \def
  27   match t with
  28   [ O => l1
  29   | S t1 => match l2 with
  30     [ nil => l1
  31     | cons n tl => sieve_aux (n::l1) (filter nat tl (\lambda x.notb (divides_b n x))) t1]].
  32
  33 definition sieve : nat \to list nat \def
  34   \lambda m.sieve_aux [] (list_n m) m.
  35
  36 definition sorted_lt \def sorted ? lt.
  37 definition sorted_gt \def sorted ? gt.
  38
  39 lemma sieve_prime : \forall t,k,l2,l1.
  40   (\forall p.(in_list ? p l1 \to prime p \land p \leq k \land \forall x.in_list ? x l2 \to p < x) \land
  41              (prime p \to p \leq k \to (\forall x.in_list ? x l2 \to p < x) \to in_list ? p l1)) \to
  42   (\forall x.(in_list ? x l2 \to 2 \leq x \land x \leq k \land \forall p.in_list ? p l1 \to \lnot p \divides x) \land
  43              (2 \leq x \to x \leq k \to (\forall p.in_list ? p l1 \to \lnot p \divides x) \to
  44               in_list ? x l2)) \to
  45   length ? l2 \leq t \to
  46   sorted_gt l1 \to
  47   sorted_lt l2 \to
  48   sorted_gt (sieve_aux l1 l2 t) \land
  49   \forall p.(in_list ? p (sieve_aux l1 l2 t) \to prime p \land p \leq k) \land
  50             (prime p \to p \leq k \to in_list ? p (sieve_aux l1 l2 t)).
  51 intro.elim t 0
  52   [intros;cut (l2 = [])
  53      [|elim l2 in H2 ⊢ %
  54         [reflexivity
  55         |simplify in H5;elim (not_le_Sn_O ? H5)]]
  56    simplify;split
  57      [assumption
  58      |intro;elim (H p);split;intros
  59         [elim (H5 H7);assumption
  60         |apply (H6 H7 H8);rewrite > Hcut;intros;elim (not_in_list_nil ? ? H9)]]
  61   |intros 4;elim l2
  62      [simplify;split;
  63         [assumption
  64         |intro;elim (H1 p);split;intros
  65            [elim (H6 H8);assumption
  66            |apply (H7 H8 H9);intros;elim (not_in_list_nil ? ? H10)]]
  67      |simplify;elim (H k (filter ? l (\lambda x.notb (divides_b a x))) (a::l1))
  68         [split;
  69            [assumption
  70            |intro;apply H8;]
  71         |split;intros
  72            [elim (in_list_cons_case ? ? ? ? H7);
  73               [rewrite > H8;split
  74                  [split
  75                     [unfold;intros;split
  76                        [elim (H3 a);elim H9
  77                           [elim H11;assumption
  78                           |apply in_list_head]
  79                        |intros;elim (le_to_or_lt_eq ? ? (divides_to_le ? ? ? H9))
  80                           [cut (1 < a) as Lt1a; [2: apply (trans_lt ??? H10 H11)]
  81                            letin a1 ≝ (smallest_factor a);
  82                            lapply (divides_smallest_factor_n a) as H14;
  83                             [2: apply (trans_lt ? (S O) ? ? Lt1a);
  84                                 apply lt_O_S
  85                             | fold unfold a1 a1 in H14;
  86                               lapply (prime_smallest_factor_n a Lt1a) as H16;
  87                               fold unfold a1 a1 in H16;
  88                               cut (a1 ≤ m) as H15;
  89                               [2: generalize in match (leb_to_Prop a1 m);
  90                                   elim (leb a1 m); simplify in H12;
  91                                    [ assumption
  92                                    | elim (lt_smallest_factor_to_not_divides a m Lt1a H10 ? H9);
  93                                      apply (not_le_to_lt ?? H12)]
  94                               | clearbody a1;
  95                                 elim (H3 a);elim H12
  96                                 [clear H13 H12;elim (H18 ? ? H14);elim (H2 a1);
  97                                  apply H13
  98                                    [assumption
  99                                    |elim H17;apply (trans_le ? ? ? ? H20);
 100                                     apply (trans_le ? ? ? H15);
 101                                     apply lt_to_le;assumption
 102                                    |intros;apply (trans_le ? (S m))
 103                                       [apply le_S_S;assumption
 104                                       |apply (trans_le ? ? ? H11);
 105                                        elim (in_list_cons_case ? ? ? ? H19)
 106                                          [rewrite > H20;apply le_n
 107                                          |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);assumption]]]
 108                                 |apply in_list_head]]]
 109                           |elim (H3 a);elim H11
 110                              [elim H13;apply lt_to_le;assumption
 111                              |apply in_list_head]
 112                           |assumption]]
 113                     |elim (H3 a);elim H9
 114                        [elim H11;assumption
 115                        |apply in_list_head]]
 116                  |intros;elim (le_to_or_lt_eq a x)
 117                     [assumption
 118                     |rewrite > H10 in H9;lapply (in_list_filter_to_p_true ? ? ? H9);
 119                      lapply (divides_n_n x);
 120                      rewrite > (divides_to_divides_b_true ? ? ? Hletin1) in Hletin
 121                        [simplify in Hletin;destruct Hletin
 122                        |rewrite < H10;elim (H3 a);elim H11
 123                           [elim H13;apply lt_to_le;assumption
 124                           |apply in_list_head]]
 125                     |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);apply (in_list_filter ? ? ? H9)]]
 126                  |elim (H2 p);elim (H9 H8);split
 127                     [assumption
 128                     |intros;apply H12;apply in_list_cons;apply (in_list_filter ? ? ? H13)]]
 129            |elim (decidable_eq_nat p a)
 130               [rewrite > H10;apply in_list_head
 131               |apply in_list_cons;elim (H2 p);apply (H12 H7 H8);intros;
 132                apply (trans_le ? a)
 133                  [elim (decidable_lt p a)
 134                     [assumption
 135                     |lapply (not_lt_to_le ? ? H14);
 136                      lapply (decidable_divides a p)
 137                        [elim Hletin1
 138                           [elim H7;lapply (H17 ? H15)
 139                              [elim H10;symmetry;assumption
 140                              |elim (H3 a);elim H18
 141                                 [elim H20;assumption
 142                                 |apply in_list_head]]
 143                           |elim (Not_lt_n_n p);apply H9;apply in_list_filter_r
 144                              [elim (H3 p);apply (in_list_tail ? ? a)
 145                                 [apply H17
 146                                    [apply prime_to_lt_SO;assumption
 147                                    |assumption
 148                                    |intros;elim H7;intro;lapply (H20 ? H21)
 149                                       [rewrite > Hletin2 in H18;elim (H11 H18);
 150                                        lapply (H23 a)
 151                                          [elim (lt_to_not_le ? ? Hletin3 Hletin)
 152                                          |apply in_list_head]
 153                                       |apply prime_to_lt_SO;elim (H2 p1);elim (H22 H18);
 154                                        elim H24;assumption]]
 155                                 |unfold;intro;apply H15;rewrite > H18;apply divides_n_n]
 156                              |rewrite > (not_divides_to_divides_b_false ? ? ? H15);
 157                                 [reflexivity
 158                                 |elim (H3 a);elim H16
 159                                    [elim H18;apply lt_to_le;assumption
 160                                    |apply in_list_head]]]]
 161                        |elim (H3 a);elim H15
 162                           [elim H17;apply lt_to_le;assumption
 163                           |apply in_list_head]]]
 164                  |elim (in_list_cons_case ? ? ? ? H13)
 165                     [rewrite > H14;apply le_n
 166                     |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);assumption]]]]
 167          |elim (H3 x);split;intros;
 168             [split
 169                [elim H7
 170                   [assumption
 171                   |apply in_list_cons;apply (in_list_filter ? ? ? H9)]
 172                |intros;elim (in_list_cons_case ? ? ? ? H10)
 173                   [rewrite > H11;intro;lapply (in_list_filter_to_p_true ? ? ? H9);
 174                    rewrite > (divides_to_divides_b_true ? ? ? H12) in Hletin
 175                      [simplify in Hletin;destruct Hletin
 176                      |elim (H3 a);elim H13
 177                         [elim H15;apply lt_to_le;assumption
 178                         |apply in_list_head]]
 179                   |elim H7
 180                      [apply H13;assumption
 181                      |apply in_list_cons;apply (in_list_filter ? ? ? H9)]]]
 182             |elim (in_list_cons_case ? ? ? ? (H8 ? ? ?))
 183                [elim (H11 x)
 184                   [rewrite > H12;apply in_list_head
 185                   |apply divides_n_n]
 186                |assumption
 187                |assumption
 188                |intros;apply H11;apply in_list_cons;assumption
 189                |apply in_list_filter_r;
 190                   [assumption
 191                   |lapply (H11 a)
 192                      [rewrite > (not_divides_to_divides_b_false ? ? ? Hletin);
 193                         [reflexivity
 194                         |elim (H3 a);elim H13
 195                            [elim H15;apply lt_to_le;assumption
 196                            |apply in_list_head]]
 197                      |apply in_list_head]]]]
 198          |apply (trans_le ? ? ? (le_length_filter ? ? ?));apply le_S_S_to_le;
 199           apply H4
 200          |apply sort_cons
 201             [assumption
 202             |intros;unfold;elim (H2 y);elim (H8 H7);
 203              apply H11;apply in_list_head]
 204          |generalize in match (sorted_cons_to_sorted ? ? ? ? H6);elim l
 205             [simplify;assumption
 206             |simplify;elim (notb (divides_b a a1));simplify
 207                [lapply (sorted_cons_to_sorted ? ? ? ? H8);lapply (H7 Hletin);
 208                 apply (sort_cons ? ? ? ? Hletin1);intros;
 209                 apply (sorted_to_minimum ? ? ? ? H8);apply (in_list_filter ? ? ? H9);
 210                |apply H7;apply (sorted_cons_to_sorted ? ? ? ? H8)]]]]]
 211 qed.
 212
 213 definition list_of_primes \def \lambda n.\lambda l.
 214 \forall p.in_list nat p l  \to prime p \land p \leq n.
 215
 216 lemma in_list_SSO_list_n : \forall n.2 \leq n \to in_list ? 2 (list_n n).
 217 intros;elim H;simplify
 218   [apply in_list_head
 219   |elim H1 in H2 ⊢ %;simplify;apply in_list_head]
 220 qed.
 221
 222 lemma le_list_n_aux_k_k : \forall n,m,k.in_list ? n (list_n_aux m k) \to
 223                           k \leq n.
 224 intros 2;elim m
 225   [simplify in H;elim (not_in_list_nil ? ? H)
 226   |simplify in H1;elim (in_list_cons_case ? ? ? ? H1)
 227      [rewrite > H2;apply le_n
 228      |apply lt_to_le;apply H;assumption]]
 229 qed.
 230
 231 lemma le_SSO_list_n : \forall m,n.in_list nat n (list_n m) \to 2 \leq n.
 232 intros;unfold list_n in H;apply (le_list_n_aux_k_k ? ? ? H);
 233 qed.
 234
 235 lemma le_list_n_aux : \forall n,m,k.in_list ? n (list_n_aux m k) \to n \leq k+m-1.
 236 intros 2;elim m
 237   [simplify in H;elim (not_in_list_nil ? ? H)
 238   |simplify in H1;elim (in_list_cons_case ? ? ? ? H1)
 239      [rewrite > H2;rewrite < plus_n_Sm;simplify;rewrite < minus_n_O;
 240       rewrite > plus_n_O in \vdash (? % ?);apply le_plus_r;apply le_O_n
 241      |rewrite < plus_n_Sm;apply (H (S k));assumption]]
 242 qed.
 243
 244 lemma le_list_n : \forall n,m.in_list ? n (list_n m) \to n \leq m.
 245 intros;unfold list_n in H;lapply (le_list_n_aux ? ? ? H);
 246 simplify in Hletin;elim m in H Hletin ⊢ %
 247    [simplify in H;elim (not_in_list_nil ? ? H)
 248    |simplify in H;assumption]
 249 qed.
 250
 251
 252 lemma le_list_n_aux_r : \forall n,m.O < m \to \forall k.k \leq n \to n \leq k+m-1 \to in_list ? n (list_n_aux m k).
 253 intros 3;elim H 0
 254   [intros;simplify;rewrite < plus_n_Sm in H2;simplify in H2;
 255    rewrite < plus_n_O in H2;rewrite < minus_n_O in H2;
 256    rewrite > (antisymmetric_le k n H1 H2);apply in_list_head
 257   |intros 5;simplify;elim H3 in H2 ⊢ %
 258      [apply in_list_head
 259      |apply in_list_cons;apply H5
 260         [apply le_S_S;assumption
 261         |rewrite < plus_n_Sm in H6;apply H6]]]
 262 qed.
 263
 264 lemma le_list_n_r : \forall n,m.S O < m \to 2 \leq n \to n \leq m \to in_list ? n (list_n m).
 265 intros;unfold list_n;apply le_list_n_aux_r
 266   [elim H;simplify
 267      [apply lt_O_S
 268      |elim H3 in H4 ⊢ %;
 269         [apply lt_O_S
 270         |simplify in H7;apply le_S;assumption]]
 271   |assumption
 272   |simplify;elim H in H2 ⊢ %;simplify;assumption]
 273 qed.
 274
 275 lemma le_length_list_n : \forall n. length ? (list_n n) \leq n.
 276 intro;cut (\forall n,k.length ? (list_n_aux n k) \leq (S n))
 277   [elim n;simplify
 278      [apply le_n
 279      |apply Hcut]
 280   |intro;elim n1;simplify
 281      [apply le_O_n
 282      |apply le_S_S;apply H]]
 283 qed.
 284
 285 lemma sorted_list_n_aux : \forall n,k.sorted_lt (list_n_aux n k).
 286 intro.elim n 0
 287   [simplify;intro;apply sort_nil
 288   |intro;simplify;intros 2;apply sort_cons
 289      [apply H
 290      |intros;lapply (le_list_n_aux_k_k ? ? ? H1);assumption]]
 291 qed.
 292
 293 lemma sieve_sound1 : \forall n.2 \leq n \to
 294 sorted_gt (sieve n) \land list_of_primes n (sieve n).
 295 intros;elim (sieve_prime n n (list_n n) [])
 296   [split
 297      [assumption
 298      |intro;unfold sieve in H3;elim (H2 p);elim (H3 H5);split;assumption]
 299   |split;intros
 300      [elim (not_in_list_nil ? ? H1)
 301      |lapply (lt_to_not_le ? ? (H3 2 ?))
 302         [apply in_list_SSO_list_n;assumption
 303         |elim Hletin;apply prime_to_lt_SO;assumption]]
 304   |split;intros
 305      [split
 306         [split
 307            [apply (le_SSO_list_n ? ? H1)
 308            |apply (le_list_n ? ? H1)]
 309         |intros;elim (not_in_list_nil ? ? H2)]
 310      |apply le_list_n_r;assumption]
 311   |apply le_length_list_n
 312   |apply sort_nil
 313   |elim n;simplify
 314      [apply sort_nil
 315      |elim n1;simplify
 316         [apply sort_nil
 317         |simplify;apply sort_cons
 318            [apply sorted_list_n_aux
 319            |intros;lapply (le_list_n_aux_k_k ? ? ? H3);
 320             assumption]]]]
 321 qed.
 322
 323 lemma sieve_sorted : \forall n.sorted_gt (sieve n).
 324 intros;elim (decidable_le 2 n)
 325   [elim (sieve_sound1 ? H);assumption
 326   |generalize in match (le_S_S_to_le ? ? (not_le_to_lt ? ? H));cases n
 327      [intro;simplify;apply sort_nil
 328      |intros;lapply (le_S_S_to_le ? ? H1);rewrite < (le_n_O_to_eq ? Hletin);
 329       simplify;apply sort_nil]]
 330 qed.
 331
 332 lemma in_list_sieve_to_prime : \forall n,p.2 \leq n \to in_list ? p (sieve n) \to
 333                                prime p.
 334 intros;elim (sieve_sound1 ? H);elim (H3 ? H1);assumption;
 335 qed.
 336
 337 lemma in_list_sieve_to_leq : \forall n,p.2 \leq n \to in_list ? p (sieve n) \to
 338                              p \leq n.
 339 intros;elim (sieve_sound1 ? H);elim (H3 ? H1);assumption;
 340 qed.
 341
 342 lemma sieve_sound2 : \forall n,p.p \leq n \to prime p \to in_list ? p (sieve n).
 343 intros;elim (sieve_prime n n (list_n n) [])
 344   [elim (H3 p);apply H5;assumption
 345   |split
 346      [intro;elim (not_in_list_nil ? ? H2)
 347      |intros;lapply (lt_to_not_le ? ? (H4 2 ?))
 348         [apply in_list_SSO_list_n;apply (trans_le ? ? ? ? H);
 349          apply prime_to_lt_SO;assumption
 350         |elim Hletin;apply prime_to_lt_SO;assumption]]
 351   |split;intros
 352      [split;intros
 353         [split
 354            [apply (le_SSO_list_n ? ? H2)
 355            |apply (le_list_n ? ? H2)]
 356         |elim (not_in_list_nil ? ? H3)]
 357      |apply le_list_n_r
 358         [apply (trans_le ? ? ? H2 H3)
 359         |assumption
 360         |assumption]]
 361   |apply le_length_list_n
 362   |apply sort_nil
 363   |elim n;simplify
 364      [apply sort_nil
 365      |elim n1;simplify
 366         [apply sort_nil
 367         |simplify;apply sort_cons
 368            [apply sorted_list_n_aux
 369            |intros;lapply (le_list_n_aux_k_k ? ? ? H4);
 370             assumption]]]]
 371 qed.
 372