使用Coq - Beginner语法证明谓词逻辑

Question

我试图在Coq中证明以下几点：

目标(对于所有x:X，P(x) /\ Q(x)) -> ((对于所有x:X，P (x)) /\ (对于所有x:X，Q(X)。

有人能帮帮忙吗？我不确定是否要拆分，做一个假设等等。

很抱歉我是个彻头彻尾的菜鸟

Answer 1

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.

Answer 2

只有一些提示:我建议你使用intros来命名你的假设，split来分隔目标，exact来提供证明术语(可能涉及proj1或proj2)。