(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/Z/times".
+set "baseuri" "cic:/matita/library_autobatch/Z/times".
include "auto/nat/lt_arith.ma".
include "auto/Z/plus.ma".
| (neg n) \Rightarrow (pos (pred ((S m) * (S n))))]].
(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer times" 'times x y = (cic:/matita/library_auto/Z/times/Ztimes.con x y).
+interpretation "integer times" 'times x y = (cic:/matita/library_autobatch/Z/times/Ztimes.con x y).
theorem Ztimes_z_OZ: \forall z:Z. z*OZ = OZ.
intro.
-elim z;auto.
+elim z;autobatch.
(*simplify;reflexivity.*)
qed.
theorem Ztimes_neg_Zopp: \forall n:nat.\forall x:Z.
neg n * x = - (pos n * x).
intros.
-elim x;auto.
+elim x;autobatch.
(*simplify;reflexivity.*)
qed.
change with (\forall x,y:Z. x*y = y*x).
intros.
elim x
-[ auto
+[ autobatch
(*rewrite > Ztimes_z_OZ.
reflexivity*)
| elim y
- [ auto
+ [ autobatch
(*simplify.
reflexivity*)
| change with (pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n)))).
- auto
+ autobatch
(*rewrite < sym_times.
reflexivity*)
| change with (neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n)))).
- auto
+ autobatch
(*rewrite < sym_times.
reflexivity*)
]
| elim y
- [ auto
+ [ autobatch
(*simplify.
reflexivity*)
| change with (neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n)))).
- auto
+ autobatch
(*rewrite < sym_times.
reflexivity*)
| change with (pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n)))).
- auto
+ autobatch
(*rewrite < sym_times.
reflexivity*)
]
unfold associative.
intros.
elim x
-[ auto
+[ autobatch
(*simplify.
reflexivity*)
| elim y
- [ auto
+ [ autobatch
(*simplify.
reflexivity*)
| elim z
- [ auto
+ [ autobatch
(*simplify.
reflexivity*)
| change with
(pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred
- [ rewrite < S_pred;auto
+ [ rewrite < S_pred;autobatch
(*[ rewrite < assoc_times.
reflexivity
| apply lt_O_times_S_S
(neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred
- [ rewrite < S_pred;auto
+ [ rewrite < S_pred;autobatch
(*[ rewrite < assoc_times.
reflexivity
| apply lt_O_times_S_S
]
]
| elim z
- [ auto
+ [ autobatch
(*simplify.
reflexivity*)
| change with
(neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred
- [ rewrite < S_pred;auto
+ [ rewrite < S_pred;autobatch
(*[ rewrite < assoc_times.
reflexivity
| apply lt_O_times_S_S
(pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
pos(pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred
- [ rewrite < S_pred;auto
+ [ rewrite < S_pred;autobatch
(*[ rewrite < assoc_times.
reflexivity
| apply lt_O_times_S_S
]
]
| elim y
- [ auto
+ [ autobatch
(*simplify.
reflexivity*)
| elim z
- [ auto
+ [ autobatch
(*simplify.
reflexivity*)
| change with
(neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred
- [ rewrite < S_pred;auto
+ [ rewrite < S_pred;autobatch
(*[ rewrite < assoc_times.
reflexivity
| apply lt_O_times_S_S
(pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred
- [ rewrite < S_pred;auto
+ [ rewrite < S_pred;autobatch
(*[ rewrite < assoc_times.
reflexivity
| apply lt_O_times_S_S
]
]
| elim z
- [ auto
+ [ autobatch
(*simplify.
reflexivity*)
| change with
(pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred
- [ rewrite < S_pred;auto
+ [ rewrite < S_pred;autobatch
(*[ rewrite < assoc_times.
reflexivity
| apply lt_O_times_S_S
(neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
neg(pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred
- [ rewrite < S_pred;auto
+ [ rewrite < S_pred;autobatch
(*[ rewrite < assoc_times.
reflexivity
| apply lt_O_times_S_S
intros.
rewrite < S_pred
[ rewrite > minus_pred_pred
- [ auto
+ [ autobatch
(*rewrite < distr_times_minus.
reflexivity*)
| apply lt_O_times_S_S
| apply lt_O_times_S_S
]
-| unfold lt.auto
+| unfold lt.autobatch
(*simplify.
unfold lt.
apply le_SO_minus.
rewrite < (times_minus1 n q p H).
reflexivity
| intro.
- auto
+ autobatch
(*rewrite < H.
simplify.
reflexivity*)
lemma Ztimes_Zplus_pos_pos_neg: \forall n,p,q:nat.
(pos n)*((pos p)+(neg q)) = (pos n)*(pos p)+ (pos n)*(neg q).
intros.
-auto.
+autobatch.
(*rewrite < sym_Zplus.
rewrite > Ztimes_Zplus_pos_neg_pos.
apply sym_Zplus.*)
| change with
(pos (pred ((S n) * ((S n1) + (S n2)))) =
pos (pred ((S n) * (S n1) + (S n) * (S n2)))).
- auto
+ autobatch
(*rewrite < distr_times_plus.
reflexivity*)
| apply Ztimes_Zplus_pos_pos_neg
| change with
(neg (pred ((S n) * ((S n1) + (S n2)))) =
neg (pred ((S n) * (S n1) + (S n) * (S n2)))).
- auto
+ autobatch
(*rewrite < distr_times_plus.
reflexivity*)
]
intros.
rewrite > Ztimes_neg_Zopp.
rewrite > distr_Ztimes_Zplus_pos.
-auto.
+autobatch.
(*rewrite > Zopp_Zplus.
rewrite < Ztimes_neg_Zopp.
rewrite < Ztimes_neg_Zopp.
theorem distributive_Ztimes_Zplus: distributive Z Ztimes Zplus.
change with (\forall x,y,z:Z. x * (y + z) = x*y + x*z).
intros.
-elim x;auto.
+elim x;autobatch.
(*[ simplify.
reflexivity
| apply distr_Ztimes_Zplus_pos