如何推理Coq中的条件？

我正在使用Coq标准库中的ListSet模块。我不确定如何在证明中推理条件。例如，我遇到以下证据有问题。为上下文提供了定义。如何推理Coq中的条件？

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

为H是真实的，如果a <> x是，如果set_mem xs是真实的唯一方法。我应该能够将H中的条件应用到a <> x以获得set_mem xs。但是，我不明白如何做到这一点。我该如何处理，分解或应用条件？

来源

2011-10-29 danportin

你试过吗？（语法可能是越野车，没有coqtop这里ATM）

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

（if <foo>是match <foo> with或多或少是相同的。你必须降低（destruct，case，...），使得比赛可以（或者对于if，事情必须减少到第一个或第二个构造函数，无论你使用何种类型的构造函数。）大多数情况下，你需要得到案例分析的值（尽管不在这里）。如果你需要它，做一个remember (<value>) as foo; destruct foo而不是直接破坏。）

来源

2011-10-30 17:01:19 nobody

我相信我的理解。 '战术破坏（Aeq_dec）'破坏'H'内的和，为总和的左右分支产生两个子目标。第一种情况产生矛盾的假设并且微不足道;第二部分介绍了归纳假设的前提。我没有意识到我可以破坏嵌套在假设内的一笔款项。感谢您指出这一点。 – danportin

如何推理Coq中的条件？

回答

相关问题