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

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

Coq

証明された証明支援器をScalaで書いてみた

この記事はTheorem Proving Advent Calendarの7日目の記事である。静的型付き関数型言語は言語処理系の実装が容易であることから多くの場合、証明支援器(proof assistant)が実装されている。例えばStandard MLではIsabelle/HOL、OCamlでCoq、HaskellでAgdaが…

VSTTE Competition - ソフトウェア検証コンテストにチームTebasakiという名前で参加した。

VSTTE (Verified Software: Theories, Tools and Experiments) 2012 という学会の併設イベントでソフトウェア検証コンテストというものが開催されることを前日に id:keigoi さんに教えてもらって参加してみた。日時は日本時間で11月9日の0時から48時間。初め…

fold_leftとfold_rightが同じになるとき

fold_leftとfold_rightの結果が同じになるときが気になったので少し調べてみた。例えば文字列のリストを連結して一つの文字列を生成する次の例はfold_leftでもfold_rightでも同様に定義できて同じ関数になる。Coqで書くと次のような感じ。 Definition xs := …

tmiyaさんの練習問題をラムダ式で解いてみた

tmiyaさんがCoq入門者向けの問題をブログで紹介していたので解いてみた。 Functional Programming Memo: [Coq] Coq-99 : Part 1 この問題はCoqを使う人だけでなく論理的な思考力を鍛える良い問題ばかりなので、ぜひとも挑戦してみるとよいと思う。このような…

CPS変換されたフィボナッチ関数の証明をしてみた

普通のフィボナッチ関数とCPS変換したフィボナッチ関数をそれぞれ定義して、それらが等価であるということを証明してみた。CPS変換についてちょっと理解できた気がする。http://ideone.com/3CQOnしかしfib_cps関数をもっと美しく定義できないものだろうか。[…

Coqプログラマの集会、Coq庵でした

発表者の皆さん。お手伝いいただいた皆さん。ありがとうございました。たくさんのCoqerが集まって、大変濃密な時間を過ごす事ができました。スライドは以下から参照できます。 Coq庵 - coqグループ

掛け算から足し算を作る(足し算の一意性について)

Coq

http://d.hatena.ne.jp/kikx/20100629#1277831079 の素晴らしい足し算の存在証明を見つけたので、その存在が一意(ユニーク)であることを証明した。元々のネタはこちら http://d.hatena.ne.jp/m-hiyama/20100629/1277774676まずは集合AとA上の掛け算とサクセ…

Coqで多変数多項式の簡約

変数全体の集合varを{}というように自然数の対応で与えられると考え、式expを以下のように定義する。 Inductive exp : Set := | Var : var -> exp | Const : nat -> exp | Binop : binop -> exp -> exp -> exp. ここで binop型の値は二項演算子(binary opera…

OCamlerのためのCoq便利モジュールを公開してみた

このBaseモジュールをインストールすれば、写真の用なコードを書くことが出来る。ダウンロード: http://sourceforge.jp/projects/coqbase/具体的には以下のことを定義した。 標準出力へ出力するprint, println関数 命令をつなげるセミコロン演算子 依存型を…

迷路の試験問題を解いてみた

Coq

参考:人材獲得作戦・4 試験問題ほか: 人生を書き換える者すらいた。 Lv4に評価されるためには、最短性の完全なチェックが必要だったのでCoqで証明してみた。まず、accessiblesという関数を定義し、以下の性質を証明した。 ここでplengthはパスの長さを計る…

Coqで多重再帰のデータ構造を証明する

Coqでは一重の再帰的なデータは例えば次の様に定義できる。 Inductive list (A: Set) : Set := Nil | Cons (x: A) (xs: list A). Coqでは再帰的データ型をInductiveコマンドで定義した場合、その型の他に list_ind というものがついでに定義される。 list_in…

Proof Party の問題をCoqで挑戦してみた。

Proof Party に行けないけど、参加してるつもりで問題に挑戦してみた。今日は名古屋で一人証明パーティ。パズルと応用問題は解いていない。東京は遠いので、Proof Partyの次回がもしあれば 名古屋か関西で開催していただければありがたいです。> ranhaさん

Coqでハノイの塔に関する証明

Coqが今流行っているらしい。twitter経由で偶然ハノイの塔をCoq形式化している記事を見つけた。 なんか巷でCoqがはやっているようなので - 菊やんの雑記帳なんかおもしろそうなので一つ簡単な命題を証明してみた。証明したこと Lemma answer_length : forall…

Coqによる証明駆動開発で Merge Sort プログラムをつくってみた

OCaml合宿で帰りの車の中でid:zyxwv さんにMergeSortの正しさをどうやって証明するか聞かれてとっさに証明できなかったので、合宿から帰ったあとに一生懸命証明してみた。プログラムと証明の全体はこちら: yoshihiro503 / mergesort / source / — Bitbucket…

Coqで型クラス(Haskell風 モナドの定義)

Coq version 8.2以降からHaskell風の型クラスが使えるようになったから使ってみることにした。Haskellで型クラスといえばMonadが有名な気がするのでHaskell風のモナドHMonadを定義しよう。Coqでの型クラスは次のように宣言するみたいだ。 Class HMonad (M: T…

しりとりの圏をCoqで実装してみた

Coq で しりとりの圏を形式化した記事を見つけた。 型によるしりとりの成立判定 - コンピュータってすごいらしい via 完全実装付きでもう一度お送りします、しりとりの圏 - 檜山正幸のキマイラ飼育記すばらしかったので、私もちょっと真似して実装してみた。…

SICPのEx 2.4 をCoqで解いてみた

SICPを読んでいたら 検証せよ という問題があったので、Coqで検証してみた。問題はペア構造のチャーチエンコーディングの話。Scheme (untyped λ) に比べて Coq (λC) は型が厳格なので、問題の定式化がちょっと大変だったけど、問題自体は簡単に証明できた。 …

Coqで高精度計算サイト 高精度計算サイトというのを見つけた。ここの電卓サービスは素晴らしく、大変感銘したのだが、一つ残念な点があった。 それは大きな数を扱うことができないということである。 例えば10^10000000のような大変大きな計算を実行すると答…

Coqで依存型

最近Agdaがはやっているみたいなので、Coqでも依存型(dependent type)を使ってみた。 実装したのは長さ n のベクトル型だ。このベクトル型を使うと、空でないとか、長さが等しいとかを型の段階で保証できるので、より安全なプログラムを書くことができるの…