Для всего введения в coq?

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

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

в Coq. Я пытаюсь доказать это противоположным образом:

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, что-то доказать и заключить все.

Есть предложения (я не собираюсь использовать противозачаточные средства)?


computer-science coq formal-methods
person Maty    schedule 11.12.2010    source источник

Ответы (1)


arrow_upward
14
arrow_downward

Чтобы имитировать ваше неформальное доказательство, я использую классическую аксиому ¬¬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.
person Marc    schedule 11.12.2010