問題タブ [compcert]

Coq の spec ファイルに次の定義があります。2 つの「int」型の値を比較する命題が必要です。これらの 2 つは 't' と 'Int.repr (i.(period1))' です。(i.period1) と (i.period2) の型は 'Z' です。

これは私のコードスニペットです:

これにより、以下のエラーが表示されます。

用語 "t" は型 "int" を持ちますが、型 "Z" を持つことが期待されます。

私も試しました：

しかし、それは私にこのエラーを与えます:

「Int.cmpu Cgt t (Int.repr (period1 i))」という用語は、「Prop」型を持つことが期待されているのに対し、「bool」型を持ちます。

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

ありがとう、

I have the following Lemma but couldn't prove it:

I found the tactic for equality (link) but can't find the one for lt/ltu or gt/gtu:

Any help will be appreciated!

Thanks,

これら2つのステートメントが等しいことをどのように証明できますか:

1. Val.shru (Val.and a (Vint b)) (Vint c) = Vint ?3434 /\ ?3434 <> d

2. Val.shru (Val.and a (Vint b)) (Vint c) <> d

コンセプトは非常にシンプルですが、それを解決するための適切な戦術を見つけることに行き詰まっています。これは実際に私が証明しようとしている Lemma です:

ありがとう、

私は定義を持っていますmy_def1：

以下のような別の定義を書き、常に を返す公理を追加my_def2したいと思います。my_def1proj_bytes vlSome bl

私の質問は、関連する情報をどのように完成させmy_def2て書くことができますか?axiomproj_bytes vl

list memvalまたは、タイプから list byte[ decode_intaccepts list byte]にキャストするにはどうすればよいですか?

の定義は次のmemvalとおりです。

Mem.load を展開しようとすると、次のエラーが表示されます。

エラー:Mem.load評価可能な参照を強制できません。

とまったく同じことDefinitionを書きましたand is unfoldable 。Mem.loadload1

EvalOp の定義は次のとおりですcompcert.backend.SplitLongproof。

この定義の奇妙な点は、andを 2 つの別個のトークンとしてcoqdoc --html認識していることです。EvalOp

Coq は、間に区切り文字 (スペース) のない 2 つのトークンを許可するのはなぜですか? それともこれはのバグcoqdocですか？助けてくれてありがとう！