使用 Coq 证明谓词逻辑 - 初学者语法

Question

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

Goal (forall 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

只是一些提示：
我建议你使用简介来命名你的假设，拆分以分隔目标，
并准确提供证明条款（可能涉及 proj1 或 proj2）。