matita/library/assembly/byte.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 set "baseuri" "cic:/matita/assembly/byte".
  16
  17 include "exadecimal.ma".
  18
  19 record byte : Type ≝ {
  20  bh: exadecimal;
  21  bl: exadecimal
  22 }.
  23
  24 definition eqbyte ≝
  25  λb,b'. eqex (bh b) (bh b') ∧ eqex (bl b) (bl b').
  26
  27 definition plusbyte ≝
  28  λb1,b2,c.
  29   match plusex (bl b1) (bl b2) c with
  30    [ couple l c' ⇒
  31       match plusex (bh b1) (bh b2) c' with
  32        [ couple h c'' ⇒ couple ? ? (mk_byte h l) c'' ]].
  33
  34 definition nat_of_byte ≝ λb:byte. 16*(bh b) + (bl b).
  35
  36 coercion cic:/matita/assembly/byte/nat_of_byte.con.
  37
  38 definition byte_of_nat ≝
  39  λn. mk_byte (exadecimal_of_nat (n / 16)) (exadecimal_of_nat n).
  40
  41 lemma byte_of_nat_nat_of_byte: ∀b. byte_of_nat (nat_of_byte b) = b.
  42  intros;
  43  elim b;
  44  elim e;
  45  elim e1;
  46  reflexivity.
  47 qed.
  48
  49 lemma lt_nat_of_byte_256: ∀b. nat_of_byte b < 256.
  50  intro;
  51  unfold nat_of_byte;
  52  letin H ≝ (lt_nat_of_exadecimal_16 (bh b)); clearbody H;
  53  letin K ≝ (lt_nat_of_exadecimal_16 (bl b)); clearbody K;
  54  unfold lt in H K ⊢ %;
  55  letin H' ≝ (le_S_S_to_le ? ? H); clearbody H'; clear H;
  56  letin K' ≝ (le_S_S_to_le ? ? K); clearbody K'; clear K;
  57  apply le_S_S;
  58  cut (16*bh b ≤ 16*15);
  59   [ letin Hf ≝ (le_plus ? ? ? ? Hcut K'); clearbody Hf;
  60     simplify in Hf:(? ? %);
  61     assumption
  62   | autobatch
  63   ]
  64 qed.
  65
  66 lemma nat_of_byte_byte_of_nat: ∀n. nat_of_byte (byte_of_nat n) = n \mod 256.
  67  intro;
  68  letin H ≝ (lt_nat_of_byte_256 (byte_of_nat n)); clearbody H;
  69  rewrite < (lt_to_eq_mod ? ? H); clear H;
  70  unfold byte_of_nat;
  71  unfold nat_of_byte;
  72  change with ((16*(exadecimal_of_nat (n/16)) + exadecimal_of_nat n) \mod 256 = n \mod 256);
  73  letin H ≝ (div_mod n 16 ?); clearbody H; [ autobatch | ];
  74  rewrite > symmetric_times in H;
  75  rewrite > nat_of_exadecimal_exadecimal_of_nat in ⊢ (? ? (? (? % ?) ?) ?);
  76  rewrite > nat_of_exadecimal_exadecimal_of_nat in ⊢ (? ? (? (? ? %) ?) ?);
  77  rewrite > H in ⊢ (? ? ? (? % ?)); clear H;
  78  rewrite > mod_plus in ⊢ (? ? % ?);
  79  rewrite > mod_plus in ⊢ (? ? ? %);
  80  apply eq_mod_to_eq_plus_mod;
  81  rewrite < mod_mod in ⊢ (? ? ? %); [ | autobatch];
  82  rewrite < mod_mod in ⊢ (? ? % ?); [ | autobatch];
  83  rewrite < (eq_mod_times_times_mod ? ? 16 256) in ⊢ (? ? (? % ?) ?); [2: reflexivity | ];
  84  rewrite < mod_mod in ⊢ (? ? % ?);
  85   [ reflexivity
  86   | autobatch
  87   ].
  88 qed.
  89
  90 axiom eq_nat_of_byte_n_nat_of_byte_mod_n_256:
  91  ∀n. byte_of_nat n = byte_of_nat (n \mod 256).
  92
  93 lemma plusbyte_ok:
  94  ∀b1,b2,c.
  95   match plusbyte b1 b2 c with
  96    [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte r + nat_of_bool c' * 256
  97    ].
  98  intros;
  99  unfold plusbyte;
 100  generalize in match (plusex_ok (bl b1) (bl b2) c);
 101  elim (plusex (bl b1) (bl b2) c);
 102  simplify in H ⊢ %;
 103  generalize in match (plusex_ok (bh b1) (bh b2) t1);
 104  elim (plusex (bh b1) (bh b2) t1);
 105  simplify in H1 ⊢ %;
 106  change in ⊢ (? ? ? (? (? % ?) ?)) with (16 * t2);
 107  unfold nat_of_byte;
 108  letin K ≝ (eq_f ? ? (λy.16*y) ? ? H1); clearbody K; clear H1;
 109  rewrite > distr_times_plus in K:(? ? ? %);
 110  rewrite > symmetric_times in K:(? ? ? (? ? (? ? %)));
 111  rewrite < associative_times in K:(? ? ? (? ? %));
 112  normalize in K:(? ? ? (? ? (? % ?)));
 113  rewrite > symmetric_times in K:(? ? ? (? ? %));
 114  rewrite > sym_plus in ⊢ (? ? ? (? % ?));
 115  rewrite > associative_plus in ⊢ (? ? ? %);
 116  letin K' ≝ (eq_f ? ? (plus t) ? ? K); clearbody K'; clear K;
 117   apply transitive_eq; [3: apply K' | skip | ];
 118  clear K';
 119  rewrite > sym_plus in ⊢ (? ? (? (? ? %) ?) ?);
 120  rewrite > associative_plus in ⊢ (? ? (? % ?) ?);
 121  rewrite > associative_plus in ⊢ (? ? % ?);
 122  rewrite > associative_plus in ⊢ (? ? (? ? %) ?);
 123  rewrite > associative_plus in ⊢ (? ? (? ? (? ? %)) ?);
 124  rewrite > sym_plus in ⊢ (? ? (? ? (? ? (? ? %))) ?);
 125  rewrite < associative_plus in ⊢ (? ? (? ? (? ? %)) ?);
 126  rewrite < associative_plus in ⊢ (? ? (? ? %) ?);
 127  rewrite < associative_plus in ⊢ (? ? (? ? (? % ?)) ?);
 128  rewrite > H; clear H;
 129  autobatch paramodulation.
 130 qed.
 131
 132 definition bpred ≝
 133  λb.
 134   match eqex (bl b) x0 with
 135    [ true ⇒ mk_byte (xpred (bh b)) (xpred (bl b))
 136    | false ⇒ mk_byte (bh b) (xpred (bl b))
 137    ].
 138
 139 lemma plusbyte_O_x:
 140  ∀b. plusbyte (mk_byte x0 x0) b false = couple ? ? b false.
 141  intros;
 142  elim b;
 143  elim e;
 144  elim e1;
 145  reflexivity.
 146 qed.
 147
 148 definition plusbytenc ≝
 149  λx,y.
 150   match plusbyte x y false with
 151    [couple res _ ⇒ res].
 152
 153 definition plusbytec ≝
 154  λx,y.
 155   match plusbyte x y false with
 156    [couple _ c ⇒ c].
 157
 158 lemma plusbytenc_O_x:
 159  ∀x. plusbytenc (mk_byte x0 x0) x = x.
 160  intros;
 161  unfold plusbytenc;
 162  rewrite > plusbyte_O_x;
 163  reflexivity.
 164 qed.
 165
 166 axiom eq_nat_of_byte_mod: ∀b. nat_of_byte b = nat_of_byte b \mod 256.
 167
 168 theorem plusbytenc_ok:
 169  ∀b1,b2:byte. nat_of_byte (plusbytenc b1 b2) = (b1 + b2) \mod 256.
 170  intros;
 171  unfold plusbytenc;
 172  generalize in match (plusbyte_ok b1 b2 false);
 173  elim (plusbyte b1 b2 false);
 174  simplify in H ⊢ %;
 175  change with (nat_of_byte t = (b1 + b2) \mod 256);
 176  rewrite < plus_n_O in H;
 177  rewrite > H; clear H;
 178  rewrite > mod_plus;
 179  letin K ≝ (eq_nat_of_byte_mod t); clearbody K;
 180  letin K' ≝ (eq_mod_times_n_m_m_O (nat_of_bool t1) 256 ?); clearbody K';
 181   [ autobatch | ];
 182  autobatch paramodulation.
 183 qed.
 184
 185 lemma eq_eqbyte_x0_x0_byte_of_nat_S_false:
 186  ∀b. b < 255 → eqbyte (mk_byte x0 x0) (byte_of_nat (S b)) = false.
 187  intros;
 188  unfold byte_of_nat;
 189  cut (b < 15 ∨ b ≥ 15);
 190   [ elim Hcut;
 191     [ unfold eqbyte;
 192       change in ⊢ (? ? (? ? %) ?) with (eqex x0 (exadecimal_of_nat (S b)));
 193       rewrite > eq_eqex_S_x0_false;
 194        [ elim (eqex (bh (mk_byte x0 x0))
 195 (bh (mk_byte (exadecimal_of_nat (S b/16)) (exadecimal_of_nat (S b)))));simplify;
 196 (*
 197  alias id "andb_sym" = "cic:/matita/nat/propr_div_mod_lt_le_totient1_aux/andb_sym.con".
 198          rewrite > andb_sym;
 199 *)
 200          reflexivity
 201        | assumption
 202        ]
 203     | unfold eqbyte;
 204       change in ⊢ (? ? (? % ?) ?) with (eqex x0 (exadecimal_of_nat (S b/16)));
 205       letin K ≝ (leq_m_n_to_eq_div_n_m_S (S b) 16 ? ?);
 206        [ autobatch
 207        | unfold in H1;
 208          apply le_S_S;
 209          assumption
 210        | clearbody K;
 211          elim K; clear K;
 212          rewrite > H2;
 213          rewrite > eq_eqex_S_x0_false;
 214           [ reflexivity
 215           | unfold lt;
 216             unfold lt in H;
 217             rewrite < H2;
 218             clear H2; clear a; clear H1; clear Hcut;
 219             elim daemon (* trivial arithmetic property over <= and div *)
 220           ]
 221        ]
 222     ]
 223   | elim daemon
 224   ].
 225 qed.
 226
 227 lemma eq_bpred_S_a_a:
 228  ∀a. a < 255 → bpred (byte_of_nat (S a)) = byte_of_nat a.
 229 elim daemon. (*
 230  intros;
 231  unfold byte_of_nat;
 232  cut (a \mod 16 = 15 ∨ a \mod 16 < 15);
 233   [ elim Hcut;
 234      [
 235      |
 236      ]
 237   | autobatch
 238   ].*)
 239 qed.
 240
 241 lemma plusbytenc_S:
 242  ∀x:byte.∀n.plusbytenc (byte_of_nat (x*n)) x = byte_of_nat (x * S n).
 243  intros;
 244  rewrite < byte_of_nat_nat_of_byte;
 245  rewrite > (plusbytenc_ok (byte_of_nat (x*n)) x);
 246  rewrite < times_n_Sm;
 247  rewrite > mod_plus;
 248  rewrite < eq_nat_of_byte_mod in ⊢ (? ? (? (? (? ? %) ?)) ?);
 249  rewrite > nat_of_byte_byte_of_nat;
 250  rewrite < mod_mod in ⊢ (? ? (? (? (? % ?) ?)) ?);
 251 elim daemon.
 252 qed.
 253
 254 lemma eq_plusbytec_x0_x0_x_false:
 255  ∀x.plusbytec (mk_byte x0 x0) x = false.
 256  intro;
 257  elim x;
 258  elim e;
 259  elim e1;
 260  reflexivity.
 261 qed.