Library Coq.Bool.Bvector
Bit vectors. Contribution by Jean Duprat (ENS Lyon).
Require Export Bool.
Require Export Sumbool.
Require Import Arith.
Open Local Scope nat_scope.
We build bit vectors in the spirit of List.v.
The size of the vector is a parameter which is too important
to be accessible only via function "length".
The first idea is to build a record with both the list and the length.
Unfortunately, this a posteriori verification leads to
numerous lemmas for handling lengths.
The second idea is to use a dependent type in which the length
is a building parameter. This leads to structural induction that
are slightly more complex and in some cases we will use a proof-term
as definition, since the type inference mechanism for pattern-matching
is sometimes weaker that the one implemented for elimination tactiques.
A vector is a list of size n whose elements belongs to a set A.
If the size is non-zero, we can extract the first component and the
rest of the vector, as well as the last component, or adding or
removing a component (carry) or repeating the last component at the
end of the vector.
We can also truncate the vector and remove its p last components or
reciprocally extend the vector by concatenation.
A unary function over A generates a function on vectors of size n by
applying f pointwise.
A binary function over A generates a function on pairs of vectors of
size n by applying f pointwise.
Shifting and truncating
Concatenation of two vectors
Uniform application on the arguments of the vector
Eta-expansion of a vector
A bit vector is a vector over booleans.
Notice that the LEAST significant bit comes first (little-endian representation).
We extract the least significant bit (head) and the rest of the vector (tail).
We compute bitwise operation on vector: negation, and, or, xor.
We compute size-preserving shifts: to the left (towards most significant bits,
we hence use Vshiftout) and to the right (towards least significant bits,
we use Vshiftin) by inserting a 'carry' bit (logical shift) or by repeating
the most significant bit (arithmetical shift).
NOTA BENE: all shift operations expect predecessor of size as parameter
(they only work on non-empty vectors).