How to prove (forall x, P x /\ Q x) -> (forall x, P x) [In Coq]

Question

How does one prove (forall x, P x /\ Q x) -> (forall x, P x) in Coq? Been trying for hours and can't figure out how to break down the antecedent to something that Coq can digest. (I'm a newb, obviously :)

Answer 1

Try

elim (H x).

Answer 2

Actually, I figured this one out when I found this:

Mathematics for Computer Scientists 2

In lesson 5 he solves the exact same problem and uses "cut (P x /\ Q x)" which re-writes the goal from "P x" to "P x /\ Q x -> P x". From there you can do some manipulations and when the goal is just "P x /\ Q x" you can apply "forall x : P x /\ Q x" and the rest is straightforward.

Answer 3

You can do it more quickly by just applying H, but this script should be more clear.

Lemma foo : forall (A:Type) (P Q: A-> Prop), (forall x, P x /\ Q x) -> (forall x, P x).
intros.
destruct (H x). 
exact H0.
Qed.

Answer 4

Assume ForAll x: P(x) /\ Q(x)
   var x; 
      P(x) //because you assumed it earlier
   ForAll x: P(x)
(ForAll x: P(x) /\ Q(x)) => (ForAll x: P(x))

Intuitivly, if for all x, P(x) AND Q(x) hold, then for all x, P(x) holds.