За пълно въвеждане в 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, да докажа нещо за него и да заключа forall.

Някакви предложения (не се ангажирам да използвам контрапозитив)?


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