coqでドモルガン 述語論理編

述語論理で、ドモルガンに相当すんのが以下の4つ
¬(∃x,P x) -> ∀x,¬ P x
∀x,¬ P x -> ¬(∃x,P x)
∃x, ¬ P x -> ¬(∀x,P x)
¬(∀x,P x) -> ∃x, ¬ P x

例によって最後のやつが排中律or二重否定則とかないと証明出来ないらしい。

Require Import Coq.Logic.Classical.
Check NNPP. (* =>  : forall P : Prop, P -> ~ ~ P -> P *)
Lemma JDM2 (T:Type) (P: T -> Prop) :
  ~(forall x, P x) -> exists x, ~(P x).
Proof.
  move=> Hyp.
  apply: NNPP.
  move=>Hnen.
  apply: Hyp.
  move=> x0. apply: NNPP.
  move=>Hnen2. apply: Hnen. exists x0. by [].
Qed.

exists x, ~(P x). に対して二重否定則適用&コンテキストに
~ (exists x, ~ P x)を上げる
現状のサブゴールに対して、最初の仮定 ~(forall x, P x) を適用
forall xをコンテキストにx0として上げる。
現状のサブゴール P x0に対して再び二重否定則適用
~~P x0
このサブゴールは
コンテキストの仮定 ~ (exists x, ~ P x)
と大体同じものなので証明終了。

テキトーだ。
何書いてるか分かんねえ....

存在量化子 exのコンストラクタ ex_introの読みかたがあやふやだった。
P -> Qは、forall _ : P, Qの糖衣構文であるというのを
ようやく。何度もSoftware Foundationを読んで来たのに、今頃、
理解することが出来た。
よきかなよきかな。