问题标签 [peano-numbers]

我正在阅读软件基础这本书来学习Coq，但我被困在了Numbers上。在这个类型定义中

当我们在定义中使用它时会O变成怎样0

我只知道O表示自然数并S取一个自然数并返回另一个自然数。我没有得到的是，当我们定义的nat数据类型在pred定义中使用时如何O表示0？而S n'pattern match给我们的前身是怎样的n。

我正在尝试通过 generateSequence 函数从数字 0 和后继函数 S 创建自然数的流/序列。

这是我所拥有的：

我知道这似乎不是解决这个问题的最佳方法，因为已经有增量运算符，并且已经有生成前 n 个自然数的捷径，但我希望 S 成为一个类或至少是对象后面还有一些其他的原因。

当我编译它时，我收到以下消息：

和

核心中定义的公共构造函数 S() 的参数太多。

我尝试过的其他事情是将 S 重写为

或将 generateSequence 函数更改为

这也不起作用。最后一个函数得到编译消息“意外的类型规范”和“意外的标记（使用';'来分隔同一行上的表达式”。

有什么办法可以解决这个问题，让println函数打印出前 10 个自然数，并且仍然使用后继类？

我已经为 Peano 数字定义了类型

现在我发现自己有两个约束Plus a b c和Plus c d e.

如何在我的类上定义一个加法操作，以便编译器能够派生Plus a (b + d) e？

我有点困惑，在自然数上定义的后继函数的内射性是否Coq是公理？根据Wikipedia/Peano axioms，它是一个公理 (7)。当我查看Coq.Init.Peano手册页时，我看到以下内容：

定义 eq_add_S nm (H: S n = S m): n = m := f_equal pred H。

提示立即 eq_add_S：核心。

它看起来像一个公理（？），但让我感到困惑的是，在该页面的顶部它说：

它陈述了关于自然数的各种引理和定理，包括皮亚诺的算术公理（在 Coq 中，这些是可证明的）

这句话有点模棱两可吧？

有人可以解释如何在没有循环的情况下完成这项工作吗？

我正在学习 coq 并试图证明 peano 算术的等式。

我陷入了一个简单的分数定律。

我们从小学就知道 (n + m) / 2 = n / 2 + m / 2。在 peano 算术中，这仅在 n 和 m 是偶数时才成立（因为除法会产生正确的结果）。

所以我们定义：

据我了解，这是一个正确且可证明的定理。我尝试了一个归纳证明，例如

这让我陷入了这样的境地

en = even (S n) 并且IHn : even n -> Nat.div2 n + Nat.div2 m = Nat.div2 (n + m)，所以我找不到应用归纳假设的方法。

经过对标准库和文档的长期研究，我找不到答案。

让我们假设有带有 dif/2 的 pure_2 Prolog 和没有 dif/2 的 pure_1 Prolog。我们能否在不使用 dif/2 的情况下实现 Peano 值的独立性，即 Peano 数？因此，让我们假设我们在 pure_2 Prolog 中有这样的 Peano 独立性：

我们可以用更纯粹的定义替换 neq(X,Y)，即来自不使用 dif/2 的 pure_1 Prolog 吗？所以我们有一个终止的 neq/2 谓词可以决定 Peano 数的不等式？那么它的定义是什么？

在 Uni，我们面临一个挑战，即使用累加器创建 Peano 数的尾递归加法。我们不允许使用任何库函数或我们创建的其他函数，但我们可以将累加器“隐藏”在辅助函数中

这是类型

我被困在如何执行累加器上，因为它对定义的类型没有任何操作，即以下是不可能的

帮助 xD

我正在编写一个可以执行 Peano 算术的 prolog 程序。

我有自然数的标准定义。

因为我想枚举自然数之间所有可能的加法关系，所以我定义了一个辅助函数（为了定义集合上的总排序）。

然后，我定义了加法

如果我在这个加法的定义上列举所有可能的关系，它工作得很好。当输出一组有限的答案时，它可以停止。

这些工作正常。

但是，如果我进行常规的前向评估，

这个程序不能停止。

我想知道：有没有办法

1. 对于任何有限的答案，给出一个有限的结果。
2. 对于任何无限答案，修复一个特定的有效答案，在有限时间内给出这个指定的答案