]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/Z/z.ma
Even more Q stuff classified.
[helm.git] / helm / software / 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 lemma pos_n_eq_S_n : \forall n : nat.
38   (pos n) = (S n).
39 intro.reflexivity. 
40 qed.
41
42 definition abs \def
43 \lambda z.
44  match z with 
45 [ OZ \Rightarrow O
46 | (pos n) \Rightarrow (S n)
47 | (neg n) \Rightarrow (S n)].
48
49 definition OZ_test \def
50 \lambda z.
51 match z with 
52 [ OZ \Rightarrow true
53 | (pos n) \Rightarrow false
54 | (neg n) \Rightarrow false].
55
56 theorem OZ_test_to_Prop :\forall z:Z.
57 match OZ_test z with
58 [true \Rightarrow z=OZ 
59 |false \Rightarrow z \neq OZ].
60 intros.elim z.
61 simplify.reflexivity.
62 simplify. unfold Not. intros (H).
63 destruct H.
64 simplify. unfold Not. intros (H).
65 destruct H.
66 qed.
67
68 (* discrimination *)
69 theorem injective_pos: injective nat Z pos.
70 unfold injective.
71 intros.
72 apply inj_S.
73 change with (abs (pos x) = abs (pos y)).
74 apply eq_f.assumption.
75 qed.
76
77 variant inj_pos : \forall n,m:nat. pos n = pos m \to n = m
78 \def injective_pos.
79
80 theorem injective_neg: injective nat Z neg.
81 unfold injective.
82 intros.
83 apply inj_S.
84 change with (abs (neg x) = abs (neg y)).
85 apply eq_f.assumption.
86 qed.
87
88 variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m
89 \def injective_neg.
90
91 theorem not_eq_OZ_pos: \forall n:nat. OZ \neq pos n.
92 unfold Not.intros (n H).
93 destruct H.
94 qed.
95
96 theorem not_eq_OZ_neg :\forall n:nat. OZ \neq neg n.
97 unfold Not.intros (n H).
98 destruct H.
99 qed.
100
101 theorem not_eq_pos_neg :\forall n,m:nat. pos n \neq neg m.
102 unfold Not.intros (n m H).
103 destruct H.
104 qed.
105
106 theorem decidable_eq_Z : \forall x,y:Z. decidable (x=y).
107 intros.unfold decidable.
108 elim x.
109 (* goal: x=OZ *)
110   elim y.
111   (* goal: x=OZ y=OZ *)
112     left.reflexivity.
113   (* goal: x=OZ 2=2 *)
114     right.apply not_eq_OZ_pos.
115   (* goal: x=OZ 2=3 *)
116     right.apply not_eq_OZ_neg.
117 (* goal: x=pos *)
118   elim y.
119   (* goal: x=pos y=OZ *)
120     right.unfold Not.intro.
121     apply (not_eq_OZ_pos n). symmetry. assumption.
122   (* goal: x=pos y=pos *)
123     elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False))).
124     left.apply eq_f.assumption.
125     right.unfold Not.intros (H_inj).apply H. destruct H_inj. reflexivity.
126   (* goal: x=pos y=neg *)
127     right.unfold Not.intro.apply (not_eq_pos_neg n n1). assumption.
128 (* goal: x=neg *)
129   elim y.
130   (* goal: x=neg y=OZ *)
131     right.unfold Not.intro.
132     apply (not_eq_OZ_neg n). symmetry. assumption.
133   (* goal: x=neg y=pos *)
134     right. unfold Not.intro. apply (not_eq_pos_neg n1 n). symmetry. assumption.
135   (* goal: x=neg y=neg *)
136     elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False))).
137     left.apply eq_f.assumption.
138     right.unfold Not.intro.apply H.apply injective_neg.assumption.
139 qed.
140
141 (* end discrimination *)
142
143 definition Zsucc \def
144 \lambda z. match z with
145 [ OZ \Rightarrow pos O
146 | (pos n) \Rightarrow pos (S n)
147 | (neg n) \Rightarrow 
148           match n with
149           [ O \Rightarrow OZ
150           | (S p) \Rightarrow neg p]].
151
152 definition Zpred \def
153 \lambda z. match z with
154 [ OZ \Rightarrow neg O
155 | (pos n) \Rightarrow 
156           match n with
157           [ O \Rightarrow OZ
158           | (S p) \Rightarrow pos p]
159 | (neg n) \Rightarrow neg (S n)].
160
161 theorem Zpred_Zsucc: \forall z:Z. Zpred (Zsucc z) = z.
162 intros.
163 elim z.
164   reflexivity.
165   reflexivity.
166   elim n.
167     reflexivity.
168     reflexivity.
169 qed.
170
171 theorem Zsucc_Zpred: \forall z:Z. Zsucc (Zpred z) = z.
172 intros.
173 elim z.
174   reflexivity.
175   elim n.
176     reflexivity.
177     reflexivity.
178   reflexivity.
179 qed.
180