読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

大阪人に関するうわさ

Section Variable Hypothesis Theorem Proof Qed tauto

世の中には大阪人に関する間違った認識があふれているように思う。
例えば、大阪人は縦縞のユニフォームを着ている、とか嫁さんが強くてカカア天下である、とかである。

今回はそのような間違った俗説を払拭するべくCoq証明してみた。

Coq < Section なにわ.

まず、次のような文を定めて、6つの噂を仮定する。ただし ~(にょろ) は否定を表す記号である。

Coq < Variable 大阪人である : Prop.
Coq < Variable たこ焼きを食べたことがある : Prop.
Coq < Variable 常に縦縞の服を着る : Prop.
Coq < Variable 嫁さんの尻に敷かれてる : Prop.
Coq < Variable 阪神の試合には欠かさず行く : Prop.
大阪人である is assumed
たこ焼きを食べたことがある is assumed
常に縦縞の服を着る is assumed
嫁さんの尻に敷かれてる is assumed
阪神の試合には欠かさず行く is assumed

Coq < Hypothesis 噂1 : 大阪人である -> 常に縦縞の服を着る.
Coq < Hypothesis 噂2 : 常に縦縞の服を着る \/ たこ焼きを食べたことがある.
Coq < Hypothesis 噂3 : 嫁さんの尻に敷かれてる -> ~ 阪神の試合には欠かさず行く.
Coq < Hypothesis 噂4 : 大阪人である <-> 阪神の試合には欠かさず行く.
Coq < Hypothesis 噂5 : ~ 大阪人である -> ~ たこ焼きを食べたことがある.
Coq < Hypothesis 噂6 : 常に縦縞の服を着る -> 大阪人である /\ 嫁さんの尻に敷かれてる.
噂1 is assumed
噂2 is assumed
噂3 is assumed
噂4 is assumed
噂5 is assumed

Coq <

これから、以上の噂たちを満たす場合に、矛盾が生じることを証明しよう。Falseは、矛盾が生じることを表すCoqの言葉である。

Coq < Theorem そんな奴おらへん : False.
1 subgoal
  
  大阪人である : Prop
  たこ焼きを食べたことがある : Prop
  常に縦縞の服を着る : Prop
  嫁さんの尻に敷かれてる : Prop
  阪神の試合には欠かさず行く : Prop
  噂1 : 大阪人である -> 常に縦縞の服を着る
  噂2 : 常に縦縞の服を着る \/ たこ焼きを食べたことがある
  噂3 : 嫁さんの尻に敷かれてる -> ~ 阪神の試合には欠かさず行く
  噂4 : 大阪人である <-> 阪神の試合には欠かさず行く
  噂5 : ~ 大阪人である -> ~ たこ焼きを食べたことがある
  噂6 : 常に縦縞の服を着る -> 大阪人である /\ 嫁さんの尻に敷かれてる
  ============================
   False

そんな奴おらへん < Proof.

そんな奴おらへん < 

Coqではこのようなシンプルな命題たちを効果的に扱うための技がある。それはtautoというタクティックだ。これはトートロジーの頭5文字をとったもので、この矛盾性を自動的に証明することができる。

さっそく試してみよう。

そんな奴おらへん < tauto.
Proof completed.

そんな奴おらへん is defined

ほんまにできた!!

End なにわ.

ソースコード