--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: *)
+(* 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".
+include "freescale/prod.ma".
+
+(* ***** *)
+(* TUPLE *)
+(* ***** *)
+
+nlemma pair_destruct_1 :
+∀T1,T2.∀x1,x2:T1.∀y1,y2:T2.
+ pair T1 T2 x1 y1 = pair T1 T2 x2 y2 → x1 = x2.
+ #T1; #T2; #x1; #x2; #y1; #y2; #H;
+ nchange with (match pair T1 T2 x2 y2 with [ pair a _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma pair_destruct_2 :
+∀T1,T2.∀x1,x2:T1.∀y1,y2:T2.
+ pair T1 T2 x1 y1 = pair T1 T2 x2 y2 → y1 = y2.
+ #T1; #T2; #x1; #x2; #y1; #y2; #H;
+ nchange with (match pair T1 T2 x2 y2 with [ pair _ b ⇒ y1 = b ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma bsymmetric_eqpair :
+∀T1,T2:Type.∀p1,p2:ProdT T1 T2.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
+ (boolSymmetric T1 f1) →
+ (boolSymmetric T2 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;
+ nnormalize;
+ nrewrite > (H x1 x2);
+ ncases (f1 x2 x1);
+ nnormalize;
+ ##[ ##1: nrewrite > (H1 y1 y2); napply (refl_eq ??)
+ ##| ##2: napply (refl_eq ??)
+ ##]
+nqed.
+
+nlemma eq_to_eqpair :
+∀T1,T2.∀p1,p2:ProdT T1 T2.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
+ (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
+ (∀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;
+ nnormalize;
+ nrewrite > (H1 ?? (pair_destruct_1 ?????? H));
+ nnormalize;
+ nrewrite > (H2 ?? (pair_destruct_2 ?????? H));
+ napply (refl_eq ??).
+nqed.
+
+nlemma eqpair_to_eq :
+∀T1,T2.∀p1,p2:ProdT T1 T2.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
+ (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
+ (∀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;
+ nnormalize in H:(%);
+ nletin K ≝ (H1 x1 x2);
+ ncases (f1 x1 x2) in H:(%) K:(%);
+ nnormalize;
+ #H3;
+ ##[ ##2: nelim (bool_destruct_false_true H3) ##]
+ #H4;
+ nrewrite > (H4 (refl_eq ??));
+ nrewrite > (H2 y1 y2 H3);
+ napply (refl_eq ??).
+nqed.
+
+nlemma triple_destruct_1 :
+∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
+ triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → x1 = x2.
+ #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
+ nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple a _ _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma triple_destruct_2 :
+∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
+ triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → y1 = y2.
+ #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
+ nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple _ b _ ⇒ y1 = b ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma triple_destruct_3 :
+∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
+ triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → z1 = z2.
+ #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
+ nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple _ _ c ⇒ z1 = c ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma bsymmetric_eqtriple :
+∀T1,T2,T3:Type.∀p1,p2:Prod3T T1 T2 T3.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
+ (boolSymmetric T1 f1) →
+ (boolSymmetric T2 f2) →
+ (boolSymmetric T3 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;
+ nnormalize;
+ nrewrite > (H x1 x2);
+ ncases (f1 x2 x1);
+ nnormalize;
+ ##[ ##1: nrewrite > (H1 y1 y2);
+ ncases (f2 y2 y1);
+ nnormalize;
+ ##[ ##1: nrewrite > (H2 z1 z2); napply (refl_eq ??)
+ ##| ##2: napply (refl_eq ??)
+ ##]
+ ##| ##2: napply (refl_eq ??)
+ ##]
+nqed.
+
+nlemma eq_to_eqtriple :
+∀T1,T2,T3.∀p1,p2:Prod3T T1 T2 T3.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
+ (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
+ (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
+ (∀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;
+ nnormalize;
+ nrewrite > (H1 ?? (triple_destruct_1 ????????? H));
+ nnormalize;
+ nrewrite > (H2 ?? (triple_destruct_2 ????????? H));
+ nnormalize;
+ nrewrite > (H3 ?? (triple_destruct_3 ????????? H));
+ napply (refl_eq ??).
+nqed.
+
+nlemma eqtriple_to_eq :
+∀T1,T2,T3.∀p1,p2:Prod3T T1 T2 T3.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
+ (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
+ (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
+ (∀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;
+ nnormalize in H:(%);
+ nletin K ≝ (H1 x1 x2);
+ ncases (f1 x1 x2) in H:(%) K:(%);
+ nnormalize;
+ ##[ ##2: #H4; nelim (bool_destruct_false_true H4) ##]
+ nletin K1 ≝ (H2 y1 y2);
+ ncases (f2 y1 y2) in K1:(%) ⊢ %;
+ nnormalize;
+ ##[ ##2: #H4; #H5; nelim (bool_destruct_false_true H5) ##]
+ #H4; #H5; #H6;
+ nrewrite > (H4 (refl_eq ??));
+ nrewrite > (H6 (refl_eq ??));
+ nrewrite > (H3 z1 z2 H5);
+ napply (refl_eq ??).
+nqed.
+
+nlemma quadruple_destruct_1 :
+∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
+ quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → x1 = x2.
+ #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
+ nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple a _ _ _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma quadruple_destruct_2 :
+∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
+ quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → y1 = y2.
+ #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
+ nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ b _ _ ⇒ y1 = b ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma quadruple_destruct_3 :
+∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
+ quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → z1 = z2.
+ #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
+ nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ _ c _ ⇒ z1 = c ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma quadruple_destruct_4 :
+∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
+ quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → v1 = v2.
+ #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
+ nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ _ _ d ⇒ v1 = d ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma bsymmetric_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.
+ (boolSymmetric T1 f1) →
+ (boolSymmetric T2 f2) →
+ (boolSymmetric T3 f3) →
+ (boolSymmetric T4 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;
+ nnormalize;
+ nrewrite > (H x1 x2);
+ ncases (f1 x2 x1);
+ nnormalize;
+ ##[ ##1: nrewrite > (H1 y1 y2);
+ ncases (f2 y2 y1);
+ nnormalize;
+ ##[ ##1: nrewrite > (H2 z1 z2);
+ ncases (f3 z2 z1);
+ nnormalize;
+ ##[ ##1: nrewrite > (H3 v1 v2); napply (refl_eq ??)
+ ##| ##2: napply (refl_eq ??)
+ ##]
+ ##| ##2: napply (refl_eq ??)
+ ##]
+ ##| ##2: napply (refl_eq ??)
+ ##]
+nqed.
+
+nlemma eq_to_eqquadruple :
+∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
+ (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
+ (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
+ (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
+ (∀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;
+ nnormalize;
+ nrewrite > (H1 ?? (quadruple_destruct_1 ???????????? H));
+ nnormalize;
+ nrewrite > (H2 ?? (quadruple_destruct_2 ???????????? H));
+ nnormalize;
+ nrewrite > (H3 ?? (quadruple_destruct_3 ???????????? H));
+ nnormalize;
+ nrewrite > (H4 ?? (quadruple_destruct_4 ???????????? H));
+ napply (refl_eq ??).
+nqed.
+
+nlemma eqquadruple_to_eq :
+∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
+ (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
+ (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
+ (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
+ (∀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;
+ nnormalize in H:(%);
+ nletin K ≝ (H1 x1 x2);
+ ncases (f1 x1 x2) in H:(%) K:(%);
+ nnormalize;
+ ##[ ##2: #H5; nelim (bool_destruct_false_true H5) ##]
+ nletin K1 ≝ (H2 y1 y2);
+ ncases (f2 y1 y2) in K1:(%) ⊢ %;
+ nnormalize;
+ ##[ ##2: #H5; #H6; nelim (bool_destruct_false_true H6) ##]
+ nletin K2 ≝ (H3 z1 z2);
+ ncases (f3 z1 z2) in K2:(%) ⊢ %;
+ nnormalize;
+ ##[ ##2: #H5; #H6; #H7; nelim (bool_destruct_false_true H7) ##]
+ #H5; #H6; #H7; #H8;
+ nrewrite > (H5 (refl_eq ??));
+ nrewrite > (H6 (refl_eq ??));
+ nrewrite > (H8 (refl_eq ??));
+ nrewrite > (H4 v1 v2 H7);
+ napply (refl_eq ??).
+nqed.
+
+nlemma quintuple_destruct_1 :
+∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
+ quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → x1 = x2.
+ #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
+ nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple a _ _ _ _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma quintuple_destruct_2 :
+∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
+ quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → y1 = y2.
+ #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
+ nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ b _ _ _ ⇒ y1 = b ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma quintuple_destruct_3 :
+∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
+ quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → z1 = z2.
+ #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
+ nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ c _ _ ⇒ z1 = c ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma quintuple_destruct_4 :
+∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
+ quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → v1 = v2.
+ #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
+ nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ _ d _ ⇒ v1 = d ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma quintuple_destruct_5 :
+∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
+ quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → w1 = w2.
+ #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
+ nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ _ _ e ⇒ w1 = e ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma bsymmetric_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.
+ (boolSymmetric T1 f1) →
+ (boolSymmetric T2 f2) →
+ (boolSymmetric T3 f3) →
+ (boolSymmetric T4 f4) →
+ (boolSymmetric T5 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;
+ nnormalize;
+ nrewrite > (H x1 x2);
+ ncases (f1 x2 x1);
+ nnormalize;
+ ##[ ##1: nrewrite > (H1 y1 y2);
+ ncases (f2 y2 y1);
+ nnormalize;
+ ##[ ##1: nrewrite > (H2 z1 z2);
+ ncases (f3 z2 z1);
+ nnormalize;
+ ##[ ##1: nrewrite > (H3 v1 v2);
+ ncases (f4 v2 v1);
+ nnormalize;
+ ##[ ##1: nrewrite > (H4 w1 w2); napply (refl_eq ??)
+ ##| ##2: napply (refl_eq ??)
+ ##]
+ ##| ##2: napply (refl_eq ??)
+ ##]
+ ##| ##2: napply (refl_eq ??)
+ ##]
+ ##| ##2: napply (refl_eq ??)
+ ##]
+nqed.
+
+nlemma eq_to_eqquintuple :
+∀T1,T2,T3,T4,T5.∀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.
+ (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
+ (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
+ (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
+ (∀v1,v2:T4.v1 = v2 → f4 v1 v2 = true) →
+ (∀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;
+ nnormalize;
+ nrewrite > (H1 ?? (quintuple_destruct_1 ??????????????? H));
+ nnormalize;
+ nrewrite > (H2 ?? (quintuple_destruct_2 ??????????????? H));
+ nnormalize;
+ nrewrite > (H3 ?? (quintuple_destruct_3 ??????????????? H));
+ nnormalize;
+ nrewrite > (H4 ?? (quintuple_destruct_4 ??????????????? H));
+ nnormalize;
+ nrewrite > (H5 ?? (quintuple_destruct_5 ??????????????? H));
+ napply (refl_eq ??).
+nqed.
+
+nlemma eqquintuple_to_eq :
+∀T1,T2,T3,T4,T5.∀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.
+ (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
+ (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
+ (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
+ (∀v1,v2:T4.f4 v1 v2 = true → v1 = v2) →
+ (∀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;
+ nnormalize in H:(%);
+ nletin K ≝ (H1 x1 x2);
+ ncases (f1 x1 x2) in H:(%) K:(%);
+ nnormalize;
+ ##[ ##2: #H6; nelim (bool_destruct_false_true H6) ##]
+ nletin K1 ≝ (H2 y1 y2);
+ ncases (f2 y1 y2) in K1:(%) ⊢ %;
+ nnormalize;
+ ##[ ##2: #H6; #H7; nelim (bool_destruct_false_true H7) ##]
+ nletin K2 ≝ (H3 z1 z2);
+ ncases (f3 z1 z2) in K2:(%) ⊢ %;
+ nnormalize;
+ ##[ ##2: #H6; #H7; #H8; nelim (bool_destruct_false_true H8) ##]
+ nletin K3 ≝ (H4 v1 v2);
+ ncases (f4 v1 v2) in K3:(%) ⊢ %;
+ nnormalize;
+ ##[ ##2: #H6; #H7; #H8; #H9; nelim (bool_destruct_false_true H9) ##]
+ #H6; #H7; #H8; #H9; #H10;
+ nrewrite > (H6 (refl_eq ??));
+ nrewrite > (H7 (refl_eq ??));
+ nrewrite > (H8 (refl_eq ??));
+ nrewrite > (H10 (refl_eq ??));
+ nrewrite > (H5 w1 w2 H9);
+ napply (refl_eq ??).
+nqed.
projects / helm.git / blobdiff