]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/library/Z.ma
added Variant theorem flavour
[helm.git] / helm / matita / library / Z.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/".
16
17 include "nat.ma".
18
19 inductive Z : Set \def
20   OZ : Z
21 | pos : nat \to Z
22 | neg : nat \to Z.
23
24 definition Z_of_nat \def
25 \lambda n. match n with
26 [ O \Rightarrow  OZ 
27 | (S n)\Rightarrow  pos n].
28
29 coercion Z_of_nat.
30
31 definition neg_Z_of_nat \def
32 \lambda n. match n with
33 [ O \Rightarrow  OZ 
34 | (S n)\Rightarrow  neg n].
35
36 definition absZ \def
37 \lambda z.
38  match z with 
39 [ OZ \Rightarrow O
40 | (pos n) \Rightarrow n
41 | (neg n) \Rightarrow n].
42
43 definition OZ_testb \def
44 \lambda z.
45 match z with 
46 [ OZ \Rightarrow true
47 | (pos n) \Rightarrow false
48 | (neg n) \Rightarrow false].
49
50 theorem OZ_discr :
51 \forall z. if_then_else (OZ_testb z) (eq Z z OZ) (Not (eq Z z OZ)). 
52 intros.elim z.simplify.reflexivity.
53 simplify.intros.
54 cut match neg e1 with 
55 [ OZ \Rightarrow True 
56 | (pos n) \Rightarrow False
57 | (neg n) \Rightarrow False].
58 apply Hcut.rewrite > H.simplify.exact I.
59 simplify.intros.
60 cut match pos e2 with 
61 [ OZ \Rightarrow True 
62 | (pos n) \Rightarrow False
63 | (neg n) \Rightarrow False].
64 apply Hcut. rewrite > H.simplify.exact I.
65 qed.
66
67 definition Zsucc \def
68 \lambda z. match z with
69 [ OZ \Rightarrow pos O
70 | (pos n) \Rightarrow pos (S n)
71 | (neg n) \Rightarrow 
72           match n with
73           [ O \Rightarrow OZ
74           | (S p) \Rightarrow neg p]].
75
76 definition Zpred \def
77 \lambda z. match z with
78 [ OZ \Rightarrow neg O
79 | (pos n) \Rightarrow 
80           match n with
81           [ O \Rightarrow OZ
82           | (S p) \Rightarrow pos p]
83 | (neg n) \Rightarrow neg (S n)].
84
85 theorem Zpred_succ: \forall z:Z. eq Z (Zpred (Zsucc z)) z.
86 intros.elim z.reflexivity.
87 elim e1.reflexivity.
88 reflexivity.
89 reflexivity.
90 qed.
91
92 theorem Zsucc_pred: \forall z:Z. eq Z (Zsucc (Zpred z)) z.
93 intros.elim z.reflexivity.
94 reflexivity.
95 elim e2.reflexivity.
96 reflexivity.
97 qed.
98
99 let rec Zplus x y : Z \def
100   match x with
101     [ OZ \Rightarrow y
102     | (pos m) \Rightarrow
103         match y with
104          [ OZ \Rightarrow x
105          | (pos n) \Rightarrow (pos (S (plus m n)))
106          | (neg n) \Rightarrow 
107               match nat_compare m n with
108                 [ LT \Rightarrow (neg (pred (minus n m)))
109                 | EQ \Rightarrow OZ
110                 | GT \Rightarrow (pos (pred (minus m n)))]]
111     | (neg m) \Rightarrow
112         match y with
113          [ OZ \Rightarrow x
114          | (pos n) \Rightarrow 
115               match nat_compare m n with
116                 [ LT \Rightarrow (pos (pred (minus n m)))
117                 | EQ \Rightarrow OZ
118                 | GT \Rightarrow (neg (pred (minus m n)))]     
119          | (neg n) \Rightarrow (neg (S (plus m n)))]].
120          
121 theorem Zplus_z_O:  \forall z:Z. eq Z (Zplus z OZ) z.
122 intro.elim z.
123 simplify.reflexivity.
124 simplify.reflexivity.
125 simplify.reflexivity.
126 qed.
127
128 theorem sym_Zplus : \forall x,y:Z. eq Z (Zplus x y) (Zplus y x).
129 intros.elim x.simplify.rewrite > Zplus_z_O.reflexivity.
130 elim y.simplify.reflexivity.
131 simplify.
132 rewrite < sym_plus.reflexivity.
133 simplify.
134 rewrite > nat_compare_invert.
135 simplify.elim nat_compare ? ?.simplify.reflexivity.
136 simplify. reflexivity.
137 simplify. reflexivity.
138 elim y.simplify.reflexivity.
139 simplify.rewrite > nat_compare_invert.
140 simplify.elim nat_compare ? ?.simplify.reflexivity.
141 simplify. reflexivity.
142 simplify. reflexivity.
143 simplify.elim (sym_plus ? ?).reflexivity.
144 qed.
145
146 theorem Zpred_neg : \forall z:Z. eq Z (Zpred z) (Zplus (neg O) z).
147 intros.elim z.
148 simplify.reflexivity.
149 simplify.reflexivity.
150 elim e2.simplify.reflexivity.
151 simplify.reflexivity.
152 qed.
153
154 theorem Zsucc_pos : \forall z:Z. eq Z (Zsucc z) (Zplus (pos O) z).
155 intros.elim z.
156 simplify.reflexivity.
157 elim e1.simplify.reflexivity.
158 simplify.reflexivity.
159 simplify.reflexivity.
160 qed.
161
162 theorem Zplus_succ_pred_pp :
163 \forall n,m. eq Z (Zplus (pos n) (pos m)) (Zplus (Zsucc (pos n)) (Zpred (pos m))).
164 intros.
165 elim n.elim m.
166 simplify.reflexivity.
167 simplify.reflexivity.
168 elim m.
169 simplify.
170 rewrite < plus_n_O.reflexivity.
171 simplify.
172 rewrite < plus_n_Sm.reflexivity.
173 qed.
174
175 theorem Zplus_succ_pred_pn :
176 \forall n,m. eq Z (Zplus (pos n) (neg m)) (Zplus (Zsucc (pos n)) (Zpred (neg m))).
177 intros.reflexivity.
178 qed.
179
180 theorem Zplus_succ_pred_np :
181 \forall n,m. eq Z (Zplus (neg n) (pos m)) (Zplus (Zsucc (neg n)) (Zpred (pos m))).
182 intros.
183 elim n.elim m.
184 simplify.reflexivity.
185 simplify.reflexivity.
186 elim m.
187 simplify.reflexivity.
188 simplify.reflexivity.
189 qed.
190
191 theorem Zplus_succ_pred_nn:
192 \forall n,m. eq Z (Zplus (neg n) (neg m)) (Zplus (Zsucc (neg n)) (Zpred (neg m))).
193 intros.
194 elim n.elim m.
195 simplify.reflexivity.
196 simplify.reflexivity.
197 elim m.
198 simplify.rewrite < plus_n_Sm.reflexivity.
199 simplify.rewrite > plus_n_Sm.reflexivity.
200 qed.
201
202 theorem Zplus_succ_pred:
203 \forall x,y. eq Z (Zplus x y) (Zplus (Zsucc x) (Zpred y)).
204 intros.
205 elim x. elim y.
206 simplify.reflexivity.
207 simplify.reflexivity.
208 rewrite < Zsucc_pos.rewrite > Zsucc_pred.reflexivity.
209 elim y.rewrite < sym_Zplus.rewrite < sym_Zplus (Zpred OZ).
210 rewrite < Zpred_neg.rewrite > Zpred_succ.
211 simplify.reflexivity.
212 rewrite < Zplus_succ_pred_nn.reflexivity.
213 apply Zplus_succ_pred_np.
214 elim y.simplify.reflexivity.
215 apply Zplus_succ_pred_pn.
216 apply Zplus_succ_pred_pp.
217 qed.
218
219 theorem Zsucc_plus_pp : 
220 \forall n,m. eq Z (Zplus (Zsucc (pos n)) (pos m)) (Zsucc (Zplus (pos n) (pos m))).
221 intros.reflexivity.
222 qed.
223
224 theorem Zsucc_plus_pn : 
225 \forall n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m))).
226 intros.
227 apply nat_double_ind
228 (\lambda n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m)))).intro.
229 intros.elim n1.
230 simplify. reflexivity.
231 elim e1.simplify. reflexivity.
232 simplify. reflexivity.
233 intros. elim n1.
234 simplify. reflexivity.
235 simplify.reflexivity.
236 intros.
237 rewrite < (Zplus_succ_pred_pn ? m1).
238 elim H.reflexivity.
239 qed.
240
241 theorem Zsucc_plus_nn : 
242 \forall n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m))).
243 intros.
244 apply nat_double_ind
245 (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m)))).intro.
246 intros.elim n1.
247 simplify. reflexivity.
248 elim e1.simplify. reflexivity.
249 simplify. reflexivity.
250 intros. elim n1.
251 simplify. reflexivity.
252 simplify.reflexivity.
253 intros.
254 rewrite < (Zplus_succ_pred_nn ? m1).
255 reflexivity.
256 qed.
257
258 theorem Zsucc_plus_np : 
259 \forall n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m))).
260 intros.
261 apply nat_double_ind
262 (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m)))).
263 intros.elim n1.
264 simplify. reflexivity.
265 elim e1.simplify. reflexivity.
266 simplify. reflexivity.
267 intros. elim n1.
268 simplify. reflexivity.
269 simplify.reflexivity.
270 intros.
271 rewrite < H.
272 rewrite < (Zplus_succ_pred_np ? (S m1)).
273 reflexivity.
274 qed.
275
276
277 theorem Zsucc_plus : \forall x,y:Z. eq Z (Zplus (Zsucc x) y) (Zsucc (Zplus x y)).
278 intros.elim x.elim y.
279 simplify. reflexivity.
280 rewrite < Zsucc_pos.reflexivity.
281 simplify.reflexivity.
282 elim y.rewrite < sym_Zplus.rewrite < sym_Zplus OZ.simplify.reflexivity.
283 apply Zsucc_plus_nn.
284 apply Zsucc_plus_np.
285 elim y.
286 rewrite < sym_Zplus OZ.reflexivity.
287 apply Zsucc_plus_pn.
288 apply Zsucc_plus_pp.
289 qed.
290
291 theorem Zpred_plus : \forall x,y:Z. eq Z (Zplus (Zpred x) y) (Zpred (Zplus x y)).
292 intros.
293 cut eq Z (Zpred (Zplus x y)) (Zpred (Zplus (Zsucc (Zpred x)) y)).
294 rewrite > Hcut.
295 rewrite > Zsucc_plus.
296 rewrite > Zpred_succ.
297 reflexivity.
298 rewrite > Zsucc_pred.
299 reflexivity.
300 qed.
301
302 theorem assoc_Zplus : 
303 \forall x,y,z:Z. eq Z (Zplus x (Zplus y z)) (Zplus (Zplus x y) z).
304 intros.elim x.simplify.reflexivity.
305 elim e1.rewrite < (Zpred_neg (Zplus y z)).
306 rewrite < (Zpred_neg y).
307 rewrite < Zpred_plus.
308 reflexivity.
309 rewrite > Zpred_plus (neg e).
310 rewrite > Zpred_plus (neg e).
311 rewrite > Zpred_plus (Zplus (neg e) y).
312 apply f_equal.assumption.
313 elim e2.rewrite < Zsucc_pos.
314 rewrite < Zsucc_pos.
315 rewrite > Zsucc_plus.
316 reflexivity.
317 rewrite > Zsucc_plus (pos e1).
318 rewrite > Zsucc_plus (pos e1).
319 rewrite > Zsucc_plus (Zplus (pos e1) y).
320 apply f_equal.assumption.
321 qed.