Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

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

like image 296
Alan Avatar asked Sep 17 '26 02:09

Alan


2 Answers

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.
like image 113
Tom Crockett Avatar answered Sep 26 '26 07:09

Tom Crockett


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

like image 21
Vinz Avatar answered Sep 26 '26 06:09

Vinz



Donate For Us

If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!