Coqで証明　述語論理　ド・モルガンの法則

Coqで述語論理版のド・モルガンの法則を証明する。
記号を使うためにUtf8、古典論理を使うためにClassicalを読み込む。
NNPPは二重否定除去であり、背理法感覚で使うことができる。
最後の命題のみ古典論理が必要になる。

Require Import Utf8 Classical.

Goal ∀(U:Type)(P:U→Prop),(¬∃x,P x)↔(∀x,¬P x).
Proof.
split.
intros.
intro.
apply H.
exists x.
assumption.
intro.
intro.
destruct H0.
specialize(H x).
exact(H H0).
Qed.

Goal ∀(U:Type)(P:U→Prop),(∃x,¬P x)→(¬∀x,P x).
Proof.
intros.
intro.
destruct H.
apply H.
eapply H0.
Qed.

Goal ∀(U:Type)(P:U→Prop),(¬∀x,P x)→(∃x,¬P x).
Proof.
intros.
apply NNPP.
contradict H.
intro.
apply NNPP.
contradict H.
exists x.
assumption.
Qed.