在下面的证明中，策略破坏做了什么?

Question

我正在阅读Benjamin Pierce的软件基础系列。在第一本书的逻辑章节中，我遇到了一个问题。在证明定理

Theorem not_exists_dist :
excluded_middle ->
forall (X:Type) (P : X -> Prop),
~ (exists x, ~ P x) -> (forall x, P x).

其中excluded_middle为

Definition excluded_middle := forall P : Prop,
P / ~ P.

定理的证明可以如下:

Proof.
unfold excluded_middle.
intros exmid X P H x.
destruct (exmid (P x)) as [H1 | H2].
- apply H1.
- destruct H.
exists x. apply H2.
Qed.

令我困惑的是第二种情况下的destruct H。destruct战术在这里做什么?这似乎和我以前所知道的不一样。(H这里是~ (exists x : X, ~ P x))。使用destruct H后，子目标由P x转换为exists x : X, ~ P x。

Answer 1

当您销毁形式为A -> B的项时，您将得到A的目标和destruct B将产生的目标。not A被定义为A -> False，所以在你的例子中，B是False,destruct B没有目标。所以你最终只得到A。

这是一个很长的证明:

Theorem not_exists_dist :
excluded_middle ->
forall (X:Type) (P : X -> Prop),
~ (exists x, ~ P x) -> (forall x, P x).
Proof.
unfold excluded_middle.
intros exmid X P H x.
destruct (exmid (P x)) as [H1 | H2].
- apply H1.
- assert(ex (fun x : X => not (P x))) as H3.
exists x. apply H2.
specialize (H H3).
destruct H.
Qed.