如何在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”，而它预计有型“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吨（Int.repr（间隔1 I））”有类型“布尔”，而它预计有类型“支柱”。

有没有什么办法可以比较这两个'int'类型或将它们转换为其他类型并返回'prop'类型？

谢谢，

Answer 1

任何bool可以通过将其等同于true转换为Prop。在你的榜样，这将导致：

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. 

它会告诉你上面的代码为勒柯克看到它：

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勒柯克库大量使用is_true为胁迫，并有使它更易于使用特殊的支持。如果你有兴趣，我建议你看看他们！