Destructing hypothesis

Using Coq
1

Hello,

Please see attached file and code.

My question is: why this “destruct” acts like this? what is happening? we have disjunctive pattern with 0 branches here… but destruct works… and changes goal… and leads us to the victory.

1
1898×363 35.7 KB 

(* Exercise: 3 stars, advanced (not_exists_dist) *)

Definition excluded_middle := forall P : Prop,
  P \/ ~P.

Theorem not_exists_dist :
  excluded_middle ->
  forall (X:Type) (P : X -> Prop),
    ~(exists x, ~P x) -> (forall x, P x).
Proof. intros EM X P H x.
       unfold not in H.
       destruct (EM (P x)) as [H2 | H3].
       apply H2.
       destruct H.
       exists x.
       apply H3. 
Qed.
2

AFAIU destruct H with H : A -> B gives A as a new goal and destructs B.
Since here B is False, destructing it solves the goal, so only the A part remains to be proved.

1 Like
3

Maybe it becomes clearer if you rearrange things a bit:

Theorem not_exists_dist :
excluded_middle ->
forall (X:Type) (P : X -> Prop),
~(exists x, ~P x) -> (forall x, P x).
Proof. intros EM X P H x.
unfold not in H.
destruct (EM (P x)) as [H2 | H3].
apply H2.
assert (exists x : X, P x -> False) as H1.
exists x.
apply H3.
specialize (H H1).
destruct H.
Qed.

So you first assert the premise of H and prove it. Then you specialize H with the proven premise and all what remains in H is False.

Destruct H then asks you to solve the goal for all possible cases in which H can be constructed. For False there is no way to construct it, so you have to solve the goal for 0 cases.

Destruct directly applied to H simply automates this a bit and asks you to prove the premise of H.

If you don’t like the destruct H you can also write “exfalso. apply H.” exfalso proves any goal assuming you can prove False in your context. Yet another way of doing this is to writhe “contradiction H” which proves any goal from a hypothesis which is False.

1 Like
4

It is so clear now. Thank you.