疑問符のついたオペレータの仮説

Question

私は過去数週間、Coq証拠アシスタントと協力してきましたが、今日は特別なことに遭遇しました。私はBenjamin Pierceの "Types and programming languages"の練習を通して練習中です。これらの演習のうちの1つでは、特定のホアレの3つ組が有効であるという自己製作プログラミング言語（Pier inの演習ではImp）を証明する必要があります。私はこの証拠をほぼ完成させましたが、私は次のものが有効であることを証明する必要があります。st X <= st Yここで、stはある状態であり、st Xはその状態のId Xに格納された値を返します。

私の仮説の状態以下：今

st : state 
H : (st X <=? st Y) = true 

私の質問は何ですか？ (st X <=? st Y) = trueを意味し、この定理をどのように使って目標を証明することができますか（これはHとほぼ同じです）？

Answer 1

(n <=? m) = true <-> n <= m（インポートに応じて、別のプレフィックスが必要になる場合があります）が必要なのはapply Nat.leb_leです。自然な質問は、どうやってそれを理解するのですか？

まず、Print ident.（本文を示す）またはCheck ident.（定型化に役立つ - 有用な定理）という定義に関する情報を得ることができます。しかし、<=?が識別子ではなく、あなたが代わりにその定義を見つけますする必要があるので、それは、表記法です：

Locate "<=?". 
(* Notation 
    "x <=? y" := Nat.leb x y : nat_scope (default interpretation) *) 

その後、我々は、関連する定理を見つけることができます。

Search Nat.leb. 
(* ... (9 other theorems *) 
    Nat.leb_le: forall n m : nat, (n <=? m) = true <-> n <= m 
    ... 
*) 

我々はまた、中間のステップをスキップすることができますより具体的な検索を行います。記法については引用符が必要です。

Search "<=?" true. (* ... (three other theorems) Nat.leb_le: forall n m : nat, (n <=? m) = true <-> n <= m *)