问题标签 [totality]

我正在尝试通过自然数计算奇偶校验和一半的下限：

我尝试了明显的实现parity：

这种类型检查并按预期工作。但是，如果我尝试标记parity为total，伊德里斯开始抱怨：

with我看到的唯一块parity是从parity (S (S n))to递归调用的块parity n，但显然这是有根据的，因为n在结构上小于S (S n).

我如何说服 Idrisparity是完全的？

考虑以下固定点：

Coq 拒绝以下固定点，因为它无法猜测递减的固定点（有时left列表会失去理智，有时它就是那个right）。

这个答案表明可以通过使用 aProgram Fixpoint并指定 a来解决这个问题{measure ((length left)+(length right))}。

我的问题是：

• 普通Fixpoint和 a 和有什么不一样Program Fixpoint？
• 是否可以在常规中显式减少参数Fixpoint？
• 目标是什么Next Obligation？

I stumbled upon what seems to be a strange behavior for Idris.

I'm using Emacs 25.3 on Ubuntu 17.04 and Idris 1.0.

Consider the following module:

When I load this (C-c C-l), I do not get a non-total function warning, and when I try it on the REPL I get this:

... as if Idris is not matching the literal 0 in the third clause. This behavior occurs also when loading the module in a normal shell (idris Strange.idr).

Shouldn't I get some kind of error about non-totality? Is this some bug in this version of Idris?

说我有以下内容Program Fixpoint：

（这个例子基本上l以一种非常愚蠢的方式返回，为了有一个简单的例子）。

在这里，我对f(stored in f_rec) 进行了递归调用，该调用仅在l包含元素时使用，它确保当我使用 时f_rec，length (tl l)确实小于length l.

但是，当我想解决义务时

我没有hd_error l = Some n我需要的假设。

（不知何故，我的印象是它被理解为“就地计算f (tl l)” let in，而不是“延迟计算直到实际使用”）。

为了说明差异，如果我“内联”let ... in语句：

这里我Heq_anonymous : Some n = hd_error []在环境中。

我的问题如下：是否有可能有我需要的假设，即有match ... with陈述生成的假设？

注意：移动let是一个解决方案，但我很想知道如果不这样做是否可行。例如，它可能在f_rec用于各种上下文的情况下很有用，以避免重复f (tl l).

只有当函数的 arg 是传递的 arg 的直接子项时才允许递归，以便 Coq 可以看到它实际上终止了？

假设我们有：

我想说服 Coq 这将终止 - 我尝试通过将范围的大小测量为abs (to - from). 但是，这并不完全有效，因为一旦范围为空（即from >= to），它就会再次开始增加。

我也尝试过测量：

使用我的自定义：

和演员：

但它遇到了我无法证明这一点的问题，None < None并且使用反身preceeds_eq使关系没有很好的基础，这让我回到了同样的问题。

有没有办法说服 Coqrange终止？我的方法完全被打破了吗？

Coq 与许多其他的不同，它接受一个可选的显式参数，该参数可用于指示定点定义的递减结构。

根据 Gallina 规范，1.3.4，

定义语法。但是从它我们知道它必须是一个标识符，而不是一个通用的度量。

但是，一般情况下，存在递归函数，终止不是很明显，或者实际上是，但是终止检查器很难找到递减结构。例如，以下程序交错两个列表，

这个函数显然终止了，而 Coq 就是想不通。原因既不是l1也不l2是每个周期都在减少。但是，如果我们考虑一个定义为 的度量length l1 + length l2呢？那么这个措施显然会减少每次递归。

所以我的问题是，在复杂的情况下，代码不容易以终止检查的方式组织，你如何教育 coq 并说服它接受定点定义？

确定一个集合是否是另一个集合的子集的函数：

为了清楚起见

• beq_nat确定两个自然数相等
• count计算给定自然数在集合中出现的次数
• remove_all从集合中删除给定自然数的每个实例

CoqIDE“无法猜测修复的递减参数。” 鉴于递归是在t（的尾部s1）的子集上完成的，为什么不能保证终止？

注意：此问题来自该网站，其作者要求不要公开发布解决方案。此外，我已经解决了这个练习，因此不需要解决方案。非常感谢您解释为什么coq无法确定终止。

作为通过有根据的关系理解递归的练习，我决定实现扩展的欧几里得算法。

扩展欧几里得算法适用于整数，所以我需要一些有根据的整数关系。我尝试使用 中的关系Zwf，但没有奏效（我需要查看更多示例）。Z我决定nat使用该函数更容易映射Z.abs_nat，然后仅用Nat.lt作关系。我们的朋友wf_inverse_image来帮助我。所以在这里我做了什么：

扩展欧几里得算法是这样的：

现在让我们看看它是否有效：

我知道如果某些定义不透明，可能会发生这种情况，但是我所有的定义都以Defined.. 好吧，其他东西是不透明的，但是什么？如果是一个库定义，那么我认为在我的代码中重新定义它不会很酷。

看来我的问题与this、this other和this有关。

我决定Program Fixpoint试一试，因为我从未使用过它。我很惊讶地发现我可以复制和粘贴我的程序。

更令人惊讶的是，它工作得很好：

什么是不透明euclids的euclids'？以及如何euclids工作？

假设我们正在编写一个 lambda 演算的实现，作为其中的一部分，我们希望能够选择一个新的非冲突名称：

由于 中的递归路径， Idris 总体检查器认为pickName不是总体的，这是go正确的：确实，总体的证明不依赖于任何在语法上更小的术语，而是依赖于观察到如果bindings有k元素，那么它将不需要不仅仅是k + 1递归调用来找到一个新的名字。但是如何用代码来表达呢？

我也倾向于外部验证，首先编写一个函数，然后编写一个（类型检查，但从不执行）证明它具有正确的属性。在这种整体情况下是否有可能pickName？

受@HTNW 启发，看起来正确的方法是使用 aVect而不是列表。从向量中删除元素将使其大小（以类型表示）在语法上更小，避免自己证明的需要。所以，（稍微重构）版本pickName将是