Ltacを知りcrushを読む
これはTheorem Proving Advent Calendarの15日目の記事である。
二回目じゃないのかって？人数不足だ。気にしてはいけない。
さて、今日の記事が何に関する記事かは見れば一目瞭然。
Coqの中のtactics記述用言語Ltacについてであり、目標はあの有名なcrushを読み解くことである。
・・・と書いたが、正直まじめに説明すると長さの関係上やっていられないので、crushの動きを簡単に知る程度にする。
なお、今回もまた内容の関係上背景をあまり長くかけないので、一通りCoqの知識を持っているものとする。
それでも無理なのだからもはやどうしようもない。
crushって何？
有名な、といっておきながらそれか、といわれそうだが、一応説明する。
crushというのは、Coqの初級者以上*1が読むと勉強になること請け合いの、Certified Programming with Dependent Typesという本（略称CPDT）*2で頻繁に使われる、証明を省略するためのtacticsである。
省略する、といったが、実際に中身を見ると確かに証明しているため、（本当の意味で省略である）admitとは異なる。
要するに、証明が自動化されているわけである。
crushの定義
このcrushだが、Ltacで記述されている。
その定義は下の通り。
Ltac crush := crush' false fail.
言うまでもなく、このcrush'もまた別に定義されている。
それらを遡ると、全体で100行前後くらいになる。
さて、crushの書いてあるソースをここで一応リンクしておきたい。
CPDTのリポジトリ中にあるCpdtTactics.vの150行目である。
手元にほしいならば先にあげたページのtarballから展開してほしい。
src/CpdtTactics.vが対象ファイルである。
コードを見るとsimplHyp、inster、crush'の三つが大きいことがわかるが、実はinsterは読まなくてよいので今回は省略し、残りの二つを読む。
ただし、今回は別に詳細を説明したいわけではないので適度に手を抜くし、また動作全体を追うことはしない。
Ltacの基本
Ltacも通常のCoqの項同様に、関数型に似た構成をとる。
パターンマッチがあり、関数があり、letがある。
また、追加としていくつかの特殊なデータがある。
たとえばgoalは特殊なデータで、仮定の集合と証明するゴールの型の組である。
これまたパターンマッチで処理する。
ただし、パターンマッチの挙動が少し異なるので、その点に関しては軽く触れておきたい。
match goal with | H : _ |- _ => ... end
こんな例を考える。なお、...は省略しているだけである。こんなコードではない。
パターンにおいて、|-の左が仮定、右がゴールである。
網羅性について
Ltacのパターンマッチは網羅的である必要はない。
たとえば上のパターンマッチは仮定が何もないケースがかかれていないが、その場合Ltacでは失敗するだけである。
証明時にエラーが出ることがあるが、要するにあれが出る、というだけだ。
必要に応じてtryなどを使うことで例外処理も可能である。
マッチングの順序
Coqのマニュアルを見ると「リニアじゃない」とかかれている。
この意味を説明するために上の例を用いる。
今書いている証明は仮定が二つあるとする。これらをH0とH1としよう。
すると、上のコードでは、まずH0がHとして束縛される。なお、ここからわかるとおり、Hは仮定の名前ではなく、パターンマッチに使われている変数である。
H0を試して失敗した場合、Coqは次にH1をHとして束縛する。
論理型プログラミングを知っている人は、バックトラックを行っていると思ってほしい。
なお、H1も失敗した場合は、このパターンマッチ全体は失敗する。
とりあえずこの二点は覚えておいてほしい。
全体の簡略化
それぞれのコードを見たいのだが、まずcrushとcrush'のコードを見る。*3
Ltac crush' lemmas invOne :=
let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence in
let rewriter := autorewrite with cpdt in *;
repeat (match goal with
| [ H : ?P |- _ ] =>
match P with
| context[JMeq] => fail 1
| _ => (rewrite H; [])
|| (rewrite H; [ | solve [ crush' lemmas invOne ] ])
|| (rewrite H; [ | solve [ crush' lemmas invOne ] | solve [ crush' lemmas invOne ] ])
end
end; autorewrite with cpdt in *)
in (sintuition; rewriter;
match lemmas with
| false => idtac
| _ => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
repeat (simplHyp invOne; intuition)); un_done
end; sintuition; rewriter; sintuition; try omega; try (elimtype False; omega)).
Ltac crush := crush' false fail.さて、crush'の定義を追うと、全ての再帰呼び出し時の引数が呼び出し時と同じであることに気づくだろう。
今回はcrushを読み解くだけなので、この前提としてcrushの引数でcrush'を部分評価してみよう。
lemmasをfalseに、invOneをfailにし、評価を行う。idtacが常に成功することを考慮すると、crushは次のcrush''と等価になる。*4
Ltac crush'' :=
let sintuition := simpl in *; intuition; try subst; repeat (simplHyp fail; intuition; try subst); try congruence in
let rewriter := autorewrite with cpdt in *;
repeat (match goal with
| [ H : ?P |- _ ] =>
match P with
| context[JMeq] => fail 1
| _ => (rewrite H; [])
|| (rewrite H; [ | solve [ crush'' ] ])
|| (rewrite H; [ | solve [ crush'' ] | solve [ crush'' ] ])
end
end; autorewrite with cpdt in *)
in (sintuition; rewriter; sintuition; rewriter; sintuition; try omega; try (elimtype False; omega)).今度はもう一つのsimplHypの番だ。
Ltac simplHyp invOne :=
let invert H F :=
inList F invOne; (inversion H; fail)
|| (inversion H; [idtac]; clear H; try subst) in
match goal with
| [ H : ex _ |- _ ] => destruct H
| [ H : ?F ?X = ?F ?Y |- ?G ] =>
(assert (X = Y); [ assumption | fail 1 ])
|| (injection H;
match goal with
| [ |- X = Y -> G ] =>
try clear H; intros; try subst
end)
| [ H : ?F ?X ?U = ?F ?Y ?V |- ?G ] =>
(assert (X = Y); [ assumption
| assert (U = V); [ assumption | fail 1 ] ])
|| (injection H;
match goal with
| [ |- U = V -> X = Y -> G ] =>
try clear H; intros; try subst
end)
| [ H : ?F _ |- _ ] => invert H F
| [ H : ?F _ _ |- _ ] => invert H F
| [ H : ?F _ _ _ |- _ ] => invert H F
| [ H : ?F _ _ _ _ |- _ ] => invert H F
| [ H : ?F _ _ _ _ _ |- _ ] => invert H F
| [ H : existT _ ?T _ = existT _ ?T _ |- _ ] => generalize (inj_pair2 _ _ _ _ _ H); clear H
| [ H : existT _ _ _ = existT _ _ _ |- _ ] => inversion H; clear H
| [ H : Some _ = Some _ |- _ ] => injection H; clear H
end.invOneをfailにしても小さくならない？それは甘いといわざるを得ない。
invertは24-28行目のブロックで呼ばれているが、invertの第一引数は常に関数が渡される。
したがって、invert H Fは常にinList F failを呼ぶ。
inListの定義は、第二引数に第一引数が入っているかを調べるものだが、真っ当に考えてfailに関数部Fが入っているはずが無い。*5
よって、このinListの呼び出しは常に失敗し、そしてinvertの呼び出しも常に失敗する。
つまり、invertを呼ぶ＝パターンマッチ失敗、と見ていい。
ではさらに書き換えていこう。*6
Ltac simplHyp' :=
match goal with
| [ H : ex _ |- _ ] => destruct H
| [ H : ?F ?X = ?F ?Y |- ?G ] =>
(assert (X = Y); [ assumption | fail 1 ])
|| (injection H;
match goal with
| [ |- X = Y -> G ] =>
try clear H; intros; try subst
end)
| [ H : ?F ?X ?U = ?F ?Y ?V |- ?G ] =>
(assert (X = Y); [ assumption
| assert (U = V); [ assumption | fail 1 ] ])
|| (injection H;
match goal with
| [ |- U = V -> X = Y -> G ] =>
try clear H; intros; try subst
end)
| [ H : existT _ ?T _ = existT _ ?T _ |- _ ] => generalize (inj_pair2 _ _ _ _ _ H); clear H
| [ H : existT _ _ _ = existT _ _ _ |- _ ] => inversion H; clear H
| [ H : Some _ = Some _ |- _ ] => injection H; clear H
end.それなりに小さくなった。
ではそれぞれを見ていこう。
simplHyp'
さて、simplHyp'は始まって早々にgoalのパターンマッチを行っている。
最初のケース（3行目）は「existsで囲まれている要素が仮定にあったら」「それを分解しなさい」といっている。
別に難しくはない。
次のケース（5行目）は「同じ関数を適用した結果が等しいという仮定があったら」「引数の等号にしなさい」である。
仮定に引数の等価性がすでにわかっている場合は無視する（6行目）*7ことにし、関数側がコンストラクタであるような場合（7-11行目）に対応している。
8行目から11行目は「実際に引数の等号が出来たか」を確認するためであり、出来てなかったら失敗するようになっている。
いちいち事前のチェックや事後のチェックにいろんな技術が必要なあたり、面倒である。
12行目のケースは先ほどの二引数版である。特に不思議なことはしていないので省略。
次のブロック（21-22行目）はexistTというコンストラクタの場合であり*8、同じ型から取れて、それが等号ならその中身も同じ、というものと、単によくわからないからinversionする、という二つに分かれる。
最後のブロックはどうでもいいだろうから無視する。*9
総じて何してるかというと、等式や述語を展開して仮定やゴールを単純にしようとしているわけである。
crush''
Ltac crush'' :=
let sintuition := simpl in *; intuition; try subst; repeat (simplHyp'; intuition; try subst); try congruence in
let rewriter := autorewrite with cpdt in *;
repeat (match goal with
| [ H : ?P |- _ ] =>
match P with
| context[JMeq] => fail 1
| _ => (rewrite H; [])
|| (rewrite H; [ | solve [ crush'' ] ])
|| (rewrite H; [ | solve [ crush'' ] | solve [ crush'' ] ])
end
end; autorewrite with cpdt in *)
in (sintuition; rewriter; sintuition; rewriter; sintuition; try omega; try (elimtype False; omega)).ほぼ再掲である。
冷静に見てみると割とやっていることはむちゃくちゃだ。
まず、sintuitionは全体をsimpl、intuitionで分解、変数を出来る限り消す、simplHyp'を試して分解して変数を消すのを失敗するまで繰り返す、等価性を使って証明してみる、といった流れ。
残りはrewriterなのだが、これがなかなか面倒くさいことをやっていて、一文なのですぐわかる。単にヒントデータベースcpdtを使ってautorewriteし、その後、全ての仮定について書き換えを試みる。
ただし、この仮定の中にJMeq（John Meyer equality）がある場合はまずいらしく、その仮定を飛ばす。また、当然その仮定が等式でなければ飛ばす。
等式の場合で前提がある場合は、その前提を再びcrushで解こうとする。
この試行が終わった場合、再びautorewriteを行い、上の試行を繰り返す。
sintuitionが構造の単純化を行い、rewriterが書き換えられそうな場所を全て書き換えていく、という中身らしい。
この内容を元に考えると、crushの中身は、単純化する、書き換える、単純化する、書き換える、単純化する、omegaで解いてみる、それで駄目なら仮定が矛盾していると思ってomegaで解いてみる、と。
思った以上にomega頼りだ。
というか、変形してomegaしてる以外なにもしない。
つまりcrushとは
がんばったomegaである。
なんだろうこの敗北感・・・
すごく読むのに時間がかかったのに・・・*10
なお、全然Ltacの勉強じゃない、という突っ込みは受け付けないのであしからず。
*1:曲がり間違っても初心者は読んではならない。
*2:正確にはまだ本になっていないが、著者いわく「本当にもうすぐMIT Pressから出るよ！」とのこと。
*3:crush'のインデントが違和感あったので修正している。
*4:ここでinsterは消えるため、今回は読まない。
*5:そもそもfailはtacticsであり、FはGallina上の関数である。
*6:この流れは部分評価ではない。Fとfailの関係を与えないと不可能。
*7:assumptionが原因の失敗では||以降が実行され、fail 1の失敗では||を突破してパターンマッチの結果が失敗となる。
*8:existのPropが全てTypeになったものだと思ってほしい。
*9:injectionがコンストラクタを展開するものだとわかれば自明。
*10:部分評価を思いついたのがある程度読み解いた後だったのが災いした。
