(** Functions with variable number of arguments *)

Require Import Coq.Lists.List.
Require Beroal.Stream.
Require Beroal.Init.

Set Implicit Arguments.

(** non-dependent type of a function with arbitrary number and types of arguments *)
Definition type (r : Type)
:= fix rec (args : list Type) : Type
:= match args with
	| nil => r
	| arg :: argss => arg -> rec argss
	end.

(** either:
- add ignored last argument;
- generalized axiom K of combinatory logic;
- weakening in sequent calculus. *)
Definition weak (a b : Type) (xs : list Type)
	: (type a xs) -> (type (b -> a) xs).
Proof.
refine (fun a b xs0 => _).
refine ((fix rec (xs : list Type) := _) xs0).
destruct xs as [|x xss].
simpl.
	refine (fun av _ => av).
simpl.
	refine (fun f av => rec _ (f av)).
Defined.

(** either:
- add a copy of the last argument as the first argument;
- generalized axiom S of combinatory logic;
- contraction in sequent calculus. *)
Definition contraction (a b : Type) (xs : list Type)
	: (b -> type (b -> a) xs) -> (type (b -> a) xs).
Proof.
refine (fun a b xs0 => _).
refine ((fix rec (xs : list Type) := _) xs0).
destruct xs as [|x xss].
simpl.
	refine (fun f bv => f bv bv).
simpl.
	refine (fun f xv => rec _ (fun bv => f bv xv)).
Defined.

(** move the last argument to the begining *)
Definition rotate (a b : Type) (xs : list Type)
	: Init.iff_Type (type (a -> b) xs) (a -> type b xs).
Proof.
refine (fun a b xs0 => (_,_)).
refine ((fix rec (xs : list Type) := _) xs0).
	destruct xs as [|x xss].
	simpl.
		refine (fun a => a).
	simpl.
		refine (fun f av xv => rec xss (f xv) av).
refine ((fix rec (xs : list Type) := _) xs0).
	destruct xs as [|x xss].
	simpl.
		refine (fun a => a).
	simpl.
		refine (fun f xv => rec xss (fun av => f av xv)).
Defined.

(** pointwise operation *)
Definition pw a0 a1 b n (op : type b (Stream.replicate n a0))
	 : type (a1 -> b) (Stream.replicate n (a1 -> a0)).
Proof.
refine (fun a0 a1 b => _).
refine (fix rec (n : nat) {struct n} := _).
destruct n as [|pn].
simpl.
	refine (fun bv _ => bv).
change ((a0 -> type b (Stream.replicate pn a0)) ->
		(a1 -> a0) -> type (a1 -> b) (Stream.replicate pn (a1 -> a0))).
	refine (fun op f => _).
	refine (@contraction _ _ _ _).
	refine (fun v => _).
	refine (rec pn (op (f v))).
Defined.