1

私はこれを証明しなければなりません:

Variable A : Set.
Variable P : A -> Prop.
Variables R : A -> A -> Prop.

Lemma pool : (forall x:A, ~P x) -> ~(exists x:A, ~ P x).

これまでのところ、私はやった：

intros.
unfold not.
intros.
elim H0.
destruct H0.
intros.
exact x0.

次に、False を証明する必要があります。どうすればいいのかわかりません。これは証明不可能でしょうか？私を正しい方向に向けることができますか？それとも、ここで何か不足していますか?

編集: Ptival さん、大変お世話になりました...質問の間違いに気付き、質問を編集しようとしたときに、誤って削除ボタンを押してしまい、パニックになり、バックスペースを押してしまいました。:(

4

1 に答える 1

1

（まあ、もう一度答える：P）

あなたの定理にはまだ欠陥があると思います（Aが空集合でない限り...）。

もしかして：

Lemma pool : (forall x:A, ~P x) -> ~(exists x:A, P x).

その場合、それは実行可能であり、これがあなたが始めることができる方法です：

Proof.
  intros A E.
  destruct E as [x P].

残りは非常に簡単で、それが本当にあなたが最初に望んでいた目標であるかどうかを理解するのはあなた次第です。

于 2012-10-22T20:47:41.650 に答える