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 [ pair l c ⇒ match plus_ex_dc_dc e1 e3 c with [ pair h c' ⇒ pair … 〈h,l〉 c' ]] =
 147   match plus_ex_dc_dc e4 e2 c with [ pair l c ⇒ match plus_ex_dc_dc e3 e1 c with [ pair h c' ⇒ pair … 〈h,l〉 c' ]]);
 148  nrewrite > (symmetric_plusex_dc_dc e4 e2 c);
 149  ncases (plus_ex_dc_dc e2 e4 c);
 150  #e5; #c1;
 151  nchange with (
 152   match plus_ex_dc_dc e1 e3 c1 with [ pair h c' ⇒ pair … 〈h,e5〉 c' ] =
 153   match plus_ex_dc_dc e3 e1 c1 with [ pair h c' ⇒ pair … 〈h,e5〉 c' ]);
 154  nrewrite > (symmetric_plusex_dc_dc e1 e3 c1);
 155  napply refl_eq.
 156 nqed.
 157
 158 nlemma symmetric_plusb8_dc_d : ∀b1,b2,c.plus_b8_dc_d b1 b2 c = plus_b8_dc_d b2 b1 c.
 159  #b1; #b2; #c;
 160  nelim b1;
 161  #e1; #e2;
 162  nelim b2;
 163  #e3; #e4;
 164  nchange with (
 165   match plus_ex_dc_dc e2 e4 c with [ pair l c ⇒ 〈plus_ex_dc_d e1 e3 c,l〉 ] =
 166   match plus_ex_dc_dc e4 e2 c with [ pair l c ⇒ 〈plus_ex_dc_d e3 e1 c,l〉 ]);
 167  nrewrite > (symmetric_plusex_dc_dc e4 e2 c);
 168  ncases (plus_ex_dc_dc e2 e4 c);
 169  #e5; #c1;
 170  nchange with (〈plus_ex_dc_d e1 e3 c1,e5〉 = 〈plus_ex_dc_d e3 e1 c1,e5〉);
 171  nrewrite > (symmetric_plusex_dc_d e1 e3 c1);
 172  napply refl_eq.
 173 nqed.
 174
 175 nlemma symmetric_plusb8_dc_c : ∀b1,b2,c.plus_b8_dc_c b1 b2 c = plus_b8_dc_c b2 b1 c.
 176  #b1; #b2; #c;
 177  nelim b1;
 178  #e1; #e2;
 179  nelim b2;
 180  #e3; #e4;
 181  nchange with (
 182   plus_ex_dc_c e1 e3 (plus_ex_dc_c e2 e4 c) =
 183   plus_ex_dc_c e3 e1 (plus_ex_dc_c e4 e2 c));
 184  nrewrite > (symmetric_plusex_dc_c e4 e2 c);
 185  nrewrite > (symmetric_plusex_dc_c e3 e1 (plus_ex_dc_c e2 e4 c));
 186  napply refl_eq.
 187 nqed.
 188
 189 nlemma symmetric_plusb8_d_dc : ∀b1,b2.plus_b8_d_dc b1 b2 = plus_b8_d_dc b2 b1.
 190  #b1; #b2;
 191  nelim b1;
 192  #e1; #e2;
 193  nelim b2;
 194  #e3; #e4;
 195  nchange with (
 196   match plus_ex_d_dc e2 e4 with [ pair l c ⇒ match plus_ex_dc_dc e1 e3 c with [ pair h c' ⇒ pair … 〈h,l〉 c' ]] =
 197   match plus_ex_d_dc e4 e2 with [ pair l c ⇒ match plus_ex_dc_dc e3 e1 c with [ pair h c' ⇒ pair … 〈h,l〉 c' ]]);
 198  nrewrite > (symmetric_plusex_d_dc e4 e2);
 199  ncases (plus_ex_d_dc e2 e4);
 200  #e5; #c;
 201  nchange with (
 202   match plus_ex_dc_dc e1 e3 c with [ pair h c' ⇒ pair … 〈h,e5〉 c' ] =
 203   match plus_ex_dc_dc e3 e1 c with [ pair h c' ⇒ pair … 〈h,e5〉 c' ]);
 204  nrewrite > (symmetric_plusex_dc_dc e1 e3 c);
 205  napply refl_eq.
 206 nqed.
 207
 208 nlemma symmetric_plusb8_d_d : ∀b1,b2.plus_b8_d_d b1 b2 = plus_b8_d_d b2 b1.
 209  #b1; #b2;
 210  nelim b1;
 211  #e1; #e2;
 212  nelim b2;
 213  #e3; #e4;
 214  nchange with (
 215   match plus_ex_d_dc e2 e4 with [ pair l c ⇒ 〈plus_ex_dc_d e1 e3 c,l〉 ] =
 216   match plus_ex_d_dc e4 e2 with [ pair l c ⇒ 〈plus_ex_dc_d e3 e1 c,l〉 ]);
 217  nrewrite > (symmetric_plusex_d_dc e4 e2);
 218  ncases (plus_ex_d_dc e2 e4);
 219  #e5; #c;
 220  nchange with (〈plus_ex_dc_d e1 e3 c,e5〉 = 〈plus_ex_dc_d e3 e1 c,e5〉);
 221  nrewrite > (symmetric_plusex_dc_d e1 e3 c);
 222  napply refl_eq.
 223 nqed.
 224
 225 nlemma symmetric_plusb8_d_c : ∀b1,b2.plus_b8_d_c b1 b2 = plus_b8_d_c b2 b1.
 226  #b1; #b2;
 227  nelim b1;
 228  #e1; #e2;
 229  nelim b2;
 230  #e3; #e4;
 231  nchange with (
 232   plus_ex_dc_c e1 e3 (plus_ex_d_c e2 e4) =
 233   plus_ex_dc_c e3 e1 (plus_ex_d_c e4 e2));
 234  nrewrite > (symmetric_plusex_d_c e4 e2);
 235  nrewrite > (symmetric_plusex_dc_c e3 e1 (plus_ex_d_c e2 e4));
 236  napply refl_eq.
 237 nqed.
 238
 239 nlemma symmetric_mulex : symmetricT exadecim byte8 mul_ex.
 240  #e1; #e2;
 241  nelim e1;
 242  nelim e2;
 243  nnormalize;
 244  napply refl_eq.
 245 nqed.
 246
 247 nlemma eqb8_to_eq : ∀b1,b2:byte8.(eq_b8 b1 b2 = true) → (b1 = b2).
 248  #b1; #b2;
 249  nelim b1;
 250  nelim b2;
 251  #e1; #e2; #e3; #e4;
 252  nchange in ⊢ (% → ?) with (((eq_ex e3 e1)⊗(eq_ex e4 e2)) = true);
 253  #H;
 254  nrewrite < (eqex_to_eq … (andb_true_true_l … H));
 255  nrewrite < (eqex_to_eq … (andb_true_true_r … H));
 256  napply refl_eq.
 257 nqed.
 258
 259 nlemma eq_to_eqb8 : ∀b1,b2.b1 = b2 → eq_b8 b1 b2 = true.
 260  #b1; #b2;
 261  nelim b1;
 262  nelim b2;
 263  #e1; #e2; #e3; #e4;
 264  #H;
 265  nrewrite < (byte8_destruct_1 … H);
 266  nrewrite < (byte8_destruct_2 … H);
 267  nchange with (((eq_ex e3 e3)⊗(eq_ex e4 e4)) = true);
 268  nrewrite > (eq_to_eqex e3 e3 (refl_eq …));
 269  nrewrite > (eq_to_eqex e4 e4 (refl_eq …));
 270  nnormalize;
 271  napply refl_eq.
 272 nqed.
 273
 274 nlemma decidable_b8_aux1 : ∀e1,e2,e3,e4.e1 ≠ e3 → 〈e1,e2〉 ≠ 〈e3,e4〉.
 275  #e1; #e2; #e3; #e4;
 276  nnormalize; #H; #H1;
 277  napply (H (byte8_destruct_1 … H1)).
 278 nqed.
 279
 280 nlemma decidable_b8_aux2 : ∀e1,e2,e3,e4.e2 ≠ e4 → 〈e1,e2〉 ≠ 〈e3,e4〉.
 281  #e1; #e2; #e3; #e4;
 282  nnormalize; #H; #H1;
 283  napply (H (byte8_destruct_2 … H1)).
 284 nqed.
 285
 286 nlemma decidable_b8 : ∀x,y:byte8.decidable (x = y).
 287  #x; nelim x; #e1; #e2;
 288  #y; nelim y; #e3; #e4;
 289  nnormalize;
 290  napply (or2_elim (e1 = e3) (e1 ≠ e3) ? (decidable_ex e1 e3) …);
 291  ##[ ##2: #H; napply (or2_intro2 … (decidable_b8_aux1 e1 e2 e3 e4 H))
 292  ##| ##1: #H; napply (or2_elim (e2 = e4) (e2 ≠ e4) ? (decidable_ex e2 e4) …);
 293           ##[ ##2: #H1; napply (or2_intro2 … (decidable_b8_aux2 e1 e2 e3 e4 H1))
 294           ##| ##1: #H1; nrewrite > H; nrewrite > H1;
 295                         napply (or2_intro1 … (refl_eq ? 〈e3,e4〉))
 296           ##]
 297  ##]
 298 nqed.
 299
 300 nlemma neqb8_to_neq : ∀b1,b2:byte8.(eq_b8 b1 b2 = false) → (b1 ≠ b2).
 301  #b1; #b2;
 302  nelim b1;
 303  nelim b2;
 304  #e1; #e2; #e3; #e4;
 305  nchange with ((((eq_ex e3 e1) ⊗ (eq_ex e4 e2)) = false) → ?);
 306  #H;
 307  napply (or2_elim ((eq_ex e3 e1) = false) ((eq_ex e4 e2) = false) ? (andb_false2 … H) …);
 308  ##[ ##1: #H1; napply (decidable_b8_aux1 … (neqex_to_neq … H1))
 309  ##| ##2: #H1; napply (decidable_b8_aux2 … (neqex_to_neq … H1))
 310  ##]
 311 nqed.
 312
 313 nlemma byte8_destruct : ∀e1,e2,e3,e4.〈e1,e2〉 ≠ 〈e3,e4〉 → e1 ≠ e3 ∨ e2 ≠ e4.
 314  #e1; #e2; #e3; #e4;
 315  nnormalize; #H;
 316  napply (or2_elim (e1 = e3) (e1 ≠ e3) ? (decidable_ex e1 e3) …);
 317  ##[ ##2: #H1; napply (or2_intro1 … H1)
 318  ##| ##1: #H1; napply (or2_elim (e2 = e4) (e2 ≠ e4) ? (decidable_ex e2 e4) …);
 319           ##[ ##2: #H2; napply (or2_intro2 … H2)
 320           ##| ##1: #H2; nrewrite > H1 in H:(%);
 321                    nrewrite > H2;
 322                    #H; nelim (H (refl_eq …))
 323           ##]
 324  ##]
 325 nqed.
 326
 327 nlemma neq_to_neqb8 : ∀b1,b2.b1 ≠ b2 → eq_b8 b1 b2 = false.
 328  #b1; #b2;
 329  nelim b1; #e1; #e2;
 330  nelim b2; #e3; #e4;
 331  #H; nchange with (((eq_ex e1 e3) ⊗ (eq_ex e2 e4)) = false);
 332  napply (or2_elim (e1 ≠ e3) (e2 ≠ e4) ? (byte8_destruct … H) …);
 333  ##[ ##1: #H1; nrewrite > (neq_to_neqex … H1); nnormalize; napply refl_eq
 334  ##| ##2: #H1; nrewrite > (neq_to_neqex … H1);
 335           nrewrite > (symmetric_andbool (eq_ex e1 e3) false);
 336           nnormalize; napply refl_eq
 337  ##]
 338 nqed.