0

Coq の spec ファイルに次の定義があります。2 つの「int」型の値を比較する命題が必要です。これらの 2 つは '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))」という用語は、「Prop」型を持つことが期待されているのに対し、「bool」型を持ちます。

これら 2 つの 'int' 型を比較したり、別のものに変換して 'prop' 型を返す方法はありますか?

ありがとう、

4

1 に答える 1

2

Anyは に等しくすることboolで に変換できます。あなたの例では、これは次のようになります。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た多くの補題が見つかる可能性があります。これには、次のコマンドを使用できます。IntInt.cmpu Cgt x y = trueSearchAbout

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 に答える