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 (*CSC: the URI must disappear: there is a bug now *)
36 interpretation "integer times" 'times x y = (cic:/matita/library_autobatch/Z/times/Ztimes.con x y).
38 theorem Ztimes_z_OZ: \forall z:Z. z*OZ = OZ.
41 (*simplify;reflexivity.*)
44 theorem Ztimes_neg_Zopp: \forall n:nat.\forall x:Z.
45 neg n * x = - (pos n * x).
48 (*simplify;reflexivity.*)
51 theorem symmetric_Ztimes : symmetric Z Ztimes.
52 change with (\forall x,y:Z. x*y = y*x).
56 (*rewrite > Ztimes_z_OZ.
62 | change with (pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n)))).
64 (*rewrite < sym_times.
66 | change with (neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n)))).
68 (*rewrite < sym_times.
75 | change with (neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n)))).
77 (*rewrite < sym_times.
79 | change with (pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n)))).
81 (*rewrite < sym_times.
87 variant sym_Ztimes : \forall x,y:Z. x*y = y*x
88 \def symmetric_Ztimes.
90 theorem associative_Ztimes: associative Z Ztimes.
106 (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
107 pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
109 [ rewrite < S_pred;autobatch
110 (*[ rewrite < assoc_times.
112 | apply lt_O_times_S_S
114 | apply lt_O_times_S_S
117 (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
118 neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
120 [ rewrite < S_pred;autobatch
121 (*[ rewrite < assoc_times.
123 | apply lt_O_times_S_S
125 | apply lt_O_times_S_S
133 (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
134 neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
136 [ rewrite < S_pred;autobatch
137 (*[ rewrite < assoc_times.
139 | apply lt_O_times_S_S
141 | apply lt_O_times_S_S
144 (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
145 pos(pred ((S n) * (S (pred ((S n1) * (S n2))))))).
147 [ rewrite < S_pred;autobatch
148 (*[ rewrite < assoc_times.
150 | apply lt_O_times_S_S
152 | apply lt_O_times_S_S
165 (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
166 neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
168 [ rewrite < S_pred;autobatch
169 (*[ rewrite < assoc_times.
171 | apply lt_O_times_S_S
173 | apply lt_O_times_S_S
176 (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
177 pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
179 [ rewrite < S_pred;autobatch
180 (*[ rewrite < assoc_times.
182 | apply lt_O_times_S_S
184 | apply lt_O_times_S_S
192 (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
193 pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
195 [ rewrite < S_pred;autobatch
196 (*[ rewrite < assoc_times.
198 | apply lt_O_times_S_S
200 | apply lt_O_times_S_S
203 (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
204 neg(pred ((S n) * (S (pred ((S n1) * (S n2))))))).
206 [ rewrite < S_pred;autobatch
207 (*[ rewrite < assoc_times.
209 | apply lt_O_times_S_S
211 | apply lt_O_times_S_S
218 variant assoc_Ztimes : \forall x,y,z:Z.
219 (x * y) * z = x * (y * z) \def
222 lemma times_minus1: \forall n,p,q:nat. lt q p \to
223 (S n) * (S (pred ((S p) - (S q)))) =
224 pred ((S n) * (S p)) - pred ((S n) * (S q)).
227 [ rewrite > minus_pred_pred
229 (*rewrite < distr_times_minus.
232 (* we now close all positivity conditions *)
233 | apply lt_O_times_S_S
234 | apply lt_O_times_S_S
236 | unfold lt.autobatch
244 lemma Ztimes_Zplus_pos_neg_pos: \forall n,p,q:nat.
245 (pos n)*((neg p)+(pos q)) = (pos n)*(neg p)+ (pos n)*(pos q).
248 change in match (p + n * (S p)) with (pred ((S n) * (S p))).
249 change in match (q + n * (S q)) with (pred ((S n) * (S q))).
250 rewrite < nat_compare_pred_pred
251 [ rewrite < nat_compare_times_l.
252 rewrite < nat_compare_S_S.
253 apply (nat_compare_elim p q)
256 change with (pos (pred ((S n) * (S (pred ((S q) - (S p)))))) =
257 pos (pred ((pred ((S n) * (S q))) - (pred ((S n) * (S p)))))).
258 rewrite < (times_minus1 n q p H).
266 change with (neg (pred ((S n) * (S (pred ((S p) - (S q)))))) =
267 neg (pred ((pred ((S n) * (S p))) - (pred ((S n) * (S q)))))).
268 rewrite < (times_minus1 n p q H).
271 (* two more positivity conditions from nat_compare_pred_pred *)
273 | apply lt_O_times_S_S
274 | apply lt_O_times_S_S
278 lemma Ztimes_Zplus_pos_pos_neg: \forall n,p,q:nat.
279 (pos n)*((pos p)+(neg q)) = (pos n)*(pos p)+ (pos n)*(neg q).
282 (*rewrite < sym_Zplus.
283 rewrite > Ztimes_Zplus_pos_neg_pos.
287 lemma distributive2_Ztimes_pos_Zplus:
288 distributive2 nat Z (\lambda n,z. (pos n) * z) Zplus.
289 change with (\forall n,y,z.
290 (pos n) * (y + z) = (pos n) * y + (pos n) * z).
297 (pos (pred ((S n) * ((S n1) + (S n2)))) =
298 pos (pred ((S n) * (S n1) + (S n) * (S n2)))).
300 (*rewrite < distr_times_plus.
302 | apply Ztimes_Zplus_pos_pos_neg
306 | apply Ztimes_Zplus_pos_neg_pos
308 (neg (pred ((S n) * ((S n1) + (S n2)))) =
309 neg (pred ((S n) * (S n1) + (S n) * (S n2)))).
311 (*rewrite < distr_times_plus.
317 variant distr_Ztimes_Zplus_pos: \forall n,y,z.
318 (pos n) * (y + z) = ((pos n) * y + (pos n) * z) \def
319 distributive2_Ztimes_pos_Zplus.
321 lemma distributive2_Ztimes_neg_Zplus :
322 distributive2 nat Z (\lambda n,z. (neg n) * z) Zplus.
323 change with (\forall n,y,z.
324 (neg n) * (y + z) = (neg n) * y + (neg n) * z).
326 rewrite > Ztimes_neg_Zopp.
327 rewrite > distr_Ztimes_Zplus_pos.
329 (*rewrite > Zopp_Zplus.
330 rewrite < Ztimes_neg_Zopp.
331 rewrite < Ztimes_neg_Zopp.
335 variant distr_Ztimes_Zplus_neg: \forall n,y,z.
336 (neg n) * (y + z) = (neg n) * y + (neg n) * z \def
337 distributive2_Ztimes_neg_Zplus.
339 theorem distributive_Ztimes_Zplus: distributive Z Ztimes Zplus.
340 change with (\forall x,y,z:Z. x * (y + z) = x*y + x*z).
345 | apply distr_Ztimes_Zplus_pos
346 | apply distr_Ztimes_Zplus_neg
350 variant distr_Ztimes_Zplus: \forall x,y,z.
351 x * (y + z) = x*y + x*z \def
352 distributive_Ztimes_Zplus.