Type Products
(* TYPE PRODUCTS *)
(* by Venanzio Capretta *)
(* Coq version 6.2.3 *)
Require Export Finite_Sets.
Require Export Type_Constructions.
(* n-ary functions between types. *)
Implicit Arguments On.
Section N_Ary_Functions.
Variables T1, T2 : Type.
(* First of all we define what we mean by an n-ary function *)
(* From a type T1 to a type T2. *)
Fixpoint
n_ary_function [n : nat] : Type :=
Cases n of
O => T2
| (S n') => T1 -> (n_ary_function n')
end.
End N_Ary_Functions.
Section N_Ary_Composition.
Variables T1, T2, T3 : Type.
(* Suppose we have an n-ary function f from T1 to T2 and a unary *)
(* function g from T2 to T3. We want to define their composition, *)
(* which is an n-ary function from T1 to T3. *)
Fixpoint
n_ary_comp [n : nat] :
(n_ary_function T1 T2 n) -> (T2 -> T3) -> (n_ary_function T1 T3 n) :=
<[n:nat](n_ary_function T1 T2 n) -> (T2 -> T3) -> (n_ary_function T1 T3 n)>
Cases n of
O => [f][g](g f)
| (S n') => [f][g][x : T1](n_ary_comp (f x) g)
end.
End N_Ary_Composition.
(* Finite products of a type A, A x A x .... x A. *)
Section Finite_Products_Definition.
Variable A : Type.
(* Product of n copies of a type. *)
Fixpoint
productT [n : nat] : Type :=
Cases n of
O => UnitT
| (S n') => (prodT A (productT n'))
end.
Definition
nilT : (productT O) := IT.
Definition
consT : (n : nat)A -> (productT n)
-> (productT (S n)) :=
[n][a][t](pairT a t).
Definition
headT : (n : nat)(productT (S n)) -> A :=
[n](!fstT ? ?).
Definition
tailT : (n : nat)(productT (S n))
-> (productT n) :=
[n](!sndT ? ?).
Lemma
productT_section :
(n : nat)(t : (productT (S n)))
(consT (headT t) (tailT t)) == t.
(* The following function add an element at the head of the result *)
(* of an m-ary function: *)
(* if (f x_1 ... x_m) = (t_1, ..., t_n) and *)
(* g = (add_one_element f a) *)
(* then (g x_1 ... x_m) = (a, t_1, ..., t_n) *)
Fixpoint
add_one_element [n, m :nat] :
(n_ary_function A (productT n) m) -> A
-> (n_ary_function A (productT (S n)) m) :=
<[m:nat](n_ary_function A (productT n) m) -> A
-> (n_ary_function A (productT (S n)) m)>
Cases m of
O => [f][a](consT a f)
| (S m') => [f][a][x:A](add_one_element (f x) a)
end.
(* Definition of an n-tuple creation: (tuple A n x_1 ... x_n) *)
(* will be the element of (productT n) with components x1 ... x_n. *)
Fixpoint
tupleT [n : nat] : (n_ary_function A (productT n) n) :=
<[n : nat](n_ary_function A (productT n) n)>
Cases n of
O => nilT
| (S n') => [x : A](add_one_element (tupleT n') x)
end.
(* Definition of projections. *)
Fixpoint
projT [n, m : nat] : (gt n m) -> (productT n) -> A :=
<[n:nat](gt n m) -> (productT n) -> A>
Cases n of
O => [p](False_rect (productT O)->A (lt_n_O m p))
| (S n') => <[m:nat](gt (S n') m) -> (productT (S n')) -> A>
Cases m of
O => [_](headT 1!n')
| (S m') => [p][t](projT (gt_S_n m' n' p)
(tailT t))
end
end.
Definition
projectionT : (n : nat)(Finite n) -> (productT n) -> A :=
[n][i](projT (fin_extr_gt i)).
(* If we have a function from the finite type (Finite n) to A, we want *)
(* to construct the n-tuple of elements of A associated with it. *)
Fixpoint
fin_set_fun_tuple [n : nat] :
((Finite n) -> A) -> (productT n) :=
<[n:nat]((Finite n) -> A) -> (productT n)>
Cases n of
O => [f]nilT
| (S n') => [f](consT (f (fin_inj (gt_Sn_O n')))
(fin_set_fun_tuple
[i : (Finite n')](f (fin_succ i))))
end.
End Finite_Products_Definition.
Implicit Arguments Off.
25/02/99, 14:36