X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Flibrary_auto%2Fauto%2Fnat%2Ffermat_little_theorem.ma;h=a04adaad8fa686679b773166690756d5d7bf5278;hb=c6e99dc27b51fee56d4d1c6f88d1a8e6ff83af5a;hp=df8aff7275aba39992d550388fbc02340af046b1;hpb=1b839e0367f89503398442b7990fb6b6d1fa2152;p=helm.git diff --git a/matita/library_auto/auto/nat/fermat_little_theorem.ma b/matita/library_auto/auto/nat/fermat_little_theorem.ma index df8aff727..a04adaad8 100644 --- a/matita/library_auto/auto/nat/fermat_little_theorem.ma +++ b/matita/library_auto/auto/nat/fermat_little_theorem.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -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". @@ -25,7 +25,7 @@ unfold permut. 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. @@ -44,29 +44,27 @@ split [ (* 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*) ] ] @@ -80,16 +78,14 @@ split [ 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*) ] ] @@ -101,41 +97,37 @@ split [ 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*) ] ] @@ -163,7 +155,7 @@ elim n [ unfold prime in H. elim H. assumption - | auto + | autobatch (*apply divides_to_le. unfold lt. apply le_n. @@ -175,7 +167,7 @@ elim n [ elim Hcut [ apply (lt_to_not_le (S n1) p) [ assumption - | auto + | autobatch (*apply divides_to_le [ unfold lt. apply le_S_S. @@ -183,7 +175,7 @@ elim n | assumption ]*) ] - | auto + | autobatch (*apply H1 [ apply (trans_lt ? (S n1)) [ unfold lt. @@ -193,7 +185,7 @@ elim n | assumption ]*) ] - | auto + | autobatch (*apply divides_times_to_divides; assumption*) ] @@ -212,7 +204,7 @@ split 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 @@ -222,7 +214,7 @@ split [ apply le_n | unfold prime in H. elim H. - auto + autobatch (*apply (trans_lt ? (S O)) [ unfold lt. apply le_n @@ -238,7 +230,7 @@ split 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)) @@ -246,9 +238,8 @@ split | 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 @@ -257,14 +248,13 @@ split ] | 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 @@ -273,15 +263,13 @@ split [ 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*) ] @@ -290,7 +278,7 @@ split ] ] |(* i = j *) - auto + autobatch (*intro. assumption*) | (* j < i *) @@ -298,7 +286,7 @@ split 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)) @@ -306,9 +294,8 @@ split | 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 @@ -317,14 +304,13 @@ split ] | 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 @@ -333,9 +319,8 @@ split [ 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 @@ -359,7 +344,7 @@ cut (O < a) [ cut (O < pred p) [ apply divides_to_congruent [ assumption - | auto + | autobatch (*change with (O < exp a (pred p)). apply lt_O_exp. assumption*) @@ -369,7 +354,7 @@ cut (O < a) | 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 @@ -397,25 +382,25 @@ cut (O < a) 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. @@ -437,7 +422,7 @@ cut (O < a) ] | unfold prime in H. elim H. - auto + autobatch (*apply (trans_lt ? (S O)) [ unfold lt. apply le_n @@ -450,11 +435,11 @@ cut (O < a) | 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*) ]