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
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.
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).
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With