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/Z/times".
17 include "nat/lt_arith.ma".
20 definition Ztimes :Z \to Z \to Z \def
27 | (pos n) \Rightarrow (pos (pred (times (S m) (S n))))
28 | (neg n) \Rightarrow (neg (pred (times (S m) (S n))))]
32 | (pos n) \Rightarrow (neg (pred (times (S m) (S n))))
33 | (neg n) \Rightarrow (pos (pred (times (S m) (S n))))]].
35 (*CSC: the URI must disappear: there is a bug now *)
36 interpretation "integer times" 'times x y = (cic:/matita/Z/times/Ztimes.con x y).
38 theorem Ztimes_z_OZ: \forall z:Z. z*OZ = OZ.
45 theorem Ztimes_neg_Zopp: \forall n:nat.\forall x:Z.
46 eq Z (Ztimes (neg n) x) (Zopp (Ztimes (pos n) x)).
52 theorem symmetric_Ztimes : symmetric Z Ztimes.
53 change with \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x).
54 intros.elim x.rewrite > Ztimes_z_OZ.reflexivity.
55 elim y.simplify.reflexivity.
56 change with eq Z (pos (pred (times (S n) (S n1)))) (pos (pred (times (S n1) (S n)))).
57 rewrite < sym_times.reflexivity.
58 change with eq Z (neg (pred (times (S n) (S n1)))) (neg (pred (times (S n1) (S n)))).
59 rewrite < sym_times.reflexivity.
60 elim y.simplify.reflexivity.
61 change with eq Z (neg (pred (times (S n) (S n1)))) (neg (pred (times (S n1) (S n)))).
62 rewrite < sym_times.reflexivity.
63 change with eq Z (pos (pred (times (S n) (S n1)))) (pos (pred (times (S n1) (S n)))).
64 rewrite < sym_times.reflexivity.
67 variant sym_Ztimes : \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x)
68 \def symmetric_Ztimes.
70 theorem associative_Ztimes: associative Z Ztimes.
71 change with \forall x,y,z:Z.eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)).
79 eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
80 (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
81 rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
82 apply lt_O_times_S_S.apply lt_O_times_S_S.
84 eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
85 (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
86 rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
87 apply lt_O_times_S_S.apply lt_O_times_S_S.
91 eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
92 (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
93 rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
94 apply lt_O_times_S_S.apply lt_O_times_S_S.
96 eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
97 (pos(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
98 rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
99 apply lt_O_times_S_S.apply lt_O_times_S_S.
101 simplify.reflexivity.
103 simplify.reflexivity.
105 eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
106 (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
107 rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
108 apply lt_O_times_S_S.apply lt_O_times_S_S.
110 eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
111 (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
112 rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
113 apply lt_O_times_S_S.apply lt_O_times_S_S.
115 simplify.reflexivity.
117 eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
118 (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
119 rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
120 apply lt_O_times_S_S.apply lt_O_times_S_S.
122 eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
123 (neg(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
124 rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
125 apply lt_O_times_S_S.apply lt_O_times_S_S.
128 variant assoc_Ztimes : \forall x,y,z:Z.
129 eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)) \def
132 lemma times_minus1: \forall n,p,q:nat. lt q p \to
133 eq nat (times (S n) (S (pred (minus (S p) (S q)))))
134 (minus (pred (times (S n) (S p)))
135 (pred (times (S n) (S q)))).
138 rewrite > minus_pred_pred.
139 rewrite < distr_times_minus.
141 (* we now close all positivity conditions *)
142 apply lt_O_times_S_S.
143 apply lt_O_times_S_S.
145 apply le_SO_minus. exact H.
148 lemma Ztimes_Zplus_pos_neg_pos: \forall n,p,q:nat.
149 (pos n)*((neg p)+(pos q)) = (pos n)*(neg p)+ (pos n)*(pos q).
152 change in match (plus p (times n (S p))) with (pred (times (S n) (S p))).
153 change in match (plus q (times n (S q))) with (pred (times (S n) (S q))).
154 rewrite < nat_compare_pred_pred.
155 rewrite < nat_compare_times_l.
156 rewrite < nat_compare_S_S.
157 apply nat_compare_elim p q.
160 change with (eq Z (pos (pred (times (S n) (S (pred (minus (S q) (S p)))))))
161 (pos (pred (minus (pred (times (S n) (S q)))
162 (pred (times (S n) (S p))))))).
163 rewrite < times_minus1 n q p H.reflexivity.
164 intro.rewrite < H.simplify.reflexivity.
166 change with (eq Z (neg (pred (times (S n) (S (pred (minus (S p) (S q)))))))
167 (neg (pred (minus (pred (times (S n) (S p)))
168 (pred (times (S n) (S q))))))).
169 rewrite < times_minus1 n p q H.reflexivity.
170 (* two more positivity conditions from nat_compare_pred_pred *)
171 apply lt_O_times_S_S.
172 apply lt_O_times_S_S.
175 lemma Ztimes_Zplus_pos_pos_neg: \forall n,p,q:nat.
176 (pos n)*((pos p)+(neg q)) = (pos n)*(pos p)+ (pos n)*(neg q).
179 rewrite > Ztimes_Zplus_pos_neg_pos.
183 lemma distributive2_Ztimes_pos_Zplus:
184 distributive2 nat Z (\lambda n,z. Ztimes (pos n) z) Zplus.
185 change with \forall n,y,z.
186 eq Z (Ztimes (pos n) (Zplus y z)) (Zplus (Ztimes (pos n) y) (Ztimes (pos n) z)).
192 eq Z (pos (pred (times (S n) (plus (S n1) (S n2)))))
193 (pos (pred (plus (times (S n) (S n1))(times (S n) (S n2))))).
194 rewrite < distr_times_plus.reflexivity.
195 apply Ztimes_Zplus_pos_pos_neg.
198 apply Ztimes_Zplus_pos_neg_pos.
200 eq Z (neg (pred (times (S n) (plus (S n1) (S n2)))))
201 (neg (pred (plus (times (S n) (S n1))(times (S n) (S n2))))).
202 rewrite < distr_times_plus.reflexivity.
205 variant distr_Ztimes_Zplus_pos: \forall n,y,z.
206 eq Z (Ztimes (pos n) (Zplus y z)) (Zplus (Ztimes (pos n) y) (Ztimes (pos n) z)) \def
207 distributive2_Ztimes_pos_Zplus.
209 lemma distributive2_Ztimes_neg_Zplus :
210 distributive2 nat Z (\lambda n,z. Ztimes (neg n) z) Zplus.
211 change with \forall n,y,z.
212 eq Z (Ztimes (neg n) (Zplus y z)) (Zplus (Ztimes (neg n) y) (Ztimes (neg n) z)).
214 rewrite > Ztimes_neg_Zopp.
215 rewrite > distr_Ztimes_Zplus_pos.
216 rewrite > Zopp_Zplus.
217 rewrite < Ztimes_neg_Zopp. rewrite < Ztimes_neg_Zopp.
221 variant distr_Ztimes_Zplus_neg: \forall n,y,z.
222 eq Z (Ztimes (neg n) (Zplus y z)) (Zplus (Ztimes (neg n) y) (Ztimes (neg n) z)) \def
223 distributive2_Ztimes_neg_Zplus.
225 theorem distributive_Ztimes_Zplus: distributive Z Ztimes Zplus.
226 change with \forall x,y,z:Z.
227 eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)).
230 simplify.reflexivity.
232 apply distr_Ztimes_Zplus_pos.
234 apply distr_Ztimes_Zplus_neg.
237 variant distr_Ztimes_Zplus: \forall x,y,z.
238 eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)) \def
239 distributive_Ztimes_Zplus.