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 (* Ultima modifica: 05/08/2009 *)
21 (* ********************************************************************** *)
23 include "num/exadecim.ma".
24 include "num/bool_lemmas.ma".
30 ndefinition exadecim_destruct1 : Πe2.ΠP:Prop.ΠH:x0 = e2.match e2 with [ x0 ⇒ P → P | _ ⇒ P ].
31 #e2; #P; ncases e2; nnormalize; #H;
32 ##[ ##1: napply (λx:P.x)
33 ##| ##*: napply False_ind;
34 nchange with (match x0 with [ x0 ⇒ False | _ ⇒ True ]);
35 nrewrite > H; nnormalize; napply I
39 ndefinition exadecim_destruct2 : Πe2.ΠP:Prop.ΠH:x1 = e2.match e2 with [ x1 ⇒ P → P | _ ⇒ P ].
40 #e2; #P; ncases e2; nnormalize; #H;
41 ##[ ##2: napply (λx:P.x)
42 ##| ##*: napply False_ind;
43 nchange with (match x1 with [ x1 ⇒ False | _ ⇒ True ]);
44 nrewrite > H; nnormalize; napply I
48 ndefinition exadecim_destruct3 : Πe2.ΠP:Prop.ΠH:x2 = e2.match e2 with [ x2 ⇒ P → P | _ ⇒ P ].
49 #e2; #P; ncases e2; nnormalize; #H;
50 ##[ ##3: napply (λx:P.x)
51 ##| ##*: napply False_ind;
52 nchange with (match x2 with [ x2 ⇒ False | _ ⇒ True ]);
53 nrewrite > H; nnormalize; napply I
57 ndefinition exadecim_destruct4 : Πe2.ΠP:Prop.ΠH:x3 = e2.match e2 with [ x3 ⇒ P → P | _ ⇒ P ].
58 #e2; #P; ncases e2; nnormalize; #H;
59 ##[ ##4: napply (λx:P.x)
60 ##| ##*: napply False_ind;
61 nchange with (match x3 with [ x3 ⇒ False | _ ⇒ True ]);
62 nrewrite > H; nnormalize; napply I
66 ndefinition exadecim_destruct5 : Πe2.ΠP:Prop.ΠH:x4 = e2.match e2 with [ x4 ⇒ P → P | _ ⇒ P ].
67 #e2; #P; ncases e2; nnormalize; #H;
68 ##[ ##5: napply (λx:P.x)
69 ##| ##*: napply False_ind;
70 nchange with (match x4 with [ x4 ⇒ False | _ ⇒ True ]);
71 nrewrite > H; nnormalize; napply I
75 ndefinition exadecim_destruct6 : Πe2.ΠP:Prop.ΠH:x5 = e2.match e2 with [ x5 ⇒ P → P | _ ⇒ P ].
76 #e2; #P; ncases e2; nnormalize; #H;
77 ##[ ##6: napply (λx:P.x)
78 ##| ##*: napply False_ind;
79 nchange with (match x5 with [ x5 ⇒ False | _ ⇒ True ]);
80 nrewrite > H; nnormalize; napply I
84 ndefinition exadecim_destruct7 : Πe2.ΠP:Prop.ΠH:x6 = e2.match e2 with [ x6 ⇒ P → P | _ ⇒ P ].
85 #e2; #P; ncases e2; nnormalize; #H;
86 ##[ ##7: napply (λx:P.x)
87 ##| ##*: napply False_ind;
88 nchange with (match x6 with [ x6 ⇒ False | _ ⇒ True ]);
89 nrewrite > H; nnormalize; napply I
93 ndefinition exadecim_destruct8 : Πe2.ΠP:Prop.ΠH:x7 = e2.match e2 with [ x7 ⇒ P → P | _ ⇒ P ].
94 #e2; #P; ncases e2; nnormalize; #H;
95 ##[ ##8: napply (λx:P.x)
96 ##| ##*: napply False_ind;
97 nchange with (match x7 with [ x7 ⇒ False | _ ⇒ True ]);
98 nrewrite > H; nnormalize; napply I
102 ndefinition exadecim_destruct9 : Πe2.ΠP:Prop.ΠH:x8 = e2.match e2 with [ x8 ⇒ P → P | _ ⇒ P ].
103 #e2; #P; ncases e2; nnormalize; #H;
104 ##[ ##9: napply (λx:P.x)
105 ##| ##*: napply False_ind;
106 nchange with (match x8 with [ x8 ⇒ False | _ ⇒ True ]);
107 nrewrite > H; nnormalize; napply I
111 ndefinition exadecim_destruct10 : Πe2.ΠP:Prop.ΠH:x9 = e2.match e2 with [ x9 ⇒ P → P | _ ⇒ P ].
112 #e2; #P; ncases e2; nnormalize; #H;
113 ##[ ##10: napply (λx:P.x)
114 ##| ##*: napply False_ind;
115 nchange with (match x9 with [ x9 ⇒ False | _ ⇒ True ]);
116 nrewrite > H; nnormalize; napply I
120 ndefinition exadecim_destruct11 : Πe2.ΠP:Prop.ΠH:xA = e2.match e2 with [ xA ⇒ P → P | _ ⇒ P ].
121 #e2; #P; ncases e2; nnormalize; #H;
122 ##[ ##11: napply (λx:P.x)
123 ##| ##*: napply False_ind;
124 nchange with (match xA with [ xA ⇒ False | _ ⇒ True ]);
125 nrewrite > H; nnormalize; napply I
129 ndefinition exadecim_destruct12 : Πe2.ΠP:Prop.ΠH:xB = e2.match e2 with [ xB ⇒ P → P | _ ⇒ P ].
130 #e2; #P; ncases e2; nnormalize; #H;
131 ##[ ##12: napply (λx:P.x)
132 ##| ##*: napply False_ind;
133 nchange with (match xB with [ xB ⇒ False | _ ⇒ True ]);
134 nrewrite > H; nnormalize; napply I
138 ndefinition exadecim_destruct13 : Πe2.ΠP:Prop.ΠH:xC = e2.match e2 with [ xC ⇒ P → P | _ ⇒ P ].
139 #e2; #P; ncases e2; nnormalize; #H;
140 ##[ ##13: napply (λx:P.x)
141 ##| ##*: napply False_ind;
142 nchange with (match xC with [ xC ⇒ False | _ ⇒ True ]);
143 nrewrite > H; nnormalize; napply I
147 ndefinition exadecim_destruct14 : Πe2.ΠP:Prop.ΠH:xD = e2.match e2 with [ xD ⇒ P → P | _ ⇒ P ].
148 #e2; #P; ncases e2; nnormalize; #H;
149 ##[ ##14: napply (λx:P.x)
150 ##| ##*: napply False_ind;
151 nchange with (match xD with [ xD ⇒ False | _ ⇒ True ]);
152 nrewrite > H; nnormalize; napply I
156 ndefinition exadecim_destruct15 : Πe2.ΠP:Prop.ΠH:xE = e2.match e2 with [ xE ⇒ P → P | _ ⇒ P ].
157 #e2; #P; ncases e2; nnormalize; #H;
158 ##[ ##15: napply (λx:P.x)
159 ##| ##*: napply False_ind;
160 nchange with (match xE with [ xE ⇒ False | _ ⇒ True ]);
161 nrewrite > H; nnormalize; napply I
165 ndefinition exadecim_destruct16 : Πe2.ΠP:Prop.ΠH:xF = e2.match e2 with [ xF ⇒ P → P | _ ⇒ P ].
166 #e2; #P; ncases e2; nnormalize; #H;
167 ##[ ##16: napply (λx:P.x)
168 ##| ##*: napply False_ind;
169 nchange with (match xF with [ xF ⇒ False | _ ⇒ True ]);
170 nrewrite > H; nnormalize; napply I
174 ndefinition exadecim_destruct_aux ≝
175 Πe1,e2.ΠP:Prop.ΠH:e1 = e2.
177 [ x0 ⇒ match e2 with [ x0 ⇒ P → P | _ ⇒ P ]
178 | x1 ⇒ match e2 with [ x1 ⇒ P → P | _ ⇒ P ]
179 | x2 ⇒ match e2 with [ x2 ⇒ P → P | _ ⇒ P ]
180 | x3 ⇒ match e2 with [ x3 ⇒ P → P | _ ⇒ P ]
181 | x4 ⇒ match e2 with [ x4 ⇒ P → P | _ ⇒ P ]
182 | x5 ⇒ match e2 with [ x5 ⇒ P → P | _ ⇒ P ]
183 | x6 ⇒ match e2 with [ x6 ⇒ P → P | _ ⇒ P ]
184 | x7 ⇒ match e2 with [ x7 ⇒ P → P | _ ⇒ P ]
185 | x8 ⇒ match e2 with [ x8 ⇒ P → P | _ ⇒ P ]
186 | x9 ⇒ match e2 with [ x9 ⇒ P → P | _ ⇒ P ]
187 | xA ⇒ match e2 with [ xA ⇒ P → P | _ ⇒ P ]
188 | xB ⇒ match e2 with [ xB ⇒ P → P | _ ⇒ P ]
189 | xC ⇒ match e2 with [ xC ⇒ P → P | _ ⇒ P ]
190 | xD ⇒ match e2 with [ xD ⇒ P → P | _ ⇒ P ]
191 | xE ⇒ match e2 with [ xE ⇒ P → P | _ ⇒ P ]
192 | xF ⇒ match e2 with [ xF ⇒ P → P | _ ⇒ P ]
195 ndefinition exadecim_destruct : exadecim_destruct_aux.
197 ##[ ##1: napply exadecim_destruct1
198 ##| ##2: napply exadecim_destruct2
199 ##| ##3: napply exadecim_destruct3
200 ##| ##4: napply exadecim_destruct4
201 ##| ##5: napply exadecim_destruct5
202 ##| ##6: napply exadecim_destruct6
203 ##| ##7: napply exadecim_destruct7
204 ##| ##8: napply exadecim_destruct8
205 ##| ##9: napply exadecim_destruct9
206 ##| ##10: napply exadecim_destruct10
207 ##| ##11: napply exadecim_destruct11
208 ##| ##12: napply exadecim_destruct12
209 ##| ##13: napply exadecim_destruct13
210 ##| ##14: napply exadecim_destruct14
211 ##| ##15: napply exadecim_destruct15
212 ##| ##16: napply exadecim_destruct16
216 nlemma symmetric_eqex : symmetricT exadecim bool eq_ex.
224 nlemma symmetric_andex : symmetricT exadecim exadecim and_ex.
232 nlemma associative_andex : ∀e1,e2,e3.(and_ex (and_ex e1 e2) e3) = (and_ex e1 (and_ex e2 e3)).
235 ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
236 ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
237 ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
238 ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
239 ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
240 ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
241 ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
242 ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
243 ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
244 ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
245 ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
246 ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
247 ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
248 ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
249 ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
250 ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
254 nlemma symmetric_orex : symmetricT exadecim exadecim or_ex.
262 nlemma associative_orex : ∀e1,e2,e3.(or_ex (or_ex e1 e2) e3) = (or_ex e1 (or_ex e2 e3)).
265 ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
266 ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
267 ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
268 ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
269 ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
270 ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
271 ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
272 ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
273 ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
274 ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
275 ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
276 ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
277 ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
278 ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
279 ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
280 ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
284 nlemma symmetric_xorex : symmetricT exadecim exadecim xor_ex.
292 nlemma associative_xorex : ∀e1,e2,e3.(xor_ex (xor_ex e1 e2) e3) = (xor_ex e1 (xor_ex e2 e3)).
295 ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
296 ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
297 ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
298 ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
299 ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
300 ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
301 ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
302 ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
303 ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
304 ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
305 ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
306 ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
307 ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
308 ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
309 ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
310 ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
314 nlemma symmetric_plusex_dc_dc : ∀e1,e2,c.plus_ex_dc_dc e1 e2 c = plus_ex_dc_dc e2 e1 c.
323 nlemma plusex_dc_dc_to_dc_d : ∀e1,e2,c.fst … (plus_ex_dc_dc e1 e2 c) = plus_ex_dc_d e1 e2 c.
332 nlemma plusex_dc_dc_to_dc_c : ∀e1,e2,c.snd … (plus_ex_dc_dc e1 e2 c) = plus_ex_dc_c e1 e2 c.
341 nlemma plusex_dc_dc_to_d_dc : ∀e1,e2.plus_ex_dc_dc e1 e2 false = plus_ex_d_dc e1 e2.
349 nlemma plusex_dc_dc_to_d_d : ∀e1,e2.fst … (plus_ex_dc_dc e1 e2 false) = plus_ex_d_d e1 e2.
357 nlemma plusex_dc_dc_to_d_c : ∀e1,e2.snd … (plus_ex_dc_dc e1 e2 false) = plus_ex_d_c e1 e2.
365 nlemma symmetric_plusex_dc_d : ∀e1,e2,c.plus_ex_dc_d e1 e2 c = plus_ex_dc_d e2 e1 c.
374 nlemma symmetric_plusex_dc_c : ∀e1,e2,c.plus_ex_dc_c e1 e2 c = plus_ex_dc_c e2 e1 c.
383 nlemma symmetric_plusex_d_dc : ∀e1,e2.plus_ex_d_dc e1 e2 = plus_ex_d_dc e2 e1.
391 nlemma plusex_d_dc_to_d_d : ∀e1,e2.fst … (plus_ex_d_dc e1 e2) = plus_ex_d_d e1 e2.
399 nlemma plusex_d_dc_to_d_c : ∀e1,e2.snd … (plus_ex_d_dc e1 e2) = plus_ex_d_c e1 e2.
407 nlemma symmetric_plusex_d_d : ∀e1,e2.plus_ex_d_d e1 e2 = plus_ex_d_d e2 e1.
415 nlemma associative_plusex_d_d : ∀e1,e2,e3.(plus_ex_d_d (plus_ex_d_d e1 e2) e3) = (plus_ex_d_d e1 (plus_ex_d_d e2 e3)).
418 ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
419 ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
420 ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
421 ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
422 ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
423 ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
424 ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
425 ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
426 ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
427 ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
428 ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
429 ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
430 ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
431 ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
432 ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
433 ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
437 nlemma symmetric_plusex_d_c : ∀e1,e2.plus_ex_d_c e1 e2 = plus_ex_d_c e2 e1.
445 nlemma eqex_to_eq : ∀e1,e2:exadecim.(eq_ex e1 e2 = true) → (e1 = e2).
450 ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply refl_eq
451 ##| ##*: #H; napply (bool_destruct … H)
455 nlemma eq_to_eqex : ∀e1,e2.e1 = e2 → eq_ex e1 e2 = true.
460 ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply refl_eq
461 ##| ##*: #H; napply (exadecim_destruct … H)
465 nlemma decidable_ex : ∀x,y:exadecim.decidable (x = y).
470 ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
471 ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (exadecim_destruct … H)
475 nlemma neqex_to_neq : ∀e1,e2:exadecim.(eq_ex e1 e2 = false) → (e1 ≠ e2).
480 ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (bool_destruct … H)
481 ##| ##*: #H; #H1; napply (exadecim_destruct … H1)
485 nlemma neq_to_neqex : ∀e1,e2.e1 ≠ e2 → eq_ex e1 e2 = false.
490 ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; nelim (H (refl_eq …))
491 ##| ##*: #H; napply refl_eq