andとorとnot: カリーハワード (2.2)

「プログラミング言語としてみると」さっきの証明は何をやっていたことになるんでしょう。

"Inductive"は、ユーザー定義の新しい命題を定義するのでした。そして、命題＝型です。つまり、ユーザー定義の新しい型を作る機能が対応します。Haskell だと "data" ですね。

data And a b = 
 Conj a b

data Or a b =
   OrIntroL a
 | OrIntroR b

Inductiveによるandとorの定義をHaskellで書き直すと、↑こうなります。公理とは、要するにコンストラクタです。はい。

class And<A,B> {
  public And(A a, B b) { ... }
}

class Or<A,B> {
  public Or(A a) { ... }
  public Or(B b) { ... }
}

Javaで書くとこんな感じです。Andは、2引数のコンストラクタを1つ持つ型です。Orは、1引数のコンストラクタが2つ。どっちを使っても作れますが、どっちかを使わないと作れません。

ちなみに False は、Coq.init.Logic.False:

Inductive False : Prop :=.

公理が一つもない…つまり証明する手段が１つも用意されていない命題、それがFalse、という定義です。Haskellでも

{-# OPTIONS_GHC -XEmptyDataDecls #-}
data False

こう、こういう変な型を定義するには追加オプションが要りますけど、作れます。

さて、あらためて、ド・モルガンの証明とはなんだったかというと…

de_morgan :: (Or a b -> False) -> And (a -> False) (b -> False)

Haskellで「この型を持つ値を作ってね！なんでもいいから！」と言われたら、どうしますか？

de_morgan f =
 Conj (\x -> f (OrIntroL x)) (\y -> f (OrIntroR y))

たとえば、こんな風に書けますね。これが、さっきCoqで作った証明です。

ひとり勉強会