helm/software/matita/contribs/ng_assembly/common/prod.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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Ultima modifica: 05/08/2009                                          *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "num/bool.ma".
  24
  25 (* ***** *)
  26 (* TUPLE *)
  27 (* ***** *)
  28
  29 ninductive ProdT (T1:Type) (T2:Type) : Type ≝
  30  pair : T1 → T2 → ProdT T1 T2.
  31
  32 ndefinition fst ≝
  33 λT1,T2:Type.λp:ProdT T1 T2.match p with [ pair  x _ ⇒ x ].
  34
  35 ndefinition snd ≝
  36 λT1,T2:Type.λp:ProdT T1 T2.match p with [ pair  _ x ⇒ x ].
  37
  38 ndefinition eq_pair ≝
  39 λT1,T2:Type.λp1,p2:ProdT T1 T2.
  40 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.
  41  match p1 with [ pair x1 y1 ⇒
  42   match p2 with [ pair x2 y2 ⇒
  43    (f1 x1 x2) ⊗ (f2 y1 y2) ]].
  44
  45 ninductive Prod3T (T1:Type) (T2:Type) (T3:Type) : Type ≝
  46 triple : T1 → T2 → T3 → Prod3T T1 T2 T3.
  47
  48 ndefinition fst3T ≝
  49 λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple x _ _ ⇒ x ].
  50
  51 ndefinition snd3T ≝
  52 λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple _ x _ ⇒ x ].
  53
  54 ndefinition thd3T ≝
  55 λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple _ _ x ⇒ x ].
  56
  57 ndefinition eq_triple ≝
  58 λT1,T2,T3:Type.λp1,p2:Prod3T T1 T2 T3.
  59 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.
  60  match p1 with [ triple x1 y1 z1 ⇒
  61   match p2 with [ triple x2 y2 z2 ⇒
  62    (f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ]].
  63
  64 ninductive Prod4T (T1:Type) (T2:Type) (T3:Type) (T4:Type) : Type ≝
  65 quadruple : T1 → T2 → T3 → T4 → Prod4T T1 T2 T3 T4.
  66
  67 ndefinition fst4T ≝
  68 λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple x _ _ _ ⇒ x ].
  69
  70 ndefinition snd4T ≝
  71 λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ x _ _ ⇒ x ].
  72
  73 ndefinition thd4T ≝
  74 λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ _ x _ ⇒ x ].
  75
  76 ndefinition fth4T ≝
  77 λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ _ _ x ⇒ x ].
  78
  79 ndefinition eq_quadruple ≝
  80 λT1,T2,T3,T4:Type.λp1,p2:Prod4T T1 T2 T3 T4.
  81 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.λf4:T4 → T4 → bool.
  82  match p1 with [ quadruple x1 y1 z1 w1 ⇒
  83   match p2 with [ quadruple x2 y2 z2 w2 ⇒
  84    (f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 w1 w2) ]].
  85
  86 ninductive Prod5T (T1:Type) (T2:Type) (T3:Type) (T4:Type) (T5:Type) : Type ≝
  87 quintuple : T1 → T2 → T3 → T4 → T5 → Prod5T T1 T2 T3 T4 T5.
  88
  89 ndefinition fst5T ≝
  90 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple x _ _ _ _ ⇒ x ].
  91
  92 ndefinition snd5T ≝
  93 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ x _ _ _ ⇒ x ].
  94
  95 ndefinition thd5T ≝
  96 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ x _ _ ⇒ x ].
  97
  98 ndefinition frth5T ≝
  99 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ _ x _ ⇒ x ].
 100
 101 ndefinition ffth5T ≝
 102 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ _ _ x ⇒ x ].
 103
 104 ndefinition eq_quintuple ≝
 105 λT1,T2,T3,T4,T5:Type.λp1,p2:Prod5T T1 T2 T3 T4 T5.
 106 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.λf4:T4 → T4 → bool.λf5:T5 → T5 → bool.
 107  match p1 with [ quintuple x1 y1 z1 w1 v1 ⇒
 108   match p2 with [ quintuple x2 y2 z2 w2 v2 ⇒
 109    (f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 w1 w2) ⊗ (f5 v1 v2) ]].