Prouver la logique des prédicats en utilisant Coq - Débutant Syntaxe

Question

J'essaie de prouver ce qui suit dans Coq:

Objectif (forall x: X, P (x)/\ Q (x)) -> ((forall x : X, P (x))/\ (pour tout x: X, Q (x))).

Quelqu'un peut-il m'aider s'il vous plaît? Je ne suis pas sûr que de diviser, faire une hypothèse, etc.

Mes excuses pour être un noob complet

Answer 1

Juste quelques conseils: Je recommande que vous utilisez intros pour nommer votre hypothèse, diviser pour séparer les objectifs, et exact de fournir les termes de preuve (qui peuvent impliquer proj1 ou proj2).

Answer 2

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.