CODEWITHSUNDEEP
predicatecoq
Alan
Alan

Reputation: 31

Proving Predicate Logic using Coq - Beginner Syntax

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

Upvotes: 3

Views: 1068

Answers (2)

Tom Crockett
Tom Crockett

Reputation: 31579

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.

Upvotes: 4

Vinz
Vinz

Reputation: 6047

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

Upvotes: 3

Related Questions