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".
19 definition Ztimes :Z \to Z \to Z \def
26 | (pos n) \Rightarrow (pos (pred (times (S m) (S n))))
27 | (neg n) \Rightarrow (neg (pred (times (S m) (S n))))]
31 | (pos n) \Rightarrow (neg (pred (times (S m) (S n))))
32 | (neg n) \Rightarrow (pos (pred (times (S m) (S n))))]].
34 theorem Ztimes_z_OZ: \forall z:Z. eq Z (Ztimes z OZ) OZ.
41 (* da spostare in nat/order *)
42 theorem S_pred: \forall n:nat.lt O n \to eq nat n (S (pred n)).
43 intro.elim n.apply False_ind.exact not_le_Sn_O O H.
44 apply eq_f.apply pred_Sn.
48 theorem symmetric_Ztimes : symmetric Z Ztimes.
49 change with \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x).
50 intros.elim x.rewrite > Ztimes_z_OZ.reflexivity.
51 elim y.simplify.reflexivity.
52 change with eq Z (pos (pred (times (S e1) (S e)))) (pos (pred (times (S e) (S e1)))).
53 rewrite < sym_times.reflexivity.
54 change with eq Z (neg (pred (times (S e1) (S e2)))) (neg (pred (times (S e2) (S e1)))).
55 rewrite < sym_times.reflexivity.
56 elim y.simplify.reflexivity.
57 change with eq Z (neg (pred (times (S e2) (S e1)))) (neg (pred (times (S e1) (S e2)))).
58 rewrite < sym_times.reflexivity.
59 change with eq Z (pos (pred (times (S e2) (S e)))) (pos (pred (times (S e) (S e2)))).
60 rewrite < sym_times.reflexivity.
63 variant sym_Ztimes : \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x)
64 \def symmetric_Ztimes.
66 theorem associative_Ztimes: associative Z Ztimes.
67 change with \forall x,y,z:Z.eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)).
69 elim x.simplify.reflexivity.
70 elim y.simplify.reflexivity.
71 elim z.simplify.reflexivity.
73 eq Z (neg (pred (times (S (pred (times (S e1) (S e)))) (S e2))))
74 (neg (pred (times (S e1) (S (pred (times (S e) (S e2))))))).
77 theorem Zpred_Zplus_neg_O : \forall z:Z. eq Z (Zpred z) (Zplus (neg O) z).
81 elim e2.simplify.reflexivity.
85 theorem Zsucc_Zplus_pos_O : \forall z:Z. eq Z (Zsucc z) (Zplus (pos O) z).
88 elim e1.simplify.reflexivity.
93 theorem Zplus_pos_pos:
94 \forall n,m. eq Z (Zplus (pos n) (pos m)) (Zplus (Zsucc (pos n)) (Zpred (pos m))).
101 rewrite < plus_n_O.reflexivity.
103 rewrite < plus_n_Sm.reflexivity.
106 theorem Zplus_pos_neg:
107 \forall n,m. eq Z (Zplus (pos n) (neg m)) (Zplus (Zsucc (pos n)) (Zpred (neg m))).
111 theorem Zplus_neg_pos :
112 \forall n,m. eq Z (Zplus (neg n) (pos m)) (Zplus (Zsucc (neg n)) (Zpred (pos m))).
115 simplify.reflexivity.
116 simplify.reflexivity.
118 simplify.reflexivity.
119 simplify.reflexivity.
122 theorem Zplus_neg_neg:
123 \forall n,m. eq Z (Zplus (neg n) (neg m)) (Zplus (Zsucc (neg n)) (Zpred (neg m))).
126 simplify.reflexivity.
127 simplify.reflexivity.
129 simplify.rewrite < plus_n_Sm.reflexivity.
130 simplify.rewrite > plus_n_Sm.reflexivity.
133 theorem Zplus_Zsucc_Zpred:
134 \forall x,y. eq Z (Zplus x y) (Zplus (Zsucc x) (Zpred y)).
137 simplify.reflexivity.
138 simplify.reflexivity.
139 rewrite < Zsucc_Zplus_pos_O.
140 rewrite > Zsucc_Zpred.reflexivity.
141 elim y.rewrite < sym_Zplus.rewrite < sym_Zplus (Zpred OZ).
142 rewrite < Zpred_Zplus_neg_O.
143 rewrite > Zpred_Zsucc.
144 simplify.reflexivity.
145 rewrite < Zplus_neg_neg.reflexivity.
147 elim y.simplify.reflexivity.
152 theorem Zplus_Zsucc_pos_pos :
153 \forall n,m. eq Z (Zplus (Zsucc (pos n)) (pos m)) (Zsucc (Zplus (pos n) (pos m))).
157 theorem Zplus_Zsucc_pos_neg:
158 \forall n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m))).
161 (\lambda n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m)))).intro.
163 simplify. reflexivity.
164 elim e1.simplify. reflexivity.
165 simplify. reflexivity.
167 simplify. reflexivity.
168 simplify.reflexivity.
170 rewrite < (Zplus_pos_neg ? m1).
174 theorem Zplus_Zsucc_neg_neg :
175 \forall n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m))).
178 (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m)))).intro.
180 simplify. reflexivity.
181 elim e1.simplify. reflexivity.
182 simplify. reflexivity.
184 simplify. reflexivity.
185 simplify.reflexivity.
187 rewrite < (Zplus_neg_neg ? m1).
191 theorem Zplus_Zsucc_neg_pos:
192 \forall n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m))).
195 (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m)))).
197 simplify. reflexivity.
198 elim e1.simplify. reflexivity.
199 simplify. reflexivity.
201 simplify. reflexivity.
202 simplify.reflexivity.
205 rewrite < (Zplus_neg_pos ? (S m1)).
209 theorem Zplus_Zsucc : \forall x,y:Z. eq Z (Zplus (Zsucc x) y) (Zsucc (Zplus x y)).
210 intros.elim x.elim y.
211 simplify. reflexivity.
212 rewrite < Zsucc_Zplus_pos_O.reflexivity.
213 simplify.reflexivity.
214 elim y.rewrite < sym_Zplus.rewrite < sym_Zplus OZ.simplify.reflexivity.
215 apply Zplus_Zsucc_neg_neg.
216 apply Zplus_Zsucc_neg_pos.
218 rewrite < sym_Zplus OZ.reflexivity.
219 apply Zplus_Zsucc_pos_neg.
220 apply Zplus_Zsucc_pos_pos.
223 theorem Zplus_Zpred: \forall x,y:Z. eq Z (Zplus (Zpred x) y) (Zpred (Zplus x y)).
225 cut eq Z (Zpred (Zplus x y)) (Zpred (Zplus (Zsucc (Zpred x)) y)).
227 rewrite > Zplus_Zsucc.
228 rewrite > Zpred_Zsucc.
230 rewrite > Zsucc_Zpred.
235 theorem associative_Zplus: associative Z Zplus.
236 change with \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z)).
238 intros.elim x.simplify.reflexivity.
239 elim e1.rewrite < (Zpred_Zplus_neg_O (Zplus y z)).
240 rewrite < (Zpred_Zplus_neg_O y).
241 rewrite < Zplus_Zpred.
243 rewrite > Zplus_Zpred (neg e).
244 rewrite > Zplus_Zpred (neg e).
245 rewrite > Zplus_Zpred (Zplus (neg e) y).
246 apply eq_f.assumption.
247 elim e2.rewrite < Zsucc_Zplus_pos_O.
248 rewrite < Zsucc_Zplus_pos_O.
249 rewrite > Zplus_Zsucc.
251 rewrite > Zplus_Zsucc (pos e1).
252 rewrite > Zplus_Zsucc (pos e1).
253 rewrite > Zplus_Zsucc (Zplus (pos e1) y).
254 apply eq_f.assumption.
257 variant assoc_Zplus : \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z))
258 \def associative_Zplus.
260 definition Zopp : Z \to Z \def
261 \lambda x:Z. match x with
263 | (pos n) \Rightarrow (neg n)
264 | (neg n) \Rightarrow (pos n) ].
266 theorem Zplus_Zopp: \forall x:Z. (eq Z (Zplus x (Zopp x)) OZ).
270 rewrite > nat_compare_n_n.
271 simplify.apply refl_eq.
273 rewrite > nat_compare_n_n.
274 simplify.apply refl_eq.