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.
43 theorem symmetric_Ztimes : symmetric Z Ztimes.
44 change with \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x).
45 intros.elim x.rewrite > Ztimes_z_OZ.reflexivity.
46 elim y.simplify.reflexivity.
47 change with eq Z (pos (pred (times (S e1) (S e)))) (pos (pred (times (S e) (S e1)))).
48 rewrite < sym_times.reflexivity.
49 change with eq Z (neg (pred (times (S e1) (S e2)))) (neg (pred (times (S e2) (S e1)))).
50 rewrite < sym_times.reflexivity.
51 elim y.simplify.reflexivity.
52 change with eq Z (neg (pred (times (S e2) (S e1)))) (neg (pred (times (S e1) (S e2)))).
53 rewrite < sym_times.reflexivity.
54 change with eq Z (pos (pred (times (S e2) (S e)))) (pos (pred (times (S e) (S e2)))).
55 rewrite < sym_times.reflexivity.
58 variant sym_Ztimes : \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x)
59 \def symmetric_Ztimes.
61 theorem associative_Ztimes: associative Z Ztimes.
62 change with \forall x,y,z:Z.eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)).
64 elim x.simplify.reflexivity.
65 elim y.simplify.reflexivity.
66 elim z.simplify.reflexivity.
68 eq Z (neg (pred (times (S (pred (times (S e1) (S e)))) (S e2))))
69 (neg (pred (times (S e1) (S (pred (times (S e) (S e2))))))).
72 theorem Zpred_Zplus_neg_O : \forall z:Z. eq Z (Zpred z) (Zplus (neg O) z).
76 elim e2.simplify.reflexivity.
80 theorem Zsucc_Zplus_pos_O : \forall z:Z. eq Z (Zsucc z) (Zplus (pos O) z).
83 elim e1.simplify.reflexivity.
88 theorem Zplus_pos_pos:
89 \forall n,m. eq Z (Zplus (pos n) (pos m)) (Zplus (Zsucc (pos n)) (Zpred (pos m))).
96 rewrite < plus_n_O.reflexivity.
98 rewrite < plus_n_Sm.reflexivity.
101 theorem Zplus_pos_neg:
102 \forall n,m. eq Z (Zplus (pos n) (neg m)) (Zplus (Zsucc (pos n)) (Zpred (neg m))).
106 theorem Zplus_neg_pos :
107 \forall n,m. eq Z (Zplus (neg n) (pos m)) (Zplus (Zsucc (neg n)) (Zpred (pos m))).
110 simplify.reflexivity.
111 simplify.reflexivity.
113 simplify.reflexivity.
114 simplify.reflexivity.
117 theorem Zplus_neg_neg:
118 \forall n,m. eq Z (Zplus (neg n) (neg m)) (Zplus (Zsucc (neg n)) (Zpred (neg m))).
121 simplify.reflexivity.
122 simplify.reflexivity.
124 simplify.rewrite < plus_n_Sm.reflexivity.
125 simplify.rewrite > plus_n_Sm.reflexivity.
128 theorem Zplus_Zsucc_Zpred:
129 \forall x,y. eq Z (Zplus x y) (Zplus (Zsucc x) (Zpred y)).
132 simplify.reflexivity.
133 simplify.reflexivity.
134 rewrite < Zsucc_Zplus_pos_O.
135 rewrite > Zsucc_Zpred.reflexivity.
136 elim y.rewrite < sym_Zplus.rewrite < sym_Zplus (Zpred OZ).
137 rewrite < Zpred_Zplus_neg_O.
138 rewrite > Zpred_Zsucc.
139 simplify.reflexivity.
140 rewrite < Zplus_neg_neg.reflexivity.
142 elim y.simplify.reflexivity.
147 theorem Zplus_Zsucc_pos_pos :
148 \forall n,m. eq Z (Zplus (Zsucc (pos n)) (pos m)) (Zsucc (Zplus (pos n) (pos m))).
152 theorem Zplus_Zsucc_pos_neg:
153 \forall n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m))).
156 (\lambda n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m)))).intro.
158 simplify. reflexivity.
159 elim e1.simplify. reflexivity.
160 simplify. reflexivity.
162 simplify. reflexivity.
163 simplify.reflexivity.
165 rewrite < (Zplus_pos_neg ? m1).
169 theorem Zplus_Zsucc_neg_neg :
170 \forall n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m))).
173 (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m)))).intro.
175 simplify. reflexivity.
176 elim e1.simplify. reflexivity.
177 simplify. reflexivity.
179 simplify. reflexivity.
180 simplify.reflexivity.
182 rewrite < (Zplus_neg_neg ? m1).
186 theorem Zplus_Zsucc_neg_pos:
187 \forall n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m))).
190 (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m)))).
192 simplify. reflexivity.
193 elim e1.simplify. reflexivity.
194 simplify. reflexivity.
196 simplify. reflexivity.
197 simplify.reflexivity.
200 rewrite < (Zplus_neg_pos ? (S m1)).
204 theorem Zplus_Zsucc : \forall x,y:Z. eq Z (Zplus (Zsucc x) y) (Zsucc (Zplus x y)).
205 intros.elim x.elim y.
206 simplify. reflexivity.
207 rewrite < Zsucc_Zplus_pos_O.reflexivity.
208 simplify.reflexivity.
209 elim y.rewrite < sym_Zplus.rewrite < sym_Zplus OZ.simplify.reflexivity.
210 apply Zplus_Zsucc_neg_neg.
211 apply Zplus_Zsucc_neg_pos.
213 rewrite < sym_Zplus OZ.reflexivity.
214 apply Zplus_Zsucc_pos_neg.
215 apply Zplus_Zsucc_pos_pos.
218 theorem Zplus_Zpred: \forall x,y:Z. eq Z (Zplus (Zpred x) y) (Zpred (Zplus x y)).
220 cut eq Z (Zpred (Zplus x y)) (Zpred (Zplus (Zsucc (Zpred x)) y)).
222 rewrite > Zplus_Zsucc.
223 rewrite > Zpred_Zsucc.
225 rewrite > Zsucc_Zpred.
230 theorem associative_Zplus: associative Z Zplus.
231 change with \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z)).
233 intros.elim x.simplify.reflexivity.
234 elim e1.rewrite < (Zpred_Zplus_neg_O (Zplus y z)).
235 rewrite < (Zpred_Zplus_neg_O y).
236 rewrite < Zplus_Zpred.
238 rewrite > Zplus_Zpred (neg e).
239 rewrite > Zplus_Zpred (neg e).
240 rewrite > Zplus_Zpred (Zplus (neg e) y).
241 apply eq_f.assumption.
242 elim e2.rewrite < Zsucc_Zplus_pos_O.
243 rewrite < Zsucc_Zplus_pos_O.
244 rewrite > Zplus_Zsucc.
246 rewrite > Zplus_Zsucc (pos e1).
247 rewrite > Zplus_Zsucc (pos e1).
248 rewrite > Zplus_Zsucc (Zplus (pos e1) y).
249 apply eq_f.assumption.
252 variant assoc_Zplus : \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z))
253 \def associative_Zplus.
255 definition Zopp : Z \to Z \def
256 \lambda x:Z. match x with
258 | (pos n) \Rightarrow (neg n)
259 | (neg n) \Rightarrow (pos n) ].
261 theorem Zplus_Zopp: \forall x:Z. (eq Z (Zplus x (Zopp x)) OZ).
265 rewrite > nat_compare_n_n.
266 simplify.apply refl_eq.
268 rewrite > nat_compare_n_n.
269 simplify.apply refl_eq.