Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

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?

like image 355
jmite Avatar asked Feb 17 '17 16:02

jmite


2 Answers

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.
like image 57
John Wiegley Avatar answered Oct 13 '22 18:10

John Wiegley


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.

like image 5
krokodil Avatar answered Oct 13 '22 19:10

krokodil