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/word32.ma".
24 include "num/word16_lemmas.ma".
30 nlemma word32_destruct_1 :
32 mk_word32 x1 y1 = mk_word32 x2 y2 → x1 = x2.
33 #x1; #x2; #y1; #y2; #H;
34 nchange with (match mk_word32 x2 y2 with [ mk_word32 a _ ⇒ x1 = a ]);
40 nlemma word32_destruct_2 :
42 mk_word32 x1 y1 = mk_word32 x2 y2 → y1 = y2.
43 #x1; #x2; #y1; #y2; #H;
44 nchange with (match mk_word32 x2 y2 with [ mk_word32 _ b ⇒ y1 = b ]);
50 nlemma symmetric_eqw32 : symmetricT word32 bool eq_w32.
55 nchange with (((eq_w16 w3 w1)⊗(eq_w16 w4 w2)) = ((eq_w16 w1 w3)⊗(eq_w16 w2 w4)));
56 nrewrite > (symmetric_eqw16 w1 w3);
57 nrewrite > (symmetric_eqw16 w2 w4);
61 nlemma symmetric_andw32 : symmetricT word32 word32 and_w32.
66 nchange with ((mk_word32 (and_w16 w3 w1) (and_w16 w4 w2)) = (mk_word32 (and_w16 w1 w3) (and_w16 w2 w4)));
67 nrewrite > (symmetric_andw16 w1 w3);
68 nrewrite > (symmetric_andw16 w2 w4);
72 nlemma associative_andw32 : ∀dw1,dw2,dw3.(and_w32 (and_w32 dw1 dw2) dw3) = (and_w32 dw1 (and_w32 dw2 dw3)).
80 nchange with (mk_word32 (and_w16 (and_w16 w1 w3) w5) (and_w16 (and_w16 w2 w4) w6) =
81 mk_word32 (and_w16 w1 (and_w16 w3 w5)) (and_w16 w2 (and_w16 w4 w6)));
82 nrewrite < (associative_andw16 w1 w3 w5);
83 nrewrite < (associative_andw16 w2 w4 w6);
87 nlemma symmetric_orw32 : symmetricT word32 word32 or_w32.
92 nchange with ((mk_word32 (or_w16 w3 w1) (or_w16 w4 w2)) = (mk_word32 (or_w16 w1 w3) (or_w16 w2 w4)));
93 nrewrite > (symmetric_orw16 w1 w3);
94 nrewrite > (symmetric_orw16 w2 w4);
98 nlemma associative_orw32 : ∀dw1,dw2,dw3.(or_w32 (or_w32 dw1 dw2) dw3) = (or_w32 dw1 (or_w32 dw2 dw3)).
106 nchange with (mk_word32 (or_w16 (or_w16 w1 w3) w5) (or_w16 (or_w16 w2 w4) w6) =
107 mk_word32 (or_w16 w1 (or_w16 w3 w5)) (or_w16 w2 (or_w16 w4 w6)));
108 nrewrite < (associative_orw16 w1 w3 w5);
109 nrewrite < (associative_orw16 w2 w4 w6);
113 nlemma symmetric_xorw32 : symmetricT word32 word32 xor_w32.
118 nchange with ((mk_word32 (xor_w16 w3 w1) (xor_w16 w4 w2)) = (mk_word32 (xor_w16 w1 w3) (xor_w16 w2 w4)));
119 nrewrite > (symmetric_xorw16 w1 w3);
120 nrewrite > (symmetric_xorw16 w2 w4);
124 nlemma associative_xorw32 : ∀dw1,dw2,dw3.(xor_w32 (xor_w32 dw1 dw2) dw3) = (xor_w32 dw1 (xor_w32 dw2 dw3)).
132 nchange with (mk_word32 (xor_w16 (xor_w16 w1 w3) w5) (xor_w16 (xor_w16 w2 w4) w6) =
133 mk_word32 (xor_w16 w1 (xor_w16 w3 w5)) (xor_w16 w2 (xor_w16 w4 w6)));
134 nrewrite < (associative_xorw16 w1 w3 w5);
135 nrewrite < (associative_xorw16 w2 w4 w6);
139 nlemma symmetric_plusw32_dc_dc : ∀dw1,dw2,c.plus_w32_dc_dc dw1 dw2 c = plus_w32_dc_dc dw2 dw1 c.
146 match plus_w16_dc_dc w2 w4 c with [ pair l c ⇒ match plus_w16_dc_dc w1 w3 c with [ pair h c' ⇒ pair … 〈h.l〉 c' ]] =
147 match plus_w16_dc_dc w4 w2 c with [ pair l c ⇒ match plus_w16_dc_dc w3 w1 c with [ pair h c' ⇒ pair … 〈h.l〉 c' ]]);
148 nrewrite > (symmetric_plusw16_dc_dc w4 w2 c);
149 ncases (plus_w16_dc_dc w2 w4 c);
152 match plus_w16_dc_dc w1 w3 c1 with [ pair h c' ⇒ pair … 〈h.w5〉 c' ] =
153 match plus_w16_dc_dc w3 w1 c1 with [ pair h c' ⇒ pair … 〈h.w5〉 c' ]);
154 nrewrite > (symmetric_plusw16_dc_dc w1 w3 c1);
158 nlemma symmetric_plusw32_dc_d : ∀dw1,dw2,c.plus_w32_dc_d dw1 dw2 c = plus_w32_dc_d dw2 dw1 c.
165 match plus_w16_dc_dc w2 w4 c with [ pair l c ⇒ 〈plus_w16_dc_d w1 w3 c.l〉 ] =
166 match plus_w16_dc_dc w4 w2 c with [ pair l c ⇒ 〈plus_w16_dc_d w3 w1 c.l〉 ]);
167 nrewrite > (symmetric_plusw16_dc_dc w4 w2 c);
168 ncases (plus_w16_dc_dc w2 w4 c);
170 nchange with (〈plus_w16_dc_d w1 w3 c1.w5〉 = 〈plus_w16_dc_d w3 w1 c1.w5〉);
171 nrewrite > (symmetric_plusw16_dc_d w1 w3 c1);
175 nlemma symmetric_plusw32_dc_c : ∀dw1,dw2,c.plus_w32_dc_c dw1 dw2 c = plus_w32_dc_c dw2 dw1 c.
182 plus_w16_dc_c w1 w3 (plus_w16_dc_c w2 w4 c) =
183 plus_w16_dc_c w3 w1 (plus_w16_dc_c w4 w2 c));
184 nrewrite > (symmetric_plusw16_dc_c w4 w2 c);
185 nrewrite > (symmetric_plusw16_dc_c w3 w1 (plus_w16_dc_c w2 w4 c));
189 nlemma symmetric_plusw32_d_dc : ∀dw1,dw2.plus_w32_d_dc dw1 dw2 = plus_w32_d_dc dw2 dw1.
196 match plus_w16_d_dc w2 w4 with [ pair l c ⇒ match plus_w16_dc_dc w1 w3 c with [ pair h c' ⇒ pair … 〈h.l〉 c' ]] =
197 match plus_w16_d_dc w4 w2 with [ pair l c ⇒ match plus_w16_dc_dc w3 w1 c with [ pair h c' ⇒ pair … 〈h.l〉 c' ]]);
198 nrewrite > (symmetric_plusw16_d_dc w4 w2);
199 ncases (plus_w16_d_dc w2 w4);
202 match plus_w16_dc_dc w1 w3 c with [ pair h c' ⇒ pair … 〈h.w5〉 c' ] =
203 match plus_w16_dc_dc w3 w1 c with [ pair h c' ⇒ pair … 〈h.w5〉 c' ]);
204 nrewrite > (symmetric_plusw16_dc_dc w1 w3 c);
208 nlemma symmetric_plusw32_d_d : ∀dw1,dw2.plus_w32_d_d dw1 dw2 = plus_w32_d_d dw2 dw1.
215 match plus_w16_d_dc w2 w4 with [ pair l c ⇒ 〈plus_w16_dc_d w1 w3 c.l〉 ] =
216 match plus_w16_d_dc w4 w2 with [ pair l c ⇒ 〈plus_w16_dc_d w3 w1 c.l〉 ]);
217 nrewrite > (symmetric_plusw16_d_dc w4 w2);
218 ncases (plus_w16_d_dc w2 w4);
220 nchange with (〈plus_w16_dc_d w1 w3 c.w5〉 = 〈plus_w16_dc_d w3 w1 c.w5〉);
221 nrewrite > (symmetric_plusw16_dc_d w1 w3 c);
225 nlemma symmetric_plusw32_d_c : ∀dw1,dw2.plus_w32_d_c dw1 dw2 = plus_w32_d_c dw2 dw1.
232 plus_w16_dc_c w1 w3 (plus_w16_d_c w2 w4) =
233 plus_w16_dc_c w3 w1 (plus_w16_d_c w4 w2));
234 nrewrite > (symmetric_plusw16_d_c w4 w2);
235 nrewrite > (symmetric_plusw16_dc_c w3 w1 (plus_w16_d_c w2 w4));
239 nlemma symmetric_mulw16 : symmetricT word16 word32 mul_w16.
245 nchange with (match mul_b8 b2 b4 with
246 [ mk_word16 t1_h t1_l ⇒ match mul_b8 b1 b4 with
247 [ mk_word16 t2_h t2_l ⇒ match mul_b8 b3 b2 with
248 [ mk_word16 t3_h t3_l ⇒ match mul_b8 b1 b3 with
249 [ mk_word16 t4_h t4_l ⇒ plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:t3_h〉.〈t3_l:〈x0,x0〉〉〉 〈〈〈x0,x0〉:t2_h〉.〈t2_l:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈t1_h:t1_l〉〉
250 ]]]] = match mul_b8 b4 b2 with
251 [ mk_word16 t1_h t1_l ⇒ match mul_b8 b3 b2 with
252 [ mk_word16 t2_h t2_l ⇒ match mul_b8 b1 b4 with
253 [ mk_word16 t3_h t3_l ⇒ match mul_b8 b3 b1 with
254 [ mk_word16 t4_h t4_l ⇒ plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:t3_h〉.〈t3_l:〈x0,x0〉〉〉 〈〈〈x0,x0〉:t2_h〉.〈t2_l:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈t1_h:t1_l〉〉
256 nrewrite < (symmetric_mulb8 b2 b4);
257 ncases (mul_b8 b2 b4);
259 nchange with (match mul_b8 b1 b4 with
260 [ mk_word16 t2_h t2_l ⇒ match mul_b8 b3 b2 with
261 [ mk_word16 t3_h t3_l ⇒ match mul_b8 b1 b3 with
262 [ mk_word16 t4_h t4_l ⇒ plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:t3_h〉.〈t3_l:〈x0,x0〉〉〉 〈〈〈x0,x0〉:t2_h〉.〈t2_l:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈b5:b6〉〉
263 ]]] = match mul_b8 b3 b2 with
264 [ mk_word16 t2_h t2_l ⇒ match mul_b8 b1 b4 with
265 [ mk_word16 t3_h t3_l ⇒ match mul_b8 b3 b1 with
266 [ mk_word16 t4_h t4_l ⇒ plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:t3_h〉.〈t3_l:〈x0,x0〉〉〉 〈〈〈x0,x0〉:t2_h〉.〈t2_l:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈b5:b6〉〉
268 ncases (mul_b8 b3 b2);
270 ncases (mul_b8 b1 b4);
272 nchange with (match mul_b8 b1 b3 with
273 [ mk_word16 t4_h t4_l ⇒ plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:b7〉.〈b8:〈x0,x0〉〉〉 〈〈〈x0,x0〉:b9〉.〈b10:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈b5:b6〉〉
274 ] = match mul_b8 b3 b1 with
275 [ mk_word16 t4_h t4_l ⇒ plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:b9〉.〈b10:〈x0,x0〉〉〉 〈〈〈x0,x0〉:b7〉.〈b8:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈b5:b6〉〉
277 nrewrite < (symmetric_mulb8 b1 b3);
278 ncases (mul_b8 b1 b3);
280 nchange with ((plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:b7〉.〈b8:〈x0,x0〉〉〉 〈〈〈x0,x0〉:b9〉.〈b10:〈x0,x0〉〉〉) 〈〈b11:b12〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈b5:b6〉〉) =
281 (plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:b9〉.〈b10:〈x0,x0〉〉〉 〈〈〈x0,x0〉:b7〉.〈b8:〈x0,x0〉〉〉) 〈〈b11:b12〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈b5:b6〉〉));
282 nrewrite > (symmetric_plusw32_d_d 〈〈〈x0,x0〉:b7〉.〈b8:〈x0,x0〉〉〉 〈〈〈x0,x0〉:b9〉.〈b10:〈x0,x0〉〉〉);
286 nlemma eqw32_to_eq : ∀dw1,dw2:word32.(eq_w32 dw1 dw2 = true) → (dw1 = dw2).
291 nchange in ⊢ (% → ?) with (((eq_w16 w3 w1)⊗(eq_w16 w4 w2)) = true);
293 nrewrite < (eqw16_to_eq … (andb_true_true_l … H));
294 nrewrite < (eqw16_to_eq … (andb_true_true_r … H));
298 nlemma eq_to_eqw32 : ∀dw1,dw2.dw1 = dw2 → eq_w32 dw1 dw2 = true.
304 nrewrite < (word32_destruct_1 … H);
305 nrewrite < (word32_destruct_2 … H);
306 nchange with (((eq_w16 w3 w3)⊗(eq_w16 w4 w4)) = true);
307 nrewrite > (eq_to_eqw16 w3 w3 (refl_eq …));
308 nrewrite > (eq_to_eqw16 w4 w4 (refl_eq …));
313 nlemma decidable_w32_aux1 : ∀w1,w2,w3,w4.w1 ≠ w3 → 〈w1.w2〉 ≠ 〈w3.w4〉.
316 napply (H (word32_destruct_1 … H1)).
319 nlemma decidable_w32_aux2 : ∀w1,w2,w3,w4.w2 ≠ w4 → 〈w1.w2〉 ≠ 〈w3.w4〉.
322 napply (H (word32_destruct_2 … H1)).
325 nlemma decidable_w32 : ∀x,y:word32.decidable (x = y).
326 #x; nelim x; #w1; #w2;
327 #y; nelim y; #w3; #w4;
329 napply (or2_elim (w1 = w3) (w1 ≠ w3) ? (decidable_w16 w1 w3) …);
330 ##[ ##2: #H; napply (or2_intro2 … (decidable_w32_aux1 w1 w2 w3 w4 H))
331 ##| ##1: #H; napply (or2_elim (w2 = w4) (w2 ≠ w4) ? (decidable_w16 w2 w4) …);
332 ##[ ##2: #H1; napply (or2_intro2 … (decidable_w32_aux2 w1 w2 w3 w4 H1))
333 ##| ##1: #H1; nrewrite > H; nrewrite > H1;
334 napply (or2_intro1 … (refl_eq ? 〈w3.w4〉))
339 nlemma neqw32_to_neq : ∀dw1,dw2:word32.(eq_w32 dw1 dw2 = false) → (dw1 ≠ dw2).
344 nchange with ((((eq_w16 w3 w1) ⊗ (eq_w16 w4 w2)) = false) → ?);
346 napply (or2_elim ((eq_w16 w3 w1) = false) ((eq_w16 w4 w2) = false) ? (andb_false2 … H) …);
347 ##[ ##1: #H1; napply (decidable_w32_aux1 … (neqw16_to_neq … H1))
348 ##| ##2: #H1; napply (decidable_w32_aux2 … (neqw16_to_neq … H1))
352 nlemma word32_destruct : ∀w1,w2,w3,w4.〈w1.w2〉 ≠ 〈w3.w4〉 → w1 ≠ w3 ∨ w2 ≠ w4.
355 napply (or2_elim (w1 = w3) (w1 ≠ w3) ? (decidable_w16 w1 w3) …);
356 ##[ ##2: #H1; napply (or2_intro1 … H1)
357 ##| ##1: #H1; napply (or2_elim (w2 = w4) (w2 ≠ w4) ? (decidable_w16 w2 w4) …);
358 ##[ ##2: #H2; napply (or2_intro2 … H2)
359 ##| ##1: #H2; nrewrite > H1 in H:(%);
361 #H; nelim (H (refl_eq …))
366 nlemma neq_to_neqw32 : ∀dw1,dw2.dw1 ≠ dw2 → eq_w32 dw1 dw2 = false.
370 #H; nchange with (((eq_w16 w1 w3) ⊗ (eq_w16 w2 w4)) = false);
371 napply (or2_elim (w1 ≠ w3) (w2 ≠ w4) ? (word32_destruct … H) …);
372 ##[ ##1: #H1; nrewrite > (neq_to_neqw16 … H1); nnormalize; napply refl_eq
373 ##| ##2: #H1; nrewrite > (neq_to_neqw16 … H1);
374 nrewrite > (symmetric_andbool (eq_w16 w1 w3) false);
375 nnormalize; napply refl_eq