matitaB/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 ndefinition succ_w24 ≝
  48 λw.match eqc ? (predc ? (zeroc ?)) (w24l w) with
  49  [ true ⇒ match eqc ? (predc ? (zeroc ?)) (w24h w) with
  50   [ true ⇒ 〈(succc ? (w24x w));(succc ? (w24h w));(succc ? (w24l w))〉
  51   | false ⇒ 〈(w24x w);(succc ? (w24h w));(succc ? (w24l w))〉 ]
  52  | false ⇒ 〈(w24x w);(w24h w);(succc ? (w24l w))〉 ].
  53
  54 nlemma word24_destruct_1 :
  55 ∀x1,x2,y1,y2,z1,z2.
  56  mk_word24 x1 y1 z1 = mk_word24 x2 y2 z2 → x1 = x2.
  57  #x1; #x2; #y1; #y2; #z1; #z2; #H;
  58  nchange with (match mk_word24 x2 y2 z2 with [ mk_word24 a _ _ ⇒ x1 = a ]);
  59  nrewrite < H;
  60  nnormalize;
  61  napply refl_eq.
  62 nqed.
  63
  64 nlemma word24_destruct_2 :
  65 ∀x1,x2,y1,y2,z1,z2.
  66  mk_word24 x1 y1 z1 = mk_word24 x2 y2 z2 → y1 = y2.
  67  #x1; #x2; #y1; #y2; #z1; #z2; #H;
  68  nchange with (match mk_word24 x2 y2 z2 with [ mk_word24 _ a _ ⇒ y1 = a ]);
  69  nrewrite < H;
  70  nnormalize;
  71  napply refl_eq.
  72 nqed.
  73
  74 nlemma word24_destruct_3 :
  75 ∀x1,x2,y1,y2,z1,z2.
  76  mk_word24 x1 y1 z1 = mk_word24 x2 y2 z2 → z1 = z2.
  77  #x1; #x2; #y1; #y2; #z1; #z2; #H;
  78  nchange with (match mk_word24 x2 y2 z2 with [ mk_word24 _ _ a ⇒ z1 = a ]);
  79  nrewrite < H;
  80  nnormalize;
  81  napply refl_eq.
  82 nqed.
  83
  84 nlemma symmetric_eqw24 : symmetricT word24 bool eq_w24.
  85  #b1; nelim b1; #e1; #e2; #e3;
  86  #b2; nelim b2; #e4; #e5; #e6;
  87  nchange with (((eqc ? e1 e4)⊗(eqc ? e2 e5)⊗(eqc ? e3 e6)) = ((eqc ? e4 e1)⊗(eqc ? e5 e2)⊗(eqc ? e6 e3)));
  88  nrewrite > (symmetric_eqc ? e1 e4);
  89  nrewrite > (symmetric_eqc ? e2 e5);
  90  nrewrite > (symmetric_eqc ? e3 e6);
  91  napply refl_eq.
  92 nqed.
  93
  94 nlemma eqw24_to_eq : ∀b1,b2.(eq_w24 b1 b2 = true) → (b1 = b2).
  95  #b1; nelim b1; #e1; #e2; #e3;
  96  #b2; nelim b2; #e4; #e5; #e6;
  97  nchange in ⊢ (% → ?) with (((eqc ? e1 e4)⊗(eqc ? e2 e5)⊗(eqc ? e3 e6)) = true);
  98  #H;
  99  nrewrite < (eqc_to_eq … (andb_true_true_r … H));
 100  nrewrite < (eqc_to_eq … (andb_true_true_r … (andb_true_true_l … H)));
 101  nrewrite < (eqc_to_eq … (andb_true_true_l … (andb_true_true_l … H)));
 102  napply refl_eq.
 103 nqed.
 104
 105 nlemma eq_to_eqw24 : ∀b1,b2.(b1 = b2) → (eq_w24 b1 b2 = true).
 106  #b1; nelim b1; #e1; #e2; #e3;
 107  #b2; nelim b2; #e4; #e5; #e6;
 108  #H;
 109  nchange with (((eqc ? e1 e4)⊗(eqc ? e2 e5)⊗(eqc ? e3 e6)) = true);
 110  nrewrite < (word24_destruct_1 … H);
 111  nrewrite < (word24_destruct_2 … H);
 112  nrewrite < (word24_destruct_3 … H);
 113  nrewrite > (eq_to_eqc ? e1 e1 (refl_eq …));
 114  nrewrite > (eq_to_eqc ? e2 e2 (refl_eq …));
 115  nrewrite > (eq_to_eqc ? e3 e3 (refl_eq …));
 116  nnormalize;
 117  napply refl_eq.
 118 nqed.
 119
 120 nlemma decidable_w24_aux1 :
 121 ∀e1,e2,e3,e4,e5,e6.e1 ≠ e4 → (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_1 … H1)).
 125 nqed.
 126
 127 nlemma decidable_w24_aux2 :
 128 ∀e1,e2,e3,e4,e5,e6.e2 ≠ e5 → (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_2 … H1)).
 132 nqed.
 133
 134 nlemma decidable_w24_aux3 :
 135 ∀e1,e2,e3,e4,e5,e6.e3 ≠ e6 → (mk_word24 e1 e2 e3) ≠ (mk_word24 e4 e5 e6).
 136  #e1; #e2; #e3; #e4; #e5; #e6;
 137  nnormalize; #H; #H1;
 138  napply (H (word24_destruct_3 … H1)).
 139 nqed.
 140
 141 nlemma decidable_w24 : ∀b1,b2:word24.(decidable (b1 = b2)).
 142  #b1; nelim b1; #e1; #e2; #e3;
 143  #b2; nelim b2; #e4; #e5; #e6;
 144  nnormalize;
 145  napply (or2_elim (e1 = e4) (e1 ≠ e4) ? (decidable_c ? e1 e4) …);
 146  ##[ ##2: #H; napply (or2_intro2 … (decidable_w24_aux1 e1 e2 e3 e4 e5 e6 H))
 147  ##| ##1: #H; napply (or2_elim (e2 = e5) (e2 ≠ e5) ? (decidable_c ? e2 e5) …);
 148           ##[ ##2: #H1; napply (or2_intro2 … (decidable_w24_aux2 e1 e2 e3 e4 e5 e6 H1))
 149           ##| ##1: #H1; napply (or2_elim (e3 = e6) (e3 ≠ e6) ? (decidable_c ? e3 e6) …);
 150                    ##[ ##2: #H2; napply (or2_intro2 … (decidable_w24_aux3 e1 e2 e3 e4 e5 e6 H2))
 151                    ##| ##1: #H2; nrewrite > H; nrewrite > H1; nrewrite > H2;
 152                                  napply (or2_intro1 … (refl_eq ? (mk_word24 e4 e5 e6)))
 153                    ##]
 154           ##]
 155  ##]
 156 nqed.
 157
 158 nlemma neqw24_to_neq : ∀b1,b2.(eq_w24 b1 b2 = false) → (b1 ≠ b2).
 159  #b1; nelim b1; #e1; #e2; #e3;
 160  #b2; nelim b2; #e4; #e5; #e6;
 161  #H;
 162  nchange in H:(%) with (((eqc ? e1 e4)⊗(eqc ? e2 e5)⊗(eqc ? e3 e6)) = false);
 163  #H1;
 164  nrewrite > (word24_destruct_1 … H1) in H:(%);
 165  nrewrite > (word24_destruct_2 … H1);
 166  nrewrite > (word24_destruct_3 … H1);
 167  nrewrite > (eq_to_eqc ? e4 e4 (refl_eq …));
 168  nrewrite > (eq_to_eqc ? e5 e5 (refl_eq …));
 169  nrewrite > (eq_to_eqc ? e6 e6 (refl_eq …));
 170  #H; ndestruct.
 171 nqed.
 172
 173 nlemma word24_destruct :
 174 ∀e1,e2,e3,e4,e5,e6.
 175  ((mk_word24 e1 e2 e3) ≠ (mk_word24 e4 e5 e6)) →
 176  (Or3 (e1 ≠ e4) (e2 ≠ e5) (e3 ≠ e6)).
 177  #e1; #e2; #e3; #e4; #e5; #e6;
 178  nnormalize; #H;
 179  napply (or2_elim (e1 = e4) (e1 ≠ e4) ? (decidable_c ? e1 e4) …);
 180  ##[ ##2: #H1; napply (or3_intro1 … H1)
 181  ##| ##1: #H1; napply (or2_elim (e2 = e5) (e2 ≠ e5) ? (decidable_c ? e2 e5) …);
 182           ##[ ##2: #H2; napply (or3_intro2 … H2)
 183           ##| ##1: #H2; napply (or2_elim (e3 = e6) (e3 ≠ e6) ? (decidable_c ? e3 e6) …);
 184                    ##[ ##2: #H3; napply (or3_intro3 … H3)
 185                    ##| ##1: #H3; nrewrite > H1 in H:(%);
 186                             nrewrite > H2; nrewrite > H3;
 187                             #H; nelim (H (refl_eq …))
 188                    ##]
 189           ##]
 190  ##]
 191 nqed.
 192
 193 nlemma neq_to_neqw24 : ∀b1,b2.((b1 ≠ b2) → (eq_w24 b1 b2 = false)).
 194  #b1; nelim b1; #e1; #e2; #e3;
 195  #b2; nelim b2; #e4; #e5; #e6;
 196  #H; nchange with (((eqc ? e1 e4)⊗(eqc ? e2 e5)⊗(eqc ? e3 e6)) = false);
 197  napply (or3_elim (e1 ≠ e4) (e2 ≠ e5) (e3 ≠ e6) ? (word24_destruct e1 e2 e3 e4 e5 e6 … H) …);
 198  ##[ ##1: #H1; nrewrite > (neq_to_neqc ? e1 e4 H1); nnormalize; napply refl_eq
 199  ##| ##2: #H1; nrewrite > (neq_to_neqc ? e2 e5 H1);
 200           nrewrite > (symmetric_andbool (eqc ? e1 e4) …);
 201           nnormalize; napply refl_eq
 202  ##| ##3: #H1; nrewrite > (neq_to_neqc ? e3 e6 H1);
 203           nrewrite > (symmetric_andbool ((eqc ? e1 e4)⊗(eqc ? e2 e5)) …);
 204           nnormalize; napply refl_eq
 205  ##]
 206 nqed.
 207
 208 nlemma word24_is_comparable : comparable.
 209  @ word24
 210   ##[ napply (mk_word24 (zeroc ?) (zeroc ?) (zeroc ?))
 211   ##| napply (λP.forallc ?
 212               (λx.forallc ?
 213                (λh.forallc ?
 214                 (λl.P (mk_word24 x h l)))))
 215   ##| napply eq_w24
 216   ##| napply eqw24_to_eq
 217   ##| napply eq_to_eqw24
 218   ##| napply neqw24_to_neq
 219   ##| napply neq_to_neqw24
 220   ##| napply decidable_w24
 221   ##| napply symmetric_eqw24
 222   ##]
 223 nqed.
 224
 225 unification hint 0 ≔ ⊢ carr word24_is_comparable ≡ word24.