helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                           Progetto FreeScale                           *)
  17 (*                                                                        *)
  18 (* Sviluppato da:                                                         *)
  19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  20 (*                                                                        *)
  21 (* Questo materiale fa parte della tesi:                                  *)
  22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
  23 (*                                                                        *)
  24 (*                    data ultima modifica 15/11/2007                     *)
  25 (* ********************************************************************** *)
  26
  27 include "freescale/bool_lemmas.ma".
  28 include "freescale/prod.ma".
  29
  30 (* ***** *)
  31 (* TUPLE *)
  32 (* ***** *)
  33
  34 nlemma pair_destruct_1 :
  35 ∀T1,T2.∀x1,x2:T1.∀y1,y2:T2.
  36  pair T1 T2 x1 y1 = pair T1 T2 x2 y2 → x1 = x2.
  37  #T1; #T2; #x1; #x2; #y1; #y2; #H;
  38  nchange with (match pair T1 T2 x2 y2 with [ pair a _ ⇒ x1 = a ]);
  39  nrewrite < H;
  40  nnormalize;
  41  napply (refl_eq ??).
  42 nqed.
  43
  44 nlemma pair_destruct_2 :
  45 ∀T1,T2.∀x1,x2:T1.∀y1,y2:T2.
  46  pair T1 T2 x1 y1 = pair T1 T2 x2 y2 → y1 = y2.
  47  #T1; #T2; #x1; #x2; #y1; #y2; #H;
  48  nchange with (match pair T1 T2 x2 y2 with [ pair _ b ⇒ y1 = b ]);
  49  nrewrite < H;
  50  nnormalize;
  51  napply (refl_eq ??).
  52 nqed.
  53
  54 nlemma symmetric_eqpair :
  55 ∀T1,T2:Type.∀p1,p2:ProdT T1 T2.
  56 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
  57  (symmetricT T1 bool f1) →
  58  (symmetricT T2 bool f2) →
  59  (eq_pair T1 T2 p1 p2 f1 f2 = eq_pair T1 T2 p2 p1 f1 f2).
  60  #T1; #T2; #p1; #p2; #f1; #f2; #H; #H1;
  61  napply (ProdT_ind T1 T2 ?? p1);
  62  #x1; #y1;
  63  napply (ProdT_ind T1 T2 ?? p2);
  64  #x2; #y2;
  65  nnormalize;
  66  nrewrite > (H x1 x2);
  67  ncases (f1 x2 x1);
  68  nnormalize;
  69  ##[ ##1: nrewrite > (H1 y1 y2); napply (refl_eq ??)
  70  ##| ##2: napply (refl_eq ??)
  71  ##]
  72 nqed.
  73
  74 nlemma eq_to_eqpair :
  75 ∀T1,T2.∀p1,p2:ProdT T1 T2.
  76 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
  77  (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
  78  (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
  79  (p1 = p2 → eq_pair T1 T2 p1 p2 f1 f2 = true).
  80  #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
  81  napply (ProdT_ind T1 T2 ?? p1);
  82  #x1; #y1;
  83  napply (ProdT_ind T1 T2 ?? p2);
  84  #x2; #y2; #H;
  85  nnormalize;
  86  nrewrite > (H1 ?? (pair_destruct_1 ?????? H));
  87  nnormalize;
  88  nrewrite > (H2 ?? (pair_destruct_2 ?????? H));
  89  napply (refl_eq ??).
  90 nqed.
  91
  92 nlemma eqpair_to_eq :
  93 ∀T1,T2.∀p1,p2:ProdT T1 T2.
  94 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
  95  (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
  96  (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
  97  (eq_pair T1 T2 p1 p2 f1 f2 = true → p1 = p2).
  98  #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
  99  napply (ProdT_ind T1 T2 ?? p1);
 100  #x1; #y1;
 101  napply (ProdT_ind T1 T2 ?? p2);
 102  #x2; #y2; #H;
 103  nnormalize in H:(%);
 104  nletin K ≝ (H1 x1 x2);
 105  ncases (f1 x1 x2) in H:(%) K:(%);
 106  nnormalize;
 107  #H3;
 108  ##[ ##2: napply (bool_destruct ??? H3) ##]
 109  #H4;
 110  nrewrite > (H4 (refl_eq ??));
 111  nrewrite > (H2 y1 y2 H3);
 112  napply (refl_eq ??).
 113 nqed.
 114
 115 nlemma triple_destruct_1 :
 116 ∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
 117  triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → x1 = x2.
 118  #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
 119  nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple a _ _ ⇒ x1 = a ]);
 120  nrewrite < H;
 121  nnormalize;
 122  napply (refl_eq ??).
 123 nqed.
 124
 125 nlemma triple_destruct_2 :
 126 ∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
 127  triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → y1 = y2.
 128  #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
 129  nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple _ b _ ⇒ y1 = b ]);
 130  nrewrite < H;
 131  nnormalize;
 132  napply (refl_eq ??).
 133 nqed.
 134
 135 nlemma triple_destruct_3 :
 136 ∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
 137  triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → z1 = z2.
 138  #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
 139  nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple _ _ c ⇒ z1 = c ]);
 140  nrewrite < H;
 141  nnormalize;
 142  napply (refl_eq ??).
 143 nqed.
 144
 145 nlemma symmetric_eqtriple :
 146 ∀T1,T2,T3:Type.∀p1,p2:Prod3T T1 T2 T3.
 147 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
 148  (symmetricT T1 bool f1) →
 149  (symmetricT T2 bool f2) →
 150  (symmetricT T3 bool f3) →
 151  (eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = eq_triple T1 T2 T3 p2 p1 f1 f2 f3).
 152  #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H; #H1; #H2;
 153  napply (Prod3T_ind T1 T2 T3 ?? p1);
 154  #x1; #y1; #z1;
 155  napply (Prod3T_ind T1 T2 T3 ?? p2);
 156  #x2; #y2; #z2;
 157  nnormalize;
 158  nrewrite > (H x1 x2);
 159  ncases (f1 x2 x1);
 160  nnormalize;
 161  ##[ ##1: nrewrite > (H1 y1 y2);
 162           ncases (f2 y2 y1);
 163           nnormalize;
 164           ##[ ##1: nrewrite > (H2 z1 z2); napply (refl_eq ??)
 165           ##| ##2: napply (refl_eq ??)
 166           ##]
 167  ##| ##2: napply (refl_eq ??)
 168  ##]
 169 nqed.
 170
 171 nlemma eq_to_eqtriple :
 172 ∀T1,T2,T3.∀p1,p2:Prod3T T1 T2 T3.
 173 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
 174  (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
 175  (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
 176  (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
 177  (p1 = p2 → eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = true).
 178  #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
 179  napply (Prod3T_ind T1 T2 T3 ?? p1);
 180  #x1; #y1; #z1;
 181  napply (Prod3T_ind T1 T2 T3 ?? p2);
 182  #x2; #y2; #z2; #H;
 183  nnormalize;
 184  nrewrite > (H1 ?? (triple_destruct_1 ????????? H));
 185  nnormalize;
 186  nrewrite > (H2 ?? (triple_destruct_2 ????????? H));
 187  nnormalize;
 188  nrewrite > (H3 ?? (triple_destruct_3 ????????? H));
 189  napply (refl_eq ??).
 190 nqed.
 191
 192 nlemma eqtriple_to_eq :
 193 ∀T1,T2,T3.∀p1,p2:Prod3T T1 T2 T3.
 194 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
 195  (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
 196  (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
 197  (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
 198  (eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = true → p1 = p2).
 199  #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
 200  napply (Prod3T_ind T1 T2 T3 ?? p1);
 201  #x1; #y1; #z1;
 202  napply (Prod3T_ind T1 T2 T3 ?? p2);
 203  #x2; #y2; #z2; #H;
 204  nnormalize in H:(%);
 205  nletin K ≝ (H1 x1 x2);
 206  ncases (f1 x1 x2) in H:(%) K:(%);
 207  nnormalize;
 208  ##[ ##2: #H4; napply (bool_destruct ??? H4) ##]
 209  nletin K1 ≝ (H2 y1 y2);
 210  ncases (f2 y1 y2) in K1:(%) ⊢ %;
 211  nnormalize;
 212  ##[ ##2: #H4; #H5; napply (bool_destruct ??? H5) ##]
 213  #H4; #H5; #H6;
 214  nrewrite > (H4 (refl_eq ??));
 215  nrewrite > (H6 (refl_eq ??));
 216  nrewrite > (H3 z1 z2 H5);
 217  napply (refl_eq ??).
 218 nqed.
 219
 220 nlemma quadruple_destruct_1 :
 221 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
 222  quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → x1 = x2.
 223  #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
 224  nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple a _ _ _ ⇒ x1 = a ]);
 225  nrewrite < H;
 226  nnormalize;
 227  napply (refl_eq ??).
 228 nqed.
 229
 230 nlemma quadruple_destruct_2 :
 231 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
 232  quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → y1 = y2.
 233  #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
 234  nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ b _ _ ⇒ y1 = b ]);
 235  nrewrite < H;
 236  nnormalize;
 237  napply (refl_eq ??).
 238 nqed.
 239
 240 nlemma quadruple_destruct_3 :
 241 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
 242  quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → z1 = z2.
 243  #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
 244  nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ _ c _ ⇒ z1 = c ]);
 245  nrewrite < H;
 246  nnormalize;
 247  napply (refl_eq ??).
 248 nqed.
 249
 250 nlemma quadruple_destruct_4 :
 251 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
 252  quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → v1 = v2.
 253  #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
 254  nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ _ _ d ⇒ v1 = d ]);
 255  nrewrite < H;
 256  nnormalize;
 257  napply (refl_eq ??).
 258 nqed.
 259
 260 nlemma symmetric_eqquadruple :
 261 ∀T1,T2,T3,T4:Type.∀p1,p2:Prod4T T1 T2 T3 T4.
 262 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
 263  (symmetricT T1 bool f1) →
 264  (symmetricT T2 bool f2) →
 265  (symmetricT T3 bool f3) →
 266  (symmetricT T4 bool f4) →
 267  (eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = eq_quadruple T1 T2 T3 T4 p2 p1 f1 f2 f3 f4).
 268  #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H; #H1; #H2; #H3;
 269  napply (Prod4T_ind T1 T2 T3 T4 ?? p1);
 270  #x1; #y1; #z1; #v1;
 271  napply (Prod4T_ind T1 T2 T3 T4 ?? p2);
 272  #x2; #y2; #z2; #v2;
 273  nnormalize;
 274  nrewrite > (H x1 x2);
 275  ncases (f1 x2 x1);
 276  nnormalize;
 277  ##[ ##1: nrewrite > (H1 y1 y2);
 278           ncases (f2 y2 y1);
 279           nnormalize;
 280           ##[ ##1: nrewrite > (H2 z1 z2);
 281                    ncases (f3 z2 z1);
 282                    nnormalize;
 283                    ##[ ##1: nrewrite > (H3 v1 v2); napply (refl_eq ??)
 284                    ##| ##2: napply (refl_eq ??)
 285                    ##]
 286           ##| ##2: napply (refl_eq ??)
 287           ##]
 288  ##| ##2: napply (refl_eq ??)
 289  ##]
 290 nqed.
 291
 292 nlemma eq_to_eqquadruple :
 293 ∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4.
 294 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
 295  (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
 296  (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
 297  (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
 298  (∀v1,v2:T4.v1 = v2 → f4 v1 v2 = true) →
 299  (p1 = p2 → eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true).
 300  #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
 301  napply (Prod4T_ind T1 T2 T3 T4 ?? p1);
 302  #x1; #y1; #z1; #v1;
 303  napply (Prod4T_ind T1 T2 T3 T4 ?? p2);
 304  #x2; #y2; #z2; #v2; #H;
 305  nnormalize;
 306  nrewrite > (H1 ?? (quadruple_destruct_1 ???????????? H));
 307  nnormalize;
 308  nrewrite > (H2 ?? (quadruple_destruct_2 ???????????? H));
 309  nnormalize;
 310  nrewrite > (H3 ?? (quadruple_destruct_3 ???????????? H));
 311  nnormalize;
 312  nrewrite > (H4 ?? (quadruple_destruct_4 ???????????? H));
 313  napply (refl_eq ??).
 314 nqed.
 315
 316 nlemma eqquadruple_to_eq :
 317 ∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4.
 318 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
 319  (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
 320  (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
 321  (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
 322  (∀v1,v2:T4.f4 v1 v2 = true → v1 = v2) →
 323  (eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true → p1 = p2).
 324  #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
 325  napply (Prod4T_ind T1 T2 T3 T4 ?? p1);
 326  #x1; #y1; #z1; #v1;
 327  napply (Prod4T_ind T1 T2 T3 T4 ?? p2);
 328  #x2; #y2; #z2; #v2; #H;
 329  nnormalize in H:(%);
 330  nletin K ≝ (H1 x1 x2);
 331  ncases (f1 x1 x2) in H:(%) K:(%);
 332  nnormalize;
 333  ##[ ##2: #H5; napply (bool_destruct ??? H5) ##]
 334  nletin K1 ≝ (H2 y1 y2);
 335  ncases (f2 y1 y2) in K1:(%) ⊢ %;
 336  nnormalize;
 337  ##[ ##2: #H5; #H6; napply (bool_destruct ??? H6) ##]
 338  nletin K2 ≝ (H3 z1 z2);
 339  ncases (f3 z1 z2) in K2:(%) ⊢ %;
 340  nnormalize;
 341  ##[ ##2: #H5; #H6; #H7; napply (bool_destruct ??? H7) ##]
 342  #H5; #H6; #H7; #H8;
 343  nrewrite > (H5 (refl_eq ??));
 344  nrewrite > (H6 (refl_eq ??));
 345  nrewrite > (H8 (refl_eq ??));
 346  nrewrite > (H4 v1 v2 H7);
 347  napply (refl_eq ??).
 348 nqed.
 349
 350 nlemma quintuple_destruct_1 :
 351 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
 352  quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → x1 = x2.
 353  #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
 354  nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple a _ _ _ _ ⇒ x1 = a ]);
 355  nrewrite < H;
 356  nnormalize;
 357  napply (refl_eq ??).
 358 nqed.
 359
 360 nlemma quintuple_destruct_2 :
 361 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
 362  quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → y1 = y2.
 363  #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
 364  nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ b _ _ _ ⇒ y1 = b ]);
 365  nrewrite < H;
 366  nnormalize;
 367  napply (refl_eq ??).
 368 nqed.
 369
 370 nlemma quintuple_destruct_3 :
 371 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
 372  quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → z1 = z2.
 373  #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
 374  nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ c _ _ ⇒ z1 = c ]);
 375  nrewrite < H;
 376  nnormalize;
 377  napply (refl_eq ??).
 378 nqed.
 379
 380 nlemma quintuple_destruct_4 :
 381 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
 382  quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → v1 = v2.
 383  #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
 384  nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ _ d _ ⇒ v1 = d ]);
 385  nrewrite < H;
 386  nnormalize;
 387  napply (refl_eq ??).
 388 nqed.
 389
 390 nlemma quintuple_destruct_5 :
 391 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
 392  quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → w1 = w2.
 393  #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
 394  nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ _ _ e ⇒ w1 = e ]);
 395  nrewrite < H;
 396  nnormalize;
 397  napply (refl_eq ??).
 398 nqed.
 399
 400 nlemma symmetric_eqquintuple :
 401 ∀T1,T2,T3,T4,T5:Type.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
 402 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
 403  (symmetricT T1 bool f1) →
 404  (symmetricT T2 bool f2) →
 405  (symmetricT T3 bool f3) →
 406  (symmetricT T4 bool f4) →
 407  (symmetricT T5 bool f5) →
 408  (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).
 409  #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H; #H1; #H2; #H3; #H4;
 410  napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p1);
 411  #x1; #y1; #z1; #v1; #w1;
 412  napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p2);
 413  #x2; #y2; #z2; #v2; #w2;
 414  nnormalize;
 415  nrewrite > (H x1 x2);
 416  ncases (f1 x2 x1);
 417  nnormalize;
 418  ##[ ##1: nrewrite > (H1 y1 y2);
 419           ncases (f2 y2 y1);
 420           nnormalize;
 421           ##[ ##1: nrewrite > (H2 z1 z2);
 422                    ncases (f3 z2 z1);
 423                    nnormalize;
 424                    ##[ ##1: nrewrite > (H3 v1 v2);
 425                             ncases (f4 v2 v1);
 426                             nnormalize;
 427                             ##[ ##1: nrewrite > (H4 w1 w2); napply (refl_eq ??)
 428                             ##| ##2: napply (refl_eq ??)
 429                             ##]
 430                    ##| ##2: napply (refl_eq ??)
 431                    ##]
 432           ##| ##2: napply (refl_eq ??)
 433           ##]
 434  ##| ##2: napply (refl_eq ??)
 435  ##]
 436 nqed.
 437
 438 nlemma eq_to_eqquintuple :
 439 ∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
 440 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
 441  (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
 442  (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
 443  (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
 444  (∀v1,v2:T4.v1 = v2 → f4 v1 v2 = true) →
 445  (∀w1,w2:T5.w1 = w2 → f5 w1 w2 = true) →
 446  (p1 = p2 → eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true).
 447  #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
 448  napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p1);
 449  #x1; #y1; #z1; #v1; #w1;
 450  napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p2);
 451  #x2; #y2; #z2; #v2; #w2; #H;
 452  nnormalize;
 453  nrewrite > (H1 ?? (quintuple_destruct_1 ??????????????? H));
 454  nnormalize;
 455  nrewrite > (H2 ?? (quintuple_destruct_2 ??????????????? H));
 456  nnormalize;
 457  nrewrite > (H3 ?? (quintuple_destruct_3 ??????????????? H));
 458  nnormalize;
 459  nrewrite > (H4 ?? (quintuple_destruct_4 ??????????????? H));
 460  nnormalize;
 461  nrewrite > (H5 ?? (quintuple_destruct_5 ??????????????? H));
 462  napply (refl_eq ??).
 463 nqed.
 464
 465 nlemma eqquintuple_to_eq :
 466 ∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
 467 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
 468  (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
 469  (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
 470  (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
 471  (∀v1,v2:T4.f4 v1 v2 = true → v1 = v2) →
 472  (∀w1,w2:T5.f5 w1 w2 = true → w1 = w2) →
 473  (eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true → p1 = p2).
 474  #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
 475  napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p1);
 476  #x1; #y1; #z1; #v1; #w1;
 477  napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p2);
 478  #x2; #y2; #z2; #v2; #w2; #H;
 479  nnormalize in H:(%);
 480  nletin K ≝ (H1 x1 x2);
 481  ncases (f1 x1 x2) in H:(%) K:(%);
 482  nnormalize;
 483  ##[ ##2: #H6; napply (bool_destruct ??? H6) ##]
 484  nletin K1 ≝ (H2 y1 y2);
 485  ncases (f2 y1 y2) in K1:(%) ⊢ %;
 486  nnormalize;
 487  ##[ ##2: #H6; #H7; napply (bool_destruct ??? H7) ##]
 488  nletin K2 ≝ (H3 z1 z2);
 489  ncases (f3 z1 z2) in K2:(%) ⊢ %;
 490  nnormalize;
 491  ##[ ##2: #H6; #H7; #H8; napply (bool_destruct ??? H8) ##]
 492  nletin K3 ≝ (H4 v1 v2);
 493  ncases (f4 v1 v2) in K3:(%) ⊢ %;
 494  nnormalize;
 495  ##[ ##2: #H6; #H7; #H8; #H9; napply (bool_destruct ??? H9) ##]
 496  #H6; #H7; #H8; #H9; #H10;
 497  nrewrite > (H6 (refl_eq ??));
 498  nrewrite > (H7 (refl_eq ??));
 499  nrewrite > (H8 (refl_eq ??));
 500  nrewrite > (H10 (refl_eq ??));
 501  nrewrite > (H5 w1 w2 H9);
 502  napply (refl_eq ??).
 503 nqed.