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)).apply lt_O_exp.assumption
 196         |cut (divides p (exp a (pred p)-(S O)) \lor divides p (pred p)!)
 197           [elim Hcut3
 198             [assumption
 199             |apply False_ind.
 200              apply (prime_to_not_divides_fact p H (pred p))
 201               [unfold lt.rewrite < (S_pred ? Hcut1).apply le_n.
 202               |assumption
 203               ]
 204             ]
 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) Hcut2).
 211             rewrite > eq_fact_pi.
 212             rewrite > exp_pi_l.
 213             apply congruent_to_divides
 214               [assumption
 215               | apply (transitive_congruent p ?
 216                         (pi (pred (pred p)) (\lambda m. a*m \mod p) (S O)))
 217                 [ apply (congruent_pi (\lambda m. a*m)).assumption
 218                 |cut (pi (pred(pred p)) (\lambda m.m) (S O)
 219                        = pi (pred(pred p)) (\lambda m.a*m \mod p) (S O))
 220                   [rewrite > Hcut3.apply congruent_n_n
 221                   |rewrite < eq_map_iter_i_pi.
 222                    rewrite < eq_map_iter_i_pi.
 223                    apply permut_to_eq_map_iter_i
 224                    [apply assoc_times
 225                    |apply sym_times
 226                    |rewrite < plus_n_Sm.
 227                     rewrite < plus_n_O.
 228                     rewrite < (S_pred ? Hcut2).
 229                     apply permut_mod[assumption|assumption]
 230                    |intros.
 231                     cut (m=O)
 232                      [rewrite > Hcut3.
 233                       rewrite < times_n_O.
 234                       apply mod_O_n.
 235                      |apply sym_eq.apply le_n_O_to_eq.apply le_S_S_to_le.assumption
 236                      ]
 237                    ]
 238                  ]
 239                ]
 240              ]
 241            ]
 242          ]
 243        ]
 244      |unfold lt.apply le_S_S_to_le.rewrite < (S_pred ? Hcut1).
 245       unfold prime in H.elim H.assumption
 246      ]
 247    |unfold prime in H.elim H.
 248     apply (trans_lt ? (S O))[unfold lt.apply le_n|assumption]
 249    ]
 250  |cut (O < a \lor O = a)
 251    [elim Hcut
 252      [assumption
 253      |apply False_ind.apply H1.rewrite < H2.apply (witness ? ? O).apply times_n_O
 254      ]
 255    |apply le_to_or_lt_eq.apply le_O_n
 256    ]
 257  ]
 258 qed.
 259