X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fassembly%2Fbyte.ma;h=f2d1dc1566b7194903c2eda58d1eafd853a37ff9;hb=32d8d8d419e0b910435da275361bb55d49bc43a9;hp=1844dc4a7499f41d166bf3c356bcf0ff99252265;hpb=818c8dc98d896d373ff6398b20a19366d4ec79a0;p=helm.git diff --git a/helm/software/matita/library/assembly/byte.ma b/helm/software/matita/library/assembly/byte.ma index 1844dc4a7..f2d1dc156 100644 --- a/helm/software/matita/library/assembly/byte.ma +++ b/helm/software/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,9 +261,10 @@ 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. -(* intros; unfold bpred; apply (bool_elim ? (eqex (bl (byte_of_nat (S a))) x0)); intros; @@ -248,26 +275,40 @@ lemma eq_bpred_S_a_a: 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)); - - - | - change in ⊢ (? ? match ? % ? in bool return ? with [true\rArr ?|false\rArr ?] ?); - unfold byte_of_nat; - unfold bpred; - simplify; -*) -elim daemon. (* - intros; - unfold byte_of_nat; - cut (a \mod 16 = 15 ∨ a \mod 16 < 15); - [ elim Hcut; - [ - | - ] - | autobatch - ].*) + 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 > div_times_ltO; [2: autobatch | ] + lapply (eq_f ? ? (λx.x/16) ? ? H1); + rewrite > div_times_ltO 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;