start Coq - wvogel日記

今日、知能や知識工学に関する授業がありました。
その中で、専門家の知識をどう利用するか、GAやGP、そしてAIの記述言語としてLispやPrologがあることなど、導入をききました。

そして実際、コンピュータに知能を持たせることは可能か、という話にもなり。
そんな講義を聞いていたら授業中ふとCoqの事を思い出しました。
Coqは証明である、という話をちらほら聞きますが、いつも気になったままで流してしまっていたので、余計に気になってくる。

よし、帰ったらやろう！ということで、Fedoraで実験することに。

sudo yum install coq coqide

としてインストール。
CoqIDEを起動して、池渕さんの書かれているプログラミングCoqの第一章から始めていく。
http://www.iij-ii.co.jp/lab/techdoc/coqt/coqt1.html
非常に読み易いです。

まだ現段階では、ここに書かれている通りのことをなぞっているだけです。
雰囲気Haskellに似ています。記述方式とか、型変数あったりとか。
C++で使うコードを検証するためHaskellを実験段階で使うことは多々ありますが、似たようなものを感じます

記事によると、

数理論理学における命題はプログラミングにおける型と一対一対応があり、証明はプログラムと一対一対応があります。それがどういうことかというと、命題は型を使って表現でき、ある命題が正しいことを証明するということは、その命題に対応する型をみたすプログラムを書くことに等しくなるのです。
プログラミングCoq（上記URLより）引用

Haskellの関数定義とCoqの形式が同様の形をしているのもあるかもしれません。
Haskellでの関数定義が、Coqでは命題にあたります。
そしてプログラムその物が証明、と。
命題の内容を満たすもの、それが証明という理解であっているでしょうか

練習問題として以下の二つがあげられています

問0. 任意の命題 A B に対して、A ならば「A ならば B」ならば Bが成り立つ。
問1. 任意の命題 A B C に対して、「A ならば B ならば C」ならば「B ならば A ならば C」が成り立つ。

やってみた。
問0.
命題は、書いてある内容を落とし込めばいいだけ

forall (A B:Prop) , A -> (A->B) -> B

これで命題は完了です。
次に証明をしてやるのですが、そもそもこれを満たすような関数にどのようなものがあるでしょうか
こういう時、Hoogleは非常に便利。

($) :: (a -> b) -> a -> b

問0.の命題を満たす関数としてこれが考えられます。では証明の中身を買いていきましょう

Definition prob0 :
forall (A B:Prop) , A -> (A->B) -> B
    := fun A B x f => f x

証明終了？でいいのかな？Coqのチェックは通ったけれど

問1.
これもまず命題から

forall (A B C :Prop) , (A->B->C) -> (B->A->C)

(->)は右結合なので、最後の()を外してやると、Haskellのflipという関数に定義が一致
よって、結局この問題の証明は次のようになります

Definition prob1 :
forall (A B C :Prop) , (A->B->C) -> (B->A->C)
  := fun A B C f x y => f y x.

なんか気づいたらのめりこんでる.....
というわけで、非常にCoqは面白い！
Haskellユーザーとして非常に入っていき易いです。