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

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

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