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