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

我正在尝试在Coq中证明以下内容:

目标(forall x:X，P(x)/ \ Q(x))->((forall x:X，P(x))/ \(forall x:X，Q(x)))。

有人可以帮忙吗？我不确定是否要拆分，做出假设等。

我很抱歉成为一个菜鸟

最佳答案

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.

关于predicate - 使用Coq证明谓词逻辑-初学者语法，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/2767262/