logic - 用基本策略证明 not (iff a (not a))

Question

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

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

我可以立即用 firstorder 来证明这一点或intuition ，但这些策略对我来说就像魔法一样，我的印象是它们涉及一些复杂的自动化。使用简单的显式策略(例如rewrite)来证明该定理的更显式方法是什么？ , destruct , apply , assert ？

Answer 1

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

然后，为了实现如此获得的目标，可以根据上下文使用多种策略，例如:

• 策略介绍、应用、精确和假设用于最小命题逻辑；
• 在存在归纳类型的情况下使用诸如析构、反转、区分或注入(inject)等策略；<
• 等，参见Coq reference manual

在您的示例中，intros、destruct、apply 和 assumion 就足够了:

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 some 是 something 的符号；简单(参见doc)。

希望这有帮助