1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/fermat_little_theorem".
19 include "nat/permutation.ma".
20 include "nat/congruence.ma".
22 theorem permut_S_mod: \forall n:nat. permut (S_mod (S n)) n.
30 change with ((S i) \mod (S n) < S n).
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)
47 [ (*qui auto non chiude il goal, chiuso invece dalla tattica
55 | rewrite > lt_to_eq_mod;
56 auto(*unfold lt;apply le_S_S;assumption*)
62 | rewrite > lt_to_eq_mod
77 apply (not_eq_O_S (i \mod (S n))).
79 rewrite < (mod_n_n (S n))
80 [ rewrite < H4 in \vdash (? ? ? (? %?)).
87 | rewrite > lt_to_eq_mod;
88 auto;(*unfold lt;apply le_S_S;assumption*)
99 apply (not_eq_O_S (j \mod (S n))).
100 rewrite < (mod_n_n (S n))
101 [ rewrite < H3 in \vdash (? ? (? %?) ?).
108 | rewrite > lt_to_eq_mod;
109 auto(*unfold lt;apply le_S_S;assumption*)
124 (*apply le_to_or_lt_eq.
128 (*apply le_to_or_lt_eq.
145 theorem eq_fact_pi: \forall n,m:nat. n < m \to n! = pi n (S_mod m).
147 simplify.reflexivity.
148 change with (S n1)*n1!=(S_mod m n1)*(pi n1 (S_mod m)).
149 unfold S_mod in \vdash (? ? ? (? % ?)).
150 rewrite > lt_to_eq_mod.
151 apply eq_f.apply H.apply (trans_lt ? (S n1)).
152 simplify. apply le_n.assumption.assumption.
156 theorem prime_to_not_divides_fact: \forall p:nat. prime p \to \forall n:nat.
157 n \lt p \to \not divides p n!.
162 apply (lt_to_not_le (S O) p)
167 (*apply divides_to_le.
172 | change with (divides p ((S n1)*n1!) \to False).
174 cut (divides p (S n1) \lor divides p n1!)
176 [ apply (lt_to_not_le (S n1) p)
179 (*apply divides_to_le
188 [ apply (trans_lt ? (S n1))
197 (*apply divides_times_to_divides;
203 theorem permut_mod: \forall p,a:nat. prime p \to
204 \lnot divides p a\to permut (\lambda n.(mod (a*n) p)) (pred p).
211 [ change with (mod (a*i) p < p).
217 apply (trans_le ? (S (S O)))
226 (*apply (trans_lt ? (S O))
235 apply (nat_compare_elim i j)
243 apply le_plus_to_minus.
244 apply (trans_le ? (pred p))
246 | rewrite > sym_plus.
252 apply (trans_lt ? (S O))
258 | apply (le_to_not_lt p (j-i)).
264 | cut (divides p a \lor divides p (j-i))
272 | apply divides_times_to_divides
274 | rewrite > distr_times_minus.
275 apply eq_mod_to_divides
279 apply (trans_lt ? (S O))
303 apply le_plus_to_minus.
304 apply (trans_le ? (pred p))
306 | rewrite > sym_plus.
312 apply (trans_lt ? (S O))
318 | apply (le_to_not_lt p (i-j)).
324 | cut (divides p a \lor divides p (i-j))
332 | apply divides_times_to_divides
334 | rewrite > distr_times_minus.
335 apply eq_mod_to_divides
339 apply (trans_lt ? (S O))
354 theorem congruent_exp_pred_SO: \forall p,a:nat. prime p \to \lnot divides p a \to
355 congruent (exp a (pred p)) (S O) p.
360 [ apply divides_to_congruent
363 (*change with (O < exp a (pred p)).
366 | cut (divides p (exp a (pred p)-(S O)) \lor divides p (pred p)!)
370 apply (prime_to_not_divides_fact p H (pred p))
373 (*rewrite < (S_pred ? Hcut1).
378 | apply divides_times_to_divides
380 | rewrite > times_minus_l.
381 rewrite > (sym_times (S O)).
382 rewrite < times_n_SO.
383 rewrite > (S_pred (pred p) Hcut2).
384 rewrite > eq_fact_pi.
386 apply congruent_to_divides
388 | apply (transitive_congruent p ?
389 (pi (pred (pred p)) (\lambda m. a*m \mod p) (S O)))
390 [ apply (congruent_pi (\lambda m. a*m)).
392 | cut (pi (pred(pred p)) (\lambda m.m) (S O)
393 = pi (pred(pred p)) (\lambda m.a*m \mod p) (S O))
396 | rewrite < eq_map_iter_i_pi.
397 rewrite < eq_map_iter_i_pi.
398 apply (permut_to_eq_map_iter_i ? ? ? ? ? (λm.m))
400 | (*NB qui auto non chiude il goal, chiuso invece dalla sola
401 ( tattica apply sys_times
404 | rewrite < plus_n_Sm.
406 rewrite < (S_pred ? Hcut2).
433 rewrite < (S_pred ? Hcut1).
441 (*apply (trans_lt ? (S O))
447 | cut (O < a \lor O = a)
454 (*apply (witness ? ? O).
458 (*apply le_to_or_lt_eq.