在下面的证明中，策略 destruct 做了什么？

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.

在下面的证明中，策略 destruct 做了什么？

What does the tactic destruct do in the proof below?

coq

coq-tactic