在coq中使用哪个矢量库？

我想知道，是否有一个常用的coq向量库，即，列表按其类型的长度进行索引。在coq中使用哪个矢量库？

一些教程引用了Bvector，但是当我尝试导入它时没有找到它。

还有Coq.Vectors.Vectordef，但在那里定义的类型只是名为t，这使我认为它是专门用于内部使用。

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

2017-02-17 jmite

我想@ejgallego在这个[coq-club thread]（https://sympa.inria.fr/sympa/arc/coq-club/2017-01/msg00099.html）回答这个问题。此外，Arthur Azevedo de Amorim的[这个答案]（http://stackoverflow.com/a/30159566/2747511）具有相同的精神：“虽然依赖类型对某些事情很有趣，但它并不清楚它们在一般情况下的有用程度。我的印象是，有些人觉得它们使用起来非常复杂，而且在类型层次上表达某些属性的好处与将它们作为单独的定理相比并不值得这种额外的复杂性。“ –

另外，您可以'需要矢量'（不需要导入）并使用合格的名称'Vector.t'。 –

@AntonTrunov你知道它为什么命名为t吗？ – jmite

通常有三种方法在勒柯克向量，每个都有自己的权衡：

电感定义向量，由勒柯克标准库提供。
与其长度断言配对的列表。可以递归嵌套的元组。

列表，用长度是那可爱的他们很容易地裹挟到列表，这样你就可以重新使用了很多的平原上操作的列表功能。归纳矢量的缺点是需要大量的依赖类型的模式匹配，这取决于你在做什么。

对于大多数的发展，我更喜欢递归元组的定义：

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

来源

2017-02-22 04:14:52

“电感矢量的缺点是需要很多独立类型的模式匹配”。是的，这似乎是Coq与Agda相比较弱。 – jmite

我在勒柯克载体广泛合作，我使用标准Coq.Vectors.Vector模块。它使用教科书归纳矢量的定义。

这个方法的主要问题是它需要繁琐的类型转换，例如在一个长度为a+b和b+a的类型不相同的情况下。

我也结束了使用Coq CoLoR库（opam instal coq-color），其中包含包CoLoR.Util.Vector.VecUtil其中包含很多有用的引理和载体的定义。最后，我写了更多的东西。

来源

2017-10-20 01:25:35 krokodil

在coq中使用哪个矢量库？

回答

相关问题