在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中使用哪個矢量庫？

回答

相關問題