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/library_autobatch/nat/fermat_little_theorem".
17 include "auto/nat/exp.ma".
18 include "auto/nat/gcd.ma".
19 include "auto/nat/permutation.ma".
20 include "auto/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 autobatch non chiude il goal, chiuso invece dalla tattica
55 | rewrite > lt_to_eq_mod;
56 unfold lt;autobatch.(*apply le_S_S;assumption*)
62 | rewrite > lt_to_eq_mod
75 apply (not_eq_O_S (i \mod (S n))).
77 rewrite < (mod_n_n (S n))
78 [ rewrite < H4 in \vdash (? ? ? (? %?)).
84 | rewrite > lt_to_eq_mod;
85 unfold lt;autobatch;(*apply le_S_S;assumption*)
95 apply (not_eq_O_S (j \mod (S n))).
96 rewrite < (mod_n_n (S n))
97 [ rewrite < H3 in \vdash (? ? (? %?) ?).
100 | unfold lt.autobatch
103 | rewrite > lt_to_eq_mod;
104 unfold lt;autobatch(*apply le_S_S;assumption*)
106 | unfold lt.autobatch
118 (*apply le_to_or_lt_eq.
122 (*apply le_to_or_lt_eq.
125 | unfold lt.autobatch
129 | unfold lt.autobatch
137 theorem eq_fact_pi: \forall n,m:nat. n < m \to n! = pi n (S_mod m).
139 simplify.reflexivity.
140 change with (S n1)*n1!=(S_mod m n1)*(pi n1 (S_mod m)).
141 unfold S_mod in \vdash (? ? ? (? % ?)).
142 rewrite > lt_to_eq_mod.
143 apply eq_f.apply H.apply (trans_lt ? (S n1)).
144 simplify. apply le_n.assumption.assumption.
148 theorem prime_to_not_divides_fact: \forall p:nat. prime p \to \forall n:nat.
149 n \lt p \to \not divides p n!.
154 apply (lt_to_not_le (S O) p)
159 (*apply divides_to_le.
164 | change with (divides p ((S n1)*n1!) \to False).
166 cut (divides p (S n1) \lor divides p n1!)
168 [ apply (lt_to_not_le (S n1) p)
171 (*apply divides_to_le
180 [ apply (trans_lt ? (S n1))
189 (*apply divides_times_to_divides;
195 theorem permut_mod: \forall p,a:nat. prime p \to
196 \lnot divides p a\to permut (\lambda n.(mod (a*n) p)) (pred p).
203 [ change with (mod (a*i) p < p).
209 apply (trans_le ? (S (S O)))
218 (*apply (trans_lt ? (S O))
227 apply (nat_compare_elim i j)
235 apply le_plus_to_minus.
236 apply (trans_le ? (pred p))
238 | rewrite > sym_plus.
241 | unfold prime in H. elim H. autobatch.
243 apply (trans_lt ? (S O))
249 | apply (le_to_not_lt p (j-i)).
251 [ unfold lt.autobatch
254 | cut (divides p a \lor divides p (j-i))
262 | apply divides_times_to_divides
264 | rewrite > distr_times_minus.
265 apply eq_mod_to_divides
266 [ unfold prime in H.elim H.autobatch
267 (*apply (trans_lt ? (S O))
291 apply le_plus_to_minus.
292 apply (trans_le ? (pred p))
294 | rewrite > sym_plus.
297 | unfold prime in H.elim H.autobatch.
299 apply (trans_lt ? (S O))
305 | apply (le_to_not_lt p (i-j)).
307 [ unfold lt.autobatch
310 | cut (divides p a \lor divides p (i-j))
318 | apply divides_times_to_divides
320 | rewrite > distr_times_minus.
321 apply eq_mod_to_divides
322 [ unfold prime in H.elim H.autobatch.
324 apply (trans_lt ? (S O))
339 theorem congruent_exp_pred_SO: \forall p,a:nat. prime p \to \lnot divides p a \to
340 congruent (exp a (pred p)) (S O) p.
345 [ apply divides_to_congruent
348 (*change with (O < exp a (pred p)).
351 | cut (divides p (exp a (pred p)-(S O)) \lor divides p (pred p)!)
355 apply (prime_to_not_divides_fact p H (pred p))
358 (*rewrite < (S_pred ? Hcut1).
363 | apply divides_times_to_divides
365 | rewrite > times_minus_l.
366 rewrite > (sym_times (S O)).
367 rewrite < times_n_SO.
368 rewrite > (S_pred (pred p) Hcut2).
369 rewrite > eq_fact_pi.
371 apply congruent_to_divides
373 | apply (transitive_congruent p ?
374 (pi (pred (pred p)) (\lambda m. a*m \mod p) (S O)))
375 [ apply (congruent_pi (\lambda m. a*m)).
377 | cut (pi (pred(pred p)) (\lambda m.m) (S O)
378 = pi (pred(pred p)) (\lambda m.a*m \mod p) (S O))
381 | rewrite < eq_map_iter_i_pi.
382 rewrite < eq_map_iter_i_pi.
383 apply (permut_to_eq_map_iter_i ? ? ? ? ? (λm.m))
385 | (*NB qui autobatch non chiude il goal, chiuso invece dalla sola
386 ( tattica apply sys_times
389 | rewrite < plus_n_Sm.
391 rewrite < (S_pred ? Hcut2).
418 rewrite < (S_pred ? Hcut1).
426 (*apply (trans_lt ? (S O))
432 | cut (O < a \lor O = a)
439 (*apply (witness ? ? O).
443 (*apply le_to_or_lt_eq.