为什么反演不能用于Coq中的普遍限定假设？

Question

我一直在学习软件基础课程，并找到了以下证明(源链接(。

Theorem not_exists_dist :
  excluded_middle ->
  forall (X:Type) (P : X -> Prop),
    ~ (exists x, ~ P x) -> (forall x, P x).
Proof.
  unfold not. intros.
  unfold excluded_middle in H.
  assert ((P x) / ((P x) -> False)) as HP.
  apply H with (P:=(P x)).
  inversion HP.
  apply H1.
  apply ex_falso_quodlibet. apply H0. exists x. apply H1.
Qed.

我很好奇，为什么有一个断言说(P x) / ((P x) -> False)，当我unfold excluded_middle in H并unfold not in H，我会得到与断言完全相同H : forall P : Prop, P / (P -> False)，只是有一个通用量词。

这一点更加明显，因为这个断言可以通过做apply H来证明，而这一步的全部原因是对新断言的假设进行inversion HP。

问题是，为什么不能在开始时直接做inversion H，而省去定义断言的额外步骤，它只是复制其中一个假设？有没有更好的方法可以做到这一点？

Answer 1

inversion只适用于归纳类型的东西，比如or。 forall不是归纳类型构造函数，因此不能对其执行inversion。人们可以扩展inversion，使其表现得像(e)destruct：如果你给它一些普遍量化的东西，它会产生额外的存在主义和证明义务，你需要履行这些义务来填补缺失的地方，以及破坏结论。但是，这不是它现在的工作方式...

人们可以通过应用H并直接破坏它来做更直接的证明：

Theorem not_exists_dist :
  excluded_middle ->
  forall (X:Type) (P : X -> Prop),
    ~ (exists x, ~ P x) -> (forall x, P x).
Proof.
  intros.
  destruct (H (P x)).
  apply H1.
  exfalso. apply H0. exists x. apply H1.
Qed.