coq - 迷失在这个练习中

Question

我必须证明这一点：

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，你帮了大忙……我注意到问题上有一个错误，当我尝试编辑问题时，我不小心点击了删除按钮，惊慌失措并按下退格键。:(

Answer 1

（哦，好吧，再次回答：P）

我相信你的定理仍然有缺陷（除非 A 是一个空集......）。

你的意思是：

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

在这种情况下，这是可行的，您可以从以下方式开始：

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

其余的很容易，由您决定是否这确实是您最初想要的目标。