在coq中使用哪个向量库? [英] Which vector library to use in coq?

问题描述

我想知道，在Coq中是否有一个常用的向量库，即通过其长度在类型中索引的列表.

I'm wondering, is there a commonly used library for vectors in coq, I.e. lists indexed by their length in their type.

有些教程参考了Bvector，但是当我尝试导入它时却找不到它.

Some tutorials reference Bvector, but it's not found when I try to import it.

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

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?

推荐答案

在Coq中，通常有三种方法来实现向量，每种方法都有自己的权衡:

There are generally three approaches to vectors in Coq, each with their own trade-offs:

1. 归纳定义的向量，由Coq标准库提供.

1. Inductively defined vectors, as provided by the Coq standard library.

列表与长度声明配对.

递归嵌套元组.

具有长度的列表很不错，因为它们很容易被强制转换为列表，因此您可以重用许多对纯列表进行操作的函数.归纳向量的缺点是需要进行很多依赖类型的模式匹配，具体取决于您对它们的处理方式.

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.

这篇关于在coq中使用哪个向量库?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！