如何在Coq中提供抗衡？ [英] How to give a counterxample in Coq?

问题描述

是否有可能为一个通常不成立的陈述提供反例？例如，所有量词不分布在连接词或上。

Is it possible to give a counterexample for a statement which doesn't hold in general? Like, for example that the all quantor does not distribute over the connective "or". How would you state that to begin with?

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.

推荐答案

这是证明类似情况的一种快速而肮脏的方法到您想要的内容：

Here is a quick and dirty way to prove something similar to what you want:

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 做到这一点，因为它们以某种方式修复了抽象 X ， P 和 Q ，因此使您的定理可能成立。

I have to quantify X P and Q inside the negation in order to be able to provide the one I want. You couldn't quite do that with your Parameters as they somehow fixed an abstract X, P and Q, thus making your theorem potentially true.

这篇关于如何在Coq中提供抗衡？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！