1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Ultima modifica: 05/08/2009 *)
21 (* ********************************************************************** *)
23 include "num/bool.ma".
29 ninductive ProdT (T1:Type) (T2:Type) : Type ≝
30 pair : T1 → T2 → ProdT T1 T2.
33 λT1,T2:Type.λp:ProdT T1 T2.match p with [ pair x _ ⇒ x ].
36 λT1,T2:Type.λp:ProdT T1 T2.match p with [ pair _ x ⇒ x ].
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) ]].
45 ninductive Prod3T (T1:Type) (T2:Type) (T3:Type) : Type ≝
46 triple : T1 → T2 → T3 → Prod3T T1 T2 T3.
49 λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple x _ _ ⇒ x ].
52 λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple _ x _ ⇒ x ].
55 λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple _ _ x ⇒ x ].
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) ]].
64 ninductive Prod4T (T1:Type) (T2:Type) (T3:Type) (T4:Type) : Type ≝
65 quadruple : T1 → T2 → T3 → T4 → Prod4T T1 T2 T3 T4.
68 λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple x _ _ _ ⇒ x ].
71 λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ x _ _ ⇒ x ].
74 λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ _ x _ ⇒ x ].
77 λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ _ _ x ⇒ x ].
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) ]].
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.
90 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple x _ _ _ _ ⇒ x ].
93 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ x _ _ _ ⇒ x ].
96 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ x _ _ ⇒ x ].
99 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ _ x _ ⇒ x ].
102 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ _ _ x ⇒ x ].
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) ]].