coq - 不理解 Coq 中假设 `destruct` 的 `~ (exists x : X, ~ P x)` 策略

Question

我是 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

虽然我理解 destruct on P/\Q and P\/Q in hypothesis，但我不明白它是如何工作的P -> False 就像这里一样。

Answer 1

让我尝试通过先做另一个证明来给出一些直觉。考虑:

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简写)

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.

从证明术语的角度来看，destruct of A/\B 与 match A/\B with conj H1 H2 => (*construct一个以你的目标为类型的术语*) 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

应用不在 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 ⊥ w​​ith 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。应用 H. 来实现相同的目的。