Forall введение в coq?

Question

Я пытаюсь (классический) доказать

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

в Coq. То, что я пытаюсь сделать, это доказать 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) 

Моя проблема с линиями (2) и (5). Я не могу понять, как выбрать произвольный элемент U, доказать что-то около его и завершить forall.

Любые предложения (я не намерен использовать контрацептив)?

Answer 1

Для того, чтобы подражать вашему неофициальному доказательству, я использую классическую аксиому ¬¬P → P (называемую NNPP) [1]. После его применения вам необходимо доказать False как с A: ¬ (∀ x: U, φ x), так и с B: ¬ (∃ x: U, φ x). A и B - ваше единственное оружие, чтобы вывести False. Попробуем A [2]. Поэтому вам нужно доказать, что ∀ x: U, φ x. Для этого возьмем произвольное t₀ и попытаемся доказать, что φ t₀ выполняется [3]. Теперь, поскольку вы находитесь в классической настройке [4], вы знаете, что выполняется либо φ t₀ (и закончено [5]), либо ¬ (φ t₀). Но последнее невозможно, так как это противоречило 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.