Coq中的反例证明

Question

在证明了命题和谓词演算中的数十个引理之后（有些比其他的更具挑战性，但通常在 intro-apply-destruct 自动驾驶仪上仍然可以证明）我从 ~forall 开始找到一个并立即被卡住。显然，我缺乏对 Coq 的理解和知识。所以，我要求一种低级 Coq 技术来证明一般形式的陈述

~forall A [B].., C -> D.  
exists A [B].., ~(C -> D).

换句话说，我希望有一个通用的 Coq recipy 来设置和触发反例。（对上述函数进行量化的主要原因是它是 Coq 中的一个（或）原始连接词。）如果你想要示例，我建议例如

~forall P Q: Prop, P -> Q.
~forall P: Prop, P -> ~P.

有一个 related question 既没有提出也没有回答我的，所以我想它不是重复的。

Answer 1

回想一下 ~ P 被定义为 P -> False。换句话说，要显示这样的陈述，假设 P 并得出矛盾就足够了。关键是你可以用任何你喜欢的方式使用 P 作为假设。在普遍量化陈述的特殊情况下，specialize 策略可能会派上用场。这种策略允许我们实例化一个具有特定值的通用量化变量。例如，

Goal ~ forall P Q, P -> Q.
Proof.
  intros contra.
  specialize (contra True False). (* replace the hypothesis 
                                     by [True -> False] *)
  apply contra. (* At this point the goal becomes [True] *)
  trivial.
Qed.

Coq中的反例证明

Proof by counterexample in Coq

coq

proof

quantifiers

negation