6

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?

jmite
  • 8,171
  • 6
  • 40
  • 81
  • 2
    I think @ejgallego answers this question in this [coq-club thread](https://sympa.inria.fr/sympa/arc/coq-club/2017-01/msg00099.html). Also, [this answer](http://stackoverflow.com/a/30159566/2747511) by Arthur Azevedo de Amorim has the same spirit: "While dependent types are interesting for some things, it not clear how useful they are in general. My impression is that some feel that they are very complicated to use, and that the benefit of having certain properties expressed at the type level versus having them as separate theorems is not worth this additional complexity." – Anton Trunov Feb 17 '17 at 16:49
  • 1
    Also, you can `Require Vector` (without importing) and use the qualified name `Vector.t`. – Anton Trunov Feb 17 '17 at 16:49
  • @AntonTrunov do you know why it's named t? – jmite Feb 17 '17 at 16:52
  • 2
    It's kind of traditional in OCaml: see e.g. [here](https://github.com/ocaml-batteries-team/batteries-included/blob/a75d25b187b8c5e111fcaf45b17fd5bd0884e8e6/src/batBitSet.mli#L36). Often, a module defines a type (`t`) and some functions operating on values of that type. – Anton Trunov Feb 17 '17 at 16:55
  • 2
    If you want something ready to use AFAICT math-comp's `tuple` is the only option, others have experimented with "the fixpoint definition", you may have luck with it too. – ejgallego Feb 17 '17 at 18:23

2 Answers2

7

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.
John Wiegley
  • 6,972
  • 1
  • 16
  • 20
  • 3
    "Inductive vectors have the downside of requiring a lot of dependently-typed pattern matching". Yeah this seems like something Coq is weaker at compared to Agda. – jmite Feb 22 '17 at 04:42
5

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.

krokodil
  • 1,326
  • 10
  • 18