如何比较Coq中的两种“int”类型？

Question

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

这是我的代码片段：

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”类型，而“t”的类型是"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来转换为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所看到的上述片段：

   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和MathComp Coq库大量使用is_true作为强制，并为使其更易于使用提供了特殊支持。如果你有兴趣的话，我建议你看看！