使用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.