问题标签 [convoy-pattern]

我正在尝试在 Coq 中编写 Eratosthenes 的筛子。我有一个功能crossout : forall {n:nat}, vector bool n -> nat -> vector bool n。当筛子找到一个素数时，它crossout会标记所有非素数，然后在结果向量上递归。筛显然不能在向量本身上进行结构递归，但它在向量的长度上是结构递归的。我想要的是做这样的事情：

但如果我这样写，Coq 会抱怨长度v'不是n. 我知道它是，但无论我如何构造函数，我似乎都无法说服 Coq 它是。有谁知道我该怎么做？

在一些依赖类型语言（例如 Idris）中实现向量加法是相当简单的。根据维基百科上的示例：

（请注意 Idris 的整体检查器如何自动推断添加Nil和非Nil向量在逻辑上是不可能的。）

我正在尝试使用自定义向量实现在 Coq 中实现等效功能，尽管它与官方Coq 库中提供的非常相似：

当 Coq 尝试检查vpadd时，会产生以下错误：

请注意，我使用False_rect指定不可能的情况，否则整体检查不会通过。但是，由于某种原因，类型检查器无法n0与n1.

我究竟做错了什么？

我正在考虑编写一个 Coq 程序来验证关系代数的某些属性。我有一些基本的数据类型可以工作，但是连接元组给我带来了一些麻烦。

这是代码的相关部分：

在函数 concatTuples 中，在 nil 的情况下，CoqIDE 给我一个错误：

我想我明白那里发生了什么；类型检查器无法弄清楚s并且concatSchema nil s是相等的。但我发现更奇怪的是，当我添加以下行时：

并将大小写更改为nil => stupid b，它可以工作。（好吧，它仍然抱怨 cons 案例，但我认为这意味着它正在接受 nil 案例。）

我对此有三个问题：

1. 有没有办法消除stupid？似乎 Coq 知道类型是相等的，它只需要某种提示。
2. 我到底该怎么做呢？我在编写类似stupid函数时遇到了很多麻烦。
3. 这甚至是异构列表的正确方法吗？这对我来说似乎是最直接的一个，但我对 Curry-Howard 以及 Coq 代码的实际含义有一个非常松散的理解。

我正在尝试使用“护航模式”来保留 3 个变量（两个参数和返回值）之间的依赖关系：

问题出现在最后一个定义中。有什么建议为什么它不起作用？

我正在尝试进行以下工作：

代替最后一个“_”，我需要一个“f t”等于“Some t'”的证据。我不知道如何从比赛中得到它。Vnth 定义为：

我在实现简单功能时遇到问题，我很确定答案是“护航模式”，但我只是不知道如何在这种特殊情况下应用它。这是一个完整的例子：

我得到的错误是：

所以基本上我想以某种方式匹配 'n' 对于 (n=S p) 它会重写 (n

我有以下问题，请看代码。

现在我想获得一个f_opt总是返回 type 值的版本A。像这样的东西：

但我收到以下错误：

非详尽的模式匹配：没有找到 pattern 的子句None。

我知道我需要对类型做一些工作，但我不明白我到底应该做什么。

我们将使用有限集的标准定义：

让我们假设我们有一些P : forall {m : nat} (x y : fin m) : Set（重要的是 的两个参数P属于同一类型）。出于演示目的，设 P 为：

现在，我们想编写一个比较两个数字的自定义函数：

这个想法很简单：我们匹配xand y，对于x = F1，y = F1我们平凡地返回相等，对于x = FS x'，y = FS y'我们递归地调用过程x'和y'，对于其他情况，我们可以平凡地返回不等式。

将这个想法直接翻译成 Coq 显然失败了：

在比赛期间x，y我们丢失了类型信息，因此我们无法将它们应用于P. 传递类型相等证明的标准技巧在这里没有帮助：

那么，也许我们可以使用该相等性证明来强制转换x具有与 ? 相同的类型 y？

我们还需要能够在以后摆脱演员阵容。但是，我注意到这 fcast eq_refl x = x还不够，因为我们需要让它与任意等价证明一起工作。我找到了一个叫做 UIP 的东西，它可以满足我的需要。

现在我们准备完成整个定义：

它通过了！但是，它不会评估任何有用的价值。例如，以下产生一个具有五个嵌套匹配项而不是一个简单值（in_right或in_left）的术语。我怀疑问题出在我使用的 UIP 公理上。

所以最后，我想出的定义几乎没有用。我也尝试过使用convoy 模式进行嵌套匹配，而不是同时匹配两个值，但我遇到了同样的障碍：一旦我对第二个值进行匹配，就P不再适用于它。我可以用其他方式吗？

我有一个异构列表，如 CPDT 中所述：

并尝试在Ensembles 列表和元素列表之间定义“逐点成员资格”谓词：

然而，Coq 抱怨这Ensembles.In (B a1) b1 b2部分：

直观地说，a1和a2是相同的，因为它们是同一个types列表的头部。我如何将它传达给 Coq？我尝试匹配elems并将cons x xs违规行更改为Ensembles.In (B x) b1 b2，但这会导致类似的错误。我还阅读了有关 Convoy 模式的信息，但不确定如何在这种情况下应用它。

我想要向量的最后 k 个元素。我参考Coq.Vectors.VectorDef编写了这段代码。

rectEucLastN说The type of this term is a product while it is expected to be (P ?n@{n1:=0%nat} ?n0@{k1:=0%nat} ?e@{n1:=0%nat; e1:=[]}).

问题是代码底部的第二行。

为什么最后一个模式有错误？