Library Coq.Vectors.VectorDef
Definitions of Vectors and functions to use them
Author: Pierre Boutillier
Institution: PPS, INRIA 12/2010
Names should be "caml name in list.ml" if exists and order of arguments
have to be the same. complain if you see mistakes ...
A vector is a list of size n whose elements belong to a set A.
An induction scheme for non-empty vectors
A vector of length 0 is nil
A vector of length S _ is cons
An induction scheme for 2 vectors of same length
The first element of a non empty vector
The last element of an non empty vector
Definition last {
A} := @
rectS _ (
fun _ _ =>
A) (
fun a =>
a) (
fun _ _ _ H =>
H).
Build a vector of n{^ th} a
The
p{^ th} element of a vector of length
m.
Computational behavior of this function should be the same as
ocaml function.
An equivalent definition of nth.
Put a at the p{^ th} place of v
Version of replace with lt
Remove the first element of a non empty vector
Destruct a non empty vector
Remove last element of a non-empty vector
Add an element at the end of a vector
Copy last element of a vector
Take first p elements of a vector
Remove p last elements of a vector
Concatenation of two vectors
Split a vector into two parts
Two definitions of the tail recursive function that appends two lists but
reverses the first one
This one has the exact expected computational behavior
This one has a better type
rev
a₁ ; a₂ ; .. ; an is
an ; a{n-1} ; .. ; a₁
Caution : There is a lot of rewrite garbage in this definition
Here are special non dependent useful instantiation of induction schemes
Uniform application on the arguments of the vector
map2 g x1 .. xn y1 .. yn = (g x1 y1) .. (g xn yn)
fold_left f b x1 .. xn = f .. (f (f b x1) x2) .. xn
fold_right f x1 .. xn b = f x1 (f x2 .. (f xn b) .. )
fold_right2 g c x1 .. xn y1 .. yn = g x1 y1 (g x2 y2 .. (g xn yn c) .. )
c is before the vectors to be compliant with "refolding".
fold_left2 f b x1 .. xn y1 .. yn = g .. (g (g a x1 y1) x2 y2) .. xn yn
vector <=> list functions