coq - coq 中的证明 - 谓词逻辑

Question

尝试在 coq 中证明以下内容：证明全称量词分布在合取 ∀x ∈ A, P x ∧ Qx ⇐⇒ (∀x ∈ A, P x) ∧ (∀x ∈ A, Qx)

到目前为止我的证明-

Parameter (A : Type).
Parameter (P Q : A -> Prop).

Lemma II3: (forall x : A, P x /\ Q x) <->
           (forall x : A, P x) /\ (forall x : A, Q x).
split.
intro H.
split.
apply H.
intros H1.
Proof.

我试图分裂、破坏和引入一个新的假设，但我似乎无法超越这一点。任何建议将不胜感激。

Answer 1

这是一个非常简单的证明，例如now intuition; apply H可以解决您的目标。

在您的情况下，您应该首先弄清楚使用笔和纸的证明是如何工作的，一旦您这样做了，Coq 中的证明将是微不足道的。