X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fassembly%2Fbyte.ma;h=2bf233ec19d0686ea9b84cd6e06b7cf12dfe18b4;hb=9ff984b29ac963eef2f79521ce9dd7cbb9ae2c59;hp=67eb0b4cf102268ff6d2a8fb741cdad6497065c4;hpb=dd67cb1d7792363f549fc5cd7afdd9af0309b301;p=helm.git diff --git a/matita/library/assembly/byte.ma b/matita/library/assembly/byte.ma index 67eb0b4cf..2bf233ec1 100644 --- a/matita/library/assembly/byte.ma +++ b/matita/library/assembly/byte.ma @@ -14,13 +14,17 @@ set "baseuri" "cic:/matita/assembly/byte". -include "exadecimal.ma". +include "assembly/exadecimal.ma". record byte : Type ≝ { bh: exadecimal; bl: exadecimal }. +notation "〈 x, y 〉" non associative with precedence 80 for @{ 'mk_byte $x $y }. +interpretation "mk_byte" 'mk_byte x y = + (cic:/matita/assembly/byte/byte.ind#xpointer(1/1/1) x y). + definition eqbyte ≝ λb,b'. eqex (bh b) (bh b') ∧ eqex (bl b) (bl b'). @@ -38,6 +42,9 @@ coercion cic:/matita/assembly/byte/nat_of_byte.con. definition byte_of_nat ≝ λn. mk_byte (exadecimal_of_nat (n / 16)) (exadecimal_of_nat n). +interpretation "byte_of_nat" 'byte_of_opcode a = + (cic:/matita/assembly/byte/byte_of_nat.con a). + lemma byte_of_nat_nat_of_byte: ∀b. byte_of_nat (nat_of_byte b) = b. intros; elim b; @@ -59,7 +66,7 @@ lemma lt_nat_of_byte_256: ∀b. nat_of_byte b < 256. [ letin Hf ≝ (le_plus ? ? ? ? Hcut K'); clearbody Hf; simplify in Hf:(? ? %); assumption - | autobatch + | apply le_times_r. apply H'. ] qed. @@ -87,15 +94,31 @@ lemma nat_of_byte_byte_of_nat: ∀n. nat_of_byte (byte_of_nat n) = n \mod 256. ]. qed. -axiom eq_nat_of_byte_n_nat_of_byte_mod_n_256: +lemma eq_nat_of_byte_n_nat_of_byte_mod_n_256: ∀n. byte_of_nat n = byte_of_nat (n \mod 256). + intro; + unfold byte_of_nat; + apply eq_f2; + [ rewrite > exadecimal_of_nat_mod in ⊢ (? ? % ?); + rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %); + apply eq_f; + elim daemon + | rewrite > exadecimal_of_nat_mod; + rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %); + rewrite > divides_to_eq_mod_mod_mod; + [ reflexivity + | apply (witness ? ? 16). reflexivity. + ] + ] +qed. lemma plusbyte_ok: ∀b1,b2,c. match plusbyte b1 b2 c with [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte r + nat_of_bool c' * 256 ]. - intros; + intros; elim daemon. + (* unfold plusbyte; generalize in match (plusex_ok (bl b1) (bl b2) c); elim (plusex (bl b1) (bl b2) c); @@ -127,6 +150,7 @@ lemma plusbyte_ok: rewrite < associative_plus in ⊢ (? ? (? ? (? % ?)) ?); rewrite > H; clear H; autobatch paramodulation. + *) qed. definition bpred ≝ @@ -163,7 +187,12 @@ lemma plusbytenc_O_x: reflexivity. qed. -axiom eq_nat_of_byte_mod: ∀b. nat_of_byte b = nat_of_byte b \mod 256. +lemma eq_nat_of_byte_mod: ∀b. nat_of_byte b = nat_of_byte b \mod 256. + intro; + lapply (lt_nat_of_byte_256 b); + rewrite > (lt_to_eq_mod ? ? Hletin) in ⊢ (? ? ? %); + reflexivity. +qed. theorem plusbytenc_ok: ∀b1,b2:byte. nat_of_byte (plusbytenc b1 b2) = (b1 + b2) \mod 256. @@ -194,11 +223,8 @@ lemma eq_eqbyte_x0_x0_byte_of_nat_S_false: change in ⊢ (? ? (? ? %) ?) with (eqex x0 (exadecimal_of_nat (S b))); rewrite > eq_eqex_S_x0_false; [ elim (eqex (bh (mk_byte x0 x0)) -(bh (mk_byte (exadecimal_of_nat (S b/16)) (exadecimal_of_nat (S b)))));simplify; -(* - alias id "andb_sym" = "cic:/matita/nat/propr_div_mod_lt_le_totient1_aux/andb_sym.con". - rewrite > andb_sym; -*) + (bh (mk_byte (exadecimal_of_nat (S b/16)) (exadecimal_of_nat (S b))))); + simplify; reflexivity | assumption ] @@ -226,7 +252,7 @@ lemma eq_eqbyte_x0_x0_byte_of_nat_S_false: apply lt_mod_m_m;autobatch |rewrite > sym_times; rewrite > sym_times in ⊢ (? ? %); (* just to speed up qed *) - normalize in \vdash (? ? %);apply Hletin; + normalize in ⊢ (? ? %);apply Hletin; ] ] ] @@ -235,20 +261,54 @@ lemma eq_eqbyte_x0_x0_byte_of_nat_S_false: ]. qed. +axiom eq_mod_O_to_exists: ∀n,m. n \mod m = 0 → ∃z. n = z*m. + lemma eq_bpred_S_a_a: ∀a. a < 255 → bpred (byte_of_nat (S a)) = byte_of_nat a. -elim daemon. (* intros; - unfold byte_of_nat; - cut (a \mod 16 = 15 ∨ a \mod 16 < 15); - [ elim Hcut; - [ - | - ] - | autobatch - ].*) + unfold bpred; + apply (bool_elim ? (eqex (bl (byte_of_nat (S a))) x0)); intros; + [ change with (mk_byte (xpred (bh (byte_of_nat (S a)))) (xpred (bl (byte_of_nat (S a)))) + = byte_of_nat a); + rewrite > (eqex_true_to_eq ? ? H1); + normalize in ⊢ (? ? (? ? %) ?); + unfold byte_of_nat; + change with (mk_byte (xpred (exadecimal_of_nat (S a/16))) xF = + mk_byte (exadecimal_of_nat (a/16)) (exadecimal_of_nat a)); + lapply (eqex_true_to_eq ? ? H1); clear H1; + unfold byte_of_nat in Hletin; + change in Hletin with (exadecimal_of_nat (S a) = x0); + lapply (eq_f ? ? nat_of_exadecimal ? ? Hletin); clear Hletin; + normalize in Hletin1:(? ? ? %); + rewrite > nat_of_exadecimal_exadecimal_of_nat in Hletin1; + elim (eq_mod_O_to_exists ? ? Hletin1); clear Hletin1; + rewrite > H1; + rewrite > lt_O_to_div_times; [2: autobatch | ] + lapply (eq_f ? ? (λx.x/16) ? ? H1); + rewrite > lt_O_to_div_times in Hletin; [2: autobatch | ] + lapply (eq_f ? ? (λx.x \mod 16) ? ? H1); + rewrite > eq_mod_times_n_m_m_O in Hletin1; + elim daemon + | change with (mk_byte (bh (byte_of_nat (S a))) (xpred (bl (byte_of_nat (S a)))) + = byte_of_nat a); + unfold byte_of_nat; + change with (mk_byte (exadecimal_of_nat (S a/16)) (xpred (exadecimal_of_nat (S a))) + = mk_byte (exadecimal_of_nat (a/16)) (exadecimal_of_nat a)); + lapply (eqex_false_to_not_eq ? ? H1); + unfold byte_of_nat in Hletin; + change in Hletin with (exadecimal_of_nat (S a) ≠ x0); + cut (nat_of_exadecimal (exadecimal_of_nat (S a)) ≠ 0); + [2: intro; + apply Hletin; + lapply (eq_f ? ? exadecimal_of_nat ? ? H2); + rewrite > exadecimal_of_nat_nat_of_exadecimal in Hletin1; + apply Hletin1 + | ]; + + elim daemon + ] qed. - + lemma plusbytenc_S: ∀x:byte.∀n.plusbytenc (byte_of_nat (x*n)) x = byte_of_nat (x * S n). intros;