helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
  19 (*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "num/word16.ma".
  24 include "num/byte8_lemmas.ma".
  25
  26 (* **** *)
  27 (* WORD *)
  28 (* **** *)
  29
  30 nlemma word16_destruct_1 :
  31 ∀x1,x2,y1,y2.
  32  mk_word16 x1 y1 = mk_word16 x2 y2 → x1 = x2.
  33  #x1; #x2; #y1; #y2; #H;
  34  nchange with (match mk_word16 x2 y2 with [ mk_word16 a _ ⇒ x1 = a ]);
  35  nrewrite < H;
  36  nnormalize;
  37  napply refl_eq.
  38 nqed.
  39
  40 nlemma word16_destruct_2 :
  41 ∀x1,x2,y1,y2.
  42  mk_word16 x1 y1 = mk_word16 x2 y2 → y1 = y2.
  43  #x1; #x2; #y1; #y2; #H;
  44  nchange with (match mk_word16 x2 y2 with [ mk_word16 _ b ⇒ y1 = b ]);
  45  nrewrite < H;
  46  nnormalize;
  47  napply refl_eq.
  48 nqed.
  49
  50 nlemma symmetric_eqw16 : symmetricT word16 bool eq_w16.
  51  #w1; #w2;
  52  nelim w1;
  53  nelim w2;
  54  #b1; #b2; #b3; #b4;
  55  nchange with (((eq_b8 b3 b1)⊗(eq_b8 b4 b2)) = ((eq_b8 b1 b3)⊗(eq_b8 b2 b4)));
  56  nrewrite > (symmetric_eqb8 b1 b3);
  57  nrewrite > (symmetric_eqb8 b2 b4);
  58  napply refl_eq.
  59 nqed.
  60
  61 nlemma symmetric_andw16 : symmetricT word16 word16 and_w16.
  62  #w1; #w2;
  63  nelim w1;
  64  nelim w2;
  65  #b1; #b2; #b3; #b4;
  66  nchange with ((mk_word16 (and_b8 b3 b1) (and_b8 b4 b2)) = (mk_word16 (and_b8 b1 b3) (and_b8 b2 b4)));
  67  nrewrite > (symmetric_andb8 b1 b3);
  68  nrewrite > (symmetric_andb8 b2 b4);
  69  napply refl_eq.
  70 nqed.
  71
  72 nlemma associative_andw16 : ∀w1,w2,w3.(and_w16 (and_w16 w1 w2) w3) = (and_w16 w1 (and_w16 w2 w3)).
  73  #w1; #w2; #w3;
  74  nelim w1;
  75  #b1; #b2;
  76  nelim w2;
  77  #b3; #b4;
  78  nelim w3;
  79  #b5; #b6;
  80  nchange with (mk_word16 (and_b8 (and_b8 b1 b3) b5) (and_b8 (and_b8 b2 b4) b6) =
  81   mk_word16 (and_b8 b1 (and_b8 b3 b5)) (and_b8 b2 (and_b8 b4 b6)));
  82  nrewrite < (associative_andb8 b1 b3 b5);
  83  nrewrite < (associative_andb8 b2 b4 b6);
  84  napply refl_eq.
  85 nqed.
  86
  87 nlemma symmetric_orw16 : symmetricT word16 word16 or_w16.
  88  #w1; #w2;
  89  nelim w1;
  90  nelim w2;
  91  #b1; #b2; #b3; #b4;
  92  nchange with ((mk_word16 (or_b8 b3 b1) (or_b8 b4 b2)) = (mk_word16 (or_b8 b1 b3) (or_b8 b2 b4)));
  93  nrewrite > (symmetric_orb8 b1 b3);
  94  nrewrite > (symmetric_orb8 b2 b4);
  95  napply refl_eq.
  96 nqed.
  97
  98 nlemma associative_orw16 : ∀w1,w2,w3.(or_w16 (or_w16 w1 w2) w3) = (or_w16 w1 (or_w16 w2 w3)).
  99  #w1; #w2; #w3;
 100  nelim w1;
 101  #b1; #b2;
 102  nelim w2;
 103  #b3; #b4;
 104  nelim w3;
 105  #b5; #b6;
 106  nchange with (mk_word16 (or_b8 (or_b8 b1 b3) b5) (or_b8 (or_b8 b2 b4) b6) =
 107   mk_word16 (or_b8 b1 (or_b8 b3 b5)) (or_b8 b2 (or_b8 b4 b6)));
 108  nrewrite < (associative_orb8 b1 b3 b5);
 109  nrewrite < (associative_orb8 b2 b4 b6);
 110  napply refl_eq.
 111 nqed.
 112
 113 nlemma symmetric_xorw16 : symmetricT word16 word16 xor_w16.
 114  #w1; #w2;
 115  nelim w1;
 116  nelim w2;
 117  #b1; #b2; #b3; #b4;
 118  nchange with ((mk_word16 (xor_b8 b3 b1) (xor_b8 b4 b2)) = (mk_word16 (xor_b8 b1 b3) (xor_b8 b2 b4)));
 119  nrewrite > (symmetric_xorb8 b1 b3);
 120  nrewrite > (symmetric_xorb8 b2 b4);
 121  napply refl_eq.
 122 nqed.
 123
 124 nlemma associative_xorw16 : ∀w1,w2,w3.(xor_w16 (xor_w16 w1 w2) w3) = (xor_w16 w1 (xor_w16 w2 w3)).
 125  #w1; #w2; #w3;
 126  nelim w1;
 127  #b1; #b2;
 128  nelim w2;
 129  #b3; #b4;
 130  nelim w3;
 131  #b5; #b6;
 132  nchange with (mk_word16 (xor_b8 (xor_b8 b1 b3) b5) (xor_b8 (xor_b8 b2 b4) b6) =
 133   mk_word16 (xor_b8 b1 (xor_b8 b3 b5)) (xor_b8 b2 (xor_b8 b4 b6)));
 134  nrewrite < (associative_xorb8 b1 b3 b5);
 135  nrewrite < (associative_xorb8 b2 b4 b6);
 136  napply refl_eq.
 137 nqed.
 138
 139 nlemma symmetric_plusw16_dc_dc : ∀w1,w2,c.plus_w16_dc_dc w1 w2 c = plus_w16_dc_dc w2 w1 c.
 140  #w1; #w2; #c;
 141  nelim w1;
 142  #b1; #b2;
 143  nelim w2;
 144  #b3; #b4;
 145  nchange with (
 146   match plus_b8_dc_dc b2 b4 c with
 147    [ pair l c ⇒ match plus_b8_dc_dc b1 b3 c with
 148     [ pair h c' ⇒ pair … 〈h:l〉 c' ]] =
 149   match plus_b8_dc_dc b4 b2 c with
 150    [ pair l c ⇒ match plus_b8_dc_dc b3 b1 c with
 151     [ pair h c' ⇒ pair … 〈h:l〉 c' ]]);
 152  nrewrite > (symmetric_plusb8_dc_dc b4 b2 c);
 153  ncases (plus_b8_dc_dc b2 b4 c);
 154  #b5; #c1;
 155  nchange with (
 156   match plus_b8_dc_dc b1 b3 c1 with
 157    [ pair h c' ⇒ pair … 〈h:b5〉 c' ] =
 158   match plus_b8_dc_dc b3 b1 c1 with
 159    [ pair h c' ⇒ pair … 〈h:b5〉 c' ]);
 160  nrewrite > (symmetric_plusb8_dc_dc b1 b3 c1);
 161  napply refl_eq.
 162 nqed.
 163
 164 nlemma symmetric_plusw16_dc_d : ∀w1,w2,c.plus_w16_dc_d w1 w2 c = plus_w16_dc_d w2 w1 c.
 165  #w1; #w2; #c;
 166  nelim w1;
 167  #b1; #b2;
 168  nelim w2;
 169  #b3; #b4;
 170  nchange with (
 171   match plus_b8_dc_dc b2 b4 c with
 172    [ pair l c ⇒ 〈plus_b8_dc_d b1 b3 c:l〉 ] =
 173   match plus_b8_dc_dc b4 b2 c with
 174    [ pair l c ⇒ 〈plus_b8_dc_d b3 b1 c:l〉 ]);
 175  nrewrite > (symmetric_plusb8_dc_dc b4 b2 c);
 176  ncases (plus_b8_dc_dc b2 b4 c);
 177  #b5; #c1;
 178  nchange with (〈plus_b8_dc_d b1 b3 c1:b5〉 = 〈plus_b8_dc_d b3 b1 c1:b5〉);
 179  nrewrite > (symmetric_plusb8_dc_d b1 b3 c1);
 180  napply refl_eq.
 181 nqed.
 182
 183 nlemma symmetric_plusw16_dc_c : ∀w1,w2,c.plus_w16_dc_c w1 w2 c = plus_w16_dc_c w2 w1 c.
 184  #w1; #w2; #c;
 185  nelim w1;
 186  #b1; #b2;
 187  nelim w2;
 188  #b3; #b4;
 189  nchange with (
 190   plus_b8_dc_c b1 b3 (plus_b8_dc_c b2 b4 c) =
 191   plus_b8_dc_c b3 b1 (plus_b8_dc_c b4 b2 c));
 192  nrewrite > (symmetric_plusb8_dc_c b4 b2 c);
 193  nrewrite > (symmetric_plusb8_dc_c b3 b1 (plus_b8_dc_c b2 b4 c));
 194  napply refl_eq.
 195 nqed.
 196
 197 nlemma symmetric_plusw16_d_dc : ∀w1,w2.plus_w16_d_dc w1 w2 = plus_w16_d_dc w2 w1.
 198  #w1; #w2;
 199  nelim w1;
 200  #b1; #b2;
 201  nelim w2;
 202  #b3; #b4;
 203  nchange with (
 204   match plus_b8_d_dc b2 b4 with
 205    [ pair l c ⇒ match plus_b8_dc_dc b1 b3 c with
 206     [ pair h c' ⇒ pair … 〈h:l〉 c' ]] =
 207   match plus_b8_d_dc b4 b2 with
 208    [ pair l c ⇒ match plus_b8_dc_dc b3 b1 c with
 209     [ pair h c' ⇒ pair … 〈h:l〉 c' ]]);
 210  nrewrite > (symmetric_plusb8_d_dc b4 b2);
 211  ncases (plus_b8_d_dc b2 b4);
 212  #b5; #c;
 213  nchange with (
 214   match plus_b8_dc_dc b1 b3 c with
 215    [ pair h c' ⇒ pair … 〈h:b5〉 c' ] =
 216   match plus_b8_dc_dc b3 b1 c with
 217    [ pair h c' ⇒ pair … 〈h:b5〉 c' ]);
 218  nrewrite > (symmetric_plusb8_dc_dc b1 b3 c);
 219  napply refl_eq.
 220 nqed.
 221
 222 nlemma symmetric_plusw16_d_d : ∀w1,w2.plus_w16_d_d w1 w2 = plus_w16_d_d w2 w1.
 223  #w1; #w2;
 224  nelim w1;
 225  #b1; #b2;
 226  nelim w2;
 227  #b3; #b4;
 228  nchange with (
 229   match plus_b8_d_dc b2 b4 with
 230    [ pair l c ⇒ 〈plus_b8_dc_d b1 b3 c:l〉 ] =
 231   match plus_b8_d_dc b4 b2 with
 232    [ pair l c ⇒ 〈plus_b8_dc_d b3 b1 c:l〉 ]);
 233  nrewrite > (symmetric_plusb8_d_dc b4 b2);
 234  ncases (plus_b8_d_dc b2 b4);
 235  #b5; #c;
 236  nchange with (〈plus_b8_dc_d b1 b3 c:b5〉 = 〈plus_b8_dc_d b3 b1 c:b5〉);
 237  nrewrite > (symmetric_plusb8_dc_d b1 b3 c);
 238  napply refl_eq.
 239 nqed.
 240
 241 nlemma symmetric_plusw16_d_c : ∀w1,w2.plus_w16_d_c w1 w2 = plus_w16_d_c w2 w1.
 242  #w1; #w2;
 243  nelim w1;
 244  #b1; #b2;
 245  nelim w2;
 246  #b3; #b4;
 247  nchange with (
 248   plus_b8_dc_c b1 b3 (plus_b8_d_c b2 b4) =
 249   plus_b8_dc_c b3 b1 (plus_b8_d_c b4 b2));
 250  nrewrite > (symmetric_plusb8_d_c b4 b2);
 251  nrewrite > (symmetric_plusb8_dc_c b3 b1 (plus_b8_d_c b2 b4));
 252  napply refl_eq.
 253 nqed.
 254
 255 nlemma symmetric_mulb8 : symmetricT byte8 word16 mul_b8.
 256  #b1; #b2;
 257  nelim b1;
 258  #e1; #e2;
 259  nelim b2;
 260  #e3; #e4;
 261  nchange with (match mul_ex e2 e4 with
 262  [ mk_byte8 t1_h t1_l ⇒ match mul_ex e1 e4 with
 263  [ mk_byte8 t2_h t2_l ⇒ match mul_ex e3 e2 with
 264  [ mk_byte8 t3_h t3_l ⇒ match mul_ex e1 e3 with
 265  [ 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〉〉
 266  ]]]] = match mul_ex e4 e2 with
 267  [ mk_byte8 t1_h t1_l ⇒ match mul_ex e3 e2 with
 268  [ mk_byte8 t2_h t2_l ⇒ match mul_ex e1 e4 with
 269  [ mk_byte8 t3_h t3_l ⇒ match mul_ex e3 e1 with
 270  [ 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〉〉
 271  ]]]]);
 272  nrewrite < (symmetric_mulex e2 e4);
 273  ncases (mul_ex e2 e4);
 274  #e5; #e6;
 275  nchange with (match mul_ex e1 e4 with
 276  [ mk_byte8 t2_h t2_l ⇒ match mul_ex e3 e2 with
 277  [ mk_byte8 t3_h t3_l ⇒ match mul_ex e1 e3 with
 278  [ 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〉〉
 279  ]]] = match mul_ex e3 e2 with
 280  [ mk_byte8 t2_h t2_l ⇒ match mul_ex e1 e4 with
 281  [ mk_byte8 t3_h t3_l ⇒ match mul_ex e3 e1 with
 282  [ 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〉〉
 283  ]]]);
 284  ncases (mul_ex e3 e2);
 285  #e7; #e8;
 286  ncases (mul_ex e1 e4);
 287  #e9; #e10;
 288  nchange with (match mul_ex e1 e3 with
 289  [ 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〉〉
 290  ] = match mul_ex e3 e1 with
 291  [ 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〉〉
 292  ]);
 293  nrewrite < (symmetric_mulex e1 e3);
 294  ncases (mul_ex e1 e3);
 295  #e11; #e12;
 296  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〉〉) =
 297   (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〉〉));
 298  nrewrite > (symmetric_plusw16_d_d 〈〈x0,e7〉:〈e8,x0〉〉 〈〈x0,e9〉:〈e10,x0〉〉);
 299  napply refl_eq.
 300 nqed.
 301
 302 nlemma eqw16_to_eq : ∀w1,w2:word16.(eq_w16 w1 w2 = true) → (w1 = w2).
 303  #w1; #w2;
 304  nelim w1;
 305  nelim w2;
 306  #b1; #b2; #b3; #b4;
 307  nchange in ⊢ (% → ?) with (((eq_b8 b3 b1)⊗(eq_b8 b4 b2)) = true);
 308  #H;
 309  nrewrite < (eqb8_to_eq … (andb_true_true_l … H));
 310  nrewrite < (eqb8_to_eq … (andb_true_true_r … H));
 311  napply refl_eq.
 312 nqed.
 313
 314 nlemma eq_to_eqw16 : ∀w1,w2.w1 = w2 → eq_w16 w1 w2 = true.
 315  #w1; #w2;
 316  nelim w1;
 317  nelim w2;
 318  #b1; #b2; #b3; #b4;
 319  #H;
 320  nrewrite < (word16_destruct_1 … H);
 321  nrewrite < (word16_destruct_2 … H);
 322  nchange with (((eq_b8 b3 b3)⊗(eq_b8 b4 b4)) = true);
 323  nrewrite > (eq_to_eqb8 b3 b3 (refl_eq …));
 324  nrewrite > (eq_to_eqb8 b4 b4 (refl_eq …));
 325  nnormalize;
 326  napply refl_eq.
 327 nqed.