variadic currying function

variadic_curry.v

Definition f_id : forall X Y, (X -> Y) -> X -> Y := fun X Y f => f.

Definition next : forall W X Y Z, ((X -> Y) -> Z) -> (W * X -> Y) -> W -> Z :=
  fun W X Y Z f g x => f (fun y => g (x,y)).

Fixpoint arity X n :=
  match n with
  | 0 => X
  | S m => X -> arity X m
  end.

Fixpoint arity_const{X n}(x : X) : arity X n :=
  match n with
  | 0 => x
  | S m => fun _ => arity_const x
  end.

Fixpoint arity_last{X n} : arity X (S n) :=
  match n with
  | 0 => fun x => x
  | S m => fun _ => arity_last
  end.

Fixpoint last_dummy_arg{X} n : arity X n -> arity X (S n) :=
  match n with
  | 0 => fun x _ => x
  | S m => fun g x => last_dummy_arg m (g x)
  end.

Fixpoint arity_map{X} n (f : X -> X) : arity X n -> arity X n :=
  match n with
  | 0 => f
  | S m => fun g x => arity_map m f (g x)
  end.

Fixpoint arity_zip{X} n (f : X -> X -> X) : arity X n -> arity X n -> arity X n :=
  match n with
  | 0 => f
  | S m => fun g1 g2 x => arity_zip m f (g1 x) (g2 x)
  end.

Fixpoint univ_closure{n} : arity Type n -> Type :=
  match n with
  | 0 => fun T => T
  | S m => fun T => forall X, univ_closure (T X)
  end.

Fixpoint curried_type n : arity Type (S (S n)) :=
  match n with
  | 0   => fun X Y => X -> Y
  | S m => fun X => arity_map _ (fun Y => X -> Y) (curried_type m)
  end.

Fixpoint n_prod n : arity Type (S n) :=
  match n with
  | 0 => fun X => X
  | S m => fun X => arity_map _ (fun Y => (X * Y)%type) (n_prod m)
  end.

Definition uncurried_type n : arity Type (S (S n)) :=
  arity_zip _ (fun X Y => X -> Y) (last_dummy_arg _ (n_prod _)) (arity_last).

Definition curry_arity n := arity_zip _ (fun X Y => X -> Y) (uncurried_type n) (curried_type n).

Definition curry_type n : Type := univ_closure (curry_arity n).

Lemma univ_closure_modus_ponens : forall n (P Q : arity Type n),
  (univ_closure (arity_zip _ (fun X Y => X -> Y) P Q)) -> (univ_closure P) -> (univ_closure Q).
Proof.
  induction n; simpl.
  tauto.
  intros.
  apply (IHn (P X1)).
  apply X.
  apply X0.
Defined.

Lemma next_univ : forall n Phi Psi, univ_closure
  (arity_zip (S (S (S n))) (fun X Y : Type => X -> Y)
     (fun _ : Type =>
      arity_zip (S (S n)) (fun X Y : Type => X -> Y) (arity_zip (S (S n)) (fun X Y : Type => X -> Y) (last_dummy_arg (S n) Phi) arity_last) Psi)
     (arity_zip (S (S (S n))) (fun X Y : Type => X -> Y)
        (arity_zip (S (S (S n))) (fun X Y : Type => X -> Y)
           (last_dummy_arg (S (S n)) (fun X x : Type => arity_map n (fun Y : Type => (X * Y)%type) (Phi x))) arity_last)
        (fun X x x0 : Type => arity_map n (fun Y : Type => X -> Y) (Psi x x0)))).
Proof.
  induction n; intros.
  simpl; intros A B C; apply next.
  simpl; intros; apply IHn.
Defined.

Lemma variadic_curry : forall n, curry_type n.
Proof.
  unfold curry_type.
  induction n; intros.
  exact f_id.
  apply (univ_closure_modus_ponens (S (S (S n))) (fun _ => curry_arity _)).
  unfold curry_arity.
  unfold curried_type.
  simpl uncurried_type.
  simpl n_prod.
  apply next_univ.
  intro; exact IHn.
Defined.