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 include "nat/congruence.ma".
  21
  22 theorem permut_S_mod: \forall n:nat. permut (S_mod (S n)) n.
  23 intro.unfold permut.split.intros.
  24 unfold S_mod.
  25 apply le_S_S_to_le.
  26 change with ((S i) \mod (S n) < S n).
  27 apply lt_mod_m_m.
  28 unfold lt.apply le_S_S.apply le_O_n.
  29 unfold injn.intros.
  30 apply inj_S.
  31 rewrite < (lt_to_eq_mod i (S n)).
  32 rewrite < (lt_to_eq_mod j (S n)).
  33 cut (i < n \lor i = n).
  34 cut (j < n \lor j = n).
  35 elim Hcut.
  36 elim Hcut1.
  37 (* i < n, j< n *)
  38 rewrite < mod_S.
  39 rewrite < mod_S.
  40 apply H2.unfold lt.apply le_S_S.apply le_O_n.
  41 rewrite > lt_to_eq_mod.
  42 unfold lt.apply le_S_S.assumption.
  43 unfold lt.apply le_S_S.assumption.
  44 unfold lt.apply le_S_S.apply le_O_n.
  45 rewrite > lt_to_eq_mod.
  46 unfold lt.apply le_S_S.assumption.
  47 unfold lt.apply le_S_S.assumption.
  48 (* i < n, j=n *)
  49 unfold S_mod in H2.
  50 simplify.
  51 apply False_ind.
  52 apply (not_eq_O_S (i \mod (S n))).
  53 apply sym_eq.
  54 rewrite < (mod_n_n (S n)).
  55 rewrite < H4 in \vdash (? ? ? (? %?)).
  56 rewrite < mod_S.assumption.
  57 unfold lt.apply le_S_S.apply le_O_n.
  58 rewrite > lt_to_eq_mod.
  59 unfold lt.apply le_S_S.assumption.
  60 unfold lt.apply le_S_S.assumption.
  61 unfold lt.apply le_S_S.apply le_O_n.
  62 (* i = n, j < n *)
  63 elim Hcut1.
  64 apply False_ind.
  65 apply (not_eq_O_S (j \mod (S n))).
  66 rewrite < (mod_n_n (S n)).
  67 rewrite < H3 in \vdash (? ? (? %?) ?).
  68 rewrite < mod_S.assumption.
  69 unfold lt.apply le_S_S.apply le_O_n.
  70 rewrite > lt_to_eq_mod.
  71 unfold lt.apply le_S_S.assumption.
  72 unfold lt.apply le_S_S.assumption.
  73 unfold lt.apply le_S_S.apply le_O_n.
  74 (* i = n, j= n*)
  75 rewrite > H3.
  76 rewrite > H4.
  77 reflexivity.
  78 apply le_to_or_lt_eq.assumption.
  79 apply le_to_or_lt_eq.assumption.
  80 unfold lt.apply le_S_S.assumption.
  81 unfold lt.apply le_S_S.assumption.
  82 qed.
  83
  84 (*
  85 theorem eq_fact_pi: \forall n,m:nat. n < m \to n! = pi n (S_mod m).
  86 intro.elim n.
  87 simplify.reflexivity.
  88 change with (S n1)*n1!=(S_mod m n1)*(pi n1 (S_mod m)).
  89 unfold S_mod in \vdash (? ? ? (? % ?)).
  90 rewrite > lt_to_eq_mod.
  91 apply eq_f.apply H.apply (trans_lt ? (S n1)).
  92 simplify. apply le_n.assumption.assumption.
  93 qed.
  94 *)
  95
  96 theorem prime_to_not_divides_fact: \forall p:nat. prime p \to \forall n:nat.
  97 n \lt p \to \not divides p n!.
  98 intros 3.elim n.unfold Not.intros.
  99 apply (lt_to_not_le (S O) p).
 100 unfold prime in H.elim H.
 101 assumption.apply divides_to_le.unfold lt.apply le_n.
 102 assumption.
 103 change with (divides p ((S n1)*n1!) \to False).
 104 intro.
 105 cut (divides p (S n1) \lor divides p n1!).
 106 elim Hcut.apply (lt_to_not_le (S n1) p).
 107 assumption.
 108 apply divides_to_le.unfold lt.apply le_S_S.apply le_O_n.
 109 assumption.apply H1.
 110 apply (trans_lt ? (S n1)).unfold lt. apply le_n.
 111 assumption.assumption.
 112 apply divides_times_to_divides.
 113 assumption.assumption.
 114 qed.
 115
 116 theorem permut_mod: \forall p,a:nat. prime p \to
 117 \lnot divides p a\to permut (\lambda n.(mod (a*n) p)) (pred p).
 118 unfold permut.intros.
 119 split.intros.apply le_S_S_to_le.
 120 apply (trans_le ? p).
 121 change with (mod (a*i) p < p).
 122 apply lt_mod_m_m.
 123 unfold prime in H.elim H.
 124 unfold lt.apply (trans_le ? (S (S O))).
 125 apply le_n_Sn.assumption.
 126 rewrite < S_pred.apply le_n.
 127 unfold prime in H.
 128 elim H.
 129 apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.
 130 unfold injn.intros.
 131 apply (nat_compare_elim i j).
 132 (* i < j *)
 133 intro.
 134 absurd (j-i \lt p).
 135 unfold lt.
 136 rewrite > (S_pred p).
 137 apply le_S_S.
 138 apply le_plus_to_minus.
 139 apply (trans_le ? (pred p)).assumption.
 140 rewrite > sym_plus.
 141 apply le_plus_n.
 142 unfold prime in H.
 143 elim H.
 144 apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.
 145 apply (le_to_not_lt p (j-i)).
 146 apply divides_to_le.unfold lt.
 147 apply le_SO_minus.assumption.
 148 cut (divides p a \lor divides p (j-i)).
 149 elim Hcut.apply False_ind.apply H1.assumption.assumption.
 150 apply divides_times_to_divides.assumption.
 151 rewrite > distr_times_minus.
 152 apply eq_mod_to_divides.
 153 unfold prime in H.
 154 elim H.
 155 apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.
 156 apply sym_eq.
 157 apply H4.
 158 (* i = j *)
 159 intro. assumption.
 160 (* j < i *)
 161 intro.
 162 absurd (i-j \lt p).
 163 unfold lt.
 164 rewrite > (S_pred p).
 165 apply le_S_S.
 166 apply le_plus_to_minus.
 167 apply (trans_le ? (pred p)).assumption.
 168 rewrite > sym_plus.
 169 apply le_plus_n.
 170 unfold prime in H.
 171 elim H.
 172 apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.
 173 apply (le_to_not_lt p (i-j)).
 174 apply divides_to_le.unfold lt.
 175 apply le_SO_minus.assumption.
 176 cut (divides p a \lor divides p (i-j)).
 177 elim Hcut.apply False_ind.apply H1.assumption.assumption.
 178 apply divides_times_to_divides.assumption.
 179 rewrite > distr_times_minus.
 180 apply eq_mod_to_divides.
 181 unfold prime in H.
 182 elim H.
 183 apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.
 184 apply H4.
 185 qed.
 186
 187 theorem congruent_exp_pred_SO: \forall p,a:nat. prime p \to \lnot divides p a \to
 188 congruent (exp a (pred p)) (S O) p.
 189 intros.
 190 cut (O < a).
 191 cut (O < p).
 192 cut (O < pred p).
 193 apply divides_to_congruent.
 194 assumption.
 195 change with (O < exp a (pred p)).
 196 apply lt_O_exp.assumption.
 197 cut (divides p (exp a (pred p)-(S O)) \lor divides p (pred p)!).
 198 elim Hcut3.
 199 assumption.
 200 apply False_ind.
 201 apply (prime_to_not_divides_fact p H (pred p)).
 202 change with (S (pred p) \le p).
 203 rewrite < S_pred.apply le_n.
 204 assumption.assumption.
 205 apply divides_times_to_divides.
 206 assumption.
 207 rewrite > times_minus_l.
 208 rewrite > (sym_times (S O)).
 209 rewrite < times_n_SO.
 210 rewrite > (S_pred (pred p)).
 211 rewrite > eq_fact_pi.
 212 (* in \vdash (? ? (? % ?)). *)
 213 rewrite > exp_pi_l.
 214 apply congruent_to_divides.
 215 assumption.
 216 apply (transitive_congruent p ?
 217 (pi (pred (pred p)) (\lambda m. a*m \mod p) (S O))).
 218 apply (congruent_pi (\lambda m. a*m)).
 219 assumption.
 220 cut (pi (pred(pred p)) (\lambda m.m) (S O)
 221 = pi (pred(pred p)) (\lambda m.a*m \mod p) (S O)).
 222 rewrite > Hcut3.apply congruent_n_n.
 223 rewrite < eq_map_iter_i_pi.
 224 rewrite < eq_map_iter_i_pi.
 225 apply permut_to_eq_map_iter_i.
 226 apply assoc_times.
 227 apply sym_times.
 228 rewrite < plus_n_Sm.rewrite < plus_n_O.
 229 rewrite < S_pred.
 230 apply permut_mod.assumption.
 231 assumption.assumption.
 232 intros.cut (m=O).
 233 rewrite > Hcut3.rewrite < times_n_O.
 234 apply mod_O_n.apply sym_eq.apply le_n_O_to_eq.
 235 apply le_S_S_to_le.assumption.
 236 assumption.
 237 change with ((S O) \le pred p).
 238 apply le_S_S_to_le.rewrite < S_pred.
 239 unfold prime in H.elim H.assumption.assumption.
 240 unfold prime in H.elim H.apply (trans_lt ? (S O)).
 241 unfold lt.apply le_n.assumption.
 242 cut (O < a \lor O = a).
 243 elim Hcut.assumption.
 244 apply False_ind.apply H1.
 245 rewrite < H2.
 246 apply (witness ? ? O).apply times_n_O.
 247 apply le_to_or_lt_eq.
 248 apply le_O_n.
 249 qed.
 250