How to prove this in Coq

Question

Lemma x: forall P Q: Set -> Prop,
              forall f: Set -> Set, 
            forall x, (P x -> Q (f x)) -> 
               (exists x, P x) -> (exists x, Q x).

I try to do it many different ways and I dont know whats wrong. This is my latest attempt:

Lemma x: forall P Q: Set -> Prop,
              forall f: Set -> Set, 
            forall x, (P x -> Q (f x)) -> 
               (exists x, P x) -> (exists x, Q x).
Proof.
  intros P Q f x H1 [x0 H2].
  exists (f x0).
  apply H1.
  assumption.
Qed.

but it produces this error: In environment P, Q : Set -> Prop f : Set -> Set x : Set H1 : P x -> Q (f x) x0 : Set H2 : P x0 Unable to unify "Q (f x)" with "Q (f x0)".

Answer 1

Your Lemma is actually false. Here is a proof that it is false:

Axiom x: forall P Q: Set -> Prop,
              forall f: Set -> Set, 
            forall x, (P x -> Q (f x)) -> 
               (exists x, P x) -> (exists x, Q x).


Lemma false : False.
Proof.
  destruct (x 
  (* P *) inhabited
  (* Q *) (fun _ => False)
  (* f *) (fun _ => False)
  (* x *) False ) as [y Hy].
  (* P x -> Q (f x) *) 
  - intros [[]]. (* trivially true, as False is not inhabited *)
  (* ∃ x, P x *) 
  - exists True. now apply inhabits.
  (* We get to assume that Q is satisfiable, but Q is always False *)
  - apply Hy.
Qed.

However, it is likely that the lemma you are trying to prove is not the one you want to prove. Is it possible you wanted to prove this lemma here instead?

Lemma x_fixed: forall P Q: Set -> Prop,
               forall f: Set -> Set, 
               (forall x, P x -> Q (f x)) -> 
               (exists x, P x) -> (exists x, Q x).
Proof.
  intros P Q f H1 [x0 H2].
  exists (f x0).
  apply H1.
  assumption.
Qed.

The difference is that the assumption is forall x, P x -> Q (f x), instead of just being P x -> Q (f x) for one specific x that is not otherwise mentioned in your goal (since it is shadowed by both exists x, P/Q x).