我是Coq的新手，并尝试通过软件基础来学习它。在"；"Coq中的逻辑"；，有一个练习not_exists_dist，我(通过猜测(完成了，但不理解：
Theorem not_exists_dist :
excluded_middle →
∀ (X:Type) (P : X → Prop),
¬ (∃ x, ¬ P x) → (∀ x, P x).
Proof.
intros em X P H x.
destruct (em (P x)) as [T | F].
- apply T.
- destruct H. (* <-- This step *)
exists x.
apply F.
Qed.
在destruct之前，上下文和目标看起来像：
em: excluded_middle
X: Type
P: X -> Prop
H: ~ (exists x : X, ~ P x)
x: X
F: ~ P x
--------------------------------------
(1/1)
P x
之后是
em: excluded_middle
X: Type
P: X -> Prop
x: X
F: ~ P x
--------------------------------------
(1/1)
exists x0 : X, ~ P x0
虽然我理解假设中P / Q和P / Q上的destruct，但我不明白它是如何在P -> False上工作的。
让我先做另一个证明，试着给出一些直觉。考虑：
Goal forall A B C : Prop, A -> C -> (A / B -> B / C -> A / B) -> A / B.
Proof.
intros. (*eval up to here*)
Admitted.
您将在*goals*中看到的是：
1 subgoal (ID 77)
A, B, C : Prop
H : A
H0 : C
H1 : A ∨ B → B ∨ C → A ∧ B
============================
A ∧ B
好的，所以我们需要展示A / B。我们可以使用split来分解和，因此我们需要显示A和B。A很容易通过假设得出，B是我们所没有的。所以，我们现在的证明脚本可能看起来像：
Goal forall A B C : Prop, A -> C -> (A / B -> B / C -> A / B) -> A / B.
Proof.
intros. split; try assumption. (*eval up to here*)
Admitted.
目标：
1 subgoal (ID 80)
A, B, C : Prop
H : A
H0 : C
H1 : A ∨ B → B ∨ C → A ∧ B
============================
B
我们到达B的唯一方法是以某种方式使用H1。让我们看看destruct H1对我们的目标有什么作用：
3 subgoals (ID 86)
A, B, C : Prop
H : A
H0 : C
============================
A ∨ B
subgoal 2 (ID 87) is:
B ∨ C
subgoal 3 (ID 93) is:
B
我们有更多的子目标！为了破坏H1，我们需要为A / B和B / C提供它的证明，否则我们不能破坏A / B！
为了完整起见：(没有split;try assumption的简写(
Goal forall A B C : Prop, A -> C -> (A / B -> B / C -> A / B) -> A / B.
Proof.
intros. split.
- assumption.
- destruct H1.
+ left. assumption.
+ right. assumption.
+ assumption.
Qed.
另一种查看方式是：H1是一个以A / B和B / C为输入的函数。destruct对其输出进行处理。为了破坏这样一个函数的结果，您需要给它一个适当的输入。然后，destruct在不引入额外目标的情况下执行案例分析。我们也可以在destructing:之前在证明脚本中这样做
Goal forall A B C : Prop, A -> C -> (A / B -> B / C -> A / B) -> A / B.
Proof.
intros. split.
- assumption.
- specialize (H1 (or_introl H) (or_intror H0)).
destruct H1.
assumption.
Qed.
从证明项的角度来看，A / B的destruct与match A / B with conj H1 H2 => (*construct a term that has your goal as its type*) end相同。我们可以将证明脚本中的destruct替换为相应的refine，它正是这样做的：
Goal forall A B C : Prop, A -> C -> (A / B -> B / C -> A / B) -> A / B.
Proof.
intros. unfold not in H0. split.
- assumption.
- specialize (H1 (or_introl H) (or_intror H0)).
refine (match H1 with conj Ha Hb => _ end).
exact Hb.
Qed.
回到你的证明。destruct之前的目标
em: excluded_middle
X: Type
P: X -> Prop
H: ~ (exists x : X, ~ P x)
x: X
F: ~ P x
--------------------------------------
(1/1)
P x
应用unfold not in H策略后，您会看到：
em: excluded_middle
X: Type
P: X -> Prop
H: (exists x : X, P x -> ⊥) -> ⊥
x: X
F: ~ P x
--------------------------------------
(1/1)
P x
现在回想一下定义：这是一个不能构造的命题，即它没有构造函数。如果你以某种方式将Ş作为一个假设，并且你进行了解构，那么你本质上看match ⊥ with end的类型，它可以是任何东西。
事实上，我们可以用它来证明任何目标：
Goal (forall (A : Prop), A) <-> False. (* <- note that this is different from *)
Proof. (* forall (A : Prop), A <-> False *)
split; intros.
- specialize (H False). assumption.
- refine (match H with end).
Qed.
它的证明词是：
(λ (A B C : Prop) (H : A) (H0 : C) (H1 : A ∨ B → B ∨ C → A ∧ B),
conj H (let H2 : A ∧ B := H1 (or_introl H) (or_intror H0) in match H2 with
| conj _ Hb => Hb
end))
无论如何，destruct在你的假设下，如果你能够展示exists x : X, ~ P x -> ⊥，H将为你的目标提供证据。
代替destruct，您也可以使用exfalso. apply H.来实现相同的功能。
通常，当t是归纳类型I的居民时，destruct t适用，为可能用于生成t的I的每个可能构造函数提供一个目标。正如你所说，H的类型是P -> False，这不是一个归纳类型，但False是。所以发生的是：destruct给了你一个第一个目标，对应于H的P假设。将H应用于该目标会产生一个类型为False的术语，这是一种归纳类型，destruct在该术语上正常工作，由于False没有构造函数，因此不会给您任何目标。归纳类型的许多策略在形式为P1 -> … -> Pn -> I的假设下是这样工作的，其中I是归纳类型：它们给你P1…Pn的副目标，然后对I工作。