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