Forall在coq中的介绍？

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)

我的问题是第(2)和(5)行.我无法弄清楚如何选择U的任意元素,证明它的一些东西,并得出一个结论.

任何建议(我不承诺使用对立面)？

Answer 1

为了模仿你的非正式证明,我使用经典公理¬¬P→P(称为NNPP)[1].在应用之后,您需要False用A:¬(∀x:U,φx)和B:¬(∃x:U,φx)来证明.A和B是你推断的唯一武器False.我们试试A [2].所以你需要证明∀x:U,φx.为了做到这一点,我们采用任意t 0并试图证明φt0成立[3].现在,由于你处于经典设置[4],你知道φt0成立(并且它已完成[5])或¬(φt0)成立.但后者是不可能的,因为它会与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.