 # Destructing hypothesis

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.

``````(* 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.
``````

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

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

It is so clear now. Thank you.