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