0

一般的に当てはまらないステートメントの反例を示すことは可能ですか？たとえば、すべての数量詞が接続の「または」に分散しない場合などです。そもそもそれをどのように述べますか？

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.
4

2 に答える 2

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それであなたの定理を潜在的に真実にします。

于 2012-12-14T04:38:23.220 に答える
1

一般に、反例を作成する場合は、式の否定を記述して、この否定が満たされていることを証明できます。

于 2012-12-17T12:26:55.157 に答える