(* ********************************************************************** *)
(* Progetto FreeScale *)
(* *)
-(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Ultima modifica: 05/08/2009 *)
(* *)
(* ********************************************************************** *)
nelim w2;
#b3; #b4;
nchange with (
- match plus_b8_dc_dc b2 b4 c with
- [ pair l c ⇒ match plus_b8_dc_dc b1 b3 c with
- [ pair h c' ⇒ pair … 〈h:l〉 c' ]] =
- match plus_b8_dc_dc b4 b2 c with
- [ pair l c ⇒ match plus_b8_dc_dc b3 b1 c with
- [ pair h c' ⇒ pair … 〈h:l〉 c' ]]);
+ match plus_b8_dc_dc b2 b4 c with [ pair l c ⇒ match plus_b8_dc_dc b1 b3 c with [ pair h c' ⇒ pair … 〈h:l〉 c' ]] =
+ match plus_b8_dc_dc b4 b2 c with [ pair l c ⇒ match plus_b8_dc_dc b3 b1 c with [ pair h c' ⇒ pair … 〈h:l〉 c' ]]);
nrewrite > (symmetric_plusb8_dc_dc b4 b2 c);
ncases (plus_b8_dc_dc b2 b4 c);
#b5; #c1;
nchange with (
- match plus_b8_dc_dc b1 b3 c1 with
- [ pair h c' ⇒ pair … 〈h:b5〉 c' ] =
- match plus_b8_dc_dc b3 b1 c1 with
- [ pair h c' ⇒ pair … 〈h:b5〉 c' ]);
+ match plus_b8_dc_dc b1 b3 c1 with [ pair h c' ⇒ pair … 〈h:b5〉 c' ] =
+ match plus_b8_dc_dc b3 b1 c1 with [ pair h c' ⇒ pair … 〈h:b5〉 c' ]);
nrewrite > (symmetric_plusb8_dc_dc b1 b3 c1);
napply refl_eq.
nqed.
nelim w2;
#b3; #b4;
nchange with (
- match plus_b8_dc_dc b2 b4 c with
- [ pair l c ⇒ 〈plus_b8_dc_d b1 b3 c:l〉 ] =
- match plus_b8_dc_dc b4 b2 c with
- [ pair l c ⇒ 〈plus_b8_dc_d b3 b1 c:l〉 ]);
+ match plus_b8_dc_dc b2 b4 c with [ pair l c ⇒ 〈plus_b8_dc_d b1 b3 c:l〉 ] =
+ match plus_b8_dc_dc b4 b2 c with [ pair l c ⇒ 〈plus_b8_dc_d b3 b1 c:l〉 ]);
nrewrite > (symmetric_plusb8_dc_dc b4 b2 c);
ncases (plus_b8_dc_dc b2 b4 c);
#b5; #c1;
nelim w2;
#b3; #b4;
nchange with (
- match plus_b8_d_dc b2 b4 with
- [ pair l c ⇒ match plus_b8_dc_dc b1 b3 c with
- [ pair h c' ⇒ pair … 〈h:l〉 c' ]] =
- match plus_b8_d_dc b4 b2 with
- [ pair l c ⇒ match plus_b8_dc_dc b3 b1 c with
- [ pair h c' ⇒ pair … 〈h:l〉 c' ]]);
+ match plus_b8_d_dc b2 b4 with [ pair l c ⇒ match plus_b8_dc_dc b1 b3 c with [ pair h c' ⇒ pair … 〈h:l〉 c' ]] =
+ match plus_b8_d_dc b4 b2 with [ pair l c ⇒ match plus_b8_dc_dc b3 b1 c with [ pair h c' ⇒ pair … 〈h:l〉 c' ]]);
nrewrite > (symmetric_plusb8_d_dc b4 b2);
ncases (plus_b8_d_dc b2 b4);
#b5; #c;
nchange with (
- match plus_b8_dc_dc b1 b3 c with
- [ pair h c' ⇒ pair … 〈h:b5〉 c' ] =
- match plus_b8_dc_dc b3 b1 c with
- [ pair h c' ⇒ pair … 〈h:b5〉 c' ]);
+ match plus_b8_dc_dc b1 b3 c with [ pair h c' ⇒ pair … 〈h:b5〉 c' ] =
+ match plus_b8_dc_dc b3 b1 c with [ pair h c' ⇒ pair … 〈h:b5〉 c' ]);
nrewrite > (symmetric_plusb8_dc_dc b1 b3 c);
napply refl_eq.
nqed.
nelim w2;
#b3; #b4;
nchange with (
- match plus_b8_d_dc b2 b4 with
- [ pair l c ⇒ 〈plus_b8_dc_d b1 b3 c:l〉 ] =
- match plus_b8_d_dc b4 b2 with
- [ pair l c ⇒ 〈plus_b8_dc_d b3 b1 c:l〉 ]);
+ match plus_b8_d_dc b2 b4 with [ pair l c ⇒ 〈plus_b8_dc_d b1 b3 c:l〉 ] =
+ match plus_b8_d_dc b4 b2 with [ pair l c ⇒ 〈plus_b8_dc_d b3 b1 c:l〉 ]);
nrewrite > (symmetric_plusb8_d_dc b4 b2);
ncases (plus_b8_d_dc b2 b4);
#b5; #c;
nnormalize;
napply refl_eq.
nqed.
+
+nlemma decidable_w16_aux1 : ∀b1,b2,b3,b4.b1 ≠ b3 → 〈b1:b2〉 ≠ 〈b3:b4〉.
+ #b1; #b2; #b3; #b4;
+ nnormalize; #H; #H1;
+ napply (H (word16_destruct_1 … H1)).
+nqed.
+
+nlemma decidable_w16_aux2 : ∀b1,b2,b3,b4.b2 ≠ b4 → 〈b1:b2〉 ≠ 〈b3:b4〉.
+ #b1; #b2; #b3; #b4;
+ nnormalize; #H; #H1;
+ napply (H (word16_destruct_2 … H1)).
+nqed.
+
+nlemma decidable_w16 : ∀x,y:word16.decidable (x = y).
+ #x; nelim x; #b1; #b2;
+ #y; nelim y; #b3; #b4;
+ nnormalize;
+ napply (or2_elim (b1 = b3) (b1 ≠ b3) ? (decidable_b8 b1 b3) …);
+ ##[ ##2: #H; napply (or2_intro2 … (decidable_w16_aux1 b1 b2 b3 b4 H))
+ ##| ##1: #H; napply (or2_elim (b2 = b4) (b2 ≠ b4) ? (decidable_b8 b2 b4) …);
+ ##[ ##2: #H1; napply (or2_intro2 … (decidable_w16_aux2 b1 b2 b3 b4 H1))
+ ##| ##1: #H1; nrewrite > H; nrewrite > H1;
+ napply (or2_intro1 … (refl_eq ? 〈b3:b4〉))
+ ##]
+ ##]
+nqed.
+
+nlemma neqw16_to_neq : ∀w1,w2:word16.(eq_w16 w1 w2 = false) → (w1 ≠ w2).
+ #w1; #w2;
+ nelim w1;
+ nelim w2;
+ #b1; #b2; #b3; #b4;
+ nchange with ((((eq_b8 b3 b1) ⊗ (eq_b8 b4 b2)) = false) → ?);
+ #H;
+ napply (or2_elim ((eq_b8 b3 b1) = false) ((eq_b8 b4 b2) = false) ? (andb_false2 … H) …);
+ ##[ ##1: #H1; napply (decidable_w16_aux1 … (neqb8_to_neq … H1))
+ ##| ##2: #H1; napply (decidable_w16_aux2 … (neqb8_to_neq … H1))
+ ##]
+nqed.
+
+nlemma word16_destruct : ∀b1,b2,b3,b4.〈b1:b2〉 ≠ 〈b3:b4〉 → b1 ≠ b3 ∨ b2 ≠ b4.
+ #b1; #b2; #b3; #b4;
+ nnormalize; #H;
+ napply (or2_elim (b1 = b3) (b1 ≠ b3) ? (decidable_b8 b1 b3) …);
+ ##[ ##2: #H1; napply (or2_intro1 … H1)
+ ##| ##1: #H1; napply (or2_elim (b2 = b4) (b2 ≠ b4) ? (decidable_b8 b2 b4) …);
+ ##[ ##2: #H2; napply (or2_intro2 … H2)
+ ##| ##1: #H2; nrewrite > H1 in H:(%);
+ nrewrite > H2;
+ #H; nelim (H (refl_eq …))
+ ##]
+ ##]
+nqed.
+
+nlemma neq_to_neqw16 : ∀w1,w2.w1 ≠ w2 → eq_w16 w1 w2 = false.
+ #w1; #w2;
+ nelim w1; #b1; #b2;
+ nelim w2; #b3; #b4;
+ #H; nchange with (((eq_b8 b1 b3) ⊗ (eq_b8 b2 b4)) = false);
+ napply (or2_elim (b1 ≠ b3) (b2 ≠ b4) ? (word16_destruct … H) …);
+ ##[ ##1: #H1; nrewrite > (neq_to_neqb8 … H1); nnormalize; napply refl_eq
+ ##| ##2: #H1; nrewrite > (neq_to_neqb8 … H1);
+ nrewrite > (symmetric_andbool (eq_b8 b1 b3) false);
+ nnormalize; napply refl_eq
+ ##]
+nqed.