(* Progetto FreeScale *)
(* *)
(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Ultima modifica: 05/08/2009 *)
+(* Sviluppo: 2008-2010 *)
(* *)
(* ********************************************************************** *)
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' ]]);
+ 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' ]);
+ 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.
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〉 ]);
+ 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;
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' ]]);
+ 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' ]);
+ 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.
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〉 ]);
+ 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;
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.