2013年12月14日

Coq/Agdaのどちらを使う?

この記事はTheorem Prover Advent Calendar 14日目の記事です。

さて、登録した時点では「Agdaが多いなあCoqかなあ」などと暢気に言っていて、また一日目のnotogawaさんは「みんなCoqのことを書くに決まってる」っぽいことをAAで言っていたわけですが、箱を開けてみたら

Σ(●△●)<Isabelleの人が一人で大半埋めてるじゃねえか!?

というわけでここではCoqとAgdaのことを書きましょう。そうしましょう。

え、CoqとAgdaのことはnotogawaさんが書いてただろって?
細けえこたぁいいんだよ!

・CoqとAgda、どちらを使うべき?


好きな方を選べば良いと思うのですが、個人的な考えを挙げます。

1:性質+証明を書くならCoqがいいです。記号処理や数学の定式化などですね。この辺りはtacticを使うという戦略がかなり効きます。ただ、これに関してはAgdaもたくさん使われていますので、それこそ好みでいいでしょう(個人的にはCoqがいいと思いますが)。
2:プログラム記述+検証についてはCoqの方がいいです。こちらは型や関数の記述自体は割と単純であることを想定しています。tacticもいいですし、SSReflectも便利(らしい)です。
3:型を複雑にして、いろいろな性質を型に持たせたプログラミングをしたいならAgdaの方がいいです。Coqだとプログラムを証明と一緒に(tacticで)書く勇気が必要になります(そうじゃないとやっていられません)。慣れればそれなりにできますが、いちいちイライラします。
4:型の階層を意識したいなら断然Agdaです。なにせCoqはSet/Prop/Typeの区別しかしませんし(内部でTypeのヒエラルキーは計算していますが、表に見えづらいです)。

1は比較的どちらでも良いですし、4は迷いようがありません。
したがって、おそらく悩むことが多いのは2/3の問題でしょう。
選択の一助になれば幸いです。

ちなみに、OCamlとHaskellの一方を使っているから、はほとんど理由になりません。
どうせ大した差ではありません。
スタートアップで一日差がつくかつかないかくらいです。

・inversion大好き


inversion tacticは便利です。(すでに何回主張したか忘れた)
簡単に説明すると、inversion tacticは「この帰納的述語が成り立つためにはどういうことが成り立っている必要がある?」というのを定義から見つけてくる優れものです。
このとき、成り立たないパターン(帰納的述語のコンストラクタのパラメータに一致しない)があるときは勝手にそれらに関して矛盾を作って証明してくれます。
(よって「起こりうるパターンが一つもない」、つまり矛盾していれば証明完了するわけですが、それはあくまで結果論)
inversionなかったらCoqの証明を勧めるとかありえませんね。
(ただしinversionの生成する項ははっきり言って読めない)
Agdaで同じこと?・・・reflection使えば、できたりするのかな・・・?

・で、証明しないの?


最近AgdaでD-Case書きまくってるので勘弁してください。
次があったら例題使って、最初の4分類が何を言いたいのか書いてもいいのですが・・・
タグ:Coq Agda
posted by chiguri at 00:14| Comment(0) | Coq

2013年12月06日

よしひろさんの問いにAgdaで答えよう

これはTheorem Prover Advent Calendarとはまったく関係のない記事である。
いや、来週くらいに書くけど。

昨日(世界のどこかの時間では)の担当だったよしひろさんが書いた記事
依存関係のある値のうちの一部をrewriteしようとしたときの問題
に最後にこんな一言があった。
> また、依存型に定評のあるAgdaではどうなるかなども興味深い。

なるほど、この問いには答えねば。
そう思いAgdaを起動してまねた記述を作る。
ファイル名はYIquestion.agdaとする。

module YIquestion where

open import Data.Nat
open import Relation.Binary.Core

postulate
f : (n : ℕ) → n > 0 → ℕ
h : (n : ℕ) (H : 2 * n > 0) → f (2 * n) H ≡ n

postulate
x : ℕ
H : x > 0

goal : (x ≡ 2 * 1) → f x H ≡ 1
goal eq = ?

同じ流れならここでeqを展開(rewrite相当)、Coqではエラーの出る展開である。
だが、エラーメッセージがなんか違うぞ・・・

Cannot decide whether there should be a case for the constructor
refl, since the unification gets stuck on unifying the inferred
indices [x] with the expected indices [2 * 1]
when checking that the expression ? has type f x H ≡ 1

(●△●)??
Hが問題とかそれ以前の問題のようだ。
え、なに?xと2*1をunifyしようとして詰まった・・・??
何を言ってるのだろう。

というヒントを元に作った正解はこちら。

goal' : (x : ℕ) → (x ≡ 2 * 1) → (H : x > 0) → f x H ≡ 1
goal' .2 refl H = h 1 H

goal : (x ≡ 2 * 1) → f x H ≡ 1
goal eq = goal' x eq H

最初のgoal'の記述は

goal' x eq H = ?

からeqを展開して作成した。
これを見ると何となく見えてくるのは、
どうもAgdaは引数が実際になんだったかしかreflで書き換えないらしい
ということである。
つまり、Coqの場合同様にHが依存していることももちろん問題だったのだが、それ以前に
xが適当に置かれた変数であるせいで、展開できない
ということの方がよっぽど問題だったという。

やっぱりAgdaのエラーメッセージはわかりにくい・・・

ちなみにCoqでは上のやり方に相当するパターンマッチではなくeq_indなどで書き換えているので注意。
posted by chiguri at 21:39| Comment(0) | Agda

2013年12月01日

進捗報告

進捗アドベントカレンダー1日目の報告書
・アドベントカレンダー
 幸いなことに23人もの発表者が集まった。こんな訳の分からないアドベントカレンダーに参加してもらって奇特に思えて仕方がないありがたい限りである。

・第一日目担当者の予想
 進捗が芳しくないこともあり、安直な方向へと進んだ結果、予想通り自分であった。自分で決めるのだから予想を外せば良いものを。

・FOSEでの発表
 いくらなんでも話を縮めるために例を簡略化しすぎたようだ。後で元担当教員にだめ出しを食らった。

・そのほか
 きっと24人目が来てくれると信じているが、来なかったら多分24日目はまた私だ。
 そして今日はやることがあってやばい。そんな先の話はどうでもいい。11月戻ってこい。

以上が私の進捗である。
さて、次はかの有名なよんた様(keita44_f4さん)である。
よんた様、進捗はいかほどでございましょうか?
posted by chiguri at 00:16| Comment(0) | 雑多

2013年11月19日

そしてまたSML#

もうあきらめたって良いと思うんだが。
SML#のビルドを試してみた。1.2.0。
どうでもいいつまらないことで詰まったのでメモ。

今度はpaxかcpioがないとダメだと言われた。
多分前も言われた。
mingw-getで入るのはbsdcpio.exeとかで、コピーして使った。
なんかしらんがlibz-1.dllがないとか言われたのでlibz1.dllの名前を書き換えてWindowsフォルダにたたき込んだ。
いろいろダメな気がする。

・・・あれ、でも割とすんなり終わった。時間はかかったけど。
posted by chiguri at 02:12| Comment(0) | PC

2013年11月05日

Windows用Agdaのインストーラで詰まったこと

講義で一斉にインストールを試したのだが、一応注意とメモとして。
10人ちょっとだが、ネットワークが死ぬのが怖いので、極力インストーラがネットワークを見に行かないようにインストーラを改変(注:この決断が正しかったことを後に知る)。
起こったエラーは次の二つ。

1)インストール時、関連するパスに日本語があるとエラーを起こす。
2)F-SecureのDeepGuardがcabalでインストールしたcpphsやなんだったか忘れたがHaskell用のmakeっぽいプログラムをトロイの木馬として認識する。

1は一応Known issueだったらしいことを後に知った。
なお、インストールパスのみならず、tempフォルダが配置されるユーザ名が日本語でもアウト。
(cabalでのAgdaインストール時に文句を言う)
もちろん後でユーザ名を変えてもユーザディレクトリ(C:\Users\ほげ の「ほげ」の部分)が日本語である限りアウトなのを付記しておく。
こんなの講義中にやられたら死ぬわ。
(ちなみに講義では新しくアカウントを作らせた)

2は困った。
幸い、cpphsの方は尋ねるだけなので、その時点で許可を出しつつF-Secureの設定から一時的にDeepGuardを停止することで回避。
Agda自体にはこれらの実行ファイルは必要ないので、後に引っかかっても特に問題なし。

こんなの一度も出たことないんだけどなあ・・・
もう21世紀も13年目なのに、また日本語ユーザ名に苦しむとか勘弁してほしい。
というかこの学科そんなアカウント作らせるの勘弁して。
いやまじめに。


ちなみにネットワークについて。
割り当ての教室に学内ネットワークが届かないという抱腹絶倒な環境だった。
cabalだけじゃなかったらどんなネットワーク環境作っても死にましたって。
(基本的にネットワークを見に行かないのだが、cabal updateだけは避けられなかったため、インストール時にネットワーク必須)
posted by chiguri at 18:39| Comment(0) | Agda