X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fnum%2Fbyte8_lemmas.ma;h=38c472806f2cf135c0e96af833ffc254b129843b;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=3fa810b46ce5b5b53565e1570f4b70eae914789d;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/num/byte8_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/byte8_lemmas.ma
index 3fa810b46..38c472806 100755
--- a/helm/software/matita/contribs/ng_assembly/num/byte8_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/byte8_lemmas.ma
@@ -16,27 +16,323 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Sviluppo: 2008-2010                                                  *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
 include "num/byte8.ma".
 include "num/exadecim_lemmas.ma".
-include "num/comp_num_lemmas.ma".
 
 (* **** *)
 (* BYTE *)
 (* **** *)
 
-ndefinition byte8_destruct_1 ≝ cn_destruct_1 byte8.
-ndefinition byte8_destruct_2 ≝ cn_destruct_2 byte8.
+nlemma byte8_destruct_1 :
+∀x1,x2,y1,y2.
+ mk_byte8 x1 y1 = mk_byte8 x2 y2 → x1 = x2.
+ #x1; #x2; #y1; #y2; #H;
+ nchange with (match mk_byte8 x2 y2 with [ mk_byte8 a _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
 
-ndefinition symmetric_eqb8 ≝ symmetric_eqcn ? eq_ex symmetric_eqex.
+nlemma byte8_destruct_2 :
+∀x1,x2,y1,y2.
+ mk_byte8 x1 y1 = mk_byte8 x2 y2 → y1 = y2.
+ #x1; #x2; #y1; #y2; #H;
+ nchange with (match mk_byte8 x2 y2 with [ mk_byte8 _ b ⇒ y1 = b ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
 
-ndefinition eqb8_to_eq ≝ eqcn_to_eq ? eq_ex eqex_to_eq.
-ndefinition eq_to_eqb8 ≝ eq_to_eqcn ? eq_ex eq_to_eqex.
+nlemma symmetric_eqb8 : symmetricT byte8 bool eq_b8.
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ #e1; #e2; #e3; #e4;
+ nchange with (((eq_ex e3 e1)⊗(eq_ex e4 e2)) = ((eq_ex e1 e3)⊗(eq_ex e2 e4)));
+ nrewrite > (symmetric_eqex e1 e3);
+ nrewrite > (symmetric_eqex e2 e4);
+ napply refl_eq.
+nqed. 
 
-ndefinition decidable_b8 ≝ decidable_cn ? decidable_ex.
+nlemma symmetric_andb8 : symmetricT byte8 byte8 and_b8.
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ #e1; #e2; #e3; #e4;
+ nchange with ((mk_byte8 (and_ex e3 e1) (and_ex e4 e2)) = (mk_byte8 (and_ex e1 e3) (and_ex e2 e4)));
+ nrewrite > (symmetric_andex e1 e3);
+ nrewrite > (symmetric_andex e2 e4);
+ napply refl_eq.
+nqed.
 
-ndefinition neqb8_to_neq ≝ neqcn_to_neq ? eq_ex neqex_to_neq.
-ndefinition neq_to_neqb8 ≝ neq_to_neqcn ? eq_ex neq_to_neqex decidable_ex.
+nlemma associative_andb8 : ∀b1,b2,b3.(and_b8 (and_b8 b1 b2) b3) = (and_b8 b1 (and_b8 b2 b3)).
+ #b1; #b2; #b3;
+ nelim b1;
+ #e1; #e2;
+ nelim b2;
+ #e3; #e4;
+ nelim b3;
+ #e5; #e6;
+ nchange with (mk_byte8 (and_ex (and_ex e1 e3) e5) (and_ex (and_ex e2 e4) e6) =
+  mk_byte8 (and_ex e1 (and_ex e3 e5)) (and_ex e2 (and_ex e4 e6)));
+ nrewrite < (associative_andex e1 e3 e5);
+ nrewrite < (associative_andex e2 e4 e6);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_orb8 : symmetricT byte8 byte8 or_b8.
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ #e1; #e2; #e3; #e4;
+ nchange with ((mk_byte8 (or_ex e3 e1) (or_ex e4 e2)) = (mk_byte8 (or_ex e1 e3) (or_ex e2 e4)));
+ nrewrite > (symmetric_orex e1 e3);
+ nrewrite > (symmetric_orex e2 e4);
+ napply refl_eq.
+nqed.
+
+nlemma associative_orb8 : ∀b1,b2,b3.(or_b8 (or_b8 b1 b2) b3) = (or_b8 b1 (or_b8 b2 b3)).
+ #b1; #b2; #b3;
+ nelim b1;
+ #e1; #e2;
+ nelim b2;
+ #e3; #e4;
+ nelim b3;
+ #e5; #e6;
+ nchange with (mk_byte8 (or_ex (or_ex e1 e3) e5) (or_ex (or_ex e2 e4) e6) =
+  mk_byte8 (or_ex e1 (or_ex e3 e5)) (or_ex e2 (or_ex e4 e6)));
+ nrewrite < (associative_orex e1 e3 e5);
+ nrewrite < (associative_orex e2 e4 e6);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_xorb8 : symmetricT byte8 byte8 xor_b8.
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ #e1; #e2; #e3; #e4;
+ nchange with ((mk_byte8 (xor_ex e3 e1) (xor_ex e4 e2)) = (mk_byte8 (xor_ex e1 e3) (xor_ex e2 e4)));
+ nrewrite > (symmetric_xorex e1 e3);
+ nrewrite > (symmetric_xorex e2 e4);
+ napply refl_eq.
+nqed.
+
+nlemma associative_xorb8 : ∀b1,b2,b3.(xor_b8 (xor_b8 b1 b2) b3) = (xor_b8 b1 (xor_b8 b2 b3)).
+ #b1; #b2; #b3;
+ nelim b1;
+ #e1; #e2;
+ nelim b2;
+ #e3; #e4;
+ nelim b3;
+ #e5; #e6;
+ nchange with (mk_byte8 (xor_ex (xor_ex e1 e3) e5) (xor_ex (xor_ex e2 e4) e6) =
+  mk_byte8 (xor_ex e1 (xor_ex e3 e5)) (xor_ex e2 (xor_ex e4 e6)));
+ nrewrite < (associative_xorex e1 e3 e5);
+ nrewrite < (associative_xorex e2 e4 e6);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusb8_dc_dc : ∀b1,b2,c.plus_b8_dc_dc b1 b2 c = plus_b8_dc_dc b2 b1 c.
+ #b1; #b2; #c;
+ nelim b1;
+ #e1; #e2;
+ nelim b2;
+ #e3; #e4;
+ nchange with (
+  match plus_ex_dc_dc e2 e4 c with [ pair l c ⇒ match plus_ex_dc_dc e1 e3 c with [ pair h c' ⇒ pair … 〈h,l〉 c' ]] =
+  match plus_ex_dc_dc e4 e2 c with [ pair l c ⇒ match plus_ex_dc_dc e3 e1 c with [ pair h c' ⇒ pair … 〈h,l〉 c' ]]);
+ nrewrite > (symmetric_plusex_dc_dc e4 e2 c);
+ ncases (plus_ex_dc_dc e2 e4 c);
+ #e5; #c1;
+ nchange with (
+  match plus_ex_dc_dc e1 e3 c1 with [ pair h c' ⇒ pair … 〈h,e5〉 c' ] =
+  match plus_ex_dc_dc e3 e1 c1 with [ pair h c' ⇒ pair … 〈h,e5〉 c' ]);
+ nrewrite > (symmetric_plusex_dc_dc e1 e3 c1);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusb8_dc_d : ∀b1,b2,c.plus_b8_dc_d b1 b2 c = plus_b8_dc_d b2 b1 c.
+ #b1; #b2; #c;
+ nelim b1;
+ #e1; #e2;
+ nelim b2;
+ #e3; #e4;
+ nchange with (
+  match plus_ex_dc_dc e2 e4 c with [ pair l c ⇒ 〈plus_ex_dc_d e1 e3 c,l〉 ] =
+  match plus_ex_dc_dc e4 e2 c with [ pair l c ⇒ 〈plus_ex_dc_d e3 e1 c,l〉 ]);
+ nrewrite > (symmetric_plusex_dc_dc e4 e2 c);
+ ncases (plus_ex_dc_dc e2 e4 c);
+ #e5; #c1;
+ nchange with (〈plus_ex_dc_d e1 e3 c1,e5〉 = 〈plus_ex_dc_d e3 e1 c1,e5〉);
+ nrewrite > (symmetric_plusex_dc_d e1 e3 c1);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusb8_dc_c : ∀b1,b2,c.plus_b8_dc_c b1 b2 c = plus_b8_dc_c b2 b1 c.
+ #b1; #b2; #c;
+ nelim b1;
+ #e1; #e2;
+ nelim b2;
+ #e3; #e4;
+ nchange with (
+  plus_ex_dc_c e1 e3 (plus_ex_dc_c e2 e4 c) =
+  plus_ex_dc_c e3 e1 (plus_ex_dc_c e4 e2 c));
+ nrewrite > (symmetric_plusex_dc_c e4 e2 c);
+ nrewrite > (symmetric_plusex_dc_c e3 e1 (plus_ex_dc_c e2 e4 c));
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusb8_d_dc : ∀b1,b2.plus_b8_d_dc b1 b2 = plus_b8_d_dc b2 b1.
+ #b1; #b2;
+ nelim b1;
+ #e1; #e2;
+ nelim b2;
+ #e3; #e4;
+ nchange with (
+  match plus_ex_d_dc e2 e4 with [ pair l c ⇒ match plus_ex_dc_dc e1 e3 c with [ pair h c' ⇒ pair … 〈h,l〉 c' ]] =
+  match plus_ex_d_dc e4 e2 with [ pair l c ⇒ match plus_ex_dc_dc e3 e1 c with [ pair h c' ⇒ pair … 〈h,l〉 c' ]]);
+ nrewrite > (symmetric_plusex_d_dc e4 e2);
+ ncases (plus_ex_d_dc e2 e4);
+ #e5; #c;
+ nchange with (
+  match plus_ex_dc_dc e1 e3 c with [ pair h c' ⇒ pair … 〈h,e5〉 c' ] =
+  match plus_ex_dc_dc e3 e1 c with [ pair h c' ⇒ pair … 〈h,e5〉 c' ]);
+ nrewrite > (symmetric_plusex_dc_dc e1 e3 c);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusb8_d_d : ∀b1,b2.plus_b8_d_d b1 b2 = plus_b8_d_d b2 b1.
+ #b1; #b2;
+ nelim b1;
+ #e1; #e2;
+ nelim b2;
+ #e3; #e4;
+ nchange with (
+  match plus_ex_d_dc e2 e4 with [ pair l c ⇒ 〈plus_ex_dc_d e1 e3 c,l〉 ] =
+  match plus_ex_d_dc e4 e2 with [ pair l c ⇒ 〈plus_ex_dc_d e3 e1 c,l〉 ]);
+ nrewrite > (symmetric_plusex_d_dc e4 e2);
+ ncases (plus_ex_d_dc e2 e4);
+ #e5; #c;
+ nchange with (〈plus_ex_dc_d e1 e3 c,e5〉 = 〈plus_ex_dc_d e3 e1 c,e5〉);
+ nrewrite > (symmetric_plusex_dc_d e1 e3 c);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusb8_d_c : ∀b1,b2.plus_b8_d_c b1 b2 = plus_b8_d_c b2 b1.
+ #b1; #b2;
+ nelim b1;
+ #e1; #e2;
+ nelim b2;
+ #e3; #e4;
+ nchange with (
+  plus_ex_dc_c e1 e3 (plus_ex_d_c e2 e4) =
+  plus_ex_dc_c e3 e1 (plus_ex_d_c e4 e2));
+ nrewrite > (symmetric_plusex_d_c e4 e2);
+ nrewrite > (symmetric_plusex_dc_c e3 e1 (plus_ex_d_c e2 e4));
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_mulex : symmetricT exadecim byte8 mul_ex.
+ #e1; #e2;
+ nelim e1;
+ nelim e2;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma eqb8_to_eq : ∀b1,b2:byte8.(eq_b8 b1 b2 = true) → (b1 = b2).
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ #e1; #e2; #e3; #e4;
+ nchange in ⊢ (% → ?) with (((eq_ex e3 e1)⊗(eq_ex e4 e2)) = true);
+ #H;
+ nrewrite < (eqex_to_eq … (andb_true_true_l … H));
+ nrewrite < (eqex_to_eq … (andb_true_true_r … H));
+ napply refl_eq.
+nqed. 
+
+nlemma eq_to_eqb8 : ∀b1,b2.b1 = b2 → eq_b8 b1 b2 = true.
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ #e1; #e2; #e3; #e4;
+ #H;
+ nrewrite < (byte8_destruct_1 … H);
+ nrewrite < (byte8_destruct_2 … H);
+ nchange with (((eq_ex e3 e3)⊗(eq_ex e4 e4)) = true);
+ nrewrite > (eq_to_eqex e3 e3 (refl_eq …));
+ nrewrite > (eq_to_eqex e4 e4 (refl_eq …)); 
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma decidable_b8_aux1 : ∀e1,e2,e3,e4.e1 ≠ e3 → 〈e1,e2〉 ≠ 〈e3,e4〉.
+ #e1; #e2; #e3; #e4;
+ nnormalize; #H; #H1;
+ napply (H (byte8_destruct_1 … H1)).
+nqed.
+
+nlemma decidable_b8_aux2 : ∀e1,e2,e3,e4.e2 ≠ e4 → 〈e1,e2〉 ≠ 〈e3,e4〉.
+ #e1; #e2; #e3; #e4;
+ nnormalize; #H; #H1;
+ napply (H (byte8_destruct_2 … H1)).
+nqed.
+
+nlemma decidable_b8 : ∀x,y:byte8.decidable (x = y).
+ #x; nelim x; #e1; #e2;
+ #y; nelim y; #e3; #e4;
+ nnormalize;
+ napply (or2_elim (e1 = e3) (e1 ≠ e3) ? (decidable_ex e1 e3) …);
+ ##[ ##2: #H; napply (or2_intro2 … (decidable_b8_aux1 e1 e2 e3 e4 H))
+ ##| ##1: #H; napply (or2_elim (e2 = e4) (e2 ≠ e4) ? (decidable_ex e2 e4) …);
+          ##[ ##2: #H1; napply (or2_intro2 … (decidable_b8_aux2 e1 e2 e3 e4 H1))
+          ##| ##1: #H1; nrewrite > H; nrewrite > H1;
+                        napply (or2_intro1 … (refl_eq ? 〈e3,e4〉))
+          ##]
+ ##]
+nqed.
+
+nlemma neqb8_to_neq : ∀b1,b2:byte8.(eq_b8 b1 b2 = false) → (b1 ≠ b2).
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ #e1; #e2; #e3; #e4;
+ nchange with ((((eq_ex e3 e1) ⊗ (eq_ex e4 e2)) = false) → ?);
+ #H;
+ napply (or2_elim ((eq_ex e3 e1) = false) ((eq_ex e4 e2) = false) ? (andb_false2 … H) …);
+ ##[ ##1: #H1; napply (decidable_b8_aux1 … (neqex_to_neq … H1))
+ ##| ##2: #H1; napply (decidable_b8_aux2 … (neqex_to_neq … H1))
+ ##]
+nqed.
+
+nlemma byte8_destruct : ∀e1,e2,e3,e4.〈e1,e2〉 ≠ 〈e3,e4〉 → e1 ≠ e3 ∨ e2 ≠ e4.
+ #e1; #e2; #e3; #e4;
+ nnormalize; #H;
+ napply (or2_elim (e1 = e3) (e1 ≠ e3) ? (decidable_ex e1 e3) …);
+ ##[ ##2: #H1; napply (or2_intro1 … H1)
+ ##| ##1: #H1; napply (or2_elim (e2 = e4) (e2 ≠ e4) ? (decidable_ex e2 e4) …);
+          ##[ ##2: #H2; napply (or2_intro2 … H2)
+          ##| ##1: #H2; nrewrite > H1 in H:(%);
+                   nrewrite > H2;
+                   #H; nelim (H (refl_eq …))
+          ##]
+ ##]
+nqed.
+
+nlemma neq_to_neqb8 : ∀b1,b2.b1 ≠ b2 → eq_b8 b1 b2 = false.
+ #b1; #b2;
+ nelim b1; #e1; #e2;
+ nelim b2; #e3; #e4;
+ #H; nchange with (((eq_ex e1 e3) ⊗ (eq_ex e2 e4)) = false);
+ napply (or2_elim (e1 ≠ e3) (e2 ≠ e4) ? (byte8_destruct … H) …);
+ ##[ ##1: #H1; nrewrite > (neq_to_neqex … H1); nnormalize; napply refl_eq
+ ##| ##2: #H1; nrewrite > (neq_to_neqex … H1);
+          nrewrite > (symmetric_andbool (eq_ex e1 e3) false);
+          nnormalize; napply refl_eq
+ ##]
+nqed.