Library Beroal.FunListArg

Functions with variable number of arguments

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

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

  • 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).

  • 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).

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).

pointwise operation
Definition pw a0 a1 b n (op : type b (Stream.replicate n a0))
         : type (a1 -> b) (Stream.replicate n (a1 -> a0)).