如何避免 Coq nats 中的堆栈溢出或分段错误？答案

【问题标题】：How can I avoid stack overflow or segmentation fault in Coq nats?如何避免 Coq nats 中的堆栈溢出或分段错误？
【发布时间】：2012-12-01 18:15:31
【问题描述】：

我目前正在与vellvm 合作，正在对其进行转换。我是 coq 新手。

在编程时，我遇到了以下警告：

警告：工作时发生堆栈溢出或分段错误 nat 中有大量数字（观察到的阈值可能从 5000 到 70000 取决于您的系统限制和执行的命令）。

生成此警告的函数会计算签名。签名分为上位和下位。给定两个代表高位和低位的 nat n1 和 n2，它计算 (n1*65536)+n2 - 这是将两个 16 位二进制数并排放置的抽象。

我很惊讶，因为 coq nat 定义似乎可以处理来自外部的大整数，这要归功于 S 构造函数。

我应该如何避免这个警告/在 coq 中使用大数字？我愿意将实现从 nat 更改为某种二进制结构。

谢谢！

【问题讨论】：

使用 nats 很麻烦，因为它们是使用 S 构建的，这意味着每个数字字面上都是 S 应用程序的序列：您可能会使用整数相反，它们具有相似的证明原理，但具有基于符号/幅度（位）的表示：coq.inria.fr/library/Coq.ZArith.BinInt.html
那我该如何使用这些操作呢？ (Zpos 1) + (Zpos 2) 似乎不起作用... - 错误：术语“1%Z”的类型为“|”而它的类型应该是“nat”。
那是因为“+”表示多种事物，具体取决于您所在的位置。实际上，“+”只是添加 nat 的语法糖，其中plus 是在两个 nat 上结构定义的。您想将plus 用于整数，它与nat（即Int_scope）的解释范围不同。阅读解释范围以及如何打开和使用它们。
谢谢，我正在与范围作斗争，这工作得很好。最后一个问题：我让它使用 Z_scope 而不是 Int_scope。那样可以么？（请回答以便我选择您的答案）

标签： binary nat bignum coq

【解决方案1】：

与在 Coq 中使用 nat 类型不同，有时（当您必须处理大数字时）使用 Z 类型会更好，这是使用符号大小对表示的整数形式化。权衡是您的证明可能会变得稍微复杂一些。 nat 非常简单，因此承认简单的证明原则。

然而，在 Coq 中，符号的广泛使用使编写定义、定理和证明变得更简单。 Coq 有一个非常小的内核（我们想要这个是因为我们希望能够相信证明检查器是正确的，并且我们可以阅读它）上面有很多符号。但是，由于事物的表示方式不同，而且只有少数好的符号，我们的符号通常会发生冲突。为了解决这个问题，coq 使用interpretation scopes 来消除符号的歧义，并将它们解析为名称（因为“+”表示add、plus 等...）。

你是对的，使用Z_scope 是+ 在Z 中的plus。

【讨论】：