I'm wondering, is there a commonly used library for vectors in coq, I.e. lists indexed by their length in their type.
Some tutorials reference Bvector, but it's not found when I try to import it.
There's Coq.Vectors.Vectordef, but the type defined there is just named t
which makes me think it's intended for internal use.
What is the best or most common practice for someone who doesn't want to roll their own library? Am I wrong about the vectors in the standard library? Or is there another Lib I'm missing? Or do people just use lists, paired with proofs of their length?
There are generally three approaches to vectors in Coq, each with their own trade-offs:
Inductively defined vectors, as provided by the Coq standard library.
Lists paired with an assertion of their length.
Recursively-nested tuples.
Lists-with-length are nice in that they're easily coerced to lists, so you can reuse a lot of functions that operate on plain lists. Inductive vectors have the downside of requiring a lot of dependently-typed pattern matching, depending on what you're doing with them.
For most developments, I prefer the recursive tuple definition:
Definition Vec : nat -> Type :=
fix vec n := match n return Type with
| O => unit
| S n => prod A (vec n)
end.
I am working extensively with vectors in Coq and I am using standard Coq.Vectors.Vector
module. It is using textbook inductive vector definition.
The main problem is with this approach is it requires tedious type casting in situations where a vector of length, say a+b
and b+a
are not the same type.
I also ended up using Coq CoLoR library (opam instal coq-color
) which includes package CoLoR.Util.Vector.VecUtil
which contains lots of useful lemmas and definitions for vectors. I ended up writing even more on top of it.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With