]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/Z/plus.ma
8fdeff3bcba158a35793a74a10a0795aa59ec59d
[helm.git] / helm / software / matita / library / Z / plus.ma
1 (**************************************************************************)
2 (*       ___                                                                *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "Z/z.ma".
16 include "nat/minus.ma".
17
18 definition Zplus :Z \to Z \to Z \def
19 \lambda x,y.
20   match x with
21     [ OZ \Rightarrow y
22     | (pos m) \Rightarrow
23         match y with
24          [ OZ \Rightarrow x
25          | (pos n) \Rightarrow (pos (pred ((S m)+(S n))))
26          | (neg n) \Rightarrow 
27               match nat_compare m n with
28                 [ LT \Rightarrow (neg (pred (n-m)))
29                 | EQ \Rightarrow OZ
30                 | GT \Rightarrow (pos (pred (m-n)))] ]
31     | (neg m) \Rightarrow
32         match y with
33          [ OZ \Rightarrow x
34          | (pos n) \Rightarrow 
35               match nat_compare m n with
36                 [ LT \Rightarrow (pos (pred (n-m)))
37                 | EQ \Rightarrow OZ
38                 | GT \Rightarrow (neg (pred (m-n)))]     
39          | (neg n) \Rightarrow (neg (pred ((S m)+(S n))))] ].
40
41 (*CSC: the URI must disappear: there is a bug now *)
42 interpretation "integer plus" 'plus x y = (cic:/matita/Z/plus/Zplus.con x y).
43          
44 theorem Zplus_z_OZ:  \forall z:Z. z+OZ = z.
45 intro.elim z.
46 simplify.reflexivity.
47 simplify.reflexivity.
48 simplify.reflexivity.
49 qed.
50
51 (* theorem symmetric_Zplus: symmetric Z Zplus. *)
52
53 theorem sym_Zplus : \forall x,y:Z. x+y = y+x.
54 intros.elim x.rewrite > Zplus_z_OZ.reflexivity.
55 elim y.simplify.reflexivity.
56 simplify.
57 rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity.
58 simplify.
59 rewrite > nat_compare_n_m_m_n.
60 simplify.elim nat_compare.simplify.reflexivity.
61 simplify. reflexivity.
62 simplify. reflexivity.
63 elim y.simplify.reflexivity.
64 simplify.rewrite > nat_compare_n_m_m_n.
65 simplify.elim nat_compare.simplify.reflexivity.
66 simplify. reflexivity.
67 simplify. reflexivity.
68 simplify.rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity.
69 qed.
70
71 theorem Zpred_Zplus_neg_O : \forall z:Z. Zpred z = (neg O)+z.
72 intros.elim z.
73   simplify.reflexivity.
74   elim n.
75     simplify.reflexivity.
76     simplify.reflexivity.
77   simplify.reflexivity.
78 qed.
79
80 theorem Zsucc_Zplus_pos_O : \forall z:Z. Zsucc z = (pos O)+z.
81 intros.elim z.
82   simplify.reflexivity.
83   simplify.reflexivity.
84   elim n.
85     simplify.reflexivity.
86     simplify.reflexivity.
87 qed.
88
89 theorem Zplus_pos_pos:
90 \forall n,m. (pos n)+(pos m) = (Zsucc (pos n))+(Zpred (pos m)).
91 intros.
92 elim n.elim m.
93 simplify.reflexivity.
94 simplify.reflexivity.
95 elim m.
96 simplify.rewrite < plus_n_Sm.
97 rewrite < plus_n_O.reflexivity.
98 simplify.rewrite < plus_n_Sm.
99 rewrite < plus_n_Sm.reflexivity.
100 qed.
101
102 theorem Zplus_pos_neg:
103 \forall n,m. (pos n)+(neg m) = (Zsucc (pos n))+(Zpred (neg m)).
104 intros.reflexivity.
105 qed.
106
107 theorem Zplus_neg_pos :
108 \forall n,m. (neg n)+(pos m) = (Zsucc (neg n))+(Zpred (pos m)).
109 intros.
110 elim n.elim m.
111 simplify.reflexivity.
112 simplify.reflexivity.
113 elim m.
114 simplify.reflexivity.
115 simplify.reflexivity.
116 qed.
117
118 theorem Zplus_neg_neg:
119 \forall n,m. (neg n)+(neg m) = (Zsucc (neg n))+(Zpred (neg m)).
120 intros.
121 elim n.elim m.
122 simplify.reflexivity.
123 simplify.reflexivity.
124 elim m.
125 simplify.rewrite > plus_n_Sm.reflexivity.
126 simplify.rewrite > plus_n_Sm.reflexivity.
127 qed.
128
129 theorem Zplus_Zsucc_Zpred:
130 \forall x,y. x+y = (Zsucc x)+(Zpred y).
131 intros.elim x. 
132   elim y.
133     simplify.reflexivity.
134     rewrite < Zsucc_Zplus_pos_O.rewrite > Zsucc_Zpred.reflexivity.
135     simplify.reflexivity.
136   elim y.
137     simplify.reflexivity.
138     apply Zplus_pos_pos.
139     apply Zplus_pos_neg.
140   elim y.
141     rewrite < sym_Zplus.rewrite < (sym_Zplus (Zpred OZ)).
142      rewrite < Zpred_Zplus_neg_O.rewrite > Zpred_Zsucc.simplify.reflexivity.
143     apply Zplus_neg_pos.
144     rewrite < Zplus_neg_neg.reflexivity.
145 qed.
146
147 theorem Zplus_Zsucc_pos_pos : 
148 \forall n,m. (Zsucc (pos n))+(pos m) = Zsucc ((pos n)+(pos m)).
149 intros.reflexivity.
150 qed.
151
152 theorem Zplus_Zsucc_pos_neg: 
153 \forall n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))).
154 intros.
155 apply (nat_elim2
156 (\lambda n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))))).intro.
157 intros.elim n1.
158 simplify. reflexivity.
159 elim n2.simplify. reflexivity.
160 simplify. reflexivity.
161 intros. elim n1.
162 simplify. reflexivity.
163 simplify.reflexivity.
164 intros.
165 rewrite < (Zplus_pos_neg ? m1).
166 elim H.reflexivity.
167 qed.
168
169 theorem Zplus_Zsucc_neg_neg : 
170 \forall n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m).
171 intros.
172 apply (nat_elim2
173 (\lambda n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m))).intro.
174 intros.elim n1.
175 simplify. reflexivity.
176 elim n2.simplify. reflexivity.
177 simplify. reflexivity.
178 intros. elim n1.
179 simplify. reflexivity.
180 simplify.reflexivity.
181 intros.
182 rewrite < (Zplus_neg_neg ? m1).
183 reflexivity.
184 qed.
185
186 theorem Zplus_Zsucc_neg_pos: 
187 \forall n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)).
188 intros.
189 apply (nat_elim2
190 (\lambda n,m. Zsucc (neg n) + (pos m) = Zsucc (neg n + pos m))).
191 intros.elim n1.
192 simplify. reflexivity.
193 elim n2.simplify. reflexivity.
194 simplify. reflexivity.
195 intros. elim n1.
196 simplify. reflexivity.
197 simplify.reflexivity.
198 intros.
199 rewrite < H.
200 rewrite < (Zplus_neg_pos ? (S m1)).
201 reflexivity.
202 qed.
203
204 theorem Zplus_Zsucc : \forall x,y:Z. (Zsucc x)+y = Zsucc (x+y).
205 intros.elim x.
206   elim y.
207     simplify. reflexivity.
208     simplify.reflexivity.
209     rewrite < Zsucc_Zplus_pos_O.reflexivity.
210   elim y.
211     rewrite < (sym_Zplus OZ).reflexivity.
212     apply Zplus_Zsucc_pos_pos.
213     apply Zplus_Zsucc_pos_neg.
214   elim y.
215     rewrite < sym_Zplus.rewrite < (sym_Zplus OZ).simplify.reflexivity.
216     apply Zplus_Zsucc_neg_pos.
217     apply Zplus_Zsucc_neg_neg.
218 qed.
219
220 theorem Zplus_Zpred: \forall x,y:Z. (Zpred x)+y = Zpred (x+y).
221 intros.
222 cut (Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y)).
223 rewrite > Hcut.
224 rewrite > Zplus_Zsucc.
225 rewrite > Zpred_Zsucc.
226 reflexivity.
227 rewrite > Zsucc_Zpred.
228 reflexivity.
229 qed.
230
231
232 theorem associative_Zplus: associative Z Zplus.
233 change with (\forall x,y,z:Z. (x + y) + z = x + (y + z)). 
234 (* simplify. *)
235 intros.elim x.
236   simplify.reflexivity.
237   elim n.
238     rewrite < Zsucc_Zplus_pos_O.rewrite < Zsucc_Zplus_pos_O.
239      rewrite > Zplus_Zsucc.reflexivity.
240     rewrite > (Zplus_Zsucc (pos n1)).rewrite > (Zplus_Zsucc (pos n1)).
241      rewrite > (Zplus_Zsucc ((pos n1)+y)).apply eq_f.assumption.
242   elim n.
243     rewrite < (Zpred_Zplus_neg_O (y+z)).rewrite < (Zpred_Zplus_neg_O y).
244      rewrite < Zplus_Zpred.reflexivity.
245     rewrite > (Zplus_Zpred (neg n1)).rewrite > (Zplus_Zpred (neg n1)).
246      rewrite > (Zplus_Zpred ((neg n1)+y)).apply eq_f.assumption.
247 qed.
248
249 variant assoc_Zplus : \forall x,y,z:Z.  (x+y)+z = x+(y+z)
250 \def associative_Zplus.
251
252 (* Zopp *)
253 definition Zopp : Z \to Z \def
254 \lambda x:Z. match x with
255 [ OZ \Rightarrow OZ
256 | (pos n) \Rightarrow (neg n)
257 | (neg n) \Rightarrow (pos n) ].
258
259 (*CSC: the URI must disappear: there is a bug now *)
260 interpretation "integer unary minus" 'uminus x = (cic:/matita/Z/plus/Zopp.con x).
261
262 theorem eq_OZ_Zopp_OZ : OZ = (- OZ).
263 reflexivity.
264 qed.
265
266 theorem Zopp_Zplus: \forall x,y:Z. -(x+y) = -x + -y.
267 intros.
268 elim x.elim y.
269 simplify. reflexivity.
270 simplify. reflexivity.
271 simplify. reflexivity.
272 elim y.
273 simplify. reflexivity.
274 simplify. reflexivity.
275 simplify. apply nat_compare_elim.
276 intro.simplify.reflexivity.
277 intro.simplify.reflexivity.
278 intro.simplify.reflexivity.
279 elim y.
280 simplify. reflexivity.
281 simplify. apply nat_compare_elim.
282 intro.simplify.reflexivity.
283 intro.simplify.reflexivity.
284 intro.simplify.reflexivity.
285 simplify.reflexivity.
286 qed.
287
288 theorem Zopp_Zopp: \forall x:Z. --x = x.
289 intro. elim x.
290 reflexivity.reflexivity.reflexivity.
291 qed.
292
293 theorem Zplus_Zopp: \forall x:Z. x+ -x = OZ.
294 intro.elim x.
295 apply refl_eq.
296 simplify.
297 rewrite > nat_compare_n_n.
298 simplify.apply refl_eq.
299 simplify.
300 rewrite > nat_compare_n_n.
301 simplify.apply refl_eq.
302 qed.
303
304 theorem injective_Zplus_l: \forall x:Z.injective Z Z (\lambda y.y+x).
305 intro.simplify.intros (z y).
306 rewrite < Zplus_z_OZ.
307 rewrite < (Zplus_z_OZ y).
308 rewrite < (Zplus_Zopp x).
309 rewrite < assoc_Zplus.
310 rewrite < assoc_Zplus.
311 apply eq_f2
312   [assumption|reflexivity]
313 qed.
314
315 theorem injective_Zplus_r: \forall x:Z.injective Z Z (\lambda y.x+y).
316 intro.simplify.intros (z y).
317 apply (injective_Zplus_l x).
318 rewrite < sym_Zplus.
319 rewrite > H.
320 apply sym_Zplus.
321 qed.
322
323 (* minus *)
324 definition Zminus : Z \to Z \to Z \def \lambda x,y:Z. x + (-y).
325
326 interpretation "integer minus" 'minus x y = (cic:/matita/Z/plus/Zminus.con x y).