Proving Predicate Logic using Coq - Beginner Syntax

3
votes

I'm trying to prove the following in Coq:

Goal (forall x:X, P(x) /\ Q(x)) -> ((forall x:X, P (x)) /\ (forall x:X, Q (x))).

Can someone please help? I'm not sure whether to split, make an assumption etc.

My apologies for being a complete noob

2
predicatecoq

2 Answers

4
votes
Goal forall (X : Type) (P Q : X->Prop), 
    (forall x : X, P x /\ Q x) -> (forall x : X, P x) /\ (forall x : X, Q x).
Proof.
  intros X P Q H; split; intro x; apply (H x).
Qed.
3
votes

Just some hints: I recommand you use intros to name your hypothesis, split to separate the goals, and exact to provide the proof terms (which may involve proj1 or proj2).