在coq中使用哪个向量库？

Question

我想知道,coq中是否有一个常用的矢量库,即它们的类型长度索引.

有些教程引用了Bvector,但是当我尝试导入它时却找不到它.

有Coq.Vectors.Vectordef,但是那里定义的类型只是命名t,这使我认为它是供内部使用的.

对于不想推出自己的图书馆的人来说,最好或最常见的做法是什么？我对标准库中的向量有误吗？还是有另一个我失踪的自由人？或者人们只是使用列表,并与他们的长度证明配对？

Answer 1

Coq中的向量通常有三种方法,每种方法都有自己的权衡:

1. 由Coq标准库提供的归纳定义的载体.

2. 列表与其长度的断言配对.

3. 递归嵌套的元组.

列表长度很好,因为它们很容易被强制列表,所以你可以重用很多在普通列表上运行的函数.归纳向量的缺点是需要大量依赖类型的模式匹配,具体取决于您正在使用它们.

对于大多数开发,我更喜欢递归元组定义:

Definition Vec : nat -> Type :=
  fix vec n := match n return Type with
               | O   => unit
               | S n => prod A (vec n)
               end.

Answer 2

我在 Coq 中广泛使用向量，并且我正在使用标准Coq.Vectors.Vector模块。它使用教科书归纳向量定义。

这种方法的主要问题是它需要在长度向量（例如a+b和b+a不是同一类型）的情况下进行繁琐的类型转换。

我还最终使用了 Coq CoLoR 库 ( opam instal coq-color)，CoLoR.Util.Vector.VecUtil其中包含包含许多有用引理和向量定义的包。我最终在上面写了更多。