coq 中的所有介绍？

发布于 2024-10-07 11:11:26 字数 422 浏览 0 评论 0原文

我试图（经典地）

~ (forall t : U, phi) -> exists t: U, ~phi

在 Coq 中证明。我想做的是用反证法证明它：

1. Assume there is no such t (so ~(exists t: U, ~phi))

2. Choose arbitrary t0:U

3. If ~phi[t/t0], then contradiction with (1)

4. Therefore, phi[t/t0]

5. Conclude (forall t:U, phi)

我的问题是第（2）行和第（5）行。我不知道怎么办选择 U 的任意元素，证明一些关于它，并结束一个forall。

有什么建议（我不致力于使用反证法）？

原文

I'm trying to (classically) prove

~ (forall t : U, phi) -> exists t: U, ~phi

in Coq. What I'm trying to do is prove it contrapositively:

1. Assume there is no such t (so ~(exists t: U, ~phi))

2. Choose arbitrary t0:U

3. If ~phi[t/t0], then contradiction with (1)

4. Therefore, phi[t/t0]

5. Conclude (forall t:U, phi)

My problem is with lines (2) and (5). I can't figure out how
to choose an arbitrary element of U, prove something about
it, and conclude a forall.

Any suggestions (I'm not committed to using the contrapositive)?

分享到QQ

分享到微博

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

发布评论

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

生死何惧 2024-10-14 11:11:26

为了模仿你的非正式证明，我使用经典公理 ØØP → P（称为 NNPP）[1]。
应用后，您需要用 A : Ø(∀ x:U, φ x) 和 B : Ø(∃ x:U, Ø x) 来证明False。 A 和 B 是你推断False的唯一武器。让我们尝试一下A[2]。所以需要证明∀ x:U, φ x。为了做到这一点，我们取任意 t₀ 并尝试证明 φ t₀ 成立 [3]。现在，由于您处于经典设置[4]，您知道 φ t₀ 成立（并且已经完成[5]）或 Ø(φ t₀) 成立。但后者是不可能的，因为它与 B [6]相矛盾。

Require Import Classical. 

Section Answer.
Variable U : Type.
Variable φ : U -> Prop.

Lemma forall_exists: 
    ~ (forall x : U, φ x) -> exists x: U, ~(φ x).
intros A.
apply NNPP.               (* [1] *)
intro B.
apply A.                  (* [2] *)
intro t₀.                 (* [3] *)
elim classic with (φ t₀). (* [4] *)
trivial.                  (* [5] *)
intro H.
elim B.                   (* [6] *)
exists t₀.
assumption.
Qed.

In order to mimic your informal proof, i use the classic axiom ¬¬P → P (called NNPP) [1].
After applying it, you need to prove False with both A : ¬(∀ x:U, φ x) and B : ¬(∃ x:U, φ x). A and B are your only weapons to deduce False. Let's try A [2]. So you need to prove that ∀ x:U, φ x. In order to do that, we take an arbitrary t₀ and try to prove that φ t₀ holds [3]. Now, since you are in classical setting[4], you know that either φ t₀ holds (and it's finished[5]) or ¬(φ t₀) holds. But the latter is impossible since it would contradict B [6].

Require Import Classical. 

Section Answer.
Variable U : Type.
Variable φ : U -> Prop.

Lemma forall_exists: 
    ~ (forall x : U, φ x) -> exists x: U, ~(φ x).
intros A.
apply NNPP.               (* [1] *)
intro B.
apply A.                  (* [2] *)
intro t₀.                 (* [3] *)
elim classic with (φ t₀). (* [4] *)
trivial.                  (* [5] *)
intro H.
elim B.                   (* [6] *)
exists t₀.
assumption.
Qed.

回复收藏 0 原文

~没有更多了~