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を読んで来たのに、今頃、
理解することが出来た。
よきかなよきかな。