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/".
18 include "datatypes/bool.ma".
20 inductive Z : Set \def
25 definition Z_of_nat \def
26 \lambda n. match n with
28 | (S n)\Rightarrow pos n].
32 definition neg_Z_of_nat \def
33 \lambda n. match n with
35 | (S n)\Rightarrow neg n].
41 | (pos n) \Rightarrow n
42 | (neg n) \Rightarrow n].
44 definition OZ_testb \def
48 | (pos n) \Rightarrow false
49 | (neg n) \Rightarrow false].
52 \forall z. if_then_else (OZ_testb z) (eq Z z OZ) (Not (eq Z z OZ)).
53 intros.elim z.simplify.reflexivity.
57 | (pos n) \Rightarrow False
58 | (neg n) \Rightarrow False].
59 apply Hcut.rewrite > H.simplify.exact I.
63 | (pos n) \Rightarrow False
64 | (neg n) \Rightarrow False].
65 apply Hcut. rewrite > H.simplify.exact I.
69 \lambda z. match z with
70 [ OZ \Rightarrow pos O
71 | (pos n) \Rightarrow pos (S n)
75 | (S p) \Rightarrow neg p]].
78 \lambda z. match z with
79 [ OZ \Rightarrow neg O
83 | (S p) \Rightarrow pos p]
84 | (neg n) \Rightarrow neg (S n)].
86 theorem Zpred_succ: \forall z:Z. eq Z (Zpred (Zsucc z)) z.
87 intros.elim z.reflexivity.
93 theorem Zsucc_pred: \forall z:Z. eq Z (Zsucc (Zpred z)) z.
94 intros.elim z.reflexivity.
100 let rec Zplus x y : Z \def
103 | (pos m) \Rightarrow
106 | (pos n) \Rightarrow (pos (S (plus m n)))
107 | (neg n) \Rightarrow
108 match nat_compare m n with
109 [ LT \Rightarrow (neg (pred (minus n m)))
111 | GT \Rightarrow (pos (pred (minus m n)))]]
112 | (neg m) \Rightarrow
115 | (pos n) \Rightarrow
116 match nat_compare m n with
117 [ LT \Rightarrow (pos (pred (minus n m)))
119 | GT \Rightarrow (neg (pred (minus m n)))]
120 | (neg n) \Rightarrow (neg (S (plus m n)))]].
122 theorem Zplus_z_O: \forall z:Z. eq Z (Zplus z OZ) z.
124 simplify.reflexivity.
125 simplify.reflexivity.
126 simplify.reflexivity.
129 theorem sym_Zplus : \forall x,y:Z. eq Z (Zplus x y) (Zplus y x).
130 intros.elim x.simplify.rewrite > Zplus_z_O.reflexivity.
131 elim y.simplify.reflexivity.
133 rewrite < sym_plus.reflexivity.
135 rewrite > nat_compare_invert.
136 simplify.elim nat_compare ? ?.simplify.reflexivity.
137 simplify. reflexivity.
138 simplify. reflexivity.
139 elim y.simplify.reflexivity.
140 simplify.rewrite > nat_compare_invert.
141 simplify.elim nat_compare ? ?.simplify.reflexivity.
142 simplify. reflexivity.
143 simplify. reflexivity.
144 simplify.elim (sym_plus ? ?).reflexivity.
147 theorem Zpred_neg : \forall z:Z. eq Z (Zpred z) (Zplus (neg O) z).
149 simplify.reflexivity.
150 simplify.reflexivity.
151 elim e2.simplify.reflexivity.
152 simplify.reflexivity.
155 theorem Zsucc_pos : \forall z:Z. eq Z (Zsucc z) (Zplus (pos O) z).
157 simplify.reflexivity.
158 elim e1.simplify.reflexivity.
159 simplify.reflexivity.
160 simplify.reflexivity.
163 theorem Zplus_succ_pred_pp :
164 \forall n,m. eq Z (Zplus (pos n) (pos m)) (Zplus (Zsucc (pos n)) (Zpred (pos m))).
167 simplify.reflexivity.
168 simplify.reflexivity.
171 rewrite < plus_n_O.reflexivity.
173 rewrite < plus_n_Sm.reflexivity.
176 theorem Zplus_succ_pred_pn :
177 \forall n,m. eq Z (Zplus (pos n) (neg m)) (Zplus (Zsucc (pos n)) (Zpred (neg m))).
181 theorem Zplus_succ_pred_np :
182 \forall n,m. eq Z (Zplus (neg n) (pos m)) (Zplus (Zsucc (neg n)) (Zpred (pos m))).
185 simplify.reflexivity.
186 simplify.reflexivity.
188 simplify.reflexivity.
189 simplify.reflexivity.
192 theorem Zplus_succ_pred_nn:
193 \forall n,m. eq Z (Zplus (neg n) (neg m)) (Zplus (Zsucc (neg n)) (Zpred (neg m))).
196 simplify.reflexivity.
197 simplify.reflexivity.
199 simplify.rewrite < plus_n_Sm.reflexivity.
200 simplify.rewrite > plus_n_Sm.reflexivity.
203 theorem Zplus_succ_pred:
204 \forall x,y. eq Z (Zplus x y) (Zplus (Zsucc x) (Zpred y)).
207 simplify.reflexivity.
208 simplify.reflexivity.
209 rewrite < Zsucc_pos.rewrite > Zsucc_pred.reflexivity.
210 elim y.rewrite < sym_Zplus.rewrite < sym_Zplus (Zpred OZ).
211 rewrite < Zpred_neg.rewrite > Zpred_succ.
212 simplify.reflexivity.
213 rewrite < Zplus_succ_pred_nn.reflexivity.
214 apply Zplus_succ_pred_np.
215 elim y.simplify.reflexivity.
216 apply Zplus_succ_pred_pn.
217 apply Zplus_succ_pred_pp.
220 theorem Zsucc_plus_pp :
221 \forall n,m. eq Z (Zplus (Zsucc (pos n)) (pos m)) (Zsucc (Zplus (pos n) (pos m))).
225 theorem Zsucc_plus_pn :
226 \forall n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m))).
229 (\lambda n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m)))).intro.
231 simplify. reflexivity.
232 elim e1.simplify. reflexivity.
233 simplify. reflexivity.
235 simplify. reflexivity.
236 simplify.reflexivity.
238 rewrite < (Zplus_succ_pred_pn ? m1).
242 theorem Zsucc_plus_nn :
243 \forall n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m))).
246 (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m)))).intro.
248 simplify. reflexivity.
249 elim e1.simplify. reflexivity.
250 simplify. reflexivity.
252 simplify. reflexivity.
253 simplify.reflexivity.
255 rewrite < (Zplus_succ_pred_nn ? m1).
259 theorem Zsucc_plus_np :
260 \forall n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m))).
263 (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m)))).
265 simplify. reflexivity.
266 elim e1.simplify. reflexivity.
267 simplify. reflexivity.
269 simplify. reflexivity.
270 simplify.reflexivity.
273 rewrite < (Zplus_succ_pred_np ? (S m1)).
278 theorem Zsucc_plus : \forall x,y:Z. eq Z (Zplus (Zsucc x) y) (Zsucc (Zplus x y)).
279 intros.elim x.elim y.
280 simplify. reflexivity.
281 rewrite < Zsucc_pos.reflexivity.
282 simplify.reflexivity.
283 elim y.rewrite < sym_Zplus.rewrite < sym_Zplus OZ.simplify.reflexivity.
287 rewrite < sym_Zplus OZ.reflexivity.
292 theorem Zpred_plus : \forall x,y:Z. eq Z (Zplus (Zpred x) y) (Zpred (Zplus x y)).
294 cut eq Z (Zpred (Zplus x y)) (Zpred (Zplus (Zsucc (Zpred x)) y)).
296 rewrite > Zsucc_plus.
297 rewrite > Zpred_succ.
299 rewrite > Zsucc_pred.
303 theorem assoc_Zplus :
304 \forall x,y,z:Z. eq Z (Zplus x (Zplus y z)) (Zplus (Zplus x y) z).
305 intros.elim x.simplify.reflexivity.
306 elim e1.rewrite < (Zpred_neg (Zplus y z)).
307 rewrite < (Zpred_neg y).
308 rewrite < Zpred_plus.
310 rewrite > Zpred_plus (neg e).
311 rewrite > Zpred_plus (neg e).
312 rewrite > Zpred_plus (Zplus (neg e) y).
313 apply f_equal.assumption.
314 elim e2.rewrite < Zsucc_pos.
316 rewrite > Zsucc_plus.
318 rewrite > Zsucc_plus (pos e1).
319 rewrite > Zsucc_plus (pos e1).
320 rewrite > Zsucc_plus (Zplus (pos e1) y).
321 apply f_equal.assumption.