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