当前位置：文江博客话题详情

如何证明(forall x, P x /\ Q x) -> （对于所有 x，P x）

发布于 2024-07-19 06:55:42 字数 118 浏览 8 评论 0原文

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

原文

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

悲凉≈ 2024-07-26 06:55:42

只需应用 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.

You can do it more quickly by just applying H, but this script
should be more clear.

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.

回复收藏 0 原文

吹梦到西洲 2024-07-26 06:55:42

尝试

elim (H x).

Try

elim (H x).

回复收藏 0 原文

娜些时光，永不杰束 2024-07-26 06:55:42

实际上，当我发现这个时，我就明白了这一点：

计算机科学家数学 2< /a>

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

回复收藏 0 原文

此生挚爱伱 2024-07-26 06:55:42

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) 成立。

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))

Intuitivly, if for all x, P(x) AND Q(x) hold, then for all x, P(x) holds.

回复收藏 0 原文

握住我的手 2024-07-26 06:55:42

答案如下：

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

here is the answer:

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.

you can find other solved exercises in this file: https://cse.buffalo.edu/~knepley/classes/cse191/ClassNotes.pdf

回复收藏 0 原文

~没有更多了~