大阪人に関するうわさ
世の中には大阪人に関する間違った認識があふれているように思う。
例えば、大阪人は縦縞のユニフォームを着ている、とか嫁さんが強くてカカア天下である、とかである。
今回はそのような間違った俗説を払拭するべくCoqで証明してみた。
Coq < Section なにわ.
まず、次のような文を定めて、６つの噂を仮定する。ただし ~（にょろ） は否定を表す記号である。
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というタクティックだ。これはトートロジーの頭５文字をとったもので、この矛盾性を自動的に証明することができる。
さっそく試してみよう。
そんな奴おらへん < tauto. Proof completed. そんな奴おらへん is defined
ほんまにできた！！
End なにわ.
