如何在 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 t (Int.repr (period1 i))" 的类型为 "bool" 而它的预期类型为 "Prop".

有什么方法可以比较这两种 'int' 类型或将它们转换为其他类型和 return '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.

这将向您显示 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 and MathComp Coq 库大量使用 is_true 作为强制转换，并特别支持使其更易于使用。如果你有兴趣，建议你看看！

如何在 Coq 中提出比较两个 'int' 类型的命题？

How to have a proposition of comparing two 'int' types in Coq?

logic

coq

compcert

强制