How to prove (forall x, P x / \ Q x) & # 8594; (for all x, P x) [In Coq]

Question

How to prove (forall x, P x / \ Q x) → (for all x, P x) in Coq? I tried for hours and could not understand how to break the antecedent that Coq can digest. (I'm new, obviously :)

Answer 1

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

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

Answer 2

Try

 elim (H x). 

Answer 3

Actually, I realized this when I found this:

Mathematics for Computer Scientists 2

In lesson 5, he solves the same problem and uses "cut (P x / \ Q x)", which rewrites the target from "P x" to "P x / \ Q x → P x". From there you can do some manipulation, and when the target is just “P x / \ Q x”, you can apply “forall x: P x / \ Q x”, and the rest is simple.

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)) 

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