MSetを使用しているcoqの証明

Question

私はまだcoqに新しいです、そして、MSetsは私にいくつかの問題を与えています。要素がリストかセットかを計算する2つの関数は、set_containsの定義が正しいと思うかどうか、もっと良い方法があれば教えてください。助けてくれてありがとう。

Require Import MSets ZArith. 
    Module mset := MSetAVL.Make Positive_as_OT. 
    Notation pos_set := mset.t. 

    Definition set_contains (x : positive) (s : pos_set) := 
     mset.mem x s. 

    Fixpoint list_contains (x : positive) (l : list positive) : bool := 
     match l with 
     | nil => false 
     | y :: l' => 
     if Pos.eqb x y then true 
     else nodelist_contains x l' 
    end. 

    Lemma nodelist_nodeset_contains : 
     forall x (s : pos_set), 
     (nodelist_contains x (mset.elements s)) = (nodeset_contains x s). 
    Proof. 
     induction s. 
     destruct list_contains. 
     destruct set_contains. 
     auto. 

set_containsは、destructsの後のベースケースでtrueと評価されています。理由はわかりません。証明のその段階の間、セットはmset.emptyにならないでしょうか？

私はまた、mset.Inで作業する方法がわからない、私はこの証明のベースケースに問題がある、明らかに私は同じ問題があります。私は最終的に状態：

Lemma nodelist_containsP : 
     forall x (l : pos_set), 
     reflect (mset.In x l) (nodeset_contains x l). 

もし私がこの証拠をどのようにしたのですか？

 intros. 
     apply iff_reflect. 
     unfold nodeset_contains. 
     symmetry. 
     apply mset.mem_spec. 
     Qed. 

Answer 1

list_containsとset_containsは、それは感覚がdestructにそれらをしようとすることはできないような機能です。 Coqは、あなたが意味していたことを推測しようとし、それぞれlist_containsとset_containsで始まる式の値を大文字にしたいと思っています。

これはあなたが望むものではありません。あなたが望むのは、同じ入力上の2つの関数の動作を観察することです。そして、あなたはそれを検査することによってそうすることができます。

これは正しい方向にあなたを送信する必要があります：

destruct s as [mset mset_isok]. 
    induction mset. 
    + unfold set_contains, mset.mem. 
    simpl. 
    reflexivity. 
    + unfold list_contains, set_contains, mset.mem. 
    simpl.