Introducción de Forall en coq?

Question

Estoy intentando (clásico) demostrar

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

en Coq. Lo que estoy tratando de hacer es demostrarlo 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) 

Mi problema es con las líneas (2) y (5). No puedo averiguar cómo para elegir un elemento arbitrario de U, probar algo sobre y concluir un breve.

¿Alguna sugerencia (no estoy comprometido a usar el contrapositivo)?

Answer 1

Para imitar su prueba informal, uso el axioma clásico ¬¬P → P (llamado NNPP) [1]. Después de aplicarlo, debe probar False con A: ¬ (∀ x: U, φ x) y B: ¬ (∃ x: U, φ x). A y B son sus únicas armas para deducir False. Probemos A [2]. Entonces necesitas probar que ∀ x: U, φ x. Para hacer eso, tomamos un t arbit arbitrario e intentamos probar que φ t₀ tiene [3]. Ahora, como estás en la configuración clásica [4], sabes que φ t₀ se mantiene (y está terminado [5]) o ¬ (φ t₀). Pero lo último es imposible ya que contradeciría a 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.