helm/software/matita/contribs/ng_assembly/num/byte8_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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Ultima modifica: 05/08/2009                                          *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "num/byte8.ma".
  24 include "num/exadecim_lemmas.ma".
  25
  26 (* **** *)
  27 (* BYTE *)
  28 (* **** *)
  29
  30 nlemma byte8_destruct_1 :
  31 ∀x1,x2,y1,y2.
  32  mk_byte8 x1 y1 = mk_byte8 x2 y2 → x1 = x2.
  33  #x1; #x2; #y1; #y2; #H;
  34  nchange with (match mk_byte8 x2 y2 with [ mk_byte8 a _ ⇒ x1 = a ]);
  35  nrewrite < H;
  36  nnormalize;
  37  napply refl_eq.
  38 nqed.
  39
  40 nlemma byte8_destruct_2 :
  41 ∀x1,x2,y1,y2.
  42  mk_byte8 x1 y1 = mk_byte8 x2 y2 → y1 = y2.
  43  #x1; #x2; #y1; #y2; #H;
  44  nchange with (match mk_byte8 x2 y2 with [ mk_byte8 _ b ⇒ y1 = b ]);
  45  nrewrite < H;
  46  nnormalize;
  47  napply refl_eq.
  48 nqed.
  49
  50 nlemma symmetric_eqb8 : symmetricT byte8 bool eq_b8.
  51  #b1; #b2;
  52  nelim b1;
  53  nelim b2;
  54  #e1; #e2; #e3; #e4;
  55  nchange with (((eq_ex e3 e1)⊗(eq_ex e4 e2)) = ((eq_ex e1 e3)⊗(eq_ex e2 e4)));
  56  nrewrite > (symmetric_eqex e1 e3);
  57  nrewrite > (symmetric_eqex e2 e4);
  58  napply refl_eq.
  59 nqed.
  60
  61 nlemma symmetric_andb8 : symmetricT byte8 byte8 and_b8.
  62  #b1; #b2;
  63  nelim b1;
  64  nelim b2;
  65  #e1; #e2; #e3; #e4;
  66  nchange with ((mk_byte8 (and_ex e3 e1) (and_ex e4 e2)) = (mk_byte8 (and_ex e1 e3) (and_ex e2 e4)));
  67  nrewrite > (symmetric_andex e1 e3);
  68  nrewrite > (symmetric_andex e2 e4);
  69  napply refl_eq.
  70 nqed.
  71
  72 nlemma associative_andb8 : ∀b1,b2,b3.(and_b8 (and_b8 b1 b2) b3) = (and_b8 b1 (and_b8 b2 b3)).
  73  #b1; #b2; #b3;
  74  nelim b1;
  75  #e1; #e2;
  76  nelim b2;
  77  #e3; #e4;
  78  nelim b3;
  79  #e5; #e6;
  80  nchange with (mk_byte8 (and_ex (and_ex e1 e3) e5) (and_ex (and_ex e2 e4) e6) =
  81   mk_byte8 (and_ex e1 (and_ex e3 e5)) (and_ex e2 (and_ex e4 e6)));
  82  nrewrite < (associative_andex e1 e3 e5);
  83  nrewrite < (associative_andex e2 e4 e6);
  84  napply refl_eq.
  85 nqed.
  86
  87 nlemma symmetric_orb8 : symmetricT byte8 byte8 or_b8.
  88  #b1; #b2;
  89  nelim b1;
  90  nelim b2;
  91  #e1; #e2; #e3; #e4;
  92  nchange with ((mk_byte8 (or_ex e3 e1) (or_ex e4 e2)) = (mk_byte8 (or_ex e1 e3) (or_ex e2 e4)));
  93  nrewrite > (symmetric_orex e1 e3);
  94  nrewrite > (symmetric_orex e2 e4);
  95  napply refl_eq.
  96 nqed.
  97
  98 nlemma associative_orb8 : ∀b1,b2,b3.(or_b8 (or_b8 b1 b2) b3) = (or_b8 b1 (or_b8 b2 b3)).
  99  #b1; #b2; #b3;
 100  nelim b1;
 101  #e1; #e2;
 102  nelim b2;
 103  #e3; #e4;
 104  nelim b3;
 105  #e5; #e6;
 106  nchange with (mk_byte8 (or_ex (or_ex e1 e3) e5) (or_ex (or_ex e2 e4) e6) =
 107   mk_byte8 (or_ex e1 (or_ex e3 e5)) (or_ex e2 (or_ex e4 e6)));
 108  nrewrite < (associative_orex e1 e3 e5);
 109  nrewrite < (associative_orex e2 e4 e6);
 110  napply refl_eq.
 111 nqed.
 112
 113 nlemma symmetric_xorb8 : symmetricT byte8 byte8 xor_b8.
 114  #b1; #b2;
 115  nelim b1;
 116  nelim b2;
 117  #e1; #e2; #e3; #e4;
 118  nchange with ((mk_byte8 (xor_ex e3 e1) (xor_ex e4 e2)) = (mk_byte8 (xor_ex e1 e3) (xor_ex e2 e4)));
 119  nrewrite > (symmetric_xorex e1 e3);
 120  nrewrite > (symmetric_xorex e2 e4);
 121  napply refl_eq.
 122 nqed.
 123
 124 nlemma associative_xorb8 : ∀b1,b2,b3.(xor_b8 (xor_b8 b1 b2) b3) = (xor_b8 b1 (xor_b8 b2 b3)).
 125  #b1; #b2; #b3;
 126  nelim b1;
 127  #e1; #e2;
 128  nelim b2;
 129  #e3; #e4;
 130  nelim b3;
 131  #e5; #e6;
 132  nchange with (mk_byte8 (xor_ex (xor_ex e1 e3) e5) (xor_ex (xor_ex e2 e4) e6) =
 133   mk_byte8 (xor_ex e1 (xor_ex e3 e5)) (xor_ex e2 (xor_ex e4 e6)));
 134  nrewrite < (associative_xorex e1 e3 e5);
 135  nrewrite < (associative_xorex e2 e4 e6);
 136  napply refl_eq.
 137 nqed.
 138
 139 nlemma symmetric_plusb8_dc_dc : ∀b1,b2,c.plus_b8_dc_dc b1 b2 c = plus_b8_dc_dc b2 b1 c.
 140  #b1; #b2; #c;
 141  nelim b1;
 142  #e1; #e2;
 143  nelim b2;
 144  #e3; #e4;
 145  nchange with (
 146   match plus_ex_dc_dc e2 e4 c with
 147    [ pair l c ⇒ match plus_ex_dc_dc e1 e3 c with
 148     [ pair h c' ⇒ pair … 〈h,l〉 c' ]] =
 149   match plus_ex_dc_dc e4 e2 c with
 150    [ pair l c ⇒ match plus_ex_dc_dc e3 e1 c with
 151     [ pair h c' ⇒ pair … 〈h,l〉 c' ]]);
 152  nrewrite > (symmetric_plusex_dc_dc e4 e2 c);
 153  ncases (plus_ex_dc_dc e2 e4 c);
 154  #e5; #c1;
 155  nchange with (
 156   match plus_ex_dc_dc e1 e3 c1 with
 157    [ pair h c' ⇒ pair … 〈h,e5〉 c' ] =
 158   match plus_ex_dc_dc e3 e1 c1 with
 159    [ pair h c' ⇒ pair … 〈h,e5〉 c' ]);
 160  nrewrite > (symmetric_plusex_dc_dc e1 e3 c1);
 161  napply refl_eq.
 162 nqed.
 163
 164 nlemma symmetric_plusb8_dc_d : ∀b1,b2,c.plus_b8_dc_d b1 b2 c = plus_b8_dc_d b2 b1 c.
 165  #b1; #b2; #c;
 166  nelim b1;
 167  #e1; #e2;
 168  nelim b2;
 169  #e3; #e4;
 170  nchange with (
 171   match plus_ex_dc_dc e2 e4 c with
 172    [ pair l c ⇒ 〈plus_ex_dc_d e1 e3 c,l〉 ] =
 173   match plus_ex_dc_dc e4 e2 c with
 174    [ pair l c ⇒ 〈plus_ex_dc_d e3 e1 c,l〉 ]);
 175  nrewrite > (symmetric_plusex_dc_dc e4 e2 c);
 176  ncases (plus_ex_dc_dc e2 e4 c);
 177  #e5; #c1;
 178  nchange with (〈plus_ex_dc_d e1 e3 c1,e5〉 = 〈plus_ex_dc_d e3 e1 c1,e5〉);
 179  nrewrite > (symmetric_plusex_dc_d e1 e3 c1);
 180  napply refl_eq.
 181 nqed.
 182
 183 nlemma symmetric_plusb8_dc_c : ∀b1,b2,c.plus_b8_dc_c b1 b2 c = plus_b8_dc_c b2 b1 c.
 184  #b1; #b2; #c;
 185  nelim b1;
 186  #e1; #e2;
 187  nelim b2;
 188  #e3; #e4;
 189  nchange with (
 190   plus_ex_dc_c e1 e3 (plus_ex_dc_c e2 e4 c) =
 191   plus_ex_dc_c e3 e1 (plus_ex_dc_c e4 e2 c));
 192  nrewrite > (symmetric_plusex_dc_c e4 e2 c);
 193  nrewrite > (symmetric_plusex_dc_c e3 e1 (plus_ex_dc_c e2 e4 c));
 194  napply refl_eq.
 195 nqed.
 196
 197 nlemma symmetric_plusb8_d_dc : ∀b1,b2.plus_b8_d_dc b1 b2 = plus_b8_d_dc b2 b1.
 198  #b1; #b2;
 199  nelim b1;
 200  #e1; #e2;
 201  nelim b2;
 202  #e3; #e4;
 203  nchange with (
 204   match plus_ex_d_dc e2 e4 with
 205    [ pair l c ⇒ match plus_ex_dc_dc e1 e3 c with
 206     [ pair h c' ⇒ pair … 〈h,l〉 c' ]] =
 207   match plus_ex_d_dc e4 e2 with
 208    [ pair l c ⇒ match plus_ex_dc_dc e3 e1 c with
 209     [ pair h c' ⇒ pair … 〈h,l〉 c' ]]);
 210  nrewrite > (symmetric_plusex_d_dc e4 e2);
 211  ncases (plus_ex_d_dc e2 e4);
 212  #e5; #c;
 213  nchange with (
 214   match plus_ex_dc_dc e1 e3 c with
 215    [ pair h c' ⇒ pair … 〈h,e5〉 c' ] =
 216   match plus_ex_dc_dc e3 e1 c with
 217    [ pair h c' ⇒ pair … 〈h,e5〉 c' ]);
 218  nrewrite > (symmetric_plusex_dc_dc e1 e3 c);
 219  napply refl_eq.
 220 nqed.
 221
 222 nlemma symmetric_plusb8_d_d : ∀b1,b2.plus_b8_d_d b1 b2 = plus_b8_d_d b2 b1.
 223  #b1; #b2;
 224  nelim b1;
 225  #e1; #e2;
 226  nelim b2;
 227  #e3; #e4;
 228  nchange with (
 229   match plus_ex_d_dc e2 e4 with
 230    [ pair l c ⇒ 〈plus_ex_dc_d e1 e3 c,l〉 ] =
 231   match plus_ex_d_dc e4 e2 with
 232    [ pair l c ⇒ 〈plus_ex_dc_d e3 e1 c,l〉 ]);
 233  nrewrite > (symmetric_plusex_d_dc e4 e2);
 234  ncases (plus_ex_d_dc e2 e4);
 235  #e5; #c;
 236  nchange with (〈plus_ex_dc_d e1 e3 c,e5〉 = 〈plus_ex_dc_d e3 e1 c,e5〉);
 237  nrewrite > (symmetric_plusex_dc_d e1 e3 c);
 238  napply refl_eq.
 239 nqed.
 240
 241 nlemma symmetric_plusb8_d_c : ∀b1,b2.plus_b8_d_c b1 b2 = plus_b8_d_c b2 b1.
 242  #b1; #b2;
 243  nelim b1;
 244  #e1; #e2;
 245  nelim b2;
 246  #e3; #e4;
 247  nchange with (
 248   plus_ex_dc_c e1 e3 (plus_ex_d_c e2 e4) =
 249   plus_ex_dc_c e3 e1 (plus_ex_d_c e4 e2));
 250  nrewrite > (symmetric_plusex_d_c e4 e2);
 251  nrewrite > (symmetric_plusex_dc_c e3 e1 (plus_ex_d_c e2 e4));
 252  napply refl_eq.
 253 nqed.
 254
 255 nlemma symmetric_mulex : symmetricT exadecim byte8 mul_ex.
 256  #e1; #e2;
 257  nelim e1;
 258  nelim e2;
 259  nnormalize;
 260  napply refl_eq.
 261 nqed.
 262
 263 nlemma eqb8_to_eq : ∀b1,b2:byte8.(eq_b8 b1 b2 = true) → (b1 = b2).
 264  #b1; #b2;
 265  nelim b1;
 266  nelim b2;
 267  #e1; #e2; #e3; #e4;
 268  nchange in ⊢ (% → ?) with (((eq_ex e3 e1)⊗(eq_ex e4 e2)) = true);
 269  #H;
 270  nrewrite < (eqex_to_eq … (andb_true_true_l … H));
 271  nrewrite < (eqex_to_eq … (andb_true_true_r … H));
 272  napply refl_eq.
 273 nqed.
 274
 275 nlemma eq_to_eqb8 : ∀b1,b2.b1 = b2 → eq_b8 b1 b2 = true.
 276  #b1; #b2;
 277  nelim b1;
 278  nelim b2;
 279  #e1; #e2; #e3; #e4;
 280  #H;
 281  nrewrite < (byte8_destruct_1 … H);
 282  nrewrite < (byte8_destruct_2 … H);
 283  nchange with (((eq_ex e3 e3)⊗(eq_ex e4 e4)) = true);
 284  nrewrite > (eq_to_eqex e3 e3 (refl_eq …));
 285  nrewrite > (eq_to_eqex e4 e4 (refl_eq …));
 286  nnormalize;
 287  napply refl_eq.
 288 nqed.