	Lean	Coq*1	Agda	Isabelle
証明の書き方	structured proof, tactic, 函数定義	tactic	函数定義	structured proof, tactic
開発環境	emacs	emacs, CoqIDE	emacs	jEdit
ドキュメント	×	◎	○	△
implicit parameter	○	○	△	(型を使わないので不要)
Equational Reasoning	○(builtinなものはOK. 独自演算子は条件付き)	？(知らない)	◎	○(基本的にbuiltinなもののみサポート)
自動証明	×(なし？)	○(auto, omegaなど)	△(emacsのautoコマンド)	◎(auto, force, sledgehammerなど)
ライブラリ	◎	○？	△	○
パフォーマンス	○？	？(知らない)	×	○

証明の書き方

なんとstructured proof(上から下向きに書ける), tactic, 函数定義の全ての書き方をサポートしている.
他の言語から入ってきた人にも優しい仕様.

開発環境

インストールはバイナリがあるのでそれを入れるだけ.
インストールするとleanemacsというアプリケーションが使えるようになる.
leanemacsではリアルタイムチェッカーが走るし, エラーメッセージも見やすいので(emacsが嫌いじゃなければ)そんなに悪くないと思う.

ドキュメント

公式サイトにTutorialとかがある.
HTML版はブラウザ上でLeanを動かすこともできてすごい.

しかしドキュメントらしきものはこのtutorial.pdfくらいしかなく, より詳細な情報でまとまった文章はおそらく存在しない.
Leanを本格的に使うならここが一番問題.

implicit parameter

カリーハワード対応を使って証明を書くような言語では, implicit parameterが使えるのは結構重要.
Coqは割と優秀と聞く一方で, Agdaは少し省略するとしょっちゅう警告ばかり出す.

ここに関してはLeanもそれなりに優秀で, たくさん省略してもエラーになったり警告が出たりはしない.

Equational Reasoning

独自演算子に対してのReasoningは, それがグローバルに定義された演算子なら, refl attributeなどを対応する命題に付与することで使えるようになる.
ただしstructure(データ型を定義するときに使う)内の演算子に対しては使えないなどの制約があるらしい.
同値関係を含む構造を定義して, それに対するreasoningを書くことが出来ないので微妙に不便.

ちなみに, reasoningはsubst(a == b & ==> P a == P bなど)を自動でやってくれるようで, 実はこれのおかげでLeanでreasoningをすると非常に証明が楽になる.
a == bを指定すると, aの部分を現在のGoalの左辺から探して代入する操作をやってくれるのでこちらでsubstを指定する必要がない.
Leanの目玉機能の一つ.

自動証明

~~ドキュメントにも書いてないから多分ないです.~~

追記:
どうもblastがそれに当たるらしい.
blast派生のコマンドがいくつかあって, 代表的なものとしてsimp(simp attributeがついた定理を適用する), rec_simp(帰納法が使える？)などがある.

ライブラリ

(駆け出しの言語にしては)標準で結構色々なものが揃っている.
HoTTライブラリが用意されているあたりもポイント.
拡張子 .hleanがそれ.

ところで, 現在LeanファイルをHTMLやpdfファイルに変換するツールなどはない.
ので.leanファイルを直接見る以外に証明を読む方法がないので(ファイルの依存関係がややこしい場合は特に)結構不便.

パフォーマンス

ちょっと書いた限り重くなったりする気配はあんまりない.
リアルタイムチェッカーが走っている割には軽くて快適. (ここでAgdaの方をチラ見する)

所感

色んな書き方ができるのは, 参入コストが下がると考えれば悪いことではないと思う.
Equational Reasoningでsubstを指定しなくていいのは予想以上に楽だったので, 普段苦労している人はこれだけでも触ってみる価値はあるかもしれない.
あとはリファレンスさえしっかり作ってくれれば2016年以降流行る可能性があるかもしれない.
むしろ流行ってくれ.

証明の例

rev.lean Listのreverseに関する証明
yoneda.lean 米田の補題の証明

参照

Lean 公式サイト
Tutorial: Theorem Proving in Lean ブラウザでLeanが遊べるハイテクチュートリアル(長い)
lean/library at master · leanprover/lean · GitHub 標準ライブラリ, 読むと勉強になる
The Lean Theorem Prover Leanの紹介スライド, 最高にクールで分かりやすいので オススメ

*1:Coq使ってないので適当言ってるかも.

2015-07-12

無限ループによる証明

Agda 後で考える Isabelle

Software FoundationsのIMPあたりをやってて疑問が湧いた.

w = while True do Skip endが停止しないことを示したい.
つまり, $\langle w, s \rangle \to s' \Rightarrow False$ を示したい. ($s, s' : \mathbb{Z} \to \mathbb{Z}$ は変数の値を保持する環境)

普通に証明するなら以下のようになると思う:
証明図の高さに関する帰納法による. まず高さが0のとき, 明らかに<w,s>→s'は公理から導くことはできないので高さ0の証明図を持たない. よって$\langle w, s \rangle \to s' \Rightarrow False$である.
次に, $\forall s, s'. \langle w, s \rangle \to s'$が高さnの証明図をもたないと仮定し, $\langle w, s \rangle \to s'$が高さ(n+1)の証明図をもたないことを証明する. $\langle w, s \rangle \to s'$が高さ(n+1)の証明図をもつことを仮定すると, wの定義とwhile-loopに関する推論規則より$\langle w, s \rangle \to s'$が高さnの証明図で示せる. これは帰納法の仮定に矛盾するので証明が完了する.

Agdaなどの依存型を持つ言語では, prop :: w -> Falseに対応する函数を作ってやればよい.
<w,s>→s'にあたるデータ型を再帰的に定義している場合, 例えばこの証明は無限ループを使ってprop (While-Loop True _ k) = kみたいにすると, 証明図の仮定に当たる, 「一つ前の」<w,s>→s'を使うことができる.
けれど一体これは何を証明していることになるんだろう？
明らかに上の証明とは違う気がするし, そもそも無限ループになっているのに証明が完了しているというのがよく分からない. 直観的には「<w,s>→s'を仮定すると全く同じ形が仮定の部分に出現する」ということが重要なんだろうという気がするけれど、そこからどうやって矛盾を導いているんだろう.

ちなみにIsabelleでは以下のようにやった.
上の証明の気持ちがある程度反映されているつもり. (と言っても証明だけでは伝わらない気もするけど)

lemma while_induction:
  assumes red: "(WHILE b DO c END) %: st ⇓ st'"
  and base: "⋀t t'. ⟦ beval3 t b = False; t' = t ⟧ ⟹ P t t'"
  and step: "⋀t t' t''. ⟦ beval3 t b = True; c %: t ⇓ t'; (WHILE b DO c END) %: t' ⇓ t''; P t' t'' ⟧ ⟹ P t t''"
  shows "P st st'"
proof-
  have "(WHILE b DO c END) %: st ⇓ st' ⟹ P st st'"
    using ceval.induct [of _ _ _ "λc0 t t'. WHILE b DO c END = c0 ⟶ P t t'"] apply rule
    apply (simp, auto, simp add: base)
    apply (fastforce simp add: step)
    apply (fastforce simp add: step)
    done
  thus ?thesis by (simp add: red)
qed
 
theorem loop_never_stops: "¬ (loop %: st ⇓ st')"
proof (unfold loop_def, auto)
  assume p: "WHILE BTrue DO SKIP END %: st ⇓ st'"
  show "False"
    using while_induction [of BTrue SKIP st st' "λ_. λ_. False"]
    by (rule, simp add: p, auto)
qed