Library Coq.Numbers.NaryFunctions
Open Local Scope type_scope.
Require Import List.
Generic dependently-typed operators about n-ary functions
The type of n-ary function: nfun A n B is
A -> ... -> A -> B with n occurences of A in this type.
Fixpoint nfun A n B :=
match n with
|
O =>
B
|
S n =>
A -> (
nfun A n B)
end.
Notation " A ^^ n --> B " := (
nfun A n B)
(
at level 50,
n at next level) :
type_scope.
napply_cst _ _ a n f iterates n times the application of a
particular constant a to the n-ary function f.
Fixpoint napply_cst (
A B:Type)(a:A)
n : (
A^^n-->B) ->
B :=
match n return (
A^^n-->B) ->
B with
|
O =>
fun x =>
x
|
S n =>
fun x =>
napply_cst _ _ a n (
x a)
end.
A generic transformation from an n-ary function to another one.
Fixpoint nfun_to_nfun (
A B C:Type)(f:B ->
C)
n :
(
A^^n-->B) -> (
A^^n-->C) :=
match n return (
A^^n-->B) -> (
A^^n-->C)
with
|
O =>
f
|
S n =>
fun g a =>
nfun_to_nfun _ _ _ f n (
g a)
end.
napply_except_last _ _ n f expects n arguments of type A,
applies n-1 of them to f and discard the last one.
napply_then_last _ _ a n f expects n arguments of type A,
applies them to f and then apply a to the result.
napply_discard _ b n expects n arguments, discards then,
and returns b.
A fold function
Fixpoint nfold A B (
f:A->B->B)(b:B)
n : (
A^^n-->B) :=
match n return (
A^^n-->B)
with
|
O =>
b
|
S n =>
fun a => (
nfold _ _ f (
f a b)
n)
end.
n-ary products : nprod A n is A*...*A*unit,
with n occurrences of A in this type.
Fixpoint nprod A n :
Type :=
match n with
|
O =>
unit
|
S n => (
A *
nprod A n)%type
end.
Notation "A ^ n" := (
nprod A n) :
type_scope.
n-ary curryfication / uncurryfication
Fixpoint ncurry (
A B:Type)
n : (
A^n ->
B) -> (
A^^n-->B) :=
match n return (
A^n ->
B) -> (
A^^n-->B)
with
|
O =>
fun x =>
x tt
|
S n =>
fun f a =>
ncurry _ _ n (
fun p =>
f (
a,p))
end.
Fixpoint nuncurry (
A B:Type)
n : (
A^^n-->B) -> (
A^n ->
B) :=
match n return (
A^^n-->B) -> (
A^n ->
B)
with
|
O =>
fun x _ =>
x
|
S n =>
fun f p =>
let (
x,p) :=
p in nuncurry _ _ n (
f x)
p
end.
Earlier functions can also be defined via ncurry/nuncurry.
For instance :
We can also us it to obtain another fold function,
equivalent to the previous one, but with a nicer expansion
(see for instance Int31.iszero).
From nprod to list
Fixpoint nprod_to_list (
A:Type)
n :
A^n ->
list A :=
match n with
|
O =>
fun _ =>
nil
|
S n =>
fun p =>
let (
x,p) :=
p in x::(nprod_to_list
_ n p)
end.
From list to nprod
This gives an additional way to write the fold