(* ********************************************************************** *)
(* 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 *)
+(* Sviluppo: 2008-2010 *)
(* *)
(* ********************************************************************** *)
nelim dw2;
#w3; #w4;
nchange with (
- match plus_w16_dc_dc w2 w4 c with
- [ pair l c ⇒ match plus_w16_dc_dc w1 w3 c with
- [ pair h c' ⇒ pair … 〈h.l〉 c' ]] =
- match plus_w16_dc_dc w4 w2 c with
- [ pair l c ⇒ match plus_w16_dc_dc w3 w1 c with
- [ pair h c' ⇒ pair … 〈h.l〉 c' ]]);
+ match plus_w16_dc_dc w2 w4 c with [ pair l c ⇒ match plus_w16_dc_dc w1 w3 c with [ pair h c' ⇒ pair … 〈h.l〉 c' ]] =
+ match plus_w16_dc_dc w4 w2 c with [ pair l c ⇒ match plus_w16_dc_dc w3 w1 c with [ pair h c' ⇒ pair … 〈h.l〉 c' ]]);
nrewrite > (symmetric_plusw16_dc_dc w4 w2 c);
ncases (plus_w16_dc_dc w2 w4 c);
#w5; #c1;
nchange with (
- match plus_w16_dc_dc w1 w3 c1 with
- [ pair h c' ⇒ pair … 〈h.w5〉 c' ] =
- match plus_w16_dc_dc w3 w1 c1 with
- [ pair h c' ⇒ pair … 〈h.w5〉 c' ]);
+ match plus_w16_dc_dc w1 w3 c1 with [ pair h c' ⇒ pair … 〈h.w5〉 c' ] =
+ match plus_w16_dc_dc w3 w1 c1 with [ pair h c' ⇒ pair … 〈h.w5〉 c' ]);
nrewrite > (symmetric_plusw16_dc_dc w1 w3 c1);
napply refl_eq.
nqed.
nelim dw2;
#w3; #w4;
nchange with (
- match plus_w16_dc_dc w2 w4 c with
- [ pair l c ⇒ 〈plus_w16_dc_d w1 w3 c.l〉 ] =
- match plus_w16_dc_dc w4 w2 c with
- [ pair l c ⇒ 〈plus_w16_dc_d w3 w1 c.l〉 ]);
+ match plus_w16_dc_dc w2 w4 c with [ pair l c ⇒ 〈plus_w16_dc_d w1 w3 c.l〉 ] =
+ match plus_w16_dc_dc w4 w2 c with [ pair l c ⇒ 〈plus_w16_dc_d w3 w1 c.l〉 ]);
nrewrite > (symmetric_plusw16_dc_dc w4 w2 c);
ncases (plus_w16_dc_dc w2 w4 c);
#w5; #c1;
nelim dw2;
#w3; #w4;
nchange with (
- match plus_w16_d_dc w2 w4 with
- [ pair l c ⇒ match plus_w16_dc_dc w1 w3 c with
- [ pair h c' ⇒ pair … 〈h.l〉 c' ]] =
- match plus_w16_d_dc w4 w2 with
- [ pair l c ⇒ match plus_w16_dc_dc w3 w1 c with
- [ pair h c' ⇒ pair … 〈h.l〉 c' ]]);
+ match plus_w16_d_dc w2 w4 with [ pair l c ⇒ match plus_w16_dc_dc w1 w3 c with [ pair h c' ⇒ pair … 〈h.l〉 c' ]] =
+ match plus_w16_d_dc w4 w2 with [ pair l c ⇒ match plus_w16_dc_dc w3 w1 c with [ pair h c' ⇒ pair … 〈h.l〉 c' ]]);
nrewrite > (symmetric_plusw16_d_dc w4 w2);
ncases (plus_w16_d_dc w2 w4);
#w5; #c;
nchange with (
- match plus_w16_dc_dc w1 w3 c with
- [ pair h c' ⇒ pair … 〈h.w5〉 c' ] =
- match plus_w16_dc_dc w3 w1 c with
- [ pair h c' ⇒ pair … 〈h.w5〉 c' ]);
+ match plus_w16_dc_dc w1 w3 c with [ pair h c' ⇒ pair … 〈h.w5〉 c' ] =
+ match plus_w16_dc_dc w3 w1 c with [ pair h c' ⇒ pair … 〈h.w5〉 c' ]);
nrewrite > (symmetric_plusw16_dc_dc w1 w3 c);
napply refl_eq.
nqed.
nelim dw2;
#w3; #w4;
nchange with (
- match plus_w16_d_dc w2 w4 with
- [ pair l c ⇒ 〈plus_w16_dc_d w1 w3 c.l〉 ] =
- match plus_w16_d_dc w4 w2 with
- [ pair l c ⇒ 〈plus_w16_dc_d w3 w1 c.l〉 ]);
+ match plus_w16_d_dc w2 w4 with [ pair l c ⇒ 〈plus_w16_dc_d w1 w3 c.l〉 ] =
+ match plus_w16_d_dc w4 w2 with [ pair l c ⇒ 〈plus_w16_dc_d w3 w1 c.l〉 ]);
nrewrite > (symmetric_plusw16_d_dc w4 w2);
ncases (plus_w16_d_dc w2 w4);
#w5; #c;
nnormalize;
napply refl_eq.
nqed.
+
+nlemma decidable_w32_aux1 : ∀w1,w2,w3,w4.w1 ≠ w3 → 〈w1.w2〉 ≠ 〈w3.w4〉.
+ #w1; #w2; #w3; #w4;
+ nnormalize; #H; #H1;
+ napply (H (word32_destruct_1 … H1)).
+nqed.
+
+nlemma decidable_w32_aux2 : ∀w1,w2,w3,w4.w2 ≠ w4 → 〈w1.w2〉 ≠ 〈w3.w4〉.
+ #w1; #w2; #w3; #w4;
+ nnormalize; #H; #H1;
+ napply (H (word32_destruct_2 … H1)).
+nqed.
+
+nlemma decidable_w32 : ∀x,y:word32.decidable (x = y).
+ #x; nelim x; #w1; #w2;
+ #y; nelim y; #w3; #w4;
+ nnormalize;
+ napply (or2_elim (w1 = w3) (w1 ≠ w3) ? (decidable_w16 w1 w3) …);
+ ##[ ##2: #H; napply (or2_intro2 … (decidable_w32_aux1 w1 w2 w3 w4 H))
+ ##| ##1: #H; napply (or2_elim (w2 = w4) (w2 ≠ w4) ? (decidable_w16 w2 w4) …);
+ ##[ ##2: #H1; napply (or2_intro2 … (decidable_w32_aux2 w1 w2 w3 w4 H1))
+ ##| ##1: #H1; nrewrite > H; nrewrite > H1;
+ napply (or2_intro1 … (refl_eq ? 〈w3.w4〉))
+ ##]
+ ##]
+nqed.
+
+nlemma neqw32_to_neq : ∀dw1,dw2:word32.(eq_w32 dw1 dw2 = false) → (dw1 ≠ dw2).
+ #dw1; #dw2;
+ nelim dw1;
+ nelim dw2;
+ #w1; #w2; #w3; #w4;
+ nchange with ((((eq_w16 w3 w1) ⊗ (eq_w16 w4 w2)) = false) → ?);
+ #H;
+ napply (or2_elim ((eq_w16 w3 w1) = false) ((eq_w16 w4 w2) = false) ? (andb_false2 … H) …);
+ ##[ ##1: #H1; napply (decidable_w32_aux1 … (neqw16_to_neq … H1))
+ ##| ##2: #H1; napply (decidable_w32_aux2 … (neqw16_to_neq … H1))
+ ##]
+nqed.
+
+nlemma word32_destruct : ∀w1,w2,w3,w4.〈w1.w2〉 ≠ 〈w3.w4〉 → w1 ≠ w3 ∨ w2 ≠ w4.
+ #w1; #w2; #w3; #w4;
+ nnormalize; #H;
+ napply (or2_elim (w1 = w3) (w1 ≠ w3) ? (decidable_w16 w1 w3) …);
+ ##[ ##2: #H1; napply (or2_intro1 … H1)
+ ##| ##1: #H1; napply (or2_elim (w2 = w4) (w2 ≠ w4) ? (decidable_w16 w2 w4) …);
+ ##[ ##2: #H2; napply (or2_intro2 … H2)
+ ##| ##1: #H2; nrewrite > H1 in H:(%);
+ nrewrite > H2;
+ #H; nelim (H (refl_eq …))
+ ##]
+ ##]
+nqed.
+
+nlemma neq_to_neqw32 : ∀dw1,dw2.dw1 ≠ dw2 → eq_w32 dw1 dw2 = false.
+ #dw1; #dw2;
+ nelim dw1; #w1; #w2;
+ nelim dw2; #w3; #w4;
+ #H; nchange with (((eq_w16 w1 w3) ⊗ (eq_w16 w2 w4)) = false);
+ napply (or2_elim (w1 ≠ w3) (w2 ≠ w4) ? (word32_destruct … H) …);
+ ##[ ##1: #H1; nrewrite > (neq_to_neqw16 … H1); nnormalize; napply refl_eq
+ ##| ##2: #H1; nrewrite > (neq_to_neqw16 … H1);
+ nrewrite > (symmetric_andbool (eq_w16 w1 w3) false);
+ nnormalize; napply refl_eq
+ ##]
+nqed.