不理解 Coq 中关于假设 ~ (exists x : X, ~ P x) 的 `destruct` 策略
Don't understand `destruct` tactic on hypothesis `~ (exists x : X, ~ P x)` in Coq
我是 Coq 的新手，尝试通过 Software foundations 学习它。在“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 上的工作原理，就像这里一样。
通常，当 t 是归纳类型 I 的居民时，destruct t 适用，为 I 的每个可能的构造函数提供一个目标用于生产 t。正如您所说，H 的类型为 P -> False，这不是归纳类型，但 False 是。那么会发生什么：destruct 给你第一个目标对应于 H 的 P 假设。将 H 应用于该目标会导致 False 类型的术语，这是一种归纳类型，destruct 可以在其上正常工作，因为 False 有没有构造函数。归纳类型的许多策略都基于 P1 -> … -> Pn -> I 形式的假设，其中 I 是归纳类型：它们为您提供 P1 … Pn 的附带目标，然后在 I.
上工作
让我先做另一个证明，试着给出一些直觉。
考虑：
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来打断and，所以我们需要显示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 shorthand）
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 相同。
我们可以用相应的 refine 替换我们的证明脚本中的 destruct ：
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 根据您的假设 H 如果您能够证明 exists x : X, ~ P x -> ⊥.
将为您的目标提供证明
除了 destruct，您还可以 exfalso. apply H. 来达到同样的目的。
我是 Coq 的新手，尝试通过 Software foundations 学习它。在“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 上的工作原理，就像这里一样。
通常，当 t 是归纳类型 I 的居民时，destruct t 适用，为 I 的每个可能的构造函数提供一个目标用于生产 t。正如您所说，H 的类型为 P -> False，这不是归纳类型，但 False 是。那么会发生什么：destruct 给你第一个目标对应于 H 的 P 假设。将 H 应用于该目标会导致 False 类型的术语，这是一种归纳类型，destruct 可以在其上正常工作，因为 False 有没有构造函数。归纳类型的许多策略都基于 P1 -> … -> Pn -> I 形式的假设，其中 I 是归纳类型：它们为您提供 P1 … Pn 的附带目标，然后在 I.
让我先做另一个证明，试着给出一些直觉。 考虑：
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来打断and，所以我们需要显示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 shorthand）
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 相同。
我们可以用相应的 refine 替换我们的证明脚本中的 destruct ：
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 根据您的假设 H 如果您能够证明 exists x : X, ~ P x -> ⊥.
除了 destruct，您还可以 exfalso. apply H. 来达到同样的目的。