在这项练习中迷失了方向

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.

然后我必须证明错误。我不知道该怎么做。这是不可证实的吗？你能把我朝正确的方向吗？还是我在这里错过了什么？

编辑：ptival，您是一个很好的帮助...我注意到这个问题上有一个错误，当我尝试编辑问题时，我不小心点击了删除按钮，惊慌失措并击中了Backspace。：（

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

其余的非常容易，并且要弄清楚这是否确实是您想要的目标。