用基本策略证明不是(如果是(不是))

Question

我在Coq中证明矛盾事物的经验是非常有限的,我找不到用基本策略证明以下定理的明确方法:

Theorem thrm : forall a, not (iff a (not a)).

我可以立即用firstorder或证明它intuition,但这些策略对我来说就像魔术一样,我的印象是它们涉及一些复杂的自动化.这将是一个更明确的方式来证明这个定理简单明确的战术,例如rewrite,destruct,apply,assert？

Answer 1

为了证明一个否定的命题not something,人们可以使用intros策略将预期错误的假设添加到上下文中,然后证明上下文确实是不一致的.这是因为事实not something是缩写something -> False.您可以通过键入Print not.或在证明期间注意到这一点,unfold not.以相应地替换目标.

然后,为了解除如此获得的目标,可以根据具体情况使用几种策略,例如:

• 战术intros,apply,exact和assumption用于最小的命题逻辑;
• 战术如destruct,inversion,discriminate或injection在感应类型的存在;
• 等,请参阅Coq参考手册

在你的榜样,intros,destruct,apply并assumption有足够的:

Theorem thrm : forall a, not (iff a (not a)).
Proof.
intros a Hiff; destruct Hiff as [H1 H2].
apply H1; apply H2; intros Ha; apply H1; assumption.
Qed.

请注意,证明也可以缩短为此等效版本:

Theorem thrm : forall a, not (iff a (not a)).
Proof. now intros a [H1 H2]; apply H1; apply H2; intros Ha; apply H1. Qed.

哪里now something是something; easy(参见文档)的符号.

希望这会有所帮助