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

Question

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

目标 (forall x:X, P(x) /\ Q(x)) -> ((forall x:X, P (x)) /\ (forall 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 来命名您的假设，拆分以分离目标，并准确提供证明术语（可能涉及 proj1 或 proj2）。