(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/fermat_little_theorem".
+set "baseuri" "cic:/matita/library_autobatch/nat/fermat_little_theorem".
include "auto/nat/exp.ma".
include "auto/nat/gcd.ma".
split
[ intros.
unfold S_mod.
- auto
+ autobatch
(*apply le_S_S_to_le.
change with ((S i) \mod (S n) < S n).
apply lt_mod_m_m.
[ (* i < n, j< n *)
rewrite < mod_S
[ rewrite < mod_S
- [ (*qui auto non chiude il goal, chiuso invece dalla tattica
+ [ (*qui autobatch non chiude il goal, chiuso invece dalla tattica
* apply H2
*)
apply H2
- | auto
+ | autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
| rewrite > lt_to_eq_mod;
- auto(*unfold lt;apply le_S_S;assumption*)
+ unfold lt;autobatch.(*apply le_S_S;assumption*)
]
- | auto
+ | autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
| rewrite > lt_to_eq_mod
- [ auto
- (*unfold lt.
- apply le_S_S.
+ [ unfold lt.autobatch
+ (*apply le_S_S.
assumption*)
- | auto
- (*unfold lt.
- apply le_S_S.
+ | unfold lt.autobatch
+ (*apply le_S_S.
assumption*)
]
]
[ rewrite < H4 in \vdash (? ? ? (? %?)).
rewrite < mod_S
[ assumption
- | auto
- (*unfold lt.
- apply le_S_S.
+ | unfold lt.autobatch
+ (*apply le_S_S.
apply le_O_n*)
| rewrite > lt_to_eq_mod;
- auto;(*unfold lt;apply le_S_S;assumption*)
+ unfold lt;autobatch;(*apply le_S_S;assumption*)
]
- | auto
- (*unfold lt.
- apply le_S_S.
+ | unfold lt.autobatch
+ (*apply le_S_S.
apply le_O_n*)
]
]
[ rewrite < H3 in \vdash (? ? (? %?) ?).
rewrite < mod_S
[ assumption
- | auto
- (*unfold lt.
- apply le_S_S.
+ | unfold lt.autobatch
+ (*apply le_S_S.
apply le_O_n*)
| rewrite > lt_to_eq_mod;
- auto(*unfold lt;apply le_S_S;assumption*)
+ unfold lt;autobatch(*apply le_S_S;assumption*)
]
- | auto
- (*unfold lt.
- apply le_S_S.
+ | unfold lt.autobatch
+ (*apply le_S_S.
apply le_O_n*)
]
|(* i = n, j= n*)
- auto
+ autobatch
(*rewrite > H3.
rewrite > H4.
reflexivity*)
]
]
- | auto
+ | autobatch
(*apply le_to_or_lt_eq.
assumption*)
]
- | auto
+ | autobatch
(*apply le_to_or_lt_eq.
assumption*)
]
- | auto
- (*unfold lt.
- apply le_S_S.
+ | unfold lt.autobatch
+ (*apply le_S_S.
assumption*)
]
- | auto
- (*unfold lt.
- apply le_S_S.
+ | unfold lt.autobatch
+ (*apply le_S_S.
assumption*)
]
]
[ unfold prime in H.
elim H.
assumption
- | auto
+ | autobatch
(*apply divides_to_le.
unfold lt.
apply le_n.
[ elim Hcut
[ apply (lt_to_not_le (S n1) p)
[ assumption
- | auto
+ | autobatch
(*apply divides_to_le
[ unfold lt.
apply le_S_S.
| assumption
]*)
]
- | auto
+ | autobatch
(*apply H1
[ apply (trans_lt ? (S n1))
[ unfold lt.
| assumption
]*)
]
- | auto
+ | autobatch
(*apply divides_times_to_divides;
assumption*)
]
apply lt_mod_m_m.
unfold prime in H.
elim H.
- auto
+ autobatch
(*unfold lt.
apply (trans_le ? (S (S O)))
[ apply le_n_Sn
[ apply le_n
| unfold prime in H.
elim H.
- auto
+ autobatch
(*apply (trans_lt ? (S O))
[ unfold lt.
apply le_n
absurd (j-i \lt p)
[ unfold lt.
rewrite > (S_pred p)
- [ auto
+ [ autobatch
(*apply le_S_S.
apply le_plus_to_minus.
apply (trans_le ? (pred p))
| rewrite > sym_plus.
apply le_plus_n
]*)
- | auto
- (*unfold prime in H.
- elim H.
+ | unfold prime in H. elim H. autobatch.
+ (*
apply (trans_lt ? (S O))
[ unfold lt.
apply le_n
]
| apply (le_to_not_lt p (j-i)).
apply divides_to_le
- [ auto
- (*unfold lt.
- apply le_SO_minus.
+ [ unfold lt.autobatch
+ (*apply le_SO_minus.
assumption*)
| cut (divides p a \lor divides p (j-i))
[ elim Hcut
[ apply False_ind.
- auto
+ autobatch
(*apply H1.
assumption*)
| assumption
[ assumption
| rewrite > distr_times_minus.
apply eq_mod_to_divides
- [ auto
- (*unfold prime in H.
- elim H.
- apply (trans_lt ? (S O))
+ [ unfold prime in H.elim H.autobatch
+ (*apply (trans_lt ? (S O))
[ unfold lt.
apply le_n
| assumption
]*)
- | auto
+ | autobatch
(*apply sym_eq.
apply H4*)
]
]
]
|(* i = j *)
- auto
+ autobatch
(*intro.
assumption*)
| (* j < i *)
absurd (i-j \lt p)
[ unfold lt.
rewrite > (S_pred p)
- [ auto
+ [ autobatch
(*apply le_S_S.
apply le_plus_to_minus.
apply (trans_le ? (pred p))
| rewrite > sym_plus.
apply le_plus_n
]*)
- | auto
- (*unfold prime in H.
- elim H.
+ | unfold prime in H.elim H.autobatch.
+ (*
apply (trans_lt ? (S O))
[ unfold lt.
apply le_n
]
| apply (le_to_not_lt p (i-j)).
apply divides_to_le
- [ auto
- (*unfold lt.
- apply le_SO_minus.
+ [ unfold lt.autobatch
+ (*apply le_SO_minus.
assumption*)
| cut (divides p a \lor divides p (i-j))
[ elim Hcut
[ apply False_ind.
- auto
+ autobatch
(*apply H1.
assumption*)
| assumption
[ assumption
| rewrite > distr_times_minus.
apply eq_mod_to_divides
- [ auto
- (*unfold prime in H.
- elim H.
+ [ unfold prime in H.elim H.autobatch.
+ (*
apply (trans_lt ? (S O))
[ unfold lt.
apply le_n
[ cut (O < pred p)
[ apply divides_to_congruent
[ assumption
- | auto
+ | autobatch
(*change with (O < exp a (pred p)).
apply lt_O_exp.
assumption*)
| apply False_ind.
apply (prime_to_not_divides_fact p H (pred p))
[ unfold lt.
- auto
+ autobatch
(*rewrite < (S_pred ? Hcut1).
apply le_n*)
| assumption
rewrite < eq_map_iter_i_pi.
apply (permut_to_eq_map_iter_i ? ? ? ? ? (λm.m))
[ apply assoc_times
- | (*NB qui auto non chiude il goal, chiuso invece dalla sola
+ | (*NB qui autobatch non chiude il goal, chiuso invece dalla sola
( tattica apply sys_times
*)
apply sym_times
| rewrite < plus_n_Sm.
rewrite < plus_n_O.
rewrite < (S_pred ? Hcut2).
- auto
+ autobatch
(*apply permut_mod
[ assumption
| assumption
]*)
| intros.
cut (m=O)
- [ auto
+ [ autobatch
(*rewrite > Hcut3.
rewrite < times_n_O.
apply mod_O_n.*)
- | auto
+ | autobatch
(*apply sym_eq.
apply le_n_O_to_eq.
apply le_S_S_to_le.
]
| unfold prime in H.
elim H.
- auto
+ autobatch
(*apply (trans_lt ? (S O))
[ unfold lt.
apply le_n
| apply False_ind.
apply H1.
rewrite < H2.
- auto
+ autobatch
(*apply (witness ? ? O).
apply times_n_O*)
]
- | auto
+ | autobatch
(*apply le_to_or_lt_eq.
apply le_O_n*)
]