]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library_auto/auto/Z/compare.ma
added library_auto/ to tests.
[helm.git] / helm / software / matita / library_auto / auto / Z / compare.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_auto/Z/compare".
16
17 include "auto/Z/orders.ma".
18 include "auto/nat/compare.ma".
19
20 (* boolean equality *)
21 definition eqZb : Z \to Z \to bool \def
22 \lambda x,y:Z.
23   match x with
24   [ OZ \Rightarrow 
25       match y with
26         [ OZ \Rightarrow true
27         | (pos q) \Rightarrow false
28         | (neg q) \Rightarrow false]
29   | (pos p) \Rightarrow 
30       match y with
31         [ OZ \Rightarrow false
32         | (pos q) \Rightarrow eqb p q
33         | (neg q) \Rightarrow false]     
34   | (neg p) \Rightarrow 
35       match y with
36         [ OZ \Rightarrow false
37         | (pos q) \Rightarrow false
38         | (neg q) \Rightarrow eqb p q]].
39
40 theorem eqZb_to_Prop: 
41 \forall x,y:Z. 
42 match eqZb x y with
43 [ true \Rightarrow x=y
44 | false \Rightarrow x \neq y].
45 intros.
46 elim x
47 [ elim y
48   [ simplify.
49     reflexivity
50   | simplify.
51     apply not_eq_OZ_pos
52   | simplify.
53     apply not_eq_OZ_neg
54   ]
55 | elim y
56   [ simplify.
57     unfold Not.
58     intro.
59     apply (not_eq_OZ_pos n).
60     auto
61     (*apply sym_eq.
62     assumption*)
63   | simplify.
64     apply eqb_elim
65     [ intro.    
66       simplify.
67       auto
68       (*apply eq_f.
69       assumption*)
70     | intro.
71       simplify.
72       unfold Not.
73       intro.
74       auto
75       (*apply H.
76       apply inj_pos.
77       assumption*)
78     ]
79   | simplify.
80     apply not_eq_pos_neg
81   ]
82 | elim y
83   [ simplify.
84     unfold Not.
85     intro.
86     apply (not_eq_OZ_neg n).
87     auto
88     (*apply sym_eq.
89     assumption*)
90   | simplify.
91     unfold Not.
92     intro.
93     apply (not_eq_pos_neg n1 n).
94     auto
95     (*apply sym_eq.
96     assumption*)
97   | simplify.  
98     apply eqb_elim
99     [ intro.
100       simplify.
101       auto
102       (*apply eq_f.
103       assumption*)
104     | intro.
105       simplify.
106       unfold Not.
107       intro.
108       auto
109       (*apply H.
110       apply inj_neg.
111       assumption*)
112     ]
113   ]
114 ]
115 qed.
116
117 theorem eqZb_elim: \forall x,y:Z.\forall P:bool \to Prop.
118 (x=y \to (P true)) \to (x \neq y \to (P false)) \to P (eqZb x y).
119 intros.
120 cut 
121 (match (eqZb x y) with
122 [ true \Rightarrow x=y
123 | false \Rightarrow x \neq y] \to P (eqZb x y))
124 [ apply Hcut.
125   (*NB qui auto non chiude il goal*)
126   apply eqZb_to_Prop
127 | elim (eqZb)
128   [ (*NB qui auto non chiude il goal*)
129     apply (H H2)
130   | (*NB qui auto non chiude il goal*)
131     apply (H1 H2)
132   ]
133 ]
134 qed.
135
136 definition Z_compare : Z \to Z \to compare \def
137 \lambda x,y:Z.
138   match x with
139   [ OZ \Rightarrow 
140     match y with 
141     [ OZ \Rightarrow EQ
142     | (pos m) \Rightarrow LT
143     | (neg m) \Rightarrow GT ]
144   | (pos n) \Rightarrow 
145     match y with 
146     [ OZ \Rightarrow GT
147     | (pos m) \Rightarrow (nat_compare n m)
148     | (neg m) \Rightarrow GT]
149   | (neg n) \Rightarrow 
150     match y with 
151     [ OZ \Rightarrow LT
152     | (pos m) \Rightarrow LT
153     | (neg m) \Rightarrow nat_compare m n ]].
154
155 theorem Z_compare_to_Prop : 
156 \forall x,y:Z. match (Z_compare x y) with
157 [ LT \Rightarrow x < y
158 | EQ \Rightarrow x=y
159 | GT \Rightarrow y < x]. 
160 intros.
161 elim x 
162 [ elim y
163   [ simplify.
164     apply refl_eq
165   | simplify.
166     exact I
167   | simplify.
168     exact I
169   ]
170 | elim y
171   [ simplify.
172     exact I
173   | simplify.
174     cut (match (nat_compare n n1) with
175     [ LT \Rightarrow n<n1
176     | EQ \Rightarrow n=n1
177     | GT \Rightarrow n1<n] \to 
178     match (nat_compare n n1) with
179     [ LT \Rightarrow (S n) \leq n1
180     | EQ \Rightarrow pos n = pos n1
181     | GT \Rightarrow (S n1) \leq n]) 
182     [ apply Hcut.
183       (*NB qui auto non chiude il goal*)
184       apply nat_compare_to_Prop 
185     | elim (nat_compare n n1)
186       [ simplify.
187         (*NB qui auto non chiude il goal*)
188         exact H
189       | simplify.
190         apply eq_f.
191         (*NB qui auto non chiude il goal*)
192         exact H
193       | simplify.
194         (*NB qui auto non chiude il goal*)
195         exact H
196       ]
197     ]
198   | simplify.
199     exact I    
200   ]
201 | elim y
202   [ simplify.
203     exact I
204   | simplify.
205     exact I
206   | simplify.
207     cut (match (nat_compare n1 n) with
208     [ LT \Rightarrow n1<n
209     | EQ \Rightarrow n1=n
210     | GT \Rightarrow n<n1] \to 
211     match (nat_compare n1 n) with
212     [ LT \Rightarrow (S n1) \leq n
213     | EQ \Rightarrow neg n = neg n1
214     | GT \Rightarrow (S n) \leq n1])
215     [ apply Hcut.
216       (*NB qui auto non chiude il goal*) 
217       apply nat_compare_to_Prop
218     | elim (nat_compare n1 n)
219       [ simplify.
220         (*NB qui auto non chiude il goal*)
221         exact H
222       | simplify.
223         apply eq_f.
224         apply sym_eq.
225         (*NB qui auto non chiude il goal*)
226         exact H
227       | simplify.
228         (*NB qui auto non chiude il goal*)
229         exact H
230       ]
231     ]
232   ]
233 ]
234 qed.