Parametric Arity Functions

(* SETOID FUNCTIONS WITH PARAMETRIC ARITY  *)
(* by Venanzio Capretta                    *)
(* Coq version 6.2.3                       *)

Require Export Setoids.
Require Export Finite_Sets.

(* We want to define types of functions whose arity is given by parameters.    The arity will be given by a natural number n and a family of n setoids    A : (Finite n) -> Setoid. *)

(* There are many ways of representing such a type. Each representation has    some advantages, so we will define operators to commute from one    representation to an other. *)

(* First representation: curried functions. *)

Fixpoint Curry_setoid_function [n:nat]
  : ((Finite n) -> Setoid) -> Setoid -> Setoid
:=
<[n:nat]((Finite n) -> Setoid) -> Setoid -> Setoid>
Cases n of
    O => [A][B]B
  | (S n') => [A][B](S_Fun (A (fin_zero n'))
                              (Curry_setoid_function n'
                                                     [i](A (fin_succ i))
                                                     B
                              )
                    )
end.

(* Second representation: functions with a functional argument.    The arguments of the function are given by a function on a finite set:    f : (i:(Finite n))(A i) -> B. *)

Section Functional_Argument_Function.

Variable n : nat.
Variable A : (Finite n) -> Setoid.
Variable B : Setoid.

(* First of all we must transform the Set (i:(Finite n))(A i) in a setoid    with the extensional equality. *)

Definition ff_eq :
  (relation (i:(Finite n))(A i))
:=[f,g](i : (Finite n)) (f i) [=] (g i).

Lemma ff_eq_equivalence : (Equiv ff_eq).

Definition FF_setoid : Setoid :=
  (setoid ff_eq_equivalence).

(* Our second representation is then a function from this setoid to B. *)

Definition Fun_arg_function : Setoid := (S_Fun FF_setoid B).

End Functional_Argument_Function.

(* The third representation takes an n-tuple as an argument:    f : A0 X ... X A(n-1) -> B. *)

(* First of all we must define the n-fold product of setoids.         *)
(* Special case for n=1 to avoid a spurious argoument of type S_unit. *)

Definition S_multi_prod_step
  : (n:nat)
    (((Finite n) -> Setoid) -> Setoid) ->
    ((Finite (S n)) -> Setoid) -> Setoid
:=
[n:nat]
<[n:nat](((Finite n) -> Setoid) -> Setoid) ->
        ((Finite (S n)) -> Setoid) -> Setoid>
Cases n of
    O => [_][A](A (fin_zero O))
  | (S n') => [n_pr][A](S_prod (A (fin_zero (S n')))
                               (n_pr [i](A (fin_succ i)))
                       )
end.

Fixpoint S_multi_prod [n:nat] : ((Finite n) -> Setoid) -> Setoid :=
<[n:nat]((Finite n) -> Setoid) -> Setoid>
Cases n of
    O => [A]S_unit
  | (S n') => (S_multi_prod_step n' (S_multi_prod n'))
end.

(* Our third representation is then a function with this setoid as domain. *)
Definition Tuple_arg_function
  : (n:nat)((Finite n)->Setoid) -> Setoid -> Setoid
:= [n,A,B](S_Fun (S_multi_prod n A) B).

(* Now we need to define operators to commute between these representations. *)

(* Conversion from the first (curried function) to the second (function    argument) representation. *)

(* Case n=0. *)

Section Conversion12_Case0.

Variable A : (Finite O) -> Setoid.
Variable B : Setoid.

Variable f : (Curry_setoid_function O A B). (* == B *)

Local conv12_case0_fun : (FF_setoid O A) -> B :=
[args]f.

Remark conv12_case0_well_defined
  : (fun_well_defined conv12_case0_fun).

Definition conv12_case0 : (Fun_arg_function O A B) :=
  (setoid_function conv12_case0_well_defined).

End Conversion12_Case0.

Lemma conv12_case0_well_defined :
  (A : (Finite O) -> Setoid)(B : Setoid)
  (fun_well_defined (conv12_case0 A B)).

Definition curry_to_fun_arg_0
  : (A : (Finite O) -> Setoid)(B : Setoid)
    (S_Fun (Curry_setoid_function O A B) (Fun_arg_function O A B))
:=
[A][B](setoid_function (conv12_case0_well_defined A B)).

Section Conversion12_CaseS.

Variable n : nat.

Variable curry_to_fun_arg_IH :
  (A : (Finite n) -> Setoid)(B : Setoid)
  (S_Fun (Curry_setoid_function n A B) (Fun_arg_function n A B)).

Variable A : (Finite (S n)) -> Setoid.
Variable B : Setoid.

Local A' : (Finite n) -> Setoid := [i](A (fin_succ i)).

Local conv12_IH :
  (S_Fun (Curry_setoid_function n A' B) (Fun_arg_function n A' B))
:= (curry_to_fun_arg_IH A' B).

Section Conv12_CaseS_function.

Variable f : (Curry_setoid_function (S n) A B).
             (* == A0 => (Curry_setoid_function n A' B) *)

Local one_less_arg : (FF_setoid (S n) A) -> (Fun_arg_function n A' B) :=
  [args](conv12_IH (f (args (fin_zero n)))).

Remark one_less_arg_well_defined
  : (fun_well_defined one_less_arg).

Local conv12_caseS_fun : (FF_setoid (S n) A) -> B :=
  [args]( (one_less_arg args) [i](args (fin_succ i)) ).

Remark conv12_caseS_well_defined
  : (fun_well_defined conv12_caseS_fun).

Definition conv12_caseS : (S_Fun (FF_setoid (S n) A) B) :=
  (setoid_function conv12_caseS_well_defined).

End Conv12_CaseS_function.

Lemma conv12_caseS_well_defined :
  (fun_well_defined conv12_caseS).

Definition curry_to_fun_arg_S :
  (S_Fun (Curry_setoid_function (S n) A B) (Fun_arg_function (S n) A B))
:=
(setoid_function conv12_caseS_well_defined).

End Conversion12_CaseS.

(* Here is the operator that covert a function in the first representation    into the second representation. *)

Fixpoint curry_to_fun_arg [n : nat]
  : (A : (Finite n) -> Setoid)(B : Setoid)
    (S_Fun (Curry_setoid_function n A B) (Fun_arg_function n A B))
:=
<[n:nat](A : (Finite n) -> Setoid)(B : Setoid)
        (S_Fun (Curry_setoid_function n A B) (Fun_arg_function n A B))>
Cases n of
    O => curry_to_fun_arg_0
  | (S n') => (curry_to_fun_arg_S n' (curry_to_fun_arg n'))
end.

(* Conversion from the second (function argument) to the first    (curried function) representation. *)

(* Case n=0. *)

Section Conversion21_Case0.

Variable A : (Finite O) -> Setoid.
Variable B : Setoid.

Local conv21_case0_fun :
  (Fun_arg_function O A B) -> (Curry_setoid_function O A B)
:=
[f](f [i](empty_finite_O (A i) i)).

Remark conv21_case0_well_defined
  : (fun_well_defined conv21_case0_fun).

Definition fun_arg_to_curry_0 :
  (S_Fun (Fun_arg_function O A B) (Curry_setoid_function O A B))
:=
(setoid_function conv21_case0_well_defined).

End Conversion21_Case0.

(* Case n = (S n'). *)

(* In this case we have first to give a preliminary definition:    suppose we have a function f : (FF_setoid n [i](A (succ i)))    and an element a0 : (A O).    We then want to define a new function         f' : (FF_setoid (S n) A)    such that (f' O) = a0 and (f' (succ i)) = (f i). *)

Section Finite_Function_Succ.

Variable n : nat.
Variable A : (Finite (S n)) -> Setoid.

Variable f : (FF_setoid n [i](A (fin_succ i))).
Variable a0 : (A (fin_zero n)).

(* First of all we define the function by cases on the argument. *)

Definition f_cases : (m : nat)(p : (gt (S n) m))(A (fin_inj p)) :=
[m:nat]
<[m:nat](p : (gt (S n) m))(A (fin_inj p))>
Cases m of
    O => [_]a0
  | (S m') => [p](eq_rec (Finite (S n)) ? A
                         (f (fin_inj (gt_S_n m' n p)))
                         ?
                         (fin_succ_inj p)
                 )
end.

Definition ff_add_new_argument : (FF_setoid (S n) A) :=
[i](eq_rec (Finite (S n)) ? A
           (f_cases (fin_extr i) (fin_extr_gt i))
           ?
           (fin_section i)
   ).

End Finite_Function_Succ.

Lemma f_cases_well_defined1 :
  (n : nat)(A : (Finite (S n))->Setoid)
  (f1, f2 : (FF_setoid n [i:(Finite n)](A (fin_succ i))))
  f1 [=] f2 ->
  (a0 : (A (fin_zero n)))
  (m:nat)(p:(gt (S n) m))
    (f_cases n A f1 a0 m p) [=] (f_cases n A f2 a0 m p).

Lemma ff_add_new_argument_well_defined1 :
  (n : nat)(A : (Finite (S n))->Setoid)(a0 : (A (fin_zero n)))
  (fun_well_defined [f](ff_add_new_argument n A f a0)).

Lemma f_cases_well_defined2 :
  (n : nat)(A : (Finite (S n))->Setoid)
  (f : (FF_setoid n [i:(Finite n)](A (fin_succ i))))
  (a1, a2 : (A (fin_zero n))) a1 [=] a2 ->
  (m:nat)(p:(gt (S n) m))
  (f_cases n A f a1 m p) [=] (f_cases n A f a2 m p).

Lemma ff_add_new_argument_well_defined2 :
  (n : nat)(A : (Finite (S n))->Setoid)
  (f : (FF_setoid n [i:(Finite n)](A (fin_succ i))))
  (fun_well_defined [a0](ff_add_new_argument n A f a0)
  ).

(* Now we ca construct the recursive step. *)

Section Conversion21_CaseS.

Variable n : nat.

Variable fun_arg_to_curry_IH :
  (A : (Finite n) -> Setoid)(B : Setoid)
  (S_Fun (Fun_arg_function n A B) (Curry_setoid_function n A B)).

Variable A : (Finite (S n)) -> Setoid.
Variable B : Setoid.

Local A' : (Finite n) -> Setoid := [i](A (fin_succ i)).

Section Conv21_CaseS_function.

Variable f : (Fun_arg_function (S n) A B).

Local f' : (a0 : (A (fin_zero n)))(FF_setoid n A') -> B :=
[a0][args : (FF_setoid n A')](f (ff_add_new_argument n A args a0)).

Remark f'_well_defined1 :
  (a0 : (A (fin_zero n)))(h1, h2 : (FF_setoid n A'))
  h1 [=] h2 -> (f' a0 h1) [=] (f' a0 h2).

Local f'_rec : (a0 : (A (fin_zero n)))(Fun_arg_function n A' B) :=
[a0](setoid_function (f'_well_defined1 a0)).

Local f_curry : (a0 : (A (fin_zero n)))(Curry_setoid_function n A' B) :=
[a0]((fun_arg_to_curry_IH A' B) (f'_rec a0)).

Remark f_curry_well_defined :
  (fun_well_defined f_curry).

Definition conv21_caseS : (Curry_setoid_function (S n) A B) :=
(setoid_function f_curry_well_defined).

End Conv21_CaseS_function.

Lemma conv21_caseS_well_defined :
  (fun_well_defined conv21_caseS).

Definition fun_arg_to_curry_S :
  (S_Fun (Fun_arg_function (S n) A B) (Curry_setoid_function (S n) A B))
:=
(setoid_function conv21_caseS_well_defined).

End Conversion21_CaseS.

(* Here is the operator that covert a function in the second representation    into the first representation. *)

Fixpoint fun_arg_to_curry [n : nat]
  : (A : (Finite n) -> Setoid)(B : Setoid)
    (S_Fun (Fun_arg_function n A B) (Curry_setoid_function n A B))
:=
<[n:nat](A : (Finite n) -> Setoid)(B : Setoid)
        (S_Fun (Fun_arg_function n A B) (Curry_setoid_function n A B))>
Cases n of
    O => fun_arg_to_curry_0
  | (S n') => (fun_arg_to_curry_S n' (fun_arg_to_curry n'))
end.

(* Proof that fun_arg_to_curry is left inverse of curry_to_fun_arg. *)
Axiom fun_arg_inv_curry :
  (n : nat)(A : (Finite n) -> Setoid)(B : Setoid)
  (f : (Curry_setoid_function n A B))
    f [=] ((fun_arg_to_curry n A B) ((curry_to_fun_arg n A B) f)).

(* Proof that curry_to_fun_arg is left inverse of fun_arg_to_curry. *)
Axiom curry_inv_fun_arg :
  (n : nat)(A : (Finite n) -> Setoid)(B : Setoid)
  (f : (Fun_arg_function n A B))
    f [=] ((curry_to_fun_arg n A B) ((fun_arg_to_curry n A B) f)).

(* STILL TO BE DONE:    1) Proof that the two operators are inverse of one another;    2) Defined operators for the third representation. *)

25/02/99, 14:36