X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fnum%2Fword16_lemmas.ma;h=56a54ae999455fc1e429df0d168d354aaf1e704e;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=9209c31e2c0875667f3985ec98c20592278eadb7;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma
index 9209c31e2..56a54ae99 100755
--- a/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Sviluppo: 2008-2010                                                  *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -27,15 +27,351 @@ include "num/byte8_lemmas.ma".
 (* WORD *)
 (* **** *)
 
-ndefinition word16_destruct_1 ≝ cn_destruct_1 word16.
-ndefinition word16_destruct_2 ≝ cn_destruct_2 word16.
+nlemma word16_destruct_1 :
+∀x1,x2,y1,y2.
+ mk_word16 x1 y1 = mk_word16 x2 y2 → x1 = x2.
+ #x1; #x2; #y1; #y2; #H;
+ nchange with (match mk_word16 x2 y2 with [ mk_word16 a _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
 
-ndefinition symmetric_eqw16 ≝ symmetric_eqcn ? eq_b8 symmetric_eqb8.
+nlemma word16_destruct_2 :
+∀x1,x2,y1,y2.
+ mk_word16 x1 y1 = mk_word16 x2 y2 → y1 = y2.
+ #x1; #x2; #y1; #y2; #H;
+ nchange with (match mk_word16 x2 y2 with [ mk_word16 _ b ⇒ y1 = b ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
 
-ndefinition eqw16_to_eq ≝ eqcn_to_eq ? eq_b8 eqb8_to_eq.
-ndefinition eq_to_eqw16 ≝ eq_to_eqcn ? eq_b8 eq_to_eqb8.
+nlemma symmetric_eqw16 : symmetricT word16 bool eq_w16.
+ #w1; #w2;
+ nelim w1;
+ nelim w2;
+ #b1; #b2; #b3; #b4;
+ nchange with (((eq_b8 b3 b1)⊗(eq_b8 b4 b2)) = ((eq_b8 b1 b3)⊗(eq_b8 b2 b4)));
+ nrewrite > (symmetric_eqb8 b1 b3);
+ nrewrite > (symmetric_eqb8 b2 b4);
+ napply refl_eq.
+nqed.
 
-ndefinition decidable_w16 ≝ decidable_cn ? decidable_b8.
+nlemma symmetric_andw16 : symmetricT word16 word16 and_w16.
+ #w1; #w2;
+ nelim w1;
+ nelim w2;
+ #b1; #b2; #b3; #b4;
+ nchange with ((mk_word16 (and_b8 b3 b1) (and_b8 b4 b2)) = (mk_word16 (and_b8 b1 b3) (and_b8 b2 b4)));
+ nrewrite > (symmetric_andb8 b1 b3);
+ nrewrite > (symmetric_andb8 b2 b4);
+ napply refl_eq.
+nqed.
 
-ndefinition neqw16_to_neq ≝ neqcn_to_neq ? eq_b8 neqb8_to_neq.
-ndefinition neq_to_neqw16 ≝ neq_to_neqcn ? eq_b8 neq_to_neqb8 decidable_b8.
+nlemma associative_andw16 : ∀w1,w2,w3.(and_w16 (and_w16 w1 w2) w3) = (and_w16 w1 (and_w16 w2 w3)).
+ #w1; #w2; #w3;
+ nelim w1;
+ #b1; #b2;
+ nelim w2;
+ #b3; #b4;
+ nelim w3;
+ #b5; #b6;
+ nchange with (mk_word16 (and_b8 (and_b8 b1 b3) b5) (and_b8 (and_b8 b2 b4) b6) =
+  mk_word16 (and_b8 b1 (and_b8 b3 b5)) (and_b8 b2 (and_b8 b4 b6)));
+ nrewrite < (associative_andb8 b1 b3 b5);
+ nrewrite < (associative_andb8 b2 b4 b6);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_orw16 : symmetricT word16 word16 or_w16.
+ #w1; #w2;
+ nelim w1;
+ nelim w2;
+ #b1; #b2; #b3; #b4;
+ nchange with ((mk_word16 (or_b8 b3 b1) (or_b8 b4 b2)) = (mk_word16 (or_b8 b1 b3) (or_b8 b2 b4)));
+ nrewrite > (symmetric_orb8 b1 b3);
+ nrewrite > (symmetric_orb8 b2 b4);
+ napply refl_eq.
+nqed.
+
+nlemma associative_orw16 : ∀w1,w2,w3.(or_w16 (or_w16 w1 w2) w3) = (or_w16 w1 (or_w16 w2 w3)).
+ #w1; #w2; #w3;
+ nelim w1;
+ #b1; #b2;
+ nelim w2;
+ #b3; #b4;
+ nelim w3;
+ #b5; #b6;
+ nchange with (mk_word16 (or_b8 (or_b8 b1 b3) b5) (or_b8 (or_b8 b2 b4) b6) =
+  mk_word16 (or_b8 b1 (or_b8 b3 b5)) (or_b8 b2 (or_b8 b4 b6)));
+ nrewrite < (associative_orb8 b1 b3 b5);
+ nrewrite < (associative_orb8 b2 b4 b6);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_xorw16 : symmetricT word16 word16 xor_w16.
+ #w1; #w2;
+ nelim w1;
+ nelim w2;
+ #b1; #b2; #b3; #b4;
+ nchange with ((mk_word16 (xor_b8 b3 b1) (xor_b8 b4 b2)) = (mk_word16 (xor_b8 b1 b3) (xor_b8 b2 b4)));
+ nrewrite > (symmetric_xorb8 b1 b3);
+ nrewrite > (symmetric_xorb8 b2 b4);
+ napply refl_eq.
+nqed.
+
+nlemma associative_xorw16 : ∀w1,w2,w3.(xor_w16 (xor_w16 w1 w2) w3) = (xor_w16 w1 (xor_w16 w2 w3)).
+ #w1; #w2; #w3;
+ nelim w1;
+ #b1; #b2;
+ nelim w2;
+ #b3; #b4;
+ nelim w3;
+ #b5; #b6;
+ nchange with (mk_word16 (xor_b8 (xor_b8 b1 b3) b5) (xor_b8 (xor_b8 b2 b4) b6) =
+  mk_word16 (xor_b8 b1 (xor_b8 b3 b5)) (xor_b8 b2 (xor_b8 b4 b6)));
+ nrewrite < (associative_xorb8 b1 b3 b5);
+ nrewrite < (associative_xorb8 b2 b4 b6);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusw16_dc_dc : ∀w1,w2,c.plus_w16_dc_dc w1 w2 c = plus_w16_dc_dc w2 w1 c.
+ #w1; #w2; #c;
+ nelim w1;
+ #b1; #b2;
+ nelim w2;
+ #b3; #b4;
+ nchange with (
+  match plus_b8_dc_dc b2 b4 c with [ pair l c ⇒ match plus_b8_dc_dc b1 b3 c with [ pair h c' ⇒ pair … 〈h:l〉 c' ]] =
+  match plus_b8_dc_dc b4 b2 c with [ pair l c ⇒ match plus_b8_dc_dc b3 b1 c with [ pair h c' ⇒ pair … 〈h:l〉 c' ]]);
+ nrewrite > (symmetric_plusb8_dc_dc b4 b2 c);
+ ncases (plus_b8_dc_dc b2 b4 c);
+ #b5; #c1;
+ nchange with (
+  match plus_b8_dc_dc b1 b3 c1 with [ pair h c' ⇒ pair … 〈h:b5〉 c' ] =
+  match plus_b8_dc_dc b3 b1 c1 with [ pair h c' ⇒ pair … 〈h:b5〉 c' ]);
+ nrewrite > (symmetric_plusb8_dc_dc b1 b3 c1);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusw16_dc_d : ∀w1,w2,c.plus_w16_dc_d w1 w2 c = plus_w16_dc_d w2 w1 c.
+ #w1; #w2; #c;
+ nelim w1;
+ #b1; #b2;
+ nelim w2;
+ #b3; #b4;
+ nchange with (
+  match plus_b8_dc_dc b2 b4 c with [ pair l c ⇒ 〈plus_b8_dc_d b1 b3 c:l〉 ] =
+  match plus_b8_dc_dc b4 b2 c with [ pair l c ⇒ 〈plus_b8_dc_d b3 b1 c:l〉 ]);
+ nrewrite > (symmetric_plusb8_dc_dc b4 b2 c);
+ ncases (plus_b8_dc_dc b2 b4 c);
+ #b5; #c1;
+ nchange with (〈plus_b8_dc_d b1 b3 c1:b5〉 = 〈plus_b8_dc_d b3 b1 c1:b5〉);
+ nrewrite > (symmetric_plusb8_dc_d b1 b3 c1);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusw16_dc_c : ∀w1,w2,c.plus_w16_dc_c w1 w2 c = plus_w16_dc_c w2 w1 c.
+ #w1; #w2; #c;
+ nelim w1;
+ #b1; #b2;
+ nelim w2;
+ #b3; #b4;
+ nchange with (
+  plus_b8_dc_c b1 b3 (plus_b8_dc_c b2 b4 c) =
+  plus_b8_dc_c b3 b1 (plus_b8_dc_c b4 b2 c));
+ nrewrite > (symmetric_plusb8_dc_c b4 b2 c);
+ nrewrite > (symmetric_plusb8_dc_c b3 b1 (plus_b8_dc_c b2 b4 c));
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusw16_d_dc : ∀w1,w2.plus_w16_d_dc w1 w2 = plus_w16_d_dc w2 w1.
+ #w1; #w2;
+ nelim w1;
+ #b1; #b2;
+ nelim w2;
+ #b3; #b4;
+ nchange with (
+  match plus_b8_d_dc b2 b4 with [ pair l c ⇒ match plus_b8_dc_dc b1 b3 c with [ pair h c' ⇒ pair … 〈h:l〉 c' ]] =
+  match plus_b8_d_dc b4 b2 with [ pair l c ⇒ match plus_b8_dc_dc b3 b1 c with [ pair h c' ⇒ pair … 〈h:l〉 c' ]]);
+ nrewrite > (symmetric_plusb8_d_dc b4 b2);
+ ncases (plus_b8_d_dc b2 b4);
+ #b5; #c;
+ nchange with (
+  match plus_b8_dc_dc b1 b3 c with [ pair h c' ⇒ pair … 〈h:b5〉 c' ] =
+  match plus_b8_dc_dc b3 b1 c with [ pair h c' ⇒ pair … 〈h:b5〉 c' ]);
+ nrewrite > (symmetric_plusb8_dc_dc b1 b3 c);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusw16_d_d : ∀w1,w2.plus_w16_d_d w1 w2 = plus_w16_d_d w2 w1.
+ #w1; #w2;
+ nelim w1;
+ #b1; #b2;
+ nelim w2;
+ #b3; #b4;
+ nchange with (
+  match plus_b8_d_dc b2 b4 with [ pair l c ⇒ 〈plus_b8_dc_d b1 b3 c:l〉 ] =
+  match plus_b8_d_dc b4 b2 with [ pair l c ⇒ 〈plus_b8_dc_d b3 b1 c:l〉 ]);
+ nrewrite > (symmetric_plusb8_d_dc b4 b2);
+ ncases (plus_b8_d_dc b2 b4);
+ #b5; #c;
+ nchange with (〈plus_b8_dc_d b1 b3 c:b5〉 = 〈plus_b8_dc_d b3 b1 c:b5〉);
+ nrewrite > (symmetric_plusb8_dc_d b1 b3 c);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusw16_d_c : ∀w1,w2.plus_w16_d_c w1 w2 = plus_w16_d_c w2 w1.
+ #w1; #w2;
+ nelim w1;
+ #b1; #b2;
+ nelim w2;
+ #b3; #b4;
+ nchange with (
+  plus_b8_dc_c b1 b3 (plus_b8_d_c b2 b4) =
+  plus_b8_dc_c b3 b1 (plus_b8_d_c b4 b2));
+ nrewrite > (symmetric_plusb8_d_c b4 b2);
+ nrewrite > (symmetric_plusb8_dc_c b3 b1 (plus_b8_d_c b2 b4));
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_mulb8 : symmetricT byte8 word16 mul_b8.
+ #b1; #b2;
+ nelim b1;
+ #e1; #e2;
+ nelim b2;
+ #e3; #e4;
+ nchange with (match mul_ex e2 e4 with
+ [ mk_byte8 t1_h t1_l ⇒ match mul_ex e1 e4 with
+ [ mk_byte8 t2_h t2_l ⇒ match mul_ex e3 e2 with
+ [ mk_byte8 t3_h t3_l ⇒ match mul_ex e1 e3 with
+ [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,t3_h〉:〈t3_l,x0〉〉 〈〈x0,t2_h〉:〈t2_l,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈t1_h,t1_l〉〉
+ ]]]] = match mul_ex e4 e2 with
+ [ mk_byte8 t1_h t1_l ⇒ match mul_ex e3 e2 with
+ [ mk_byte8 t2_h t2_l ⇒ match mul_ex e1 e4 with
+ [ mk_byte8 t3_h t3_l ⇒ match mul_ex e3 e1 with
+ [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,t3_h〉:〈t3_l,x0〉〉 〈〈x0,t2_h〉:〈t2_l,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈t1_h,t1_l〉〉
+ ]]]]);
+ nrewrite < (symmetric_mulex e2 e4);
+ ncases (mul_ex e2 e4);
+ #e5; #e6;
+ nchange with (match mul_ex e1 e4 with
+ [ mk_byte8 t2_h t2_l ⇒ match mul_ex e3 e2 with
+ [ mk_byte8 t3_h t3_l ⇒ match mul_ex e1 e3 with
+ [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,t3_h〉:〈t3_l,x0〉〉 〈〈x0,t2_h〉:〈t2_l,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉
+ ]]] = match mul_ex e3 e2 with
+ [ mk_byte8 t2_h t2_l ⇒ match mul_ex e1 e4 with
+ [ mk_byte8 t3_h t3_l ⇒ match mul_ex e3 e1 with
+ [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,t3_h〉:〈t3_l,x0〉〉 〈〈x0,t2_h〉:〈t2_l,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉
+ ]]]);
+ ncases (mul_ex e3 e2);
+ #e7; #e8;
+ ncases (mul_ex e1 e4);
+ #e9; #e10;
+ nchange with (match mul_ex e1 e3 with
+ [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,e7〉:〈e8,x0〉〉 〈〈x0,e9〉:〈e10,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉
+ ] = match mul_ex e3 e1 with
+ [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,e9〉:〈e10,x0〉〉 〈〈x0,e7〉:〈e8,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉
+ ]);
+ nrewrite < (symmetric_mulex e1 e3);
+ ncases (mul_ex e1 e3);
+ #e11; #e12;
+ nchange with ((plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,e7〉:〈e8,x0〉〉 〈〈x0,e9〉:〈e10,x0〉〉) 〈〈e11,e12〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉) =
+  (plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,e9〉:〈e10,x0〉〉 〈〈x0,e7〉:〈e8,x0〉〉) 〈〈e11,e12〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉));
+ nrewrite > (symmetric_plusw16_d_d 〈〈x0,e7〉:〈e8,x0〉〉 〈〈x0,e9〉:〈e10,x0〉〉);
+ napply refl_eq.
+nqed.
+
+nlemma eqw16_to_eq : ∀w1,w2:word16.(eq_w16 w1 w2 = true) → (w1 = w2).
+ #w1; #w2;
+ nelim w1;
+ nelim w2;
+ #b1; #b2; #b3; #b4;
+ nchange in ⊢ (% → ?) with (((eq_b8 b3 b1)⊗(eq_b8 b4 b2)) = true);
+ #H;
+ nrewrite < (eqb8_to_eq … (andb_true_true_l … H));
+ nrewrite < (eqb8_to_eq … (andb_true_true_r … H));
+ napply refl_eq.
+nqed.
+
+nlemma eq_to_eqw16 : ∀w1,w2.w1 = w2 → eq_w16 w1 w2 = true.
+ #w1; #w2;
+ nelim w1;
+ nelim w2;
+ #b1; #b2; #b3; #b4;
+ #H;
+ nrewrite < (word16_destruct_1 … H);
+ nrewrite < (word16_destruct_2 … H);
+ nchange with (((eq_b8 b3 b3)⊗(eq_b8 b4 b4)) = true);
+ nrewrite > (eq_to_eqb8 b3 b3 (refl_eq …));
+ nrewrite > (eq_to_eqb8 b4 b4 (refl_eq …)); 
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma decidable_w16_aux1 : ∀b1,b2,b3,b4.b1 ≠ b3 → 〈b1:b2〉 ≠ 〈b3:b4〉.
+ #b1; #b2; #b3; #b4;
+ nnormalize; #H; #H1;
+ napply (H (word16_destruct_1 … H1)).
+nqed.
+
+nlemma decidable_w16_aux2 : ∀b1,b2,b3,b4.b2 ≠ b4 → 〈b1:b2〉 ≠ 〈b3:b4〉.
+ #b1; #b2; #b3; #b4;
+ nnormalize; #H; #H1;
+ napply (H (word16_destruct_2 … H1)).
+nqed.
+
+nlemma decidable_w16 : ∀x,y:word16.decidable (x = y).
+ #x; nelim x; #b1; #b2;
+ #y; nelim y; #b3; #b4;
+ nnormalize;
+ napply (or2_elim (b1 = b3) (b1 ≠ b3) ? (decidable_b8 b1 b3) …);
+ ##[ ##2: #H; napply (or2_intro2 … (decidable_w16_aux1 b1 b2 b3 b4 H))
+ ##| ##1: #H; napply (or2_elim (b2 = b4) (b2 ≠ b4) ? (decidable_b8 b2 b4) …);
+          ##[ ##2: #H1; napply (or2_intro2 … (decidable_w16_aux2 b1 b2 b3 b4 H1))
+          ##| ##1: #H1; nrewrite > H; nrewrite > H1;
+                        napply (or2_intro1 … (refl_eq ? 〈b3:b4〉))
+          ##]
+ ##]
+nqed.
+
+nlemma neqw16_to_neq : ∀w1,w2:word16.(eq_w16 w1 w2 = false) → (w1 ≠ w2).
+ #w1; #w2;
+ nelim w1;
+ nelim w2;
+ #b1; #b2; #b3; #b4;
+ nchange with ((((eq_b8 b3 b1) ⊗ (eq_b8 b4 b2)) = false) → ?);
+ #H;
+ napply (or2_elim ((eq_b8 b3 b1) = false) ((eq_b8 b4 b2) = false) ? (andb_false2 … H) …);
+ ##[ ##1: #H1; napply (decidable_w16_aux1 … (neqb8_to_neq … H1))
+ ##| ##2: #H1; napply (decidable_w16_aux2 … (neqb8_to_neq … H1))
+ ##]
+nqed.
+
+nlemma word16_destruct : ∀b1,b2,b3,b4.〈b1:b2〉 ≠ 〈b3:b4〉 → b1 ≠ b3 ∨ b2 ≠ b4.
+ #b1; #b2; #b3; #b4;
+ nnormalize; #H;
+ napply (or2_elim (b1 = b3) (b1 ≠ b3) ? (decidable_b8 b1 b3) …);
+ ##[ ##2: #H1; napply (or2_intro1 … H1)
+ ##| ##1: #H1; napply (or2_elim (b2 = b4) (b2 ≠ b4) ? (decidable_b8 b2 b4) …);
+          ##[ ##2: #H2; napply (or2_intro2 … H2)
+          ##| ##1: #H2; nrewrite > H1 in H:(%);
+                   nrewrite > H2;
+                   #H; nelim (H (refl_eq …))
+          ##]
+ ##]
+nqed.
+
+nlemma neq_to_neqw16 : ∀w1,w2.w1 ≠ w2 → eq_w16 w1 w2 = false.
+ #w1; #w2;
+ nelim w1; #b1; #b2;
+ nelim w2; #b3; #b4;
+ #H; nchange with (((eq_b8 b1 b3) ⊗ (eq_b8 b2 b4)) = false);
+ napply (or2_elim (b1 ≠ b3) (b2 ≠ b4) ? (word16_destruct … H) …);
+ ##[ ##1: #H1; nrewrite > (neq_to_neqb8 … H1); nnormalize; napply refl_eq
+ ##| ##2: #H1; nrewrite > (neq_to_neqb8 … H1);
+          nrewrite > (symmetric_andbool (eq_b8 b1 b3) false);
+          nnormalize; napply refl_eq
+ ##]
+nqed.