matita/library_auto/auto/nat/fermat_little_theorem.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 (*       \ /        This file 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/fermat_little_theorem".
  16
  17 include "auto/nat/exp.ma".
  18 include "auto/nat/gcd.ma".
  19 include "auto/nat/permutation.ma".
  20 include "auto/nat/congruence.ma".
  21
  22 theorem permut_S_mod: \forall n:nat. permut (S_mod (S n)) n.
  23 intro.
  24 unfold permut.
  25 split
  26 [ intros.
  27   unfold S_mod.
  28   auto
  29   (*apply le_S_S_to_le.
  30   change with ((S i) \mod (S n) < S n).
  31   apply lt_mod_m_m.
  32   unfold lt.
  33   apply le_S_S.
  34   apply le_O_n*)
  35 | unfold injn.
  36   intros.
  37   apply inj_S.
  38   rewrite < (lt_to_eq_mod i (S n))
  39   [ rewrite < (lt_to_eq_mod j (S n))
  40     [ cut (i < n \lor i = n)
  41       [ cut (j < n \lor j = n)
  42         [ elim Hcut
  43           [ elim Hcut1
  44             [ (* i < n, j< n *)
  45               rewrite < mod_S
  46               [ rewrite < mod_S
  47                 [ (*qui auto non chiude il goal, chiuso invece dalla tattica
  48                    * apply H2
  49                    *)
  50                   apply H2
  51                 | auto
  52                   (*unfold lt.
  53                   apply le_S_S.
  54                   apply le_O_n*)
  55                 | rewrite > lt_to_eq_mod;
  56                     auto(*unfold lt;apply le_S_S;assumption*)
  57                 ]
  58               | auto
  59                 (*unfold lt.
  60                 apply le_S_S.
  61                 apply le_O_n*)
  62               | rewrite > lt_to_eq_mod
  63                 [ auto
  64                   (*unfold lt.
  65                   apply le_S_S.
  66                   assumption*)
  67                 | auto
  68                   (*unfold lt.
  69                   apply le_S_S.
  70                   assumption*)
  71                 ]
  72               ]
  73             | (* i < n, j=n *)
  74               unfold S_mod in H2.
  75               simplify.
  76               apply False_ind.
  77               apply (not_eq_O_S (i \mod (S n))).
  78               apply sym_eq.
  79               rewrite < (mod_n_n (S n))
  80               [ rewrite < H4 in \vdash (? ? ? (? %?)).
  81                 rewrite < mod_S
  82                 [ assumption
  83                 | auto
  84                   (*unfold lt.
  85                   apply le_S_S.
  86                   apply le_O_n*)
  87                 | rewrite > lt_to_eq_mod;
  88                     auto;(*unfold lt;apply le_S_S;assumption*)
  89                 ]
  90               | auto
  91                 (*unfold lt.
  92                 apply le_S_S.
  93                 apply le_O_n*)
  94               ]
  95             ]
  96           | (* i = n, j < n *)
  97             elim Hcut1
  98             [ apply False_ind.
  99               apply (not_eq_O_S (j \mod (S n))).
 100               rewrite < (mod_n_n (S n))
 101               [ rewrite < H3 in \vdash (? ? (? %?) ?).
 102                 rewrite < mod_S
 103                 [ assumption
 104                 | auto
 105                   (*unfold lt.
 106                   apply le_S_S.
 107                   apply le_O_n*)
 108                 | rewrite > lt_to_eq_mod;
 109                     auto(*unfold lt;apply le_S_S;assumption*)
 110                 ]
 111               | auto
 112                 (*unfold lt.
 113                 apply le_S_S.
 114                 apply le_O_n*)
 115               ]
 116             |(* i = n, j= n*)
 117               auto
 118               (*rewrite > H3.
 119               rewrite > H4.
 120               reflexivity*)
 121             ]
 122           ]
 123         | auto
 124           (*apply le_to_or_lt_eq.
 125           assumption*)
 126         ]
 127       | auto
 128         (*apply le_to_or_lt_eq.
 129         assumption*)
 130       ]
 131     | auto
 132       (*unfold lt.
 133       apply le_S_S.
 134       assumption*)
 135     ]
 136   | auto
 137     (*unfold lt.
 138     apply le_S_S.
 139     assumption*)
 140   ]
 141 ]
 142 qed.
 143
 144 (*
 145 theorem eq_fact_pi: \forall n,m:nat. n < m \to n! = pi n (S_mod m).
 146 intro.elim n.
 147 simplify.reflexivity.
 148 change with (S n1)*n1!=(S_mod m n1)*(pi n1 (S_mod m)).
 149 unfold S_mod in \vdash (? ? ? (? % ?)).
 150 rewrite > lt_to_eq_mod.
 151 apply eq_f.apply H.apply (trans_lt ? (S n1)).
 152 simplify. apply le_n.assumption.assumption.
 153 qed.
 154 *)
 155
 156 theorem prime_to_not_divides_fact: \forall p:nat. prime p \to \forall n:nat.
 157 n \lt p \to \not divides p n!.
 158 intros 3.
 159 elim n
 160 [ unfold Not.
 161   intros.
 162   apply (lt_to_not_le (S O) p)
 163   [ unfold prime in H.
 164     elim H.
 165     assumption
 166   | auto
 167     (*apply divides_to_le.
 168     unfold lt.
 169     apply le_n.
 170     assumption*)
 171   ]
 172 | change with (divides p ((S n1)*n1!) \to False).
 173   intro.
 174   cut (divides p (S n1) \lor divides p n1!)
 175   [ elim Hcut
 176     [ apply (lt_to_not_le (S n1) p)
 177       [ assumption
 178       | auto
 179         (*apply divides_to_le
 180         [ unfold lt.
 181           apply le_S_S.
 182           apply le_O_n
 183         | assumption
 184         ]*)
 185       ]
 186     | auto
 187       (*apply H1
 188       [ apply (trans_lt ? (S n1))
 189         [ unfold lt.
 190           apply le_n
 191         | assumption
 192         ]
 193       | assumption
 194       ]*)
 195     ]
 196   | auto
 197     (*apply divides_times_to_divides;
 198       assumption*)
 199   ]
 200 ]
 201 qed.
 202
 203 theorem permut_mod: \forall p,a:nat. prime p \to
 204 \lnot divides p a\to permut (\lambda n.(mod (a*n) p)) (pred p).
 205 unfold permut.
 206 intros.
 207 split
 208 [ intros.
 209   apply le_S_S_to_le.
 210   apply (trans_le ? p)
 211   [ change with (mod (a*i) p < p).
 212     apply lt_mod_m_m.
 213     unfold prime in H.
 214     elim H.
 215     auto
 216     (*unfold lt.
 217     apply (trans_le ? (S (S O)))
 218     [ apply le_n_Sn
 219     | assumption
 220     ]*)
 221   | rewrite < S_pred
 222     [ apply le_n
 223     | unfold prime in H.
 224       elim H.
 225       auto
 226       (*apply (trans_lt ? (S O))
 227       [ unfold lt.
 228         apply le_n
 229       | assumption
 230       ]*)
 231     ]
 232   ]
 233 | unfold injn.
 234   intros.
 235   apply (nat_compare_elim i j)
 236   [ (* i < j *)
 237     intro.
 238     absurd (j-i \lt p)
 239     [ unfold lt.
 240       rewrite > (S_pred p)
 241       [ auto
 242         (*apply le_S_S.
 243         apply le_plus_to_minus.
 244         apply (trans_le ? (pred p))
 245         [ assumption
 246         | rewrite > sym_plus.
 247           apply le_plus_n
 248         ]*)
 249       | auto
 250         (*unfold prime in H.
 251         elim H.
 252         apply (trans_lt ? (S O))
 253         [ unfold lt.
 254           apply le_n
 255         | assumption
 256         ]*)
 257       ]
 258     | apply (le_to_not_lt p (j-i)).
 259       apply divides_to_le
 260       [ auto
 261         (*unfold lt.
 262         apply le_SO_minus.
 263         assumption*)
 264       | cut (divides p a \lor divides p (j-i))
 265         [ elim Hcut
 266           [ apply False_ind.
 267             auto
 268             (*apply H1.
 269             assumption*)
 270           | assumption
 271           ]
 272         | apply divides_times_to_divides
 273           [ assumption
 274           | rewrite > distr_times_minus.
 275             apply eq_mod_to_divides
 276             [ auto
 277               (*unfold prime in H.
 278               elim H.
 279               apply (trans_lt ? (S O))
 280               [ unfold lt.
 281                 apply le_n
 282               | assumption
 283               ]*)
 284             | auto
 285               (*apply sym_eq.
 286               apply H4*)
 287             ]
 288           ]
 289         ]
 290       ]
 291     ]
 292   |(* i = j *)
 293     auto
 294     (*intro.
 295     assumption*)
 296   | (* j < i *)
 297     intro.
 298     absurd (i-j \lt p)
 299     [ unfold lt.
 300       rewrite > (S_pred p)
 301       [ auto
 302         (*apply le_S_S.
 303         apply le_plus_to_minus.
 304         apply (trans_le ? (pred p))
 305         [ assumption
 306         | rewrite > sym_plus.
 307           apply le_plus_n
 308         ]*)
 309       | auto
 310         (*unfold prime in H.
 311         elim H.
 312         apply (trans_lt ? (S O))
 313         [ unfold lt.
 314           apply le_n
 315         | assumption
 316         ]*)
 317       ]
 318     | apply (le_to_not_lt p (i-j)).
 319       apply divides_to_le
 320       [ auto
 321         (*unfold lt.
 322         apply le_SO_minus.
 323         assumption*)
 324       | cut (divides p a \lor divides p (i-j))
 325         [ elim Hcut
 326           [ apply False_ind.
 327             auto
 328             (*apply H1.
 329             assumption*)
 330           | assumption
 331           ]
 332         | apply divides_times_to_divides
 333           [ assumption
 334           | rewrite > distr_times_minus.
 335             apply eq_mod_to_divides
 336             [ auto
 337               (*unfold prime in H.
 338               elim H.
 339               apply (trans_lt ? (S O))
 340               [ unfold lt.
 341                 apply le_n
 342               | assumption
 343               ]*)
 344             | apply H4
 345             ]
 346           ]
 347         ]
 348       ]
 349     ]
 350   ]
 351 ]
 352 qed.
 353
 354 theorem congruent_exp_pred_SO: \forall p,a:nat. prime p \to \lnot divides p a \to
 355 congruent (exp a (pred p)) (S O) p.
 356 intros.
 357 cut (O < a)
 358 [ cut (O < p)
 359   [ cut (O < pred p)
 360     [ apply divides_to_congruent
 361       [ assumption
 362       | auto
 363         (*change with (O < exp a (pred p)).
 364         apply lt_O_exp.
 365         assumption*)
 366       | cut (divides p (exp a (pred p)-(S O)) \lor divides p (pred p)!)
 367         [ elim Hcut3
 368           [ assumption
 369           | apply False_ind.
 370             apply (prime_to_not_divides_fact p H (pred p))
 371             [ unfold lt.
 372               auto
 373               (*rewrite < (S_pred ? Hcut1).
 374               apply le_n*)
 375             | assumption
 376             ]
 377           ]
 378         | apply divides_times_to_divides
 379           [ assumption
 380           | rewrite > times_minus_l.
 381             rewrite > (sym_times (S O)).
 382             rewrite < times_n_SO.
 383             rewrite > (S_pred (pred p) Hcut2).
 384             rewrite > eq_fact_pi.
 385             rewrite > exp_pi_l.
 386             apply congruent_to_divides
 387             [ assumption
 388             | apply (transitive_congruent p ?
 389                   (pi (pred (pred p)) (\lambda m. a*m \mod p) (S O)))
 390               [ apply (congruent_pi (\lambda m. a*m)).
 391                 assumption
 392               | cut (pi (pred(pred p)) (\lambda m.m) (S O)
 393                      = pi (pred(pred p)) (\lambda m.a*m \mod p) (S O))
 394                 [ rewrite > Hcut3.
 395                   apply congruent_n_n
 396                 | rewrite < eq_map_iter_i_pi.
 397                   rewrite < eq_map_iter_i_pi.
 398                   apply (permut_to_eq_map_iter_i ? ? ? ? ? (λm.m))
 399                   [ apply assoc_times
 400                   | (*NB qui auto non chiude il goal, chiuso invece dalla sola
 401                      ( tattica apply sys_times
 402                      *)
 403                     apply sym_times
 404                   | rewrite < plus_n_Sm.
 405                     rewrite < plus_n_O.
 406                     rewrite < (S_pred ? Hcut2).
 407                     auto
 408                     (*apply permut_mod
 409                     [ assumption
 410                     | assumption
 411                     ]*)
 412                   | intros.
 413                     cut (m=O)
 414                     [ auto
 415                       (*rewrite > Hcut3.
 416                       rewrite < times_n_O.
 417                       apply mod_O_n.*)
 418                     | auto
 419                       (*apply sym_eq.
 420                       apply le_n_O_to_eq.
 421                       apply le_S_S_to_le.
 422                       assumption*)
 423                     ]
 424                   ]
 425                 ]
 426               ]
 427             ]
 428           ]
 429         ]
 430       ]
 431     | unfold lt.
 432       apply le_S_S_to_le.
 433       rewrite < (S_pred ? Hcut1).
 434       unfold prime in H.
 435       elim H.
 436       assumption
 437     ]
 438   | unfold prime in H.
 439     elim H.
 440     auto
 441     (*apply (trans_lt ? (S O))
 442     [ unfold lt.
 443       apply le_n
 444     | assumption
 445     ]*)
 446   ]
 447 | cut (O < a \lor O = a)
 448   [ elim Hcut
 449     [ assumption
 450     | apply False_ind.
 451       apply H1.
 452       rewrite < H2.
 453       auto
 454       (*apply (witness ? ? O).
 455       apply times_n_O*)
 456     ]
 457   | auto
 458     (*apply le_to_or_lt_eq.
 459     apply le_O_n*)
 460   ]
 461 ]
 462 qed.
 463