2012年1月22日日曜日

coq2scalaをさわってみた

http://proofcafe.org/wiki/Coq2Scala を試してみました。

インストールはhgでソースコードとってきて、
./configure
make world
make install
でおk。

Extraction Language Scala. が使えちゃうCoqがインストールされます。

使ってみた

とりあえず自然数と足し算を定義してみます。


吐き出されたScalaのコード。


Notationは無視される?
パラメータとらない場合はcase object使って欲しいかも・・・・
あとインデントも付くとうれしい。

ClassとInstanceを使ってみる

Monoidを定義してみた。

私はtraitとimplicit parameterでかっこ良く変換されるのかな!?と期待。


結果は・・・・・


(´・ω・`)ショボーン
明示的にインスタンスを渡して関数を得る感じですね。
まぁ、まだまだ開発途中なのでこれからどうなるかはわかりません。

最後に証明付きコード


proof-editing mode楽しいです。
ScalaでPDDの時代が来るかもですね。

2012年1月10日火曜日

Coqはじめました。

あけましておめでとうございます。

何か新しいことをはじめようと思い、Coqに手を出しました。

まだ慣れていないけど、なかなか楽しいです。

証明楽しいとかどんな変態(褒め言葉)なんだ!

と思っていましたが、私も無事変態の仲間に入ることが出来ました。

Coqをはじめる

Coqを使い始めたきっかけは冬休みの宿題で読書感想文です。

私は選んだ本はもちろん「数学ガール」。

なかなかおもしろいのでオススメです。

数学が得意というわけでもない私は、理解の手助けとしてプログラムを書こうと思いました。

そこでCoqの登場です!

本に出てくる命題を証明していくことにしました。

Coqに関する資料は決して多くありませんが、良いチュートリアルがあるので、まずはこれらを参考にしましょう。

書いてみた

正の整数型を作って加算を定義し、結合法則と交換法則を証明してみました。


結合法則はスラスラと書けて、「うはwっww楽勝www」とほざいていたのですが、交換法則は丸一日かかりました・・・・・

この中で使われているタクティクは
  • intros (導入)
  • induction (帰納)
  • reflexivity (再帰?反射?)
  • simpl (簡約)
  • rewrite (書き換え)
  • assert (表明)
  • replace (置換)
だけです。

プログラミングに慣れている人は、こういったタクティクを覚えていくだけで書けるようになると思います。

書いてみて

私はパズルを解くようなものだと感じました。

Qed. が書けたときはとても嬉しいです。

自然数の定義、自然数の加算・比較、整数の定義、ソースコードをみるだけでも勉強になります。

一度は触ってみてはどうでしょう。

Coq、おもしろいですよ!