问题标签 [totality]

我正在尝试在 Coq 中定义 Ackermann-Peters 函数，但收到一条我不理解的错误消息。如您所见，我a, b将 Ackermann 的论点打包成一对ab；我提供了一个为参数定义排序函数的排序。然后我使用Function表单来定义 Ackermann 本身，并为它提供参数的排序函数ab。

我得到的是以下错误消息：

错误：没有这样的部分变量或假设：ack。

我不确定是什么困扰了 Coq，但是在搜索互联网时，我发现了一个建议，使用通过排序或度量定义的递归函数可能存在问题，其中递归调用发生在匹配中。但是，使用投影fst和生成不同的错误消息snd。if-then-else有人可以建议如何在 Coq 中定义 Ackermann 吗？

编辑

我收到一条错误消息：递归调用 dpProof 的主要参数等于

如果我不使用相互递归并使用嵌套固定点，它将结合并通过终止检查器。这是成功组合的代码。

我想更深入地了解它无法通过终止检查的原因？是因为他们无法猜测参数递减吗？有什么方法可以使用相互递归来表达我的功能dpGraphProc？

另外我如何编写dpGraphProc检查整个列表的函数？这里的说法不知怎么用cs'。

我在玩 Coq。具体来说，我正在尝试实现合并排序，然后证明它有效。

我的实现尝试是：

因此，我得到的错误是：

我对这些错误的解释是 l 和 l0 是没有头部的 ls、x 和没有 x 的 ls 以及 x 之后的元素（我猜它决定称为 y？）。我没有在这些列表之一上递归而是在本地定义的列表上递归，这很疯狂。

我是否只允许递归直接来自模式匹配的事物？如果是，这似乎是一个严重的限制。有没有办法解决它？我猜 Coq 无法判断该函数将终止。有什么方法可以证明左右都小于 xs 吗？

我正在尝试game为组合游戏定义归纳类型。我想要一个比较方法来判断两个游戏是lessOrEq、greatOrEq还是。然后我可以检查两个游戏是否相等，如果它们都是和。lessOrConfgreatOrConflessOrEqgreatOrEq

但是当我尝试定义用于进行此检查的相互递归方法时，我得到：

错误：无法猜测 的递减参数fix。

我认为这是因为每次递归调用只有一个游戏或另一个游戏的大小减小（但不是两者都减小）。我如何向 Coq 表明这一点？

这是我的代码。失败的部分是gameCompare, innerGCompare, listGameCompare,的相互递归定义gameListCompare。

我正在使用一个搜索一系列值的函数。

我希望能够对这个功能进行推理。

但是，我似乎无法让 coq 的内置感应原理工具工作。

看起来 coq 是为处理相互递归而不是嵌套递归而设置的。在这种情况下，我基本上有 2 个嵌套的 for 循环。

然而，翻译成相互递归也不是那么容易：

但这会产生错误

对内部的递归调用具有等于“ n + n”而不是“ i1”的主要参数。

所以，看起来我需要使用 measure 让它直接接受定义。我有时会重置 j 很困惑。但是，在嵌套设置中，这是有道理的，因为 i 减少了，而 i 是外循环。

那么，有没有一种处理嵌套递归的标准方法，而不是相互递归？有没有更简单的方法来推理这些案例，而不涉及制作单独的归纳定理？由于我还没有找到自动生成它的方法，我想我还是坚持直接写归纳原理。

我想证明计算a和b终止之间的累积和。

我用一个Acc lt x术语来表明递归减少了，像这样

它清除所有子目标，但不会在Qed语句中进行类型检查。Coq 抱怨：

我想我应该以某种方式L1表明H递归调用中术语中的参数实际上更小，但是我该怎么做呢？

我正在尝试在 Coq 中编写一个用于计算自然除法的函数，但我在定义它时遇到了一些麻烦，因为它不是结构递归。

我的代码是：

如你所见，Coq 不喜欢我的函数 div，它说

错误：无法猜测 的递减参数fix。

我如何在 Coq 中为此功能提供终止证明？我可以证明如果 n>O ^ n<=m -> (mn) < m。

有什么类似s的策略simpl吗Program Fixpoint？

特别是，如何证明以下琐碎的陈述？

显然，这个玩具示例没有Program Fixpoint必要，但我在更复杂的设置中面临同样的问题，我需要证明Program Fixpoint手动终止。

当出现以下代码时：

伊德里斯给出了一个错误：

我已经用其他几种方式重写了这段代码，但无法让 Idris 将其识别为全部。我错了它是完全的，还是伊德里斯无法确定它是完全的？如果它本质上是完全的，我该如何重写它以便 Idris 将其识别为完全？

Agda 中的大小类型是什么？我试图阅读有关MiniAgda的论文，但由于以下几点未能继续：

1. 为什么数据类型在它们的大小上是通用的？据我所知，大小是归纳树的深度。
2. 为什么数据类型在它们的大小上是协变的，即 i <= j -> T_i <= T_j ？
3. >和模式是什么#意思？