coq - 如何在 Coq 中给出反例？

Question

是否可以为一般不成立的陈述提供反例？例如，所有量不分布在连接词“或”上。你会如何开始呢？

Parameter X : Set.
Parameter P : X -> Prop.
Parameter Q : X -> Prop.

(* This holds in general *)
Theorem forall_distributes_over_and
  : (forall x:X, P x /\ Q x) -> ((forall x:X, P x) /\ (forall x:X, Q x)).
Proof.
intro H. split. apply H. apply H.
Qed.

(* This doesn't hold in general *)
Theorem forall_doesnt_distributes_over_or
  : (forall x:X, P x \/ Q x) -> ((forall x:X, P x) \/ (forall x:X, Q x)).
Abort.

Answer 1

这是一种快速而肮脏的方法来证明类似于您想要的东西：

Theorem forall_doesnt_distributes_over_or:
  ~ (forall X P Q, (forall x:X, P x \/ Q x) -> ((forall x:X, P x) \/ (forall x:X, Q x))).
Proof.
  intros H.
  assert (X : forall x : bool, x = true \/ x = false).
  destruct x; intuition.
  specialize (H _ (fun b => b = true) (fun b => b = false) X).
  destruct H as [H|H].
  now specialize (H false).
  now specialize (H true).
Qed.

我必须在否定中量化 XP 和 Q 才能提供我想要的。你不能用你Parameter的 s 完全做到这一点，因为它们以某种方式固定了一个抽象X,P和Q，从而使你的定理可能为真。

Answer 2

一般来说，如果你想产生一个反例，你可以陈述这个公式的否定，然后证明这个否定是成立的。