Coq 演習 4

「Coq による定理証明入門」の続き。2.2.6 まで読んだ。

演習問題 4.

Lemma Ex41: ~~(exists x: A, P x) -> (exists x: A, ~~P x).
Proof.
intros.
apply NNPP in H.
destruct H.
exists x.
intro.
contradiction.
Qed.

Lemma Ex42: ~(exists x: A,(~P x)) -> (forall x: A, P x).
Proof.
intros.
apply NNPP.
intro.
apply H.
exists x.
trivial.
Qed.

Lemma Ex43: (exists x, P x) <-> ~(forall x, ~P x).
Proof.
split.
intros.
intro.
destruct H.
apply (H0 x).
trivial.

intros.
apply NNPP.
intro.
apply H.
intro.
intro.
apply H0.
exists x.
trivial.
Qed.

4. $${\exists x(P(x) \leftrightarrow \forall yP(y))}$$ はギブアップ。。これって成り立つのかを含めてまだリテラシーが足りてないのでまた戻って来たい。