Coq中的Forall介绍？

Question

我正在尝试（经典地）证明。

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

我的问题出在第二行和第五行。我无法确定如何选择U的任意元素，证明其中的某些内容，并得出一个forall。

有什么建议吗（我并不一定要使用反命题）？

- Maty

Answer 1

为了模仿您的非正式证明，我使用经典公理 ¬¬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.

- Marc