如何证明 (forall x, P x /\ Q x) -> (forall x, P x)答案

【问题标题】：How to prove (forall x, P x /\ Q x) -> (forall x, P x)如何证明 (forall x, P x /\ Q x) -> (forall x, P x)
【发布时间】：2023-05-09 09:16:01
【问题描述】：

如何在 Coq 中证明 (forall x, P x /\ Q x) -> (forall x, P x)？已经尝试了几个小时，但无法弄清楚如何将先行词分解为 Coq 可以消化的东西。（显然我是新手 :)

【问题讨论】：

您在寻找 ∧ (U+2227: LOGICAL AND) 和 ∀ (U+2200: FOR ALL)吗？

标签： proof coq

【解决方案1】：

你可以通过应用 H 来更快地做到这一点，但是这个脚本应该更清楚。

Lemma foo : forall (A:Type) (P Q: A-> Prop), (forall x, P x /\ Q x) -> (forall x, P x).
intros.
destruct (H x). 
exact H0.
Qed.

【讨论】：

【解决方案2】：

试试

elim (H x).

【讨论】：

【解决方案3】：

其实，当我发现这个时，我想出了这个：

Mathematics for Computer Scientists 2

在第 5 课中，他解决了完全相同的问题并使用“cut (P x /\ Q x)”将目标从“P x”重写为“P x /\ Q x -> P x”。从那里您可以进行一些操作，当目标只是“P x /\ Q x”时，您可以应用“forall x : P x /\ Q x”，其余的都很简单。

【讨论】：

【解决方案4】：

Assume ForAll x: P(x) /\ Q(x)
   var x; 
      P(x) //because you assumed it earlier
   ForAll x: P(x)
(ForAll x: P(x) /\ Q(x)) => (ForAll x: P(x))

直观地说，如果对于所有 x，P(x) AND Q(x) 成立，那么对于所有 x，P(x) 成立。

【讨论】：

【解决方案5】：

答案如下：

Lemma fa_dist_and   (A : Set) (P : A -> Prop) (Q: A -> Prop): 

(forall x, P x) /\ (forall x, Q x) <-> (forall x : A, P x /\ Q x).

Proof.

split.

intro H.

(destruct H).

intro H1.

split.

(apply H).

(apply H0).

intro H.

split.

intro H1.

(apply H).

intro H1.

(apply H).

Qed.

您可以在此文件中找到其他已解决的练习：https://cse.buffalo.edu/~knepley/classes/cse191/ClassNotes.pdf

【讨论】：

嗨，欢迎来到 SO！欢迎您对本网站的所有贡献，但请避免回答已经有正确答案的旧帖子，尤其是当您没有回答原始问题时。