Per tutti l'introduzione in coq?

Question

Sto cercando di (classicamente) dimostrare

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

in Coq. Quello che sto cercando di fare è dimostrarlo 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) 

Il mio problema è con le linee (2) e (5). Non riesco a capire come scegliere un elemento arbitrario di U, provare qualcosa su e concludere un forall.

Eventuali suggerimenti (non sono impegnato a utilizzare il controspositivo)?

Answer 1

Per simulare la tua prova informale, io uso il classico assioma ¬¬P → P (chiamato NNPP) [1]. Dopo averlo applicato, è necessario provare False con A: ¬ (∀ x: U, φ x) e B: ¬ (∃ x: U, φ x). A e B sono le tue uniche armi a dedurre False. Proviamo A [2]. Quindi è necessario dimostrare che ∀ x: U, φ x. Per fare ciò, prendiamo un arbitrario e proviamo a dimostrare che φ t tiene [3]. Ora, dato che ci si trova nell'impostazione classica [4], si sa che φ t₀ tiene (ed è finito [5]) o ¬ (φ t₀). Ma quest'ultimo è impossibile in quanto contraddirebbe 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.