(**************************************************************************)
(* ********************************************************************** *)
-(* Progetto FreeScale *)
+(* Progetto FreeScale *)
(* *)
-(* Sviluppato da: *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
(* *)
-(* Questo materiale fa parte della tesi: *)
-(* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
-(* *)
-(* data ultima modifica 15/11/2007 *)
(* ********************************************************************** *)
include "freescale/bool_lemmas.ma".
napply (refl_eq ??).
nqed.
-nlemma bsymmetric_eqpair :
+nlemma symmetric_eqpair :
∀T1,T2:Type.∀p1,p2:ProdT T1 T2.
∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
(symmetricT T1 bool f1) →
(symmetricT T2 bool f2) →
(eq_pair T1 T2 p1 p2 f1 f2 = eq_pair T1 T2 p2 p1 f1 f2).
#T1; #T2; #p1; #p2; #f1; #f2; #H; #H1;
- ncases p1;
- ncases p2;
- #x2; #y2; #x1; #y1;
+ napply (ProdT_ind T1 T2 ?? p1);
+ #x1; #y1;
+ napply (ProdT_ind T1 T2 ?? p2);
+ #x2; #y2;
nnormalize;
nrewrite > (H x1 x2);
ncases (f1 x2 x1);
(∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
(p1 = p2 → eq_pair T1 T2 p1 p2 f1 f2 = true).
#T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
- ncases p1;
- ncases p2;
- #x2; #y2; #x1; #y1; #H;
+ napply (ProdT_ind T1 T2 ?? p1);
+ #x1; #y1;
+ napply (ProdT_ind T1 T2 ?? p2);
+ #x2; #y2; #H;
nnormalize;
nrewrite > (H1 ?? (pair_destruct_1 ?????? H));
nnormalize;
(∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
(eq_pair T1 T2 p1 p2 f1 f2 = true → p1 = p2).
#T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
- ncases p1;
- ncases p2;
- #x2; #y2; #x1; #y1; #H;
+ napply (ProdT_ind T1 T2 ?? p1);
+ #x1; #y1;
+ napply (ProdT_ind T1 T2 ?? p2);
+ #x2; #y2; #H;
nnormalize in H:(%);
nletin K ≝ (H1 x1 x2);
ncases (f1 x1 x2) in H:(%) K:(%);
napply (refl_eq ??).
nqed.
-nlemma bsymmetric_eqtriple :
+nlemma symmetric_eqtriple :
∀T1,T2,T3:Type.∀p1,p2:Prod3T T1 T2 T3.
∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
(symmetricT T1 bool f1) →
(symmetricT T3 bool f3) →
(eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = eq_triple T1 T2 T3 p2 p1 f1 f2 f3).
#T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H; #H1; #H2;
- ncases p1;
- ncases p2;
- #x2; #y2; #z2; #x1; #y1; #z1;
+ napply (Prod3T_ind T1 T2 T3 ?? p1);
+ #x1; #y1; #z1;
+ napply (Prod3T_ind T1 T2 T3 ?? p2);
+ #x2; #y2; #z2;
nnormalize;
nrewrite > (H x1 x2);
ncases (f1 x2 x1);
(∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
(p1 = p2 → eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = true).
#T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
- ncases p1;
- ncases p2;
- #x2; #y2; #z2; #x1; #y1; #z1; #H;
+ napply (Prod3T_ind T1 T2 T3 ?? p1);
+ #x1; #y1; #z1;
+ napply (Prod3T_ind T1 T2 T3 ?? p2);
+ #x2; #y2; #z2; #H;
nnormalize;
nrewrite > (H1 ?? (triple_destruct_1 ????????? H));
nnormalize;
(∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
(eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = true → p1 = p2).
#T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
- ncases p1;
- ncases p2;
- #x2; #y2; #z2; #x1; #y1; #z1; #H;
+ napply (Prod3T_ind T1 T2 T3 ?? p1);
+ #x1; #y1; #z1;
+ napply (Prod3T_ind T1 T2 T3 ?? p2);
+ #x2; #y2; #z2; #H;
nnormalize in H:(%);
nletin K ≝ (H1 x1 x2);
ncases (f1 x1 x2) in H:(%) K:(%);
napply (refl_eq ??).
nqed.
-nlemma bsymmetric_eqquadruple :
+nlemma symmetric_eqquadruple :
∀T1,T2,T3,T4:Type.∀p1,p2:Prod4T T1 T2 T3 T4.
∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
(symmetricT T1 bool f1) →
(symmetricT T4 bool f4) →
(eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = eq_quadruple T1 T2 T3 T4 p2 p1 f1 f2 f3 f4).
#T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H; #H1; #H2; #H3;
- ncases p1;
- ncases p2;
- #x2; #y2; #z2; #v2; #x1; #y1; #z1; #v1;
+ napply (Prod4T_ind T1 T2 T3 T4 ?? p1);
+ #x1; #y1; #z1; #v1;
+ napply (Prod4T_ind T1 T2 T3 T4 ?? p2);
+ #x2; #y2; #z2; #v2;
nnormalize;
nrewrite > (H x1 x2);
ncases (f1 x2 x1);
(∀v1,v2:T4.v1 = v2 → f4 v1 v2 = true) →
(p1 = p2 → eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true).
#T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
- ncases p1;
- ncases p2;
- #x2; #y2; #z2; #v2; #x1; #y1; #z1; #v1; #H;
+ napply (Prod4T_ind T1 T2 T3 T4 ?? p1);
+ #x1; #y1; #z1; #v1;
+ napply (Prod4T_ind T1 T2 T3 T4 ?? p2);
+ #x2; #y2; #z2; #v2; #H;
nnormalize;
nrewrite > (H1 ?? (quadruple_destruct_1 ???????????? H));
nnormalize;
(∀v1,v2:T4.f4 v1 v2 = true → v1 = v2) →
(eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true → p1 = p2).
#T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
- ncases p1;
- ncases p2;
- #x2; #y2; #z2; #v2; #x1; #y1; #z1; #v1; #H;
+ napply (Prod4T_ind T1 T2 T3 T4 ?? p1);
+ #x1; #y1; #z1; #v1;
+ napply (Prod4T_ind T1 T2 T3 T4 ?? p2);
+ #x2; #y2; #z2; #v2; #H;
nnormalize in H:(%);
nletin K ≝ (H1 x1 x2);
ncases (f1 x1 x2) in H:(%) K:(%);
napply (refl_eq ??).
nqed.
-nlemma bsymmetric_eqquintuple :
+nlemma symmetric_eqquintuple :
∀T1,T2,T3,T4,T5:Type.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
(symmetricT T1 bool f1) →
(symmetricT T5 bool f5) →
(eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = eq_quintuple T1 T2 T3 T4 T5 p2 p1 f1 f2 f3 f4 f5).
#T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H; #H1; #H2; #H3; #H4;
- ncases p1;
- ncases p2;
- #x2; #y2; #z2; #v2; #w2; #x1; #y1; #z1; #v1; #w1;
+ napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p1);
+ #x1; #y1; #z1; #v1; #w1;
+ napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p2);
+ #x2; #y2; #z2; #v2; #w2;
nnormalize;
nrewrite > (H x1 x2);
ncases (f1 x2 x1);
(∀w1,w2:T5.w1 = w2 → f5 w1 w2 = true) →
(p1 = p2 → eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true).
#T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
- ncases p1;
- ncases p2;
- #x2; #y2; #z2; #v2; #w2; #x1; #y1; #z1; #v1; #w1; #H;
+ napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p1);
+ #x1; #y1; #z1; #v1; #w1;
+ napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p2);
+ #x2; #y2; #z2; #v2; #w2; #H;
nnormalize;
nrewrite > (H1 ?? (quintuple_destruct_1 ??????????????? H));
nnormalize;
(∀w1,w2:T5.f5 w1 w2 = true → w1 = w2) →
(eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true → p1 = p2).
#T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
- ncases p1;
- ncases p2;
- #x2; #y2; #z2; #v2; #w2; #x1; #y1; #z1; #v1; #w1; #H;
+ napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p1);
+ #x1; #y1; #z1; #v1; #w1;
+ napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p2);
+ #x2; #y2; #z2; #v2; #w2; #H;
nnormalize in H:(%);
nletin K ≝ (H1 x1 x2);
ncases (f1 x1 x2) in H:(%) K:(%);