CODEWITHSUNDEEP
listvectorcoqproofdependent-type
Joey Eremondi
Joey Eremondi

Reputation: 8433

Which vector library to use in coq?

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?

Upvotes: 8

Views: 1645

Answers (2)

krokodil
krokodil

Reputation: 1366

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.

Upvotes: 5

John Wiegley
John Wiegley

Reputation: 7182

There are generally three approaches to vectors in Coq, each with their own trade-offs:

  1. Inductively defined vectors, as provided by the Coq standard library.

  2. Lists paired with an assertion of their length.

  3. 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.

Upvotes: 8

Related Questions