Just $ A sandbox

プログラミングと計算機科学とかわいさ

あのとき知りたかったCoqの話

最近Coqをかいていて、まぁ自分は基本姿勢として「CoqにはProof Assistantの方向性として共感できないのでもっとよいものが出てきて早く駆逐してほしい」だったのだけれど、
たくさん書いてると多少偏見もなおって考えを改めたりした部分があるのでまとめることにした。

Agda/Lean/Isabelleの経験がそれなりにある人間から見た、「あのとき知りたかったCoqのハナシ」という
誰にウケるのかわかんない感じで書くけど「Agdaしか使えないけどCoq気になる」みたいな人間(いるのか?)がもしいたら参考にしてください。

強み: 圧倒的implicit parameterの強力さ

implicit parameterの推論は本当にヤバイぐらい強力でAgdaなどハナシにならないのでめっちゃ楽。
おそらくほぼ最大限の推論をしてくれる

あとCoercionとかも結構強いので積極的に使っていこう

Ltacを使うことのキモさ

Ltacはキモいわかるって感じなんだけど、別にそんなたくさんのtacticsを使い分ける必要はあんまりなくて
挙動がよくわからん謎のtacticsは使わなくてもまぁ大丈夫なので多分ナントカなると思う。

自分は実際intro, destruct, apply, rewrite, exists, constructor, refineぐらいしか使ってない。
もちろんたくさん覚えておくと便利なんだろうけど無理して使わなくても
案外なんとでもなるなと。(これは後述するreasoningを使っていることにも関係してる)

ssreflectとかよくわかんなくて使ってないけど別に困ってないので、
キモい証明を生成したくない人は使わなくてもいいんじゃないでしょうか。

Notation, 特にEquational Reasoningに関して

今やってるのが圏論なのでそれ特有の話題にはなるけど、
Notationは意外と強力で(Isabelleとかと比べても遜色ないぐらい)結構自由に定義ができる。

上手く使うとEquational Reasoning(一個前の記事とか参照)もちゃんと定義できたりするので
このへんを使うと意外と読みやすい証明がかけたりする。

証明の読みやすさ

上の話とも関連するけど、具体的に定義を与えるときはできる限り構成をわかりやすく見やすくする工夫をすると証明が読みやすくなるかもしれない。
例えば上のようにNotationを上手く使うとか。

もちろんtacticsベースな以上どうしようもない部分はあるけど。
割り切りは大事。

hole system

Agdaだとholeが作れてアレが案外便利なんだけど
Coqで若干近いことができるrefine tacticというのがある。

refineはhole(_)つきのtermを渡すことができて、その下でholeの部分の証明を要求される。
つまりhole以外の部分をまず埋めてからholeの部分を証明するということができるので
証明をsmall-stepに分割できる。

上手く使うとhole感出て便利。

CIC <-> Ltac

CICからLtacへの変換(正確にはCICのtermを適用して証明をする)はexact tacticを使えばいい。
逆にLtacをCICのtermにするにはltac: (...)と書くといい。

上手くやるとLeanみたいに複数の証明手法を混ぜて証明がかける。

auto command

Coqのauto系コマンドは雑魚です。
ほぼ役に立たないと思ったほうがいい。

Agda/Leanユーザーへ: 君のところの言語もautoはゴミ同然でしょ
Isabelleユーザーへ: ようこそauto縛りの世界へ(dependent typeベースだからしゃーないので諦めて)

sledgehammerほしいめっちゃわかる。

Text Structure

すごく長い証明を一歩ずつ進めたい場合。

Sectionを上手く使おう。
定義や定理のまとまりをSectionで分けて組み合わせていくといい。

Agdaでいうmodule相当の機能だけど、Agdaでいうwhereがないのでこういう感じになる。

performance

いい感じ。
ファイルごとにコンパイル(?)してるだけあってロードも早いのでちゃんと実用に耐えうるレベルに来ている感じがある。

環境

ProofGeneralにcompany-coqを入れるのが多分最強。
emacs使わない人は知らない。

Unicode Symbols

実はあまり知られてないことだけどUnicode symbolは普通に使える。(今すぐRequire Import Utf8.しよう)
Agda-userはProofGeneralのinput methodをagda-inputにするのもいい。
company-coqはTeXっぽいunicode input methodを提供してくれるのでこいつでも十分いい感じ。

特にAgda/Isabelleユーザーはせっかくなのでバリバリ使おう。