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最好避免，除非您需要证明的某些计算行为。但是，老实说，在推理原语时，我们仍在努力解决这些问题......