helm/matita/library/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/nat/fermat_little_theorem".
  16
  17 include "nat/exp.ma".
  18 include "nat/gcd.ma".
  19 include "nat/permutation.ma".
  20
  21 theorem permut_mod: \forall p,a:nat. prime p \to
  22 \lnot divides p a\to permut (\lambda n.(mod (a*n) p)) (pred p).
  23 unfold permut.intros.
  24 split.intros.apply le_S_S_to_le.
  25 apply trans_le ? p.
  26 change with mod (a*i) p < p.
  27 apply lt_mod_m_m.
  28 simplify in H.elim H.
  29 simplify.apply trans_le ? (S (S O)).
  30 apply le_n_Sn.assumption.
  31 rewrite < S_pred.apply le_n.
  32 unfold prime in H.
  33 elim H.
  34 apply trans_lt ? (S O).simplify.apply le_n.assumption.
  35 unfold injn.intros.
  36 apply nat_compare_elim i j.
  37 (* i < j *)
  38 intro.
  39 absurd j-i \lt p.
  40 simplify.
  41 rewrite > S_pred p.
  42 apply le_S_S.
  43 apply le_plus_to_minus.
  44 apply trans_le ? (pred p).assumption.
  45 rewrite > sym_plus.
  46 apply le_plus_n.
  47 unfold prime in H.
  48 elim H.
  49 apply trans_lt ? (S O).simplify.apply le_n.assumption.
  50 apply le_to_not_lt p (j-i).
  51 apply divides_to_le.simplify.
  52 apply le_SO_minus.assumption.
  53 cut divides p a \lor divides p (j-i).
  54 elim Hcut.apply False_ind.apply H1.assumption.assumption.
  55 apply divides_times_to_divides.assumption.
  56 rewrite > distr_times_minus.
  57 apply eq_mod_to_divides.
  58 unfold prime in H.
  59 elim H.
  60 apply trans_lt ? (S O).simplify.apply le_n.assumption.
  61 apply sym_eq.
  62 apply H4.
  63 (* i = j *)
  64 intro. assumption.
  65 (* j < i *)
  66 intro.
  67 absurd i-j \lt p.
  68 simplify.
  69 rewrite > S_pred p.
  70 apply le_S_S.
  71 apply le_plus_to_minus.
  72 apply trans_le ? (pred p).assumption.
  73 rewrite > sym_plus.
  74 apply le_plus_n.
  75 unfold prime in H.
  76 elim H.
  77 apply trans_lt ? (S O).simplify.apply le_n.assumption.
  78 apply le_to_not_lt p (i-j).
  79 apply divides_to_le.simplify.
  80 apply le_SO_minus.assumption.
  81 cut divides p a \lor divides p (i-j).
  82 elim Hcut.apply False_ind.apply H1.assumption.assumption.
  83 apply divides_times_to_divides.assumption.
  84 rewrite > distr_times_minus.
  85 apply eq_mod_to_divides.
  86 unfold prime in H.
  87 elim H.
  88 apply trans_lt ? (S O).simplify.apply le_n.assumption.
  89 apply H4.
  90 qed.
  91
  92 (*
  93 theorem bad : \forall p,a:nat. prime p \to \lnot divides p a \to
  94 mod (exp a (pred p)) p = (S O).
  95 intros.
  96 cut map_iter p (\lambda x.x) times (S O) =
  97 map_iter p (\lambda n.(mod (a*n) p)) times (S O).
  98 *)