0

我在 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 t (Int.repr (period1 i))”具有“bool”类型，而预期具有“Prop”类型。

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

谢谢，

4

1 回答 1

2

通过将Any等同于 ，bool可以将其转换为 a 。在您的示例中，这将导致：Proptrue

   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.

在幕后，Coqis_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强制转换，并特别支持使其更易于使用。如果你有兴趣，我建议你看看他们！

于 2016-07-26T12:03:57.043 回答