primitive-types - 证明中的原始操作

Question

为了学习依赖类型，我正在用 Idris 重写我的旧 Haskell 游戏。目前游戏“引擎”使用内置的整数类型，例如Word8. 我想证明一些涉及这些数字的数值属性的引理（例如，双重否定是身份）。但是，不可能对原始算术运算的行为说些什么。什么会更好，只使用believe_me或其他手动操作（至少对于最基本的属性），或者使用 和其他“高级”数字类型重写我的Nat代码Fin？

Answer 1

我建议您使用postulate任何您需要的原始属性，当然，注意只使用对所讨论的数字类型实际上是正确的东西（这基本上只是意味着要小心溢出）。所以你可以这样说：

postulate add_commutes : (x, y : Int) -> x + y = y + x

believe_me除非您需要证明的某些计算行为，否则最好避免。但是，老实说，在推理原语时，我们仍在努力解决这些问题……

Answer 2

我相信目前通常最好在可以使用Nat时使用。Idris 开发人员计划最终实现一种通用机制，用于在编译中用快速原始类型替换对证明友好的类型，但目前这只发生在Nat. 如果你真的想要，你可以believe_me通过，但你最终会得到在证明中不太容易使用的函数。请注意，如果您决定使用believe_me，那么您还应该考虑really_believe_me，这显然使类型检查器更可信。