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