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/Z/times".
17 include "auto/nat/lt_arith.ma".
18 include "auto/Z/plus.ma".
20 definition Ztimes :Z \to Z \to Z \def
27 | (pos n) \Rightarrow (pos (pred ((S m) * (S n))))
28 | (neg n) \Rightarrow (neg (pred ((S m) * (S n))))]
32 | (pos n) \Rightarrow (neg (pred ((S m) * (S n))))
33 | (neg n) \Rightarrow (pos (pred ((S m) * (S n))))]].
35 interpretation "integer times" 'times x y = (Ztimes x y).
37 theorem Ztimes_z_OZ: \forall z:Z. z*OZ = OZ.
40 (*simplify;reflexivity.*)
43 theorem Ztimes_neg_Zopp: \forall n:nat.\forall x:Z.
44 neg n * x = - (pos n * x).
47 (*simplify;reflexivity.*)
50 theorem symmetric_Ztimes : symmetric Z Ztimes.
51 change with (\forall x,y:Z. x*y = y*x).
55 (*rewrite > Ztimes_z_OZ.
61 | change with (pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n)))).
63 (*rewrite < sym_times.
65 | change with (neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n)))).
67 (*rewrite < sym_times.
74 | change with (neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n)))).
76 (*rewrite < sym_times.
78 | change with (pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n)))).
80 (*rewrite < sym_times.
86 variant sym_Ztimes : \forall x,y:Z. x*y = y*x
87 \def symmetric_Ztimes.
89 theorem associative_Ztimes: associative Z Ztimes.
105 (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
106 pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
108 [ rewrite < S_pred;autobatch
109 (*[ rewrite < assoc_times.
111 | apply lt_O_times_S_S
113 | apply lt_O_times_S_S
116 (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
117 neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
119 [ rewrite < S_pred;autobatch
120 (*[ rewrite < assoc_times.
122 | apply lt_O_times_S_S
124 | apply lt_O_times_S_S
132 (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
133 neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
135 [ rewrite < S_pred;autobatch
136 (*[ rewrite < assoc_times.
138 | apply lt_O_times_S_S
140 | apply lt_O_times_S_S
143 (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
144 pos(pred ((S n) * (S (pred ((S n1) * (S n2))))))).
146 [ rewrite < S_pred;autobatch
147 (*[ rewrite < assoc_times.
149 | apply lt_O_times_S_S
151 | apply lt_O_times_S_S
164 (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
165 neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
167 [ rewrite < S_pred;autobatch
168 (*[ rewrite < assoc_times.
170 | apply lt_O_times_S_S
172 | apply lt_O_times_S_S
175 (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
176 pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
178 [ rewrite < S_pred;autobatch
179 (*[ rewrite < assoc_times.
181 | apply lt_O_times_S_S
183 | apply lt_O_times_S_S
191 (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
192 pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
194 [ rewrite < S_pred;autobatch
195 (*[ rewrite < assoc_times.
197 | apply lt_O_times_S_S
199 | apply lt_O_times_S_S
202 (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
203 neg(pred ((S n) * (S (pred ((S n1) * (S n2))))))).
205 [ rewrite < S_pred;autobatch
206 (*[ rewrite < assoc_times.
208 | apply lt_O_times_S_S
210 | apply lt_O_times_S_S
217 variant assoc_Ztimes : \forall x,y,z:Z.
218 (x * y) * z = x * (y * z) \def
221 lemma times_minus1: \forall n,p,q:nat. lt q p \to
222 (S n) * (S (pred ((S p) - (S q)))) =
223 pred ((S n) * (S p)) - pred ((S n) * (S q)).
226 [ rewrite > minus_pred_pred
228 (*rewrite < distr_times_minus.
231 (* we now close all positivity conditions *)
232 | apply lt_O_times_S_S
233 | apply lt_O_times_S_S
235 | unfold lt.autobatch
243 lemma Ztimes_Zplus_pos_neg_pos: \forall n,p,q:nat.
244 (pos n)*((neg p)+(pos q)) = (pos n)*(neg p)+ (pos n)*(pos q).
247 change in match (p + n * (S p)) with (pred ((S n) * (S p))).
248 change in match (q + n * (S q)) with (pred ((S n) * (S q))).
249 rewrite < nat_compare_pred_pred
250 [ rewrite < nat_compare_times_l.
251 rewrite < nat_compare_S_S.
252 apply (nat_compare_elim p q)
255 change with (pos (pred ((S n) * (S (pred ((S q) - (S p)))))) =
256 pos (pred ((pred ((S n) * (S q))) - (pred ((S n) * (S p)))))).
257 rewrite < (times_minus1 n q p H).
265 change with (neg (pred ((S n) * (S (pred ((S p) - (S q)))))) =
266 neg (pred ((pred ((S n) * (S p))) - (pred ((S n) * (S q)))))).
267 rewrite < (times_minus1 n p q H).
270 (* two more positivity conditions from nat_compare_pred_pred *)
272 | apply lt_O_times_S_S
273 | apply lt_O_times_S_S
277 lemma Ztimes_Zplus_pos_pos_neg: \forall n,p,q:nat.
278 (pos n)*((pos p)+(neg q)) = (pos n)*(pos p)+ (pos n)*(neg q).
281 (*rewrite < sym_Zplus.
282 rewrite > Ztimes_Zplus_pos_neg_pos.
286 lemma distributive2_Ztimes_pos_Zplus:
287 distributive2 nat Z (\lambda n,z. (pos n) * z) Zplus.
288 change with (\forall n,y,z.
289 (pos n) * (y + z) = (pos n) * y + (pos n) * z).
296 (pos (pred ((S n) * ((S n1) + (S n2)))) =
297 pos (pred ((S n) * (S n1) + (S n) * (S n2)))).
299 (*rewrite < distr_times_plus.
301 | apply Ztimes_Zplus_pos_pos_neg
305 | apply Ztimes_Zplus_pos_neg_pos
307 (neg (pred ((S n) * ((S n1) + (S n2)))) =
308 neg (pred ((S n) * (S n1) + (S n) * (S n2)))).
310 (*rewrite < distr_times_plus.
316 variant distr_Ztimes_Zplus_pos: \forall n,y,z.
317 (pos n) * (y + z) = ((pos n) * y + (pos n) * z) \def
318 distributive2_Ztimes_pos_Zplus.
320 lemma distributive2_Ztimes_neg_Zplus :
321 distributive2 nat Z (\lambda n,z. (neg n) * z) Zplus.
322 change with (\forall n,y,z.
323 (neg n) * (y + z) = (neg n) * y + (neg n) * z).
325 rewrite > Ztimes_neg_Zopp.
326 rewrite > distr_Ztimes_Zplus_pos.
328 (*rewrite > Zopp_Zplus.
329 rewrite < Ztimes_neg_Zopp.
330 rewrite < Ztimes_neg_Zopp.
334 variant distr_Ztimes_Zplus_neg: \forall n,y,z.
335 (neg n) * (y + z) = (neg n) * y + (neg n) * z \def
336 distributive2_Ztimes_neg_Zplus.
338 theorem distributive_Ztimes_Zplus: distributive Z Ztimes Zplus.
339 change with (\forall x,y,z:Z. x * (y + z) = x*y + x*z).
344 | apply distr_Ztimes_Zplus_pos
345 | apply distr_Ztimes_Zplus_neg
349 variant distr_Ztimes_Zplus: \forall x,y,z.
350 x * (y + z) = x*y + x*z \def
351 distributive_Ztimes_Zplus.