如何在 Coq 中比较两个“int”类型？

Question

我在 Coq 的规范文件中有以下定义。我需要一个比较两个“int”类型值的命题。这两个是 't' 和 'Int.repr (i.(period1))'。(i.period1) 和 (i.period2) 的类型为 'Z'。

这是我的代码 sn-p:

Definition trans_uni_r_reject (i: invariant) (om os: block) (rid roff rval t: int) (m: mem) :=
  ( t > (Int.repr (i.(period1)))        
 /\ t < (Int.repr (i.(period2)))
 /\  master_eval_reject i om os rid roff rval m).

这给了我以下错误：

术语“t”的类型为“int”，而预期的类型为“Z”。

---

我也试过了：

   (Int.cmpu Cgt t (Int.repr (i.(period1))))
/\ (Int.cmpu Clt t (Int.repr (i.(period2))))
/\ (master_eval_reject i om os rid roff rval m).

但它给了我这个错误：

术语“Int.cmpu Cgt t (Int.repr (period1 i))”的类型为“bool”，而预期的类型为“Prop”。

有什么方法可以比较这两种“int”类型或将它们转换为其他类型并返回“prop”类型？

谢谢，

Answer 1

任何bool 都可以转换为Prop，方法是将其等同于true。在您的示例中，这将导致：

   Int.cmpu Cgt t (Int.repr (i.(period1))) = true
/\ Int.cmpu Clt t (Int.repr (i.(period2))) = true
/\ master_eval_reject i om os rid roff rval m.

如果您在Int.cmpu 运算符上搜索结果，您可能会在Int 模块中找到许多以Int.cmpu Cgt x y = true 表示的引理。为此，您可以使用SearchAbout 命令：

SearchAbout Int.cmpu. (* Looks for all results on Int.cmpu *)
SearchAbout Int.cmpu Cgt (* Looks for all results that mention
                            Int.cmpu and Cgt *)

强制

将布尔值等同于 true 非常普遍，以至于人们经常声明强制来使用布尔值，就好像它们是命题一样：

Definition is_true (b : bool) : Prop := b = true.
Coercion is_true : bool >-> Sortclass.

现在，您可以在预期命题的上下文中使用任何布尔值：

   Int.cmpu Cgt t (Int.repr (i.(period1)))
/\ Int.cmpu Clt t (Int.repr (i.(period2)))
/\ master_eval_reject i om os rid roff rval m.

在幕后，Coq 在这些事件周围插入对is_true 的隐形调用。但是，您应该知道，强制仍然出现在您的术语中。你可以通过发出一个特殊的命令来看到这一点，

Set Printing Coercions.

它会向你展示 Coq 看到的上面的 sn-p：

   is_true (Int.cmpu Cgt t (Int.repr (i.(period1))))
/\ is_true (Int.cmpu Clt t (Int.repr (i.(period2))))
/\ master_eval_reject i om os rid roff rval m.

（要撤消上一步，只需运行Unset Printing Coercions。）

因为默认情况下不打印强制转换，所以您可能需要一些时间才能有效地使用它们。 Ssreflect and MathComp Coq 库大量使用 is_true 作为强制转换，并特别支持使其更易于使用。如果你有兴趣，我建议你看看他们！