Don't understand `destruct` tactic on hypothesis `~ (exists x : X, ~ P x)` in Coq

Question

I'm new to Coq and try to learn it through Software foundations. In the chapter "Logic in Coq", there is an exercise not_exists_dist which I completed (by guessing) but not understand:

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.

Before the destruct, the context and goal looks like:

em: excluded_middle
X: Type
P: X -> Prop
H: ~ (exists x : X, ~ P x)
x: X
F: ~ P x
--------------------------------------
(1/1)
P x

And after it

em: excluded_middle
X: Type
P: X -> Prop
x: X
F: ~ P x
--------------------------------------
(1/1)
exists x0 : X, ~ P x0

While I understand destruct on P /\ Q and P \/ Q in hypothesis, I don't understand how it works on P -> False like here.

NaCl NaCl · Accepted Answer · 2021-05-17T10:17:28

Let me try to give some intuition behind this by doing another proof first. Consider:

Goal forall A B C : Prop, A -> C -> (A \/ B -> B \/ C -> A /\ B) -> A /\ B. 
Proof.
  intros. (*eval up to here*)
Admitted.

What you will see in *goals* is:

1 subgoal (ID 77)
  
  A, B, C : Prop
  H : A
  H0 : C
  H1 : A ∨ B → B ∨ C → A ∧ B
  ============================
  A ∧ B

Ok, so we need to show A /\ B. We can use split to break the and apart, thus we need to show A and B. A follows easily by assumption, B is something we do not have. So, our proof script now might look like:

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.

With goals:

1 subgoal (ID 80)
  
  A, B, C : Prop
  H : A
  H0 : C
  H1 : A ∨ B → B ∨ C → A ∧ B
  ============================
  B

The only way we can get to the B is by somehow using H1. Let's see what destruct H1 does to our goals:

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

We get additional subgoals! In order to destruct H1 we need to provide it proofs for A \/ B and B \/ C, we cannot destruct A /\ B otherwise!

For the sake of completeness: (without the 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.

Another way to view it is this: H1 is a function that takes A \/ B and B \/ C as input. destruct works on its output. In order to destruct the result of such a function, you need to give it an appropriate input. Then, destruct performs a case analysis without introducing additional goals. We can do that in the proof script as well before 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.

From a proof term perspective, destruct of A /\ B is the same as match A /\ B with conj H1 H2 => (*construct a term that has your goal as its type*) end. We can replace the destruct in our proof script with a corresponding refine that does exactly that:

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.

Back to your proof. Your goals before destruct

em: excluded_middle
X: Type
P: X -> Prop
H: ~ (exists x : X, ~ P x)
x: X
F: ~ P x
--------------------------------------
(1/1)
P x

After applying the unfold not in H tactic you see:

em: excluded_middle
X: Type
P: X -> Prop
H: (exists x : X, P x -> ⊥) -> ⊥
x: X
F: ~ P x
--------------------------------------
(1/1)
P x

Now recall the definition of ⊥: It's a proposition that cannot be constructed, i.e. it has no constructors. If you somehow have ⊥ as an assumption and you destruct, you essentially look at the type of match ⊥ with end, which can be anything.

In fact, we can prove any goal with it:

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.

Its proofterm is:

(λ (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))

Anyhow, destruct on your assumption H will give you a proof for your goal if you are able to show exists x : X, ~ P x -> ⊥.

Instead of destruct, you could also do exfalso. apply H. to achieve the same thing.

Don't understand `destruct` tactic on hypothesis `~ (exists x : X, ~ P x)` in Coq

2 Answers