1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "num/comp_ext.ma".
24 include "num/bool_lemmas.ma".
30 nrecord comp_num (T:Type) : Type ≝
40 (feq (cnH ? cn1) (cnH ? cn2)) ⊗ (feq (cnL ? cn1) (cnL ? cn2)).
42 nlemma cn_destruct_1 :
44 mk_comp_num T x1 y1 = mk_comp_num T x2 y2 → x1 = x2.
45 #T; #x1; #x2; #y1; #y2; #H;
46 nchange with (match mk_comp_num ? x2 y2 with [ mk_comp_num a _ ⇒ x1 = a ]);
52 nlemma cn_destruct_2 :
54 mk_comp_num T x1 y1 = mk_comp_num T x2 y2 → y1 = y2.
55 #T; #x1; #x2; #y1; #y2; #H;
56 nchange with (match mk_comp_num ? x2 y2 with [ mk_comp_num _ b ⇒ y1 = b ]);
62 nlemma symmetric_eqcn :
64 (symmetricT T bool feq) →
65 (symmetricT (comp_num T) bool (eq_cn T feq)).
67 #b1; nelim b1; #e1; #e2;
68 #b2; nelim b2; #e3; #e4;
69 nchange with (((feq e1 e3)⊗(feq e2 e4)) = ((feq e3 e1)⊗(feq e4 e2)));
77 (∀x,y:T.(feq x y = true) → (x = y)) →
79 ((eq_cn T feq b1 b2 = true) → (b1 = b2))).
80 #T; #feq; #H; #b1; #b2;
83 nchange in ⊢ (% → ?) with (((feq e1 e3)⊗(feq e2 e4)) = true);
85 nrewrite < (H … (andb_true_true_l … H1));
86 nrewrite < (H … (andb_true_true_r … H1));
92 (∀x,y:T.(x = y) → (feq x y = true)) →
94 ((b1 = b2) → (eq_cn T feq b1 b2 = true))).
95 #T; #feq; #H; #b1; #b2;
99 nrewrite < (cn_destruct_1 … H1);
100 nrewrite < (cn_destruct_2 … H1);
101 nchange with (((feq e1 e1)⊗(feq e2 e2)) = true);
102 nrewrite > (H e1 e1 (refl_eq …));
103 nrewrite > (H e2 e2 (refl_eq …));
108 nlemma decidable_cn_aux1 :
109 ∀T.∀e1,e2,e3,e4:T.e1 ≠ e3 → (mk_comp_num T e1 e2) ≠ (mk_comp_num T e3 e4).
110 #T; #e1; #e2; #e3; #e4;
112 napply (H (cn_destruct_1 … H1)).
115 nlemma decidable_cn_aux2 :
116 ∀T.∀e1,e2,e3,e4:T.e2 ≠ e4 → (mk_comp_num T e1 e2) ≠ (mk_comp_num T e3 e4).
117 #T; #e1; #e2; #e3; #e4;
119 napply (H (cn_destruct_2 … H1)).
122 nlemma decidable_cn :
123 ∀T.(∀x,y:T.decidable (x = y)) →
125 (decidable (b1 = b2))).
127 #b1; nelim b1; #e1; #e2;
128 #b2; nelim b2; #e3; #e4;
130 napply (or2_elim (e1 = e3) (e1 ≠ e3) ? (H e1 e3) …);
131 ##[ ##2: #H1; napply (or2_intro2 … (decidable_cn_aux1 T e1 e2 e3 e4 H1))
132 ##| ##1: #H1; napply (or2_elim (e2 = e4) (e2 ≠ e4) ? (H e2 e4) …);
133 ##[ ##2: #H2; napply (or2_intro2 … (decidable_cn_aux2 T e1 e2 e3 e4 H2))
134 ##| ##1: #H2; nrewrite > H1; nrewrite > H2;
135 napply (or2_intro1 … (refl_eq ? (mk_comp_num T e3 e4)))
140 nlemma neqcn_to_neq :
141 ∀T.∀feq:T → T → bool.
142 (∀x,y:T.(feq x y = false) → (x ≠ y)) →
144 ((eq_cn T feq b1 b2 = false) → (b1 ≠ b2))).
145 #T; #feq; #H; #b1; #b2;
148 nchange with ((((feq e1 e3) ⊗ (feq e2 e4)) = false) → ?);
150 napply (or2_elim ((feq e1 e3) = false) ((feq e2 e4) = false) ? (andb_false2 … H1) …);
151 ##[ ##1: #H2; napply (decidable_cn_aux1 … (H … H2))
152 ##| ##2: #H2; napply (decidable_cn_aux2 … (H … H2))
157 ∀T.(∀x,y:T.decidable (x = y)) →
159 ((mk_comp_num T e1 e2) ≠ (mk_comp_num T e3 e4)) →
160 ((e1 ≠ e3) ∨ (e2 ≠ e4))).
161 #T; #H; #e1; #e2; #e3; #e4;
163 napply (or2_elim (e1 = e3) (e1 ≠ e3) ? (H e1 e3) …);
164 ##[ ##2: #H2; napply (or2_intro1 … H2)
165 ##| ##1: #H2; napply (or2_elim (e2 = e4) (e2 ≠ e4) ? (H e2 e4) …);
166 ##[ ##2: #H3; napply (or2_intro2 … H3)
167 ##| ##1: #H3; nrewrite > H2 in H1:(%);
169 #H1; nelim (H1 (refl_eq …))
174 nlemma neq_to_neqcn :
175 ∀T.∀feq:T → T → bool.
176 (∀x,y:T.(x ≠ y) → (feq x y = false)) →
177 (∀x,y:T.decidable (x = y)) →
179 ((b1 ≠ b2) → (eq_cn T feq b1 b2 = false))).
180 #T; #feq; #H; #H1; #b1; #b2;
183 #H2; nchange with (((feq e1 e3) ⊗ (feq e2 e4)) = false);
184 napply (or2_elim (e1 ≠ e3) (e2 ≠ e4) ? (cn_destruct T H1 e1 e2 e3 e4 … H2) …);
185 ##[ ##1: #H3; nrewrite > (H … H3); nnormalize; napply refl_eq
186 ##| ##2: #H3; nrewrite > (H … H3);
187 nrewrite > (symmetric_andbool (feq e1 e3) false);
188 nnormalize; napply refl_eq
192 nlemma cn_is_comparable : comparable → comparable.
195 ##[ napply (mk_comp_num ? (zeroc ?) (zeroc ?))
197 ##| napply (λP.forallc T
199 (λl.P (mk_comp_num ? h l))))
201 ##| napply (eq_cn ? (eqc T))
203 ##| napply (eqcn_to_eq … (eqc_to_eq T))
205 ##| napply (eq_to_eqcn … (eq_to_eqc T))
207 ##| napply (neqcn_to_neq … (neqc_to_neq T))
209 ##| napply (neq_to_neqcn … (neq_to_neqc T));
210 napply (decidable_c T)
212 ##| napply (decidable_cn … (decidable_c T))
214 ##| napply (symmetric_eqcn … (symmetric_eqc T))
218 nlemma cn_is_comparable_ext : comparable_ext → comparable_ext.
220 #ltc; #lec; #gtc; #gec; #andc; #orc; #xorc;
221 #getMSBc; #setMSBc; #clrMSBc; #getLSBc; #setLSBc; #clrLSBc;
222 #rcrc; #shrc; #rorc; #rclc; #shlc; #rolc; #notc;
223 #plusc_dc_dc; #plusc_d_dc; #plusc_dc_d; #plusc_d_d; #plusc_dc_c; #plusc_d_c;
224 #predc; #succc; #complc; #absc; #inrangec;
225 napply (mk_comparable_ext);
226 ##[ napply (cn_is_comparable c)
228 ##| napply (λx,y.(ltc (cnH ? x) (cnH ? y)) ⊕
229 (((eqc c) (cnH ? x) (cnH ? y)) ⊗ (ltc (cnL ? x) (cnL ? y))))
231 ##| napply (λx,y.(ltc (cnH ? x) (cnH ? y)) ⊕
232 (((eqc c) (cnH ? x) (cnH ? y)) ⊗ (lec (cnL ? x) (cnL ? y))))
234 ##| napply (λx,y.(gtc (cnH ? x) (cnH ? y)) ⊕
235 (((eqc c) (cnH ? x) (cnH ? y)) ⊗ (gtc (cnL ? x) (cnL ? y))))
237 ##| napply (λx,y.(gtc (cnH ? x) (cnH ? y)) ⊕
238 (((eqc c) (cnH ? x) (cnH ? y)) ⊗ (gec (cnL ? x) (cnL ? y))))
240 ##| napply (λx,y.mk_comp_num ? (andc (cnH ? x) (cnH ? y))
241 (andc (cnL ? x) (cnL ? y)))
243 ##| napply (λx,y.mk_comp_num ? (orc (cnH ? x) (cnH ? y))
244 (orc (cnL ? x) (cnL ? y)))
246 ##| napply (λx,y.mk_comp_num ? (xorc (cnH ? x) (cnH ? y))
247 (xorc (cnL ? x) (cnL ? y)))
249 ##| napply (λx.getMSBc (cnH ? x))
251 ##| napply (λx.mk_comp_num ? (setMSBc (cnH ? x)) (cnL ? x))
253 ##| napply (λx.mk_comp_num ? (clrMSBc (cnH ? x)) (cnL ? x))
255 ##| napply (λx.getLSBc (cnL ? x))
257 ##| napply (λx.mk_comp_num ? (cnH ? x) (setLSBc (cnL ? x)))
259 ##| napply (λx.mk_comp_num ? (cnH ? x) (clrLSBc (cnL ? x)))
261 ##| napply (λcy,x.match rcrc cy (cnH ? x) with
262 [ pair cy' cnh' ⇒ match rcrc cy' (cnL ? x) with
263 [ pair cy'' cnl' ⇒ pair … cy'' (mk_comp_num ? cnh' cnl')]])
265 ##| napply (λx.match shrc (cnH ? x) with
266 [ pair cy' cnh' ⇒ match rcrc cy' (cnL ? x) with
267 [ pair cy'' cnl' ⇒ pair … cy'' (mk_comp_num ? cnh' cnl')]])
269 ##| napply (λx.match shrc (cnH ? x) with
270 [ pair cy' cnh' ⇒ match rcrc cy' (cnL ? x) with
271 [ pair cy'' cnl' ⇒ mk_comp_num ?
272 (match cy'' with [ true ⇒ setMSBc
273 | false ⇒ λh.h ] cnh') cnl']])
275 ##| napply (λcy,x.match rclc cy (cnL ? x) with
276 [ pair cy' cnl' ⇒ match rclc cy' (cnH ? x) with
277 [ pair cy'' cnh' ⇒ pair … cy'' (mk_comp_num ? cnh' cnl')]])
279 ##| napply (λx.match shlc (cnL ? x) with
280 [ pair cy' cnl' ⇒ match rclc cy' (cnH ? x) with
281 [ pair cy'' cnh' ⇒ pair … cy'' (mk_comp_num ? cnh' cnl')]])
283 ##| napply (λx.match shlc (cnL ? x) with
284 [ pair cy' cnl' ⇒ match rclc cy' (cnH ? x) with
285 [ pair cy'' cnh' ⇒ mk_comp_num ?
286 cnh' (match cy'' with [ true ⇒ setLSBc
287 | false ⇒ λh.h ] cnl')]])
289 ##| napply (λx.mk_comp_num ? (notc (cnH ? x)) (notc (cnL ? x)))
291 ##| napply (λcy,x,y.match plusc_dc_dc cy (cnL ? x) (cnL ? y) with
292 [ pair cy' cnl' ⇒ match plusc_dc_dc cy' (cnH ? x) (cnH ? y) with
293 [ pair cy'' cnh' ⇒ pair … cy'' (mk_comp_num ? cnh' cnl')]])
295 ##| napply (λx,y.match plusc_d_dc (cnL ? x) (cnL ? y) with
296 [ pair cy' cnl' ⇒ match plusc_dc_dc cy' (cnH ? x) (cnH ? y) with
297 [ pair cy'' cnh' ⇒ pair … cy'' (mk_comp_num ? cnh' cnl')]])
299 ##| napply (λcy,x,y.match plusc_dc_dc cy (cnL ? x) (cnL ? y) with
300 [ pair cy' cnl' ⇒ mk_comp_num ? (plusc_dc_d cy' (cnH ? x) (cnH ? y)) cnl'])
302 ##| napply (λx,y.match plusc_d_dc (cnL ? x) (cnL ? y) with
303 [ pair cy' cnl' ⇒ mk_comp_num ? (plusc_dc_d cy' (cnH ? x) (cnH ? y)) cnl'])
305 ##| napply (λcy,x,y.plusc_dc_c (plusc_dc_c cy (cnL ? x) (cnL ? y))
308 ##| napply (λx,y.plusc_dc_c (plusc_d_c (cnL ? x) (cnL ? y))
311 ##| napply (λx.match (eqc c) (zeroc c) (cnL ? x) with
312 [ true ⇒ mk_comp_num ? (predc (cnH ? x)) (predc (cnL ? x))
313 | false ⇒ mk_comp_num ? (cnH ? x) (predc (cnL ? x)) ])
315 ##| napply (λx.match (eqc c) (predc (zeroc c)) (cnL ? x) with
316 [ true ⇒ mk_comp_num ? (succc (cnH ? x)) (succc (cnL ? x))
317 | false ⇒ mk_comp_num ? (cnH ? x) (succc (cnL ? x)) ])
319 ##| napply (λx.(match (eqc c) (zeroc c) (cnL ? x) with
320 [ true ⇒ mk_comp_num ? (complc (cnH ? x)) (complc (cnL ? x))
321 | false ⇒ mk_comp_num ? (notc (cnH ? x)) (complc (cnL ? x)) ]))
323 ##| napply (λx.match getMSBc (cnH ? x) with
324 [ true ⇒ match (eqc c) (zeroc c) (cnL ? x) with
325 [ true ⇒ mk_comp_num ? (complc (cnH ? x)) (complc (cnL ? x))
326 | false ⇒ mk_comp_num ? (notc (cnH ? x)) (complc (cnL ? x)) ]
329 ##| napply (λx,inf,sup.
330 match (ltc (cnH ? inf) (cnH ? sup)) ⊕
331 (((eqc c) (cnH ? inf) (cnH ? sup)) ⊗ (lec (cnL ? inf) (cnL ? sup))) with
332 [ true ⇒ and_bool | false ⇒ or_bool ]
333 ((ltc (cnH ? inf) (cnH ? x)) ⊕
334 (((eqc c) (cnH ? inf) (cnH ? x)) ⊗ (lec (cnL ? inf) (cnL ? x))))
335 ((ltc (cnH ? x) (cnH ? sup)) ⊕
336 (((eqc c) (cnH ? x) (cnH ? sup)) ⊗ (lec (cnL ? x) (cnL ? sup)))))
340 ndefinition zeroc ≝ λx:comparable_ext.zeroc (comp_base x).
341 ndefinition forallc ≝ λx:comparable_ext.forallc (comp_base x).
342 ndefinition eqc ≝ λx:comparable_ext.eqc (comp_base x).
343 ndefinition eqc_to_eq ≝ λx:comparable_ext.eqc_to_eq (comp_base x).
344 ndefinition eq_to_eqc ≝ λx:comparable_ext.eq_to_eqc (comp_base x).
345 ndefinition neqc_to_neq ≝ λx:comparable_ext.neqc_to_neq (comp_base x).
346 ndefinition neq_to_neqc ≝ λx:comparable_ext.neq_to_neqc (comp_base x).
347 ndefinition decidable_c ≝ λx:comparable_ext.decidable_c (comp_base x).
348 ndefinition symmetric_eqc ≝ λx:comparable_ext.symmetric_eqc (comp_base x).
351 unification hint 0 ≔ S: comparable;
353 X ≟ (cn_is_comparable S)
354 (*********************************************) ⊢