(** 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.