Forall introduction in coq?

Question

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

Perl

Answer 1

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.

Beeson