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

Question

我目前正在与vellvm合作,开发一个转型.我是一个新手.

编程时,我面临以下警告:

警告:在nat中使用大数字时会发生堆栈溢出或分段错误(观察到的阈值可能会在5000到70000之间变化,具体取决于您的系统限制和执行的命令).

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

由于S构造函数,coq nat定义似乎从外部处理大的int,所以我感到非常惊讶.

我应该如何避免此警告/使用coq中的大数字？我愿意将实现从nat更改为某种二进制构造.

谢谢!

Answer 1

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

然而，在 Coq 中，广泛使用了符号来简化定义、定理和证明的编写。Coq 有一个非常小的内核（我们想要这个是因为我们希望能够相信证明检查器是正确的，我们可以阅读它），上面有很多符号。然而，由于事物有不同的表示，而且只有少数几个好的符号，我们的符号通常会发生冲突。为了突破这个，COQ用途解释作用域消除歧义的符号，并把它们分解成的名字（因为“+”手段add，plus等...）。

你是对的， using Z_scopeis where, +for plusinside Z。