How to prove this DeMorgan law without using automation tactics in Coq?

Question

This is the law I'm trying to prove here:

Goal forall (X : Type) (p : X -> Prop), (exists x, ~ p x) <-> ~ (forall x, p x).

Here's my code up to a point where I don't know in which direction to head:

Proof. 
  intros. split.
  - intros. destruct H as [x H]. intros nh. apply H. apply (nh x).
  - intros H.

What is shown as the subgoal and the premises I have seem to be provable, but what's the move?

I've tried going with exfalso., to apply H. afterwards. Which gives me another premise of x : X and a subgoal of px.

Don't know what to do after. Thanks for the help!

Answer 1

The right-to-left direction is not provable in intuitionistic logic. Coming up with a witness for the existential requires any axiom that moves you to classical logic. For instance, with the principle of excluded middle:

Axiom excluded_middle : forall (P : Prop), P \/ ~ P.

Goal  forall (X : Type) (p : X -> Prop),
  (exists x, ~ p x) <-> ~ (forall x, p x).
Proof. 
  intros. split.
  - intros. destruct H as [x H]. intros nh. apply H. apply (nh x).
  - intros Hnfapx.
    (* new hyp:  Hnfapx : ~ (forall x, p x) *)
    pose proof (excluded_middle (exists x, ~ p x)) as [? | Hnexnpx]; [assumption|].
    (* new hyp:  Hnexnpx : ~ (exists x, ~ p x)
       from this (and excluded middle again) we can deduce (forall x, p x)
       this contradicts Hnfapx *)
    exfalso. apply Hnfapx. intros x.
    (* new hyp:  x : X
       goal:     p x *)
    pose proof (excluded_middle (p x)) as [? | Hnpx]; [assumption|].
    (* new hyp:   Hnpx : ~ p x
       so there exists x such that ~ p x
       this contradicts Hnexnpx *)
    exfalso. apply Hnexnpx. exists x. assumption.
Qed.

More generally, intuitionistic logic loses (some directions of) the De Morgan laws. Indeed, a De Morgan law expresses a duality between two logical connectives through negation. This is fine in classical logic because double negation cancels out. But that’s not the case in intuitionistic logic: the elimination of double negation (∀ P, ¬¬P → P) is not provable. This principle is, in fact, equivalent to the principle of excluded middle. (However, (∀ P, ¬¬¬P → ¬P) is provable.)

That’s why intuitionistic logic requires both quantifiers ∃ and ∀: none is definable in terms of the other one.

(This was first said as comments; I was expecting someone to come up with a more thorough answer but, since no-one did, I am posting mine now. Thanks @Arthur Azevedo De Amorim for correcting me on which axiom is sufficient.)