]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/library_auto/auto/Z/z.ma
Stuff moved from old Matita.
[helm.git] / matita / matita / contribs / library_auto / auto / Z / 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/library_autobatch/Z/z".
16
17 include "datatypes/bool.ma".
18 include "auto/nat/nat.ma".
19
20 inductive Z : Set \def
21   OZ : Z
22 | pos : nat \to Z
23 | neg : nat \to Z.
24
25 definition Z_of_nat \def
26 \lambda n. match n with
27 [ O \Rightarrow  OZ 
28 | (S n)\Rightarrow  pos n].
29
30 coercion cic:/matita/library_autobatch/Z/z/Z_of_nat.con.
31
32 definition neg_Z_of_nat \def
33 \lambda n. match n with
34 [ O \Rightarrow  OZ 
35 | (S n)\Rightarrow  neg n].
36
37 definition abs \def
38 \lambda z.
39  match z with 
40 [ OZ \Rightarrow O
41 | (pos n) \Rightarrow (S n)
42 | (neg n) \Rightarrow (S n)].
43
44 definition OZ_test \def
45 \lambda z.
46 match z with 
47 [ OZ \Rightarrow true
48 | (pos n) \Rightarrow false
49 | (neg n) \Rightarrow false].
50
51 theorem OZ_test_to_Prop :\forall z:Z.
52 match OZ_test z with
53 [true \Rightarrow z=OZ 
54 |false \Rightarrow z \neq OZ].
55 intros.
56 elim z
57 [ (*qui autobatch non chiude il goal*)
58   simplify.
59   reflexivity
60 | simplify.
61   unfold Not.
62   intros (H).
63   (*qui autobatch non chiude il goal*)
64   destruct H
65 | simplify.
66   unfold Not.
67   intros (H).
68   (*qui autobatch non chiude il goal*)
69   destruct H
70 ]
71 qed.
72
73 (* discrimination *)
74 theorem injective_pos: injective nat Z pos.
75 unfold injective.
76 intros.
77 apply inj_S.
78 change with (abs (pos x) = abs (pos y)).
79 autobatch.
80 (*apply eq_f.
81 assumption.*)
82 qed.
83
84 variant inj_pos : \forall n,m:nat. pos n = pos m \to n = m
85 \def injective_pos.
86
87 theorem injective_neg: injective nat Z neg.
88 unfold injective.
89 intros.
90 apply inj_S.
91 change with (abs (neg x) = abs (neg y)).
92 autobatch.
93 (*apply eq_f.
94 assumption.*)
95 qed.
96
97 variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m
98 \def injective_neg.
99
100 theorem not_eq_OZ_pos: \forall n:nat. OZ \neq pos n.
101 unfold Not.
102 intros (n H).
103 (*qui autobatch non chiude il goal*)
104 destruct H.
105 qed.
106
107 theorem not_eq_OZ_neg :\forall n:nat. OZ \neq neg n.
108 unfold Not.
109 intros (n H).
110 (*qui autobatch non chiude il goal*)
111 destruct H.
112 qed.
113
114 theorem not_eq_pos_neg :\forall n,m:nat. pos n \neq neg m.
115 unfold Not.
116 intros (n m H).
117 (*qui autobatch non chiude il goal*)
118 destruct H.
119 qed.
120
121 theorem decidable_eq_Z : \forall x,y:Z. decidable (x=y).
122 intros.
123 unfold decidable.
124 elim x
125 [ (* goal: x=OZ *)
126   elim y
127   [ (* goal: x=OZ y=OZ *)
128     autobatch
129     (*left.
130     reflexivity*)
131   | (* goal: x=OZ 2=2 *)
132     autobatch
133     (*right.
134     apply not_eq_OZ_pos*)
135   | (* goal: x=OZ 2=3 *)
136     autobatch
137     (*right.
138     apply not_eq_OZ_neg*)
139   ]
140 | (* goal: x=pos *)
141   elim y
142   [ (* goal: x=pos y=OZ *)
143     right.
144     unfold Not.
145     intro.
146     apply (not_eq_OZ_pos n).
147     autobatch
148     (*symmetry. 
149     assumption*)
150   | (* goal: x=pos y=pos *)
151     elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False)))
152     [ autobatch
153       (*left.
154       apply eq_f.
155       assumption*)
156     | right.
157       unfold Not.      
158       intros (H_inj).
159       autobatch
160       (*apply H. 
161       destruct H_inj. 
162       assumption*)
163     ]
164   | (* goal: x=pos y=neg *)
165     autobatch
166     (*right.
167     unfold Not.
168     intro.
169     apply (not_eq_pos_neg n n1). 
170     assumption*)
171   ]
172 | (* goal: x=neg *)
173   elim y
174   [ (* goal: x=neg y=OZ *)
175     right.
176     unfold Not.
177     intro.
178     apply (not_eq_OZ_neg n).
179     autobatch
180     (*symmetry.
181     assumption*)
182   | (* goal: x=neg y=pos *)
183     right.
184     unfold Not.
185     intro.
186     apply (not_eq_pos_neg n1 n).
187     autobatch
188     (*symmetry.
189     assumption*)
190   | (* goal: x=neg y=neg *)
191     elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False)))
192     [ autobatch
193       (*left.
194       apply eq_f.
195       assumption*)
196     | right.
197       unfold Not.
198       intro.
199       autobatch
200       (*apply H.
201       apply injective_neg.
202       assumption*)
203     ]
204   ]
205 ]
206 qed.
207
208 (* end discrimination *)
209
210 definition Zsucc \def
211 \lambda z. match z with
212 [ OZ \Rightarrow pos O
213 | (pos n) \Rightarrow pos (S n)
214 | (neg n) \Rightarrow 
215           match n with
216           [ O \Rightarrow OZ
217           | (S p) \Rightarrow neg p]].
218
219 definition Zpred \def
220 \lambda z. match z with
221 [ OZ \Rightarrow neg O
222 | (pos n) \Rightarrow 
223           match n with
224           [ O \Rightarrow OZ
225           | (S p) \Rightarrow pos p]
226 | (neg n) \Rightarrow neg (S n)].
227
228 theorem Zpred_Zsucc: \forall z:Z. Zpred (Zsucc z) = z.
229 intros.
230 elim z
231 [ reflexivity
232 | reflexivity
233 | elim n
234   [ reflexivity
235   | reflexivity
236   ]
237 ]
238 qed.
239
240 theorem Zsucc_Zpred: \forall z:Z. Zsucc (Zpred z) = z.
241 intros.
242 elim z
243 [ reflexivity
244 | elim n
245   [ reflexivity
246   | reflexivity
247   ]
248 | reflexivity
249 ]
250 qed.
251