如何在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爲脅迫，並有使它更易於使用特殊的支持。如果你有興趣，我建議你看看他們！