使用Coq的证明谓词逻辑 - 初级语法

Question

我试图证明在Coq的以下内容：

目标（的forall X：X，P（X）/ \ Q（X）） - >（（X的forall ：X，P（x））/ \（全部x：X，Q（x）））。

有人可以帮忙吗？我不知道是否分割，做一个假设等

我的道歉，作为一个完整的小白

Answer 1

只是一些提示： 我建议您使用前奏命名你的假设，分割，分离的目标，并且确切地提供证明术语（其可能涉及proj1或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.