Hatena::ブログ(Diary)

memo

2018-05-13

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

00:09

述語論理で、ドモルガンに相当すんのが以下の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を読んで来たのに、今頃、

理解することが出来た。

よきかなよきかな。

トラックバック - http://d.hatena.ne.jp/morita_non/20180513/1526224153