Wstępne wprowadzenie w coq?

Question

Próbuję (klasycznie) udowodnić

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

w Coq. Próbuję to udowodnić w sposób przeciwny:

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) 

Mój problem dotyczy linii (2) i (5). Nie mogę się dowiedzieć, jak wybrać dowolny element U, dowieść czegoś o tym, że jest on , i zawrzeć forall.

Jakieś sugestie (nie jestem zobowiązana do używania contrapositive)?

Answer 1

Aby naśladować twój nieformalny dowód, używam klasycznego aksjomatu ¬P → P (zwanego NNPP) [1]. Po zastosowaniu należy udowodnić, że False zawiera oba A: ¬ (∀ x: U, φ x) i B: ¬ (∃ x: U, φ x). A i B są twoją jedyną bronią do wydedukowania False. Spróbujmy [2]. Musisz udowodnić, że ∀ x: U, φ x. Aby to zrobić, podejmujemy arbitralne t ₀ i staramy się udowodnić, że φ t₀ posiada [3]. Teraz, skoro jesteś w ustawieniu klasycznym [4], wiesz, że albo φ t₀ zatrzymuje (i skończył [5]), albo ¬ (φ t₀). Ale to drugie jest niemożliwe, ponieważ byłoby to sprzeczne z 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.