helm/software/matita/contribs/ng_assembly/num/word24_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 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "num/byte8_lemmas.ma".
  24 include "num/word24.ma".
  25
  26 (* **** *)
  27 (* BYTE *)
  28 (* **** *)
  29
  30 nlemma word24_destruct_1 :
  31 ∀x1,x2,y1,y2,z1,z2.
  32  mk_word24 x1 y1 z1 = mk_word24 x2 y2 z2 → x1 = x2.
  33  #x1; #x2; #y1; #y2; #z1; #z2; #H;
  34  nchange with (match mk_word24 x2 y2 z2 with [ mk_word24 a _ _ ⇒ x1 = a ]);
  35  nrewrite < H;
  36  nnormalize;
  37  napply refl_eq.
  38 nqed.
  39
  40 nlemma word24_destruct_2 :
  41 ∀x1,x2,y1,y2,z1,z2.
  42  mk_word24 x1 y1 z1 = mk_word24 x2 y2 z2 → y1 = y2.
  43  #x1; #x2; #y1; #y2; #z1; #z2; #H;
  44  nchange with (match mk_word24 x2 y2 z2 with [ mk_word24 _ a _ ⇒ y1 = a ]);
  45  nrewrite < H;
  46  nnormalize;
  47  napply refl_eq.
  48 nqed.
  49
  50 nlemma word24_destruct_3 :
  51 ∀x1,x2,y1,y2,z1,z2.
  52  mk_word24 x1 y1 z1 = mk_word24 x2 y2 z2 → z1 = z2.
  53  #x1; #x2; #y1; #y2; #z1; #z2; #H;
  54  nchange with (match mk_word24 x2 y2 z2 with [ mk_word24 _ _ a ⇒ z1 = a ]);
  55  nrewrite < H;
  56  nnormalize;
  57  napply refl_eq.
  58 nqed.
  59
  60 nlemma symmetric_eqw24 : symmetricT word24 bool eq_w24.
  61  #b1; nelim b1; #e1; #e2; #e3;
  62  #b2; nelim b2; #e4; #e5; #e6;
  63  nchange with (((eq_b8 e1 e4)⊗(eq_b8 e2 e5)⊗(eq_b8 e3 e6)) = ((eq_b8 e4 e1)⊗(eq_b8 e5 e2)⊗(eq_b8 e6 e3)));
  64  nrewrite > (symmetric_eqb8 e1 e4);
  65  nrewrite > (symmetric_eqb8 e2 e5);
  66  nrewrite > (symmetric_eqb8 e3 e6);
  67  napply refl_eq.
  68 nqed.
  69
  70 nlemma eqw24_to_eq : ∀b1,b2.(eq_w24 b1 b2 = true) → (b1 = b2).
  71  #b1; nelim b1; #e1; #e2; #e3;
  72  #b2; nelim b2; #e4; #e5; #e6;
  73  nchange in ⊢ (% → ?) with (((eq_b8 e1 e4)⊗(eq_b8 e2 e5)⊗(eq_b8 e3 e6)) = true);
  74  #H;
  75  nrewrite < (eqb8_to_eq … (andb_true_true_r … H));
  76  nrewrite < (eqb8_to_eq … (andb_true_true_r … (andb_true_true_l … H)));
  77  nrewrite < (eqb8_to_eq … (andb_true_true_l … (andb_true_true_l … H)));
  78  napply refl_eq.
  79 nqed.
  80
  81 nlemma eq_to_eqw24 : ∀b1,b2.(b1 = b2) → (eq_w24 b1 b2 = true).
  82  #b1; nelim b1; #e1; #e2; #e3;
  83  #b2; nelim b2; #e4; #e5; #e6;
  84  #H;
  85  nchange with (((eq_b8 e1 e4)⊗(eq_b8 e2 e5)⊗(eq_b8 e3 e6)) = true);
  86  nrewrite < (word24_destruct_1 … H);
  87  nrewrite < (word24_destruct_2 … H);
  88  nrewrite < (word24_destruct_3 … H);
  89  nrewrite > (eq_to_eqb8 e1 e1 (refl_eq …));
  90  nrewrite > (eq_to_eqb8 e2 e2 (refl_eq …));
  91  nrewrite > (eq_to_eqb8 e3 e3 (refl_eq …));
  92  nnormalize;
  93  napply refl_eq.
  94 nqed.
  95
  96 nlemma decidable_w24_aux1 :
  97 ∀e1,e2,e3,e4,e5,e6.e1 ≠ e4 → (mk_word24 e1 e2 e3) ≠ (mk_word24 e4 e5 e6).
  98  #e1; #e2; #e3; #e4; #e5; #e6;
  99  nnormalize; #H; #H1;
 100  napply (H (word24_destruct_1 … H1)).
 101 nqed.
 102
 103 nlemma decidable_w24_aux2 :
 104 ∀e1,e2,e3,e4,e5,e6.e2 ≠ e5 → (mk_word24 e1 e2 e3) ≠ (mk_word24 e4 e5 e6).
 105  #e1; #e2; #e3; #e4; #e5; #e6;
 106  nnormalize; #H; #H1;
 107  napply (H (word24_destruct_2 … H1)).
 108 nqed.
 109
 110 nlemma decidable_w24_aux3 :
 111 ∀e1,e2,e3,e4,e5,e6.e3 ≠ e6 → (mk_word24 e1 e2 e3) ≠ (mk_word24 e4 e5 e6).
 112  #e1; #e2; #e3; #e4; #e5; #e6;
 113  nnormalize; #H; #H1;
 114  napply (H (word24_destruct_3 … H1)).
 115 nqed.
 116
 117 nlemma decidable_w24 : ∀b1,b2:word24.(decidable (b1 = b2)).
 118  #b1; nelim b1; #e1; #e2; #e3;
 119  #b2; nelim b2; #e4; #e5; #e6;
 120  nnormalize;
 121  napply (or2_elim (e1 = e4) (e1 ≠ e4) ? (decidable_b8 e1 e4) …);
 122  ##[ ##2: #H; napply (or2_intro2 … (decidable_w24_aux1 e1 e2 e3 e4 e5 e6 H))
 123  ##| ##1: #H; napply (or2_elim (e2 = e5) (e2 ≠ e5) ? (decidable_b8 e2 e5) …);
 124           ##[ ##2: #H1; napply (or2_intro2 … (decidable_w24_aux2 e1 e2 e3 e4 e5 e6 H1))
 125           ##| ##1: #H1; napply (or2_elim (e3 = e6) (e3 ≠ e6) ? (decidable_b8 e3 e6) …);
 126                    ##[ ##2: #H2; napply (or2_intro2 … (decidable_w24_aux3 e1 e2 e3 e4 e5 e6 H2))
 127                    ##| ##1: #H2; nrewrite > H; nrewrite > H1; nrewrite > H2;
 128                                  napply (or2_intro1 … (refl_eq ? (mk_word24 e4 e5 e6)))
 129                    ##]
 130           ##]
 131  ##]
 132 nqed.
 133
 134 nlemma neqw24_to_neq : ∀b1,b2.(eq_w24 b1 b2 = false) → (b1 ≠ b2).
 135  #b1; nelim b1; #e1; #e2; #e3;
 136  #b2; nelim b2; #e4; #e5; #e6;
 137  #H;
 138  nchange in H:(%) with (((eq_b8 e1 e4)⊗(eq_b8 e2 e5)⊗(eq_b8 e3 e6)) = false);
 139  #H1;
 140  nrewrite > (word24_destruct_1 … H1) in H:(%);
 141  nrewrite > (word24_destruct_2 … H1);
 142  nrewrite > (word24_destruct_3 … H1);
 143  nrewrite > (eq_to_eqb8 e4 e4 (refl_eq …));
 144  nrewrite > (eq_to_eqb8 e5 e5 (refl_eq …));
 145  nrewrite > (eq_to_eqb8 e6 e6 (refl_eq …));
 146  #H; ndestruct.
 147 nqed.
 148
 149 nlemma word24_destruct :
 150 ∀e1,e2,e3,e4,e5,e6.
 151  ((mk_word24 e1 e2 e3) ≠ (mk_word24 e4 e5 e6)) →
 152  (Or3 (e1 ≠ e4) (e2 ≠ e5) (e3 ≠ e6)).
 153  #e1; #e2; #e3; #e4; #e5; #e6;
 154  nnormalize; #H;
 155  napply (or2_elim (e1 = e4) (e1 ≠ e4) ? (decidable_b8 e1 e4) …);
 156  ##[ ##2: #H1; napply (or3_intro1 … H1)
 157  ##| ##1: #H1; napply (or2_elim (e2 = e5) (e2 ≠ e5) ? (decidable_b8 e2 e5) …);
 158           ##[ ##2: #H2; napply (or3_intro2 … H2)
 159           ##| ##1: #H2; napply (or2_elim (e3 = e6) (e3 ≠ e6) ? (decidable_b8 e3 e6) …);
 160                    ##[ ##2: #H3; napply (or3_intro3 … H3)
 161                    ##| ##1: #H3; nrewrite > H1 in H:(%);
 162                             nrewrite > H2; nrewrite > H3;
 163                             #H; nelim (H (refl_eq …))
 164                    ##]
 165           ##]
 166  ##]
 167 nqed.
 168
 169 nlemma neq_to_neqw24 : ∀b1,b2.((b1 ≠ b2) → (eq_w24 b1 b2 = false)).
 170  #b1; nelim b1; #e1; #e2; #e3;
 171  #b2; nelim b2; #e4; #e5; #e6;
 172  #H; nchange with (((eq_b8 e1 e4)⊗(eq_b8 e2 e5)⊗(eq_b8 e3 e6)) = false);
 173  napply (or3_elim (e1 ≠ e4) (e2 ≠ e5) (e3 ≠ e6) ? (word24_destruct e1 e2 e3 e4 e5 e6 … H) …);
 174  ##[ ##1: #H1; nrewrite > (neq_to_neqb8 e1 e4 H1); nnormalize; napply refl_eq
 175  ##| ##2: #H1; nrewrite > (neq_to_neqb8 e2 e5 H1);
 176           nrewrite > (symmetric_andbool (eq_b8 e1 e4) …);
 177           nnormalize; napply refl_eq
 178  ##| ##3: #H1; nrewrite > (neq_to_neqb8 e3 e6 H1);
 179           nrewrite > (symmetric_andbool ((eq_b8 e1 e4)⊗(eq_b8 e2 e5)) …);
 180           nnormalize; napply refl_eq
 181  ##]
 182 nqed.