]> matita.cs.unibo.it Git - helm.git/blob - matita/library/Z/z.ma
(co)inductive type declarations are now documented
[helm.git] / matita / library / 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/Z/z".
16
17 include "datatypes/bool.ma".
18 include "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/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 n
42 | (neg n) \Rightarrow 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.elim z.
56 simplify.reflexivity.
57 simplify. unfold Not. intros (H).
58 discriminate H.
59 simplify. unfold Not. intros (H).
60 discriminate H.
61 qed.
62
63 (* discrimination *)
64 theorem injective_pos: injective nat Z pos.
65 unfold injective.
66 intros.
67 change with (abs (pos x) = abs (pos y)).
68 apply eq_f.assumption.
69 qed.
70
71 variant inj_pos : \forall n,m:nat. pos n = pos m \to n = m
72 \def injective_pos.
73
74 theorem injective_neg: injective nat Z neg.
75 unfold injective.
76 intros.
77 change with (abs (neg x) = abs (neg y)).
78 apply eq_f.assumption.
79 qed.
80
81 variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m
82 \def injective_neg.
83
84 theorem not_eq_OZ_pos: \forall n:nat. OZ \neq pos n.
85 unfold Not.intros (n H).
86 discriminate H.
87 qed.
88
89 theorem not_eq_OZ_neg :\forall n:nat. OZ \neq neg n.
90 unfold Not.intros (n H).
91 discriminate H.
92 qed.
93
94 theorem not_eq_pos_neg :\forall n,m:nat. pos n \neq neg m.
95 unfold Not.intros (n m H).
96 discriminate H.
97 qed.
98
99 theorem decidable_eq_Z : \forall x,y:Z. decidable (x=y).
100 intros.unfold decidable.
101 elim x.
102 (* goal: x=OZ *)
103   elim y.
104   (* goal: x=OZ y=OZ *)
105     left.reflexivity.
106   (* goal: x=OZ 2=2 *)
107     right.apply not_eq_OZ_pos.
108   (* goal: x=OZ 2=3 *)
109     right.apply not_eq_OZ_neg.
110 (* goal: x=pos *)
111   elim y.
112   (* goal: x=pos y=OZ *)
113     right.unfold Not.intro.
114     apply (not_eq_OZ_pos n). symmetry. assumption.
115   (* goal: x=pos y=pos *)
116     elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False))).
117     left.apply eq_f.assumption.
118     right.unfold Not.intros (H_inj).apply H. injection H_inj. assumption.
119   (* goal: x=pos y=neg *)
120     right.unfold Not.intro.apply (not_eq_pos_neg n n1). assumption.
121 (* goal: x=neg *)
122   elim y.
123   (* goal: x=neg y=OZ *)
124     right.unfold Not.intro.
125     apply (not_eq_OZ_neg n). symmetry. assumption.
126   (* goal: x=neg y=pos *)
127     right. unfold Not.intro. apply (not_eq_pos_neg n1 n). symmetry. assumption.
128   (* goal: x=neg y=neg *)
129     elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False))).
130     left.apply eq_f.assumption.
131     right.unfold Not.intro.apply H.apply injective_neg.assumption.
132 qed.
133
134 (* end discrimination *)
135
136 definition Zsucc \def
137 \lambda z. match z with
138 [ OZ \Rightarrow pos O
139 | (pos n) \Rightarrow pos (S n)
140 | (neg n) \Rightarrow 
141           match n with
142           [ O \Rightarrow OZ
143           | (S p) \Rightarrow neg p]].
144
145 definition Zpred \def
146 \lambda z. match z with
147 [ OZ \Rightarrow neg O
148 | (pos n) \Rightarrow 
149           match n with
150           [ O \Rightarrow OZ
151           | (S p) \Rightarrow pos p]
152 | (neg n) \Rightarrow neg (S n)].
153
154 theorem Zpred_Zsucc: \forall z:Z. Zpred (Zsucc z) = z.
155 intros.
156 elim z.
157   reflexivity.
158   reflexivity.
159   elim n.
160     reflexivity.
161     reflexivity.
162 qed.
163
164 theorem Zsucc_Zpred: \forall z:Z. Zsucc (Zpred z) = z.
165 intros.
166 elim z.
167   reflexivity.
168   elim n.
169     reflexivity.
170     reflexivity.
171   reflexivity.
172 qed.
173