Forall Einführung in Coq?

Question

ich bin versucht (klassisch) beweisen

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

in Coq. Was ich versuche, es zu tun beweisen 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) 

Mein Problem mit Linien (2) und (5). Ich kann nicht herausfinden, wie ein beliebiges Element von U wählen, etwas über es beweisen und einen Forall abschließen.

Irgendwelche Vorschläge (Ich bin nicht verpflichtet, das Kontrapositiv zu verwenden)?

Answer 1

Um Ihren informellen Beweis nachzuahmen, verwende ich das klassische Axiom ¬P → P (NNPP genannt) [1]. Nach dem Anwenden müssen Sie False mit A: ¬ (∀ x: U, φ x) und B: ¬ (∃ x: U, φ x) nachweisen. A und B sind deine einzigen Waffen, um False abzuleiten. Versuchen wir A [2]. Sie müssen also beweisen, dass ∀ x: U, φ x. Um dies zu tun, nehmen wir ein beliebiges t₀ und versuchen zu beweisen, dass φ t₀ gilt [3]. Jetzt, da Sie in klassischer Einstellung sind [4], wissen Sie, dass entweder φ t₀ gilt (und es ist abgeschlossen [5]) oder ¬ (φ t₀). Letzteres ist jedoch unmöglich, da es B [6] widersprechen würde.

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.