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.