helm/software/matita/contribs/ng_assembly2/num/word24.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.ma".
  24
  25 (* ********* *)
  26 (* BYTE+WORD *)
  27 (* ********* *)
  28
  29 nrecord word24 : Type ≝
  30  {
  31  w24x: byte8;
  32  w24h: byte8;
  33  w24l: byte8
  34  }.
  35
  36 (* \langle \rangle *)
  37 notation "〈x;y;z〉" non associative with precedence 80
  38  for @{ 'mk_word24 $x $y $z }.
  39 interpretation "mk_word24" 'mk_word24 x y z = (mk_word24 x y z).
  40
  41 (* operatore = *)
  42 ndefinition eq_w24 ≝
  43 λw1,w2.(eqc ? (w24x w1) (w24x w2)) ⊗
  44        (eqc ? (w24h w1) (w24h w2)) ⊗
  45        (eqc ? (w24l w1) (w24l w2)).
  46
  47 nlemma word24_destruct_1 :
  48 ∀x1,x2,y1,y2,z1,z2.
  49  mk_word24 x1 y1 z1 = mk_word24 x2 y2 z2 → x1 = x2.
  50  #x1; #x2; #y1; #y2; #z1; #z2; #H;
  51  nchange with (match mk_word24 x2 y2 z2 with [ mk_word24 a _ _ ⇒ x1 = a ]);
  52  nrewrite < H;
  53  nnormalize;
  54  napply refl_eq.
  55 nqed.
  56
  57 nlemma word24_destruct_2 :
  58 ∀x1,x2,y1,y2,z1,z2.
  59  mk_word24 x1 y1 z1 = mk_word24 x2 y2 z2 → y1 = y2.
  60  #x1; #x2; #y1; #y2; #z1; #z2; #H;
  61  nchange with (match mk_word24 x2 y2 z2 with [ mk_word24 _ a _ ⇒ y1 = a ]);
  62  nrewrite < H;
  63  nnormalize;
  64  napply refl_eq.
  65 nqed.
  66
  67 nlemma word24_destruct_3 :
  68 ∀x1,x2,y1,y2,z1,z2.
  69  mk_word24 x1 y1 z1 = mk_word24 x2 y2 z2 → z1 = z2.
  70  #x1; #x2; #y1; #y2; #z1; #z2; #H;
  71  nchange with (match mk_word24 x2 y2 z2 with [ mk_word24 _ _ a ⇒ z1 = a ]);
  72  nrewrite < H;
  73  nnormalize;
  74  napply refl_eq.
  75 nqed.
  76
  77 nlemma symmetric_eqw24 : symmetricT word24 bool eq_w24.
  78  #b1; nelim b1; #e1; #e2; #e3;
  79  #b2; nelim b2; #e4; #e5; #e6;
  80  nchange with (((eqc ? e1 e4)⊗(eqc ? e2 e5)⊗(eqc ? e3 e6)) = ((eqc ? e4 e1)⊗(eqc ? e5 e2)⊗(eqc ? e6 e3)));
  81  nrewrite > (symmetric_eqc ? e1 e4);
  82  nrewrite > (symmetric_eqc ? e2 e5);
  83  nrewrite > (symmetric_eqc ? e3 e6);
  84  napply refl_eq.
  85 nqed.
  86
  87 nlemma eqw24_to_eq : ∀b1,b2.(eq_w24 b1 b2 = true) → (b1 = b2).
  88  #b1; nelim b1; #e1; #e2; #e3;
  89  #b2; nelim b2; #e4; #e5; #e6;
  90  nchange in ⊢ (% → ?) with (((eqc ? e1 e4)⊗(eqc ? e2 e5)⊗(eqc ? e3 e6)) = true);
  91  #H;
  92  nrewrite < (eqc_to_eq … (andb_true_true_r … H));
  93  nrewrite < (eqc_to_eq … (andb_true_true_r … (andb_true_true_l … H)));
  94  nrewrite < (eqc_to_eq … (andb_true_true_l … (andb_true_true_l … H)));
  95  napply refl_eq.
  96 nqed.
  97
  98 nlemma eq_to_eqw24 : ∀b1,b2.(b1 = b2) → (eq_w24 b1 b2 = true).
  99  #b1; nelim b1; #e1; #e2; #e3;
 100  #b2; nelim b2; #e4; #e5; #e6;
 101  #H;
 102  nchange with (((eqc ? e1 e4)⊗(eqc ? e2 e5)⊗(eqc ? e3 e6)) = true);
 103  nrewrite < (word24_destruct_1 … H);
 104  nrewrite < (word24_destruct_2 … H);
 105  nrewrite < (word24_destruct_3 … H);
 106  nrewrite > (eq_to_eqc ? e1 e1 (refl_eq …));
 107  nrewrite > (eq_to_eqc ? e2 e2 (refl_eq …));
 108  nrewrite > (eq_to_eqc ? e3 e3 (refl_eq …));
 109  nnormalize;
 110  napply refl_eq.
 111 nqed.
 112
 113 nlemma decidable_w24_aux1 :
 114 ∀e1,e2,e3,e4,e5,e6.e1 ≠ e4 → (mk_word24 e1 e2 e3) ≠ (mk_word24 e4 e5 e6).
 115  #e1; #e2; #e3; #e4; #e5; #e6;
 116  nnormalize; #H; #H1;
 117  napply (H (word24_destruct_1 … H1)).
 118 nqed.
 119
 120 nlemma decidable_w24_aux2 :
 121 ∀e1,e2,e3,e4,e5,e6.e2 ≠ e5 → (mk_word24 e1 e2 e3) ≠ (mk_word24 e4 e5 e6).
 122  #e1; #e2; #e3; #e4; #e5; #e6;
 123  nnormalize; #H; #H1;
 124  napply (H (word24_destruct_2 … H1)).
 125 nqed.
 126
 127 nlemma decidable_w24_aux3 :
 128 ∀e1,e2,e3,e4,e5,e6.e3 ≠ e6 → (mk_word24 e1 e2 e3) ≠ (mk_word24 e4 e5 e6).
 129  #e1; #e2; #e3; #e4; #e5; #e6;
 130  nnormalize; #H; #H1;
 131  napply (H (word24_destruct_3 … H1)).
 132 nqed.
 133
 134 nlemma decidable_w24 : ∀b1,b2:word24.(decidable (b1 = b2)).
 135  #b1; nelim b1; #e1; #e2; #e3;
 136  #b2; nelim b2; #e4; #e5; #e6;
 137  nnormalize;
 138  napply (or2_elim (e1 = e4) (e1 ≠ e4) ? (decidable_c ? e1 e4) …);
 139  ##[ ##2: #H; napply (or2_intro2 … (decidable_w24_aux1 e1 e2 e3 e4 e5 e6 H))
 140  ##| ##1: #H; napply (or2_elim (e2 = e5) (e2 ≠ e5) ? (decidable_c ? e2 e5) …);
 141           ##[ ##2: #H1; napply (or2_intro2 … (decidable_w24_aux2 e1 e2 e3 e4 e5 e6 H1))
 142           ##| ##1: #H1; napply (or2_elim (e3 = e6) (e3 ≠ e6) ? (decidable_c ? e3 e6) …);
 143                    ##[ ##2: #H2; napply (or2_intro2 … (decidable_w24_aux3 e1 e2 e3 e4 e5 e6 H2))
 144                    ##| ##1: #H2; nrewrite > H; nrewrite > H1; nrewrite > H2;
 145                                  napply (or2_intro1 … (refl_eq ? (mk_word24 e4 e5 e6)))
 146                    ##]
 147           ##]
 148  ##]
 149 nqed.
 150
 151 nlemma neqw24_to_neq : ∀b1,b2.(eq_w24 b1 b2 = false) → (b1 ≠ b2).
 152  #b1; nelim b1; #e1; #e2; #e3;
 153  #b2; nelim b2; #e4; #e5; #e6;
 154  #H;
 155  nchange in H:(%) with (((eqc ? e1 e4)⊗(eqc ? e2 e5)⊗(eqc ? e3 e6)) = false);
 156  #H1;
 157  nrewrite > (word24_destruct_1 … H1) in H:(%);
 158  nrewrite > (word24_destruct_2 … H1);
 159  nrewrite > (word24_destruct_3 … H1);
 160  nrewrite > (eq_to_eqc ? e4 e4 (refl_eq …));
 161  nrewrite > (eq_to_eqc ? e5 e5 (refl_eq …));
 162  nrewrite > (eq_to_eqc ? e6 e6 (refl_eq …));
 163  #H; ndestruct.
 164 nqed.
 165
 166 nlemma word24_destruct :
 167 ∀e1,e2,e3,e4,e5,e6.
 168  ((mk_word24 e1 e2 e3) ≠ (mk_word24 e4 e5 e6)) →
 169  (Or3 (e1 ≠ e4) (e2 ≠ e5) (e3 ≠ e6)).
 170  #e1; #e2; #e3; #e4; #e5; #e6;
 171  nnormalize; #H;
 172  napply (or2_elim (e1 = e4) (e1 ≠ e4) ? (decidable_c ? e1 e4) …);
 173  ##[ ##2: #H1; napply (or3_intro1 … H1)
 174  ##| ##1: #H1; napply (or2_elim (e2 = e5) (e2 ≠ e5) ? (decidable_c ? e2 e5) …);
 175           ##[ ##2: #H2; napply (or3_intro2 … H2)
 176           ##| ##1: #H2; napply (or2_elim (e3 = e6) (e3 ≠ e6) ? (decidable_c ? e3 e6) …);
 177                    ##[ ##2: #H3; napply (or3_intro3 … H3)
 178                    ##| ##1: #H3; nrewrite > H1 in H:(%);
 179                             nrewrite > H2; nrewrite > H3;
 180                             #H; nelim (H (refl_eq …))
 181                    ##]
 182           ##]
 183  ##]
 184 nqed.
 185
 186 nlemma neq_to_neqw24 : ∀b1,b2.((b1 ≠ b2) → (eq_w24 b1 b2 = false)).
 187  #b1; nelim b1; #e1; #e2; #e3;
 188  #b2; nelim b2; #e4; #e5; #e6;
 189  #H; nchange with (((eqc ? e1 e4)⊗(eqc ? e2 e5)⊗(eqc ? e3 e6)) = false);
 190  napply (or3_elim (e1 ≠ e4) (e2 ≠ e5) (e3 ≠ e6) ? (word24_destruct e1 e2 e3 e4 e5 e6 … H) …);
 191  ##[ ##1: #H1; nrewrite > (neq_to_neqc ? e1 e4 H1); nnormalize; napply refl_eq
 192  ##| ##2: #H1; nrewrite > (neq_to_neqc ? e2 e5 H1);
 193           nrewrite > (symmetric_andbool (eqc ? e1 e4) …);
 194           nnormalize; napply refl_eq
 195  ##| ##3: #H1; nrewrite > (neq_to_neqc ? e3 e6 H1);
 196           nrewrite > (symmetric_andbool ((eqc ? e1 e4)⊗(eqc ? e2 e5)) …);
 197           nnormalize; napply refl_eq
 198  ##]
 199 nqed.
 200
 201 nlemma word24_is_comparable : comparable.
 202  @ word24
 203   ##[ napply (mk_word24 (zeroc ?) (zeroc ?) (zeroc ?))
 204   ##| napply (λP.forallc ?
 205               (λx.forallc ?
 206                (λh.forallc ?
 207                 (λl.P (mk_word24 x h l)))))
 208   ##| napply eq_w24
 209   ##| napply eqw24_to_eq
 210   ##| napply eq_to_eqw24
 211   ##| napply neqw24_to_neq
 212   ##| napply neq_to_neqw24
 213   ##| napply decidable_w24
 214   ##| napply symmetric_eqw24
 215   ##]
 216 nqed.
 217
 218 unification hint 0 ≔ ⊢ carr word24_is_comparable ≡ word24.