Coqの条件文についての考え方を教えてください。

Question

私はCoq標準ライブラリのListSetモジュールを使って作業しています。私は、証明で条件文を推論する方法が不明です。たとえば、私は次の証明に問題があります。定義は文脈のために提供される。

Fixpoint set_mem (x : A) (xs : set) : bool := 
match xs with 
    | nil  => false 
    | cons y ys => 
     match Aeq_dec x y with 
     | left _ => true 
     | right _ => set_mem x ys 
     end 
end. 

Definition set_In : A -> set -> Prop := In (A := A). 

Lemma set_mem_correct1 : forall (x : A) (xs : set), 
    set_mem x xs = true -> set_In x xs. 
Proof. intros. induction xs. 
    discriminate. 
    simpl; destruct Aeq_dec with a x. 
    intuition. 
    simpl in H. 

現在の証拠状態が仮説としてAeq_decのinr含みます。私は帰納の基本事例とinlがAeq_decである帰納的事例を捨てました。

A : Type 
    Aeq_dec : forall x y : A, {x = y} + {x <> y} 
    x : A 
    a : A 
    xs : list A 
    H : (if Aeq_dec x a then true else set_mem x xs) = true 
    IHxs : set_mem x xs = true -> set_In x xs 
    n : a <> x 
    ============================ 
    a = x \/ set_In x xs 

set_mem xsがtrueの場合a <> xがある場合Hが真になるための唯一の方法。私はset_mem xsを得るためにHの条件をa <> xに適用できるはずです。しかし、私はこれを行う方法を理解していません。条件付き取引を処理、分解、または適用するにはどうすればよいですか？

Answer 1

これを試しましたか？ if <foo>がmatch <foo> withとほぼ同じである。あなたがcase、（destructを削減する必要があります、...）試合ができるように、（

destruct (Aeq_dec x a); 
[ subst; elim (n eq_refl) 
| right; apply (IHxs H) 
]. 

（構文は、バギー、気圧ここにいないcoqtopてもよいです） （または、ifの場合は、使用するタイプの最初のコンストラクタまたは2番目のコンストラクタのいずれかに減らなければなりません）ほとんどの場合、大文字と小文字を区別するための値が必要ですあなたが必要な場合は、直接破壊する代わりにremember (<value>) as foo; destruct fooを実行してください。）