(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/chinese_reminder".
+set "baseuri" "cic:/matita/library_autobatch/nat/chinese_reminder".
include "auto/nat/exp.ma".
include "auto/nat/gcd.ma".
rewrite < assoc_times.
rewrite < times_plus_l.
rewrite > eq_minus_plus_plus_minus
- [ auto
+ [ autobatch
(*rewrite < times_minus_l.
rewrite > sym_plus.
apply (eq_times_plus_to_congruent ? ? ? ((b+(a+b*m)*a2)-b*a2))
| apply le_times_l.
apply (trans_le ? ((a+b*m)*a2))
[ apply le_times_l.
- apply (trans_le ? (b*m));auto
+ apply (trans_le ? (b*m));autobatch
(*[ rewrite > times_n_SO in \vdash (? % ?).
apply le_times_r.
assumption
[ apply lt_to_le.
change with (O + a2*m < a1*n).
apply lt_minus_to_plus.
- auto
+ autobatch
(*rewrite > H5.
unfold lt.
apply le_n*)
rewrite > distr_times_minus.
rewrite < assoc_times.
rewrite < eq_plus_minus_minus_minus
- [ auto
+ [ autobatch
(*rewrite < times_n_SO.
rewrite < times_minus_l.
rewrite < sym_plus.
]*)
| rewrite > assoc_times.
apply le_times_r.
- (*auto genera un'esecuzione troppo lunga*)
- apply (trans_le ? (a1*n - a2*m));auto
+ (*autobatch genera un'esecuzione troppo lunga*)
+ apply (trans_le ? (a1*n - a2*m));autobatch
(*[ rewrite > H5.
apply le_n
| apply (le_minus_m ? (a2*m))
]*)
| apply le_times_l.
apply le_times_l.
- auto
+ autobatch
(*apply (trans_le ? (b*m))
[ rewrite > times_n_SO in \vdash (? % ?).
apply le_times_r.
[ apply lt_to_le.
change with (O + a2*m < a1*n).
apply lt_minus_to_plus.
- auto
+ autobatch
(*rewrite > H5.
unfold lt.
apply le_n*)
rewrite > distr_times_minus.
rewrite < assoc_times.
rewrite < eq_plus_minus_minus_minus
- [ auto
+ [ autobatch
(*rewrite < times_n_SO.
rewrite < times_minus_l.
rewrite < sym_plus.
]*)
| rewrite > assoc_times.
apply le_times_r.
- apply (trans_le ? (a2*m - a1*n));auto
+ apply (trans_le ? (a2*m - a1*n));autobatch
(*[ rewrite > H5.
apply le_n
| apply (le_minus_m ? (a1*n))
| rewrite > assoc_times.
rewrite > assoc_times.
apply le_times_l.
- auto
+ autobatch
(*apply (trans_le ? (a*n))
[ rewrite > times_n_SO in \vdash (? % ?).
apply le_times_r.
[ apply lt_to_le.
change with (O + a1*n < a2*m).
apply lt_minus_to_plus.
- auto
+ autobatch
(*rewrite > H5.
unfold lt.
apply le_n*)
rewrite > assoc_plus.
rewrite < times_plus_l.
rewrite > eq_minus_plus_plus_minus
- [ auto
+ [ autobatch
(*rewrite < times_minus_l.
rewrite > sym_plus.
apply (eq_times_plus_to_congruent ? ? ? ((a+(b+a*n)*a1)-a*a1))
| apply le_times_l.
apply (trans_le ? ((b+a*n)*a1))
[ apply le_times_l.
- auto
+ autobatch
(*apply (trans_le ? (a*n))
[ rewrite > times_n_SO in \vdash (? % ?).
apply le_times_r.
[ apply lt_to_le.
change with (O + a1*n < a2*m).
apply lt_minus_to_plus.
- auto
+ autobatch
(*rewrite > H5.
unfold lt.
apply le_n*)
]
]
(* proof of the cut *)
-| (* qui auto non conclude il goal *)
+| (* qui autobatch non conclude il goal *)
rewrite < H2.
apply eq_minus_gcd
]
apply sym_eq.
change with (congruent a1 (a1 \mod (m*n)) m).
rewrite < sym_times.
- auto
+ autobatch
(*apply congruent_n_mod_times;assumption*)
| assumption
]
[ unfold congruent.
apply sym_eq.
change with (congruent a1 (a1 \mod (m*n)) n).
- auto
+ autobatch
(*apply congruent_n_mod_times;assumption*)
| assumption
]
]
| apply lt_mod_m_m.
- auto
+ autobatch
(*rewrite > (times_n_O O).
apply lt_times;assumption*)
]
qed.
theorem cr_pair2: cr_pair (S(S O)) (S(S(S O))) (S O) O = (S(S(S O))).
-auto.
+autobatch.
(*simplify.
reflexivity.*)
qed.
[ rewrite > H3.
simplify.
intro.
- auto
+ autobatch
(*split
[ reflexivity
| apply eqb_true_to_eq.
]*)
| simplify.
intro.
- (* l'invocazione di auto qui genera segmentation fault *)
+ (* l'invocazione di autobatch qui genera segmentation fault *)
apply False_ind.
- (* l'invocazione di auto qui genera segmentation fault *)
+ (* l'invocazione di autobatch qui genera segmentation fault *)
apply not_eq_true_false.
- (* l'invocazione di auto qui genera segmentation fault *)
+ (* l'invocazione di autobatch qui genera segmentation fault *)
apply sym_eq.
assumption
]
[ apply (ex_intro ? ? a1).
split
[ split
- [ auto
+ [ autobatch
(*rewrite < minus_n_n.
apply le_O_n*)
| elim H3.
| apply (nat_case (m*n))
[ apply le_O_n
| intro.
- auto
+ autobatch
(*rewrite < pred_Sn.
apply le_n*)
]
[ cut (a1 \mod n = b)
[ rewrite > (eq_to_eqb_true ? ? Hcut).
rewrite > (eq_to_eqb_true ? ? Hcut1).
- (* l'invocazione di auto qui non chiude il goal *)
+ (* l'invocazione di autobatch qui non chiude il goal *)
simplify.
reflexivity
| rewrite < (lt_to_eq_mod b n);
| rewrite < (lt_to_eq_mod a m);assumption
]
]
- | auto
+ | autobatch
(*apply (le_to_lt_to_lt ? b)
[ apply le_O_n
| assumption
]*)
- | auto
+ | autobatch
(*apply (le_to_lt_to_lt ? a)
[ apply le_O_n
| assumption