如何在 Coq 中证明 (forall x, P x /\ Q x) -> (forall x, P x)？已经尝试了几个小时，但无法弄清楚如何将先行词分解为 Coq 可以消化的东西。（我是新手，显然:)
问问题
3194 次
5 回答
6
您可以通过仅应用 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.
于 2010-06-03T20:14:39.693 回答
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”，剩下的就很简单了。
于 2009-05-09T17:11:08.583 回答
2
尝试
elim (H x).
于 2009-05-07T19:49:37.770 回答
2
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) 成立。
于 2010-06-03T20:24:19.437 回答
-1
这是答案：
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
于 2019-10-27T20:56:27.737 回答