Just a universally quantified hypotesis in Coq proof

Question

Another hard goal (for me, of course) is the following:

Goal ~(forall P Q : nat -> Prop,
          (exists x, P x) /\ (exists x, Q x) -> (exists x, P x /\ Q x)).
~
(forall P Q : nat -> Prop,
 (exists x : nat, P x) /\ (exists x : nat, Q x) ->
 exists x : nat, P x /\ Q x)
Proof.
~
(forall P Q : nat -> Prop,
 (exists x : nat, P x) /\ (exists x : nat, Q x) ->
 exists x : nat, P x /\ Q x)

I absolutely have no idea of what could I do. If I introduce something, I get a universal quantifier in the hypotesis, and then I can't do anything with it.

I suppose that it exists a standard way for managing such kind of situations, but I was not able to find it out.

Answer (Ptival)

To progress in that proof, you will have to exhibit an instance of P and an instance of Q such that your hypothesis produces a contradiction.

A simple way to go is to use:

P : fun x => x = 0
Q : fun x => x = 1

In order to work with the hypothesis introduced, you might want to use the tactic specialize:

Goal ~(forall P Q : nat -> Prop,
          (exists x, P x) /\ (exists x, Q x) -> (exists x, P x /\ Q x)).
~
(forall P Q : nat -> Prop,
 (exists x : nat, P x) /\ (exists x : nat, Q x) ->
 exists x : nat, P x /\ Q x)
Proof.
~
(forall P Q : nat -> Prop,
 (exists x : nat, P x) /\ (exists x : nat, Q x) ->
 exists x : nat, P x /\ Q x)
  intro H.
H: forall P Q : nat -> Prop,
(exists x : nat, P x) /\ (exists x : nat, Q x) ->
exists x : nat, P x /\ Q x
False
  specialize (H (fun x => x = 0) (fun x => x = 1)).
H: (exists x : nat, (fun x0 : nat => x0 = 0) x) /\
(exists x : nat, (fun x0 : nat => x0 = 1) x) ->
exists x : nat,
  (fun x0 : nat => x0 = 0) x /\
  (fun x0 : nat => x0 = 1) x
False

It allows you to apply one of your hypothesis on some input (when the hypothesis is a function). From now on, you should be able to derive a contradiction easily.

Alternatively to specialize, you can also do:

  pose proof (H (fun x => x = 0) (fun x => x = 1)) as Happlied.
H: forall P Q : nat -> Prop,
(exists x : nat, P x) /\ (exists x : nat, Q x) ->
exists x : nat, P x /\ Q x
Happlied: (exists x : nat, (fun x0 : nat => x0 = 0) x) /\
(exists x : nat, (fun x0 : nat => x0 = 1) x) ->
exists x : nat,
  (fun x0 : nat => x0 = 0) x /\
  (fun x0 : nat => x0 = 1) x
False

Which will conserve H and give you another term Happlied (you choose the name) for the application.

Answer (Matteo Zanchi)

The answer of Ptival did the trick. Here is the code of the complete proof:

Goal ~(forall P Q : nat -> Prop,
          (exists x, P x) /\ (exists x, Q x) -> (exists x, P x /\ Q x)).
~
(forall P Q : nat -> Prop,
 (exists x : nat, P x) /\ (exists x : nat, Q x) ->
 exists x : nat, P x /\ Q x)
Proof.
~
(forall P Q : nat -> Prop,
 (exists x : nat, P x) /\ (exists x : nat, Q x) ->
 exists x : nat, P x /\ Q x)
  unfold not.
(forall P Q : nat -> Prop,
 (exists x : nat, P x) /\ (exists x : nat, Q x) ->
 exists x : nat, P x /\ Q x) -> False intros.
H: forall P Q : nat -> Prop,
(exists x : nat, P x) /\ (exists x : nat, Q x) ->
exists x : nat, P x /\ Q x
False
  destruct (H (fun x => x = 0) (fun x => x = 1)).
H: forall P Q : nat -> Prop,
(exists x : nat, P x) /\ (exists x : nat, Q x) ->
exists x : nat, P x /\ Q x
(exists x : nat, x = 0) /\ (exists x : nat, x = 1)
H: forall P Q : nat -> Prop,
(exists x : nat, P x) /\ (exists x : nat, Q x) ->
exists x : nat, P x /\ Q x
x: nat
H0: x = 0 /\ x = 1
False
  -
H: forall P Q : nat -> Prop,
(exists x : nat, P x) /\ (exists x : nat, Q x) ->
exists x : nat, P x /\ Q x
(exists x : nat, x = 0) /\ (exists x : nat, x = 1) split.
H: forall P Q : nat -> Prop,
(exists x : nat, P x) /\ (exists x : nat, Q x) ->
exists x : nat, P x /\ Q x
exists x : nat, x = 0
H: forall P Q : nat -> Prop,
(exists x : nat, P x) /\ (exists x : nat, Q x) ->
exists x : nat, P x /\ Q x
exists x : nat, x = 1
    +
H: forall P Q : nat -> Prop,
(exists x : nat, P x) /\ (exists x : nat, Q x) ->
exists x : nat, P x /\ Q x
exists x : nat, x = 0 exists 0.
H: forall P Q : nat -> Prop,
(exists x : nat, P x) /\ (exists x : nat, Q x) ->
exists x : nat, P x /\ Q x
0 = 0 reflexivity.
    +
H: forall P Q : nat -> Prop,
(exists x : nat, P x) /\ (exists x : nat, Q x) ->
exists x : nat, P x /\ Q x
exists x : nat, x = 1 exists 1.
H: forall P Q : nat -> Prop,
(exists x : nat, P x) /\ (exists x : nat, Q x) ->
exists x : nat, P x /\ Q x
1 = 1 reflexivity.
  -
H: forall P Q : nat -> Prop,
(exists x : nat, P x) /\ (exists x : nat, Q x) ->
exists x : nat, P x /\ Q x
x: nat
H0: x = 0 /\ x = 1
False destruct H0.
H: forall P Q : nat -> Prop,
(exists x : nat, P x) /\ (exists x : nat, Q x) ->
exists x : nat, P x /\ Q x
x: nat
H0: x = 0
H1: x = 1
False rewrite H0 in H1.
H: forall P Q : nat -> Prop,
(exists x : nat, P x) /\ (exists x : nat, Q x) ->
exists x : nat, P x /\ Q x
x: nat
H0: x = 0
H1: 0 = 1
False inversion H1.
Qed.