使用MSet的coq證明

Question

所以我對coq仍然陌生，MSets給我一些問題。這裏有兩個函數來計算一個元素是否在列表或集合中，如果你認爲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評估爲真，在破壞後的基本情況下，我不知道爲什麼。在證明的這個階段，這個集合是不是會變成空白的？

我也不知道如何使用mset。在這個證明的基礎案例中遇到了麻煩，顯然我有同樣的問題。我想最終狀態：

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開始的表達式的值。

這不是你想要的。你想要的是在相同的輸入上觀察兩個函數的行爲。你可以通過檢查來做到這一點。

這應該送你在正確的方向：

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