tree@SSReflect

「Ssreflect って何ですか?」

「ごめんね,正直言って,よくわかってないんだ」

「は ?」

「あ,いや,えーと,決定可能な命題が? reflection でいい感じに扱える? みたいな?」

「は ?」

1 前書き,あるいは言い訳

飛ばしてもなんら問題はない.

1.1 いざ,歴史を紐解かん

Ssreflect なるものの存在を知ったのは随分と前,学部を卒業した頃には既に知っていたような記憶があるから,修士を終えて半年経った今から数えれば,少なくとも 2 年以上は昔の話になる. しかし,そこに付随する記憶は決して 「Ssreflect 使いこなしてーの証明バリバリQ.E.D!」 といったものではなく , 「インストールできねぇ」 の一言に尽きる.とにかくインストールできなかったので,何度も挑戦した挙句早々と諦めた,そんな記憶しかない.上手くいったことが一度でもあれば使った記憶があるだろうから,使った記憶が無いということで,対偶取ってそういうことである.

そんな風にモヤモヤとしていたわけだが,今年の 7 月…頃,既に記憶は定かではないが,さすがにそろそろちゃんと使ってみようと思い立ち, Ssreflect を導入したのである.ちょうど新型の Macbook Air を買った時期であったから,失敗したらぜーんぶ消してやり直せばいいや,という雑な目論見が功を奏したような記憶はある.あるが,辛い記憶はすぐに忘れてしまいたいと思うのが人の常であるから,これ以上の情報は望めないし,おそらく数カ月後にはスムーズに導入できたという記憶へと挿げ替えられていることだろう.ゆえに,導入記録的なものはここには載せない.載せることができない.ご容赦されたい.

とはいえ,ここ最近は Ssreflect を勉強しようという動きが其処彼処であるようで,導入のガイド的なものをちょくちょく見かけるようになった.もし Ssreflect をまだ導入しておらず,使ってみたいと思っている人は,それらガイドを参照すると良いのではないだろうか.そして願わくば私にレクチャー願いたい.母艦の iMac には未だ Ssreflect を導入できていない. 27 inch のディスプレイにフルスクリーン表示した emacs 上で Proof General を使って Coq!! はすっごく楽しいのだ.そこに Ssreflect を導入したらなんと幸せなことだろうか!

寝っ転がっての定理証明なら Macbook Air だけどね.

1.2 枝葉末節

さて,導入記録を書かないのであればここに何を前書いておくのか,という話である.ここに記すは以降で連々ねる Coq (with Ssreflect) コード,即ち定理とその証明に取り組んだその動機だ. 細かい話は Coq のコードと併せて述べることになるが,大雑把な道筋はここで示しておこう.

まず,この記事(またの名をチラシの裏)で行うことは以下の 3 つである.

  1. 木構造を相互再帰的に定義
  2. それを Ssreflect に於ける eqType モジュールの一実装とする
  3. seq と同様に x ∈ t という所属性判定を定義

これら 3 つはこの順番で行われる.その理由は流れを追ってもらえれば明らかになるであろう.ここでは,そもそも木構造を Ssreflect 上で取り扱おう,あるいは Ssrefelect に取り込もうと思ったのはなぜか,という部分について触れておく.

8月頃1,業務でフローグラフ2 の制御依存解析をするコードを書く機会があった. 制御依存解析が何かというと,プログラム中の各式について,その式が実行されるかどうかの実権を握っている式を見つけ出すこと3だ. その制御依存解析をするにあたっては, 支配関係木(dominator tree) と呼ばれるある木構造を求める作業が要となるのだが,ここで私は愚かしくも,制御依存解析やら何やらに関して素人であるにもかかわらず,これらに関わる諸々を定理証明系で扱えたら素晴らしいではないかと考えたのである.支配関係木を求めるアルゴリズムには複雑なものが多く,証明も難解だ.物の定義は単純であるのにそれを求めるアルゴリズムが複雑という場合こそ,定理証明系の出番であろう.アルゴリズムを解きほぐし具に分析することは,アルゴリズムの正当性を確かめるには欠かせない.定理証明系で扱うということはそうせざるを得ない状況に持っていくということである.

支配関係木はその名の通り木構造である.また,制御依存解析の対象となるフローグラフは頂点数が有限のグラフであり, Ssreflect には fingraph というモジュールが用意されている.

端的に言えばこれだけの理由で Ssreflect 使おう! と走りだした. そして現在の進捗状況は,

  • 木構造をそれらしく Ssreflect で扱えるようにした
  • 支配関係を定義し,半順序であることを証明
  • 有限グラフの深さ優先探索木を構成(する関数を定義.係る定理の記述や証明はこれから)

といったところだ.ちなみに,これらの取り組みは業務とは一切関係がない.完全なる趣味の領域である.ゆえに作業時間は主に平日の夜.または土日祝日であった.

今の取り組みの一応の目標地点として,支配関係木を求めるとあるアルゴリズムの正当性の証明を Coq を使って与えることを掲げていはいるのだが,そもそも,対象のアルゴリズムをどのようにして Coq で記述するのか,停止性の証明をどうやって与えるか,などなどの問題が山積しているため,これは気を長く持つ必要のある目標である.飽きが来ない程度にゆっくりのんびりやっていきたい.

そして,本記事は上記リストの一番上,「木構造をそれらしく Ssreflect で扱えるようにした」ことについて纏めた物である. 他 2 つについては,追々纏めて記事とする予定である.

2 番目についてはもしかしたら gist に載せたコード を見た方もいらっしゃるかもしれない. 見たことなかった方のうち何割かの方々も今,見たと思う. 正直なところ,これについては説明すべき事柄が「支配関係を定義し,半順序であることを証明」という一文にほとんど含まれているので,いったい他に何を書いたらいいのかさっぱりだが,最悪,支配関係の定義を書けばよいだろうと高を括っている.とにかく,期待せずにお待ちいただければ幸いである.

1.3 本題

それでは,本文に比して異様に長い言い訳を終えたところで本題に入ろう.

本稿は https://github.com/mathink/digraphtree.v の中身について解説を行うつもりで書かれている.

次節では相互再帰を用いて木構造 tree と森構造 forest を定義する.これは Coq のリファレンスマニュアルにも乗っている例だが,以降の説明に欠かせない部分もあるので一通り流れを追っていこう.そして,相互再帰的な型の取扱いの例として,木の走査を行う 2 つの関数の定義とそれらの間の関係について記述した定理の証明を行う. 第 3 節では, treeforest を Ssreflect の eqType の実装とする.等価性判定が決定可能であることが,リフレクションによって様々な場面で利用できるようになる. 続く 第 4 節で,所属性判定関数を定義し,seq のように x ∈ t という形で木 t が頂点 x を持つかどうかの判定ができるようになる.これを用いて,最後に木の走査が正しく行われていることの証明をする.

一つ注意していただきたいのは,あくまで私の作業をそれっぽい形に纏めたものがこの記事である,というスタンスなので,論文のようにしっかりとした出来のものを想定するのは危険だということだ.わからないことにはわからないと書いてあるが,それ以外の部分についても過度の信用は禁物である. とはいえある程度参照に堪える物に仕上げたいという気持ちは持っているので,何か気になるところ等があれば @mathink などへ遠慮無くお伝えいただけるとありがたい.

加えて, Coq を使ったことがないとコードについては何が何だかさっぱりとなること間違いなしだが,近頃は日本語での資料も増えてきたことだしこの機に Coq を使ってみてはいかがだろうか.

2 木と森の話

モリゾーとキッコロと呼ばれる物体が記憶の底から蘇ってきたが,関係はない.

相互再帰的に木と森を定義する例は Coq'Art の 14.3 節やリファレンスマニュアルの 4章13章 にあるので,背景知識や詳細な解説等はそちらを参照されたい. Coq'Art は購入の必要がありますが,いい本なので皆様お買い求めください.そして和訳してください.

ここでは相互帰納的にデータ型を定義した後,相互再帰関数や相互帰納原理についても軽く触れていく. 以降の節に関わる部分もあるが,細かい技術的,または理論的詳細には立ち入らず, tree.v でやっていることの大まかな流れだけを追いたいという場合には, データ型の定義さえ確認しておけば,他は飛ばしてしまっても差し支えないだろう.

2.1 相互帰納的データ型

二分木を表すデータ型を定義すると Coq なら次のようになる.

Inductive btree (T: Type) :=
| bleaf: btree T
| bnode (a: T)(l r: btree T): btree T.

これは,二分木とは葉であるかもしくは 2 つの子を持つ節のどちらかであるということを述べている. 今回用いる木構造は子の数が任意の有限個であるから,例えば次のような定義だろうか.

Inductive ntree (T: Type) :=
| nleaf: ntree T
| nnode (x: T)(child: list (ntree T)): ntree T.

これもきっと悪くはないのだろう.子が任意有限個というのだから,リストにするのは自然な形の定義だ. しかし,今回はこの形ではなく,次のようにして相互帰納的に木と森を定義することにした.

Inductive tree (T: Type) :=
| node (x: T)(c: forest T)
with
forest (T: Type) :=
| leaf 
| sibl (t: tree T)(f: forest T).

グラフ理論において,木の集まりは森であり4,森を束ねれば木となる. それに倣ったほうが将来的にフローグラフを扱う際の理論展開の見通しが良くなるのではないかという予想や, treeforest で纏まったことによるすっきり感,そして,相互再帰を使うことによって得られるなんだかちょっと小難しい数学してるっぽい感,などなどを考慮した結果の選択である.

Coq に於いて相互帰納的にデータ型を定義した後にすべき事は,帰納原理を作ることだ. 通常であれば,帰納的なデータ型を定義した殆どの場合,Coq が自動生成してくれる帰納原理で大抵の定理を証明するには十分である.しかし,相互帰納的に定義されたデータ型に於いては,自動生成される帰納原理では不便な場合が出てくる.

それを確認するためにも,まずは木と森に対して pre-order と post-order で走査を行う関数を定義して,これらに関する定理の証明に臨んでみよう.

2.2 相互再帰関数

走査関数は相互帰納的なデータ型を引数に取って再帰的に走査していくので,関数は相互再帰的に定義される.

pre-order で走査する関数

Fixpoint preorder_tree t :=
  match t with
    | node x f => x :: preorder_forest f
  end with
preorder_forest f :=
  match f with
    | leaf => [::]
    | sibl t f => preorder_tree t ++ preorder_forest f
  end.

と,post-order で走査する関数

Fixpoint postorder_tree t :=
  match t with
    | node x f => rcons (postorder_forest f) x
  end with
postorder_forest f :=
  match f with
    | leaf => [::]
    | sibl t f => postorder_tree t ++ postorder_forest f
  end.

だ. Ssreflect を使っているため,空リストは [] ではなく [::] と書いている. rcons は末尾に要素を追加する関数である.

preorder_treeposorder_tree の間には以下の関係が成り立つ.

forall t: tree T, preorder_tree (rev_tree t) = rev (postorder_tree t).

日本語に直すと「任意の木について, post-order で走査した順序を反転させると,反転させた木を pre-order で走査したものは等しい」となる.日本語に直す必要があったかはさておき,未定義の関数 rev_tree を出してしまったが rev_tree という名前から何をやっているのか察していただきたい.これも相互再帰関数なので,併せて rev_forest という関数も定義されている.

この定理の証明をやってみよう.とりあえず t について帰納法かな? と挑んでみると,

Theorem pre_rev_eq_rev_post_tree t:
  preorder_tree (rev_tree t) = rev (postorder_tree t).
Proof.
  induction t.
  rewrite rev_rcons.

と進めてみたあたりで次のようなゴールが出てきていると思う.

x :: preorder_forest (rev_forest c) = x :: rev (postorder_forest c)

ここで「なるほど,よく考えたら treeforest にしたものでも同じことが言えるはずだ.そしてそれがこの定理の補題として必要なのか.ふむふむ」と勢いだけで突っ走り

Theorem pre_rev_eq_rev_post_forest t:
  preorder_forest (rev_forest t) = rev (postorder_forest t).

という定理の証明に挑むと

preorder_tree (rev_tree t) = rev (postorder_tree t).

という補題を示す必要が生じる.なんだか見覚えがないだろうか.なければ数行遡るとよい.

見事にループが出来上がった.

このループをいくら繰り返したところで終わりは見えてこない. このような状況を打破するためにはどうすればよいのだろうか.

どちらかを先に証明しようとするともう片方が必要になってしまうのが問題なわけだから,同時に証明すればよい.つまり,次の定理を証明すればよい.

Theorem pre_rev_eq_rev_post:
  (forall t, preorder_tree (rev_tree t) = rev (postorder_tree t))/\
  (forall f, preorder_forest (rev_forest f) = rev (postorder_forest f)).

確かにこの定理を証明すればよいのだが,問題はこの定理をどのように証明するのか,ということだ. この証明には下準備がいる.具体的には,新たな帰納原理の構成である.

2.3 相互帰納原理

時間は戻って諸々の定理の証明に臨む直前である.

相互帰納的に treeforest を定義すると, treeforest そのそれぞれに 3 つ,計 6 つの帰納原理が自動的に得られる.そのうち 2 つを以下に示す.

tree_ind
     : forall (T : Prop) (P : tree T -> Prop),
       (forall (x : T) (c : forest T), P (node x c)) ->
       forall t : tree T, P t
forest_ind
     : forall (T : Prop) (P : forest T -> Prop),
       P leaf ->
       (forall (t : tree T) (f0 : forest T), P f0 -> P (sibl t f0)) ->
       forall f1 : forest T, P f1

これらを使って証明に臨んでいたことが上手く行かなかった原因なのだが, その理由を個人的な理解の範疇でざっくりとしてふんわりな雰囲気だけ述べておこう.

対象となる関数が相互再帰的に定義されているのにこれらの帰納原理にはそんな素振りが一切見られないからである. これらの帰納原理は証明には不十分であったということだ. その不十分さは, tree_rect の仮定に於いて c に対する言及がないことから伺える.

では,証明に十分な帰納原理をどう作るのかという話になる.答えは簡単だ.

Coq に作ってもらう.

Scheme コマンドを使って, Coq に作ってもらう.

Coq がやってくれる.

細かい話は置いといて,

Scheme tree_forest_ind := Induction for tree Sort Prop
  with forest_tree_ind := Induction for forest Sort Prop.

というコマンドを実行すると,新たに2つの帰納原理 tree_forest_indforest_tree_ind が手に入る. Induction for の部分に帰納原理を作っている感を覚えてもらえれば with で 2 つを同時に,相互再帰的に作っているのだなぁ,という雰囲気を感じ取れるのではないだろうか. これらの型を示しておこう.

tree_forest_ind
     : forall (T : Type) (P : tree T -> Prop) (Q : forest T -> Prop),
       (forall (x : T) (c : forest T), Q c -> P (node x c)) ->
       Q leaf ->
       (forall t : tree T, P t -> forall f : forest T, Q f -> Q (sibl t f)) ->
       forall t : tree T, P t

forest_tree_ind
     : forall (T : Type) (P : tree T -> Prop) (Q : forest T -> Prop),
       (forall (x : T) (c : forest T), Q c -> P (node x c)) ->
       Q leaf ->
       (forall t : tree T, P t -> forall f : forest T, Q f -> Q (sibl t f)) ->
       forall f2 : forest T, Q f2

これらはそれぞれ treeforest 型のデータについての言明が証明のゴールであるときに適用可能だ. ただし,適用に際して tree については述語 Q を, forest については述語 P を明示的に与えなければいけないということに注意が必要だ.ゴールからはそれが何かはわからないからである.

さて,これらはどうやら仮定部には違いがないようだから,くっつけてしまおう.

Combined Scheme tree_forest_mut_ind from tree_forest_ind, forest_tree_ind.

というコマンドを実行すると,

tree_forest_mut_ind
     : forall (T : Type) (P : tree T -> Prop) (Q : forest T -> Prop),
       (forall (x : T) (c : forest T), Q c -> P (node x c)) ->
       Q leaf ->
       (forall t : tree T, P t -> forall f : forest T, Q f -> Q (sibl t f)) ->
       (forall t : tree T, P t)/\(forall f2 : forest T, Q f2)

という補題が得られる5

証明したかった定理

Theorem pre_rev_eq_rev_post:
  (forall t, preorder_tree (rev_tree t) = rev (postorder_tree t))/\
  (forall f, preorder_forest (rev_forest f) = rev (postorder_forest f)).

にうってつけの形をしているのが見て取れるだろう.実際うってつけだ. この定理の証明はまず tree_forest_mut_ind を適用することから始まり, 後は流れに身を任せれば終わる. どのくらい身を任せているかは 証明を実際に見ていただければおわかりいただけると思う

この定理さえ証明してしまえば,元々証明したかった

Theorem pre_rev_eq_rev_post_tree t:
  preorder_tree (rev_tree t) = rev (postorder_tree t).

とか,おまけの

Theorem pre_rev_eq_rev_post_forest t:
  preorder_forest (rev_forest t) = rev (postorder_forest t).

が成り立つことはもはや自明である.

2.4 総合

ここまで,

  1. 相互帰納的データ型を定義
  2. 相互再帰関数を構成
  3. 相互帰納原理を使って定理証明

という 3 ステップを非常に大雑把にではあるが,順番に追ってきた.

相互再帰は通常の再帰の一般化だ.「相互」の字を取ってしまえば Coq を使い始めたばかりの人にも馴染みのあるプロセスではなかろうか. with が入って少々見た目がややこしくはなっているが,基本的にやるべきことは変わらない.

定義して関数書いて定理証明だ.

3 等価性判定

新たに定義した treeforest は,正確には型構成子だ.任意の型 T に対して,新たな型 tree T, forest T を構成する.

このとき,型 T の等価性が決定可能であれば型 tree Tforest T それぞれに於ける等価性も決定可能となる. 等価性が決定可能であれば,その決定手続きを関数中に用いることができる. 他にも色々とメリットがあったはずなのだが,どうにも記憶に登ってこないので潔く話を変えよう.

SSReflect の eqType は「等価性が決定可能な型」の型である. T: eqType だとすると x y: T に対して x = y が常に決定可能であるということだ. eqType 自体は型とその上の決定可能な等価性判定からなる構造体なのだが, coercion6 などの様々な道具によって,型同様に扱うことが出来る仕組みが提供されている.

最初に述べたように,型 T の等価性が決定可能であれば型 tree T の等価性も決定可能である. 即ち T: eqType であるなら tree T: eqType となるはずだ.

では,そうするためにはどうすればよいのだろうか.

同じようなことを実際に行っている例を見て真似ればよいのだ. 実際, tree.v に於ける eqType 絡みの部分は seq についてのそれに倣ったものである. というわけでまずは seq.v の,特に T: eqType に対して seq T: eqType となることをどのようにして実現しているのか,という部分について見ていく.

注意しておくと,以降の記述に eqType の細かい部分の説明や,それに関わる仕組みの解説等はほとんどない. これまでも大概だったが,以降はより「私の作業録」感が強くなっていく. Coq にはまだ使いこなせていない機能が多く,そしてそれらを駆使する SSReflect についてはなおさらである.

3.1 EqSeq

seq.v の冒頭にはこんな記述がある.

Notation seq := list.
Notation Cons T := (@cons T) (only parsing).
Notation Nil T := (@nil T) (only parsing).

つまり seq とは list そのものであった.おしまい.

というわけにもいかない.そもそも本題はそこではない. 以降の記述を見ていくと様々な記法や定理などがずらずらずらずらと並べられているが,今回注目すべき部分はコードのおそらくは真ん中辺りに位置する Seqtion EqSeq. ~ End EqSeq. の中身である. このセクション全体はそれなりの大きさをしているが seq TeqType たらしめるための部分は最初の 20 行程度だ.

Section EqSeq.

Variables (n0 : nat) (T : eqType) (x0 : T).
Notation Local nth := (nth x0).
Implicit Type s : seq T.
Implicit Types x y z : T.

Fixpoint eqseq s1 s2 {struct s2} :=
  match s1, s2 with
  | [::], [::] => true
  | x1 :: s1', x2 :: s2' => (x1 == x2) && eqseq s1' s2'
  | _, _ => false
  end.

Lemma eqseqP : Equality.axiom eqseq.

Canonical seq_eqMixin := EqMixin eqseqP.
Canonical seq_eqType := Eval hnf in EqType (seq T) seq_eqMixin.

...

これはその該当部分を引用してきたものである. セクション最初の変数宣言のうち, n0x0 の出番はここには無いので無視してよい. nth についても同様だ.

変数宣言やその下にある Implicit コマンドによって,以降の文脈では TeqType のインスタンスであり, sx などは基本的に宣言された通りの型を持つと解釈される7 ようになる.

これらの宣言部が終わった後,まず最初に行われているのは eqseq T 上の等価性の決定手続きである eqseq の構成である. 等価性判定が決定可能だというためには,実際に判定関数を作る必要があるし,作れば十分だ. 定義自体も難しくはないが,要素の比較の際に TeqType のインスタンスであることを利用している. 当たり前のようだが, seq TeqType のインスタンスであるためにはまず TeqType のインスタンスでなければならないことはここから伺える. 当たり前に思えることでも,確認はしておこう.しないとたまに怪我をする.

また,@<code>x = y@</code> は =xy 型が eqType のインスタンスであるときにその等価性の決定手続きを表す記法である. ある型を eqType のインスタンスにするということは,その型に対してもこの記法が使えるようにするという意味でもある.

さて,定義して関数書いて定理証明という流れに則れば,次にすべきは証明である. その示されるべき補題 eqseqP とそれを利用した残り 2 行を改めて以下に引用しておこう.

Lemma eqseqP : Equality.axiom eqseq.

Canonical seq_eqMixin := EqMixin eqseqP.
Canonical seq_eqType := Eval hnf in EqType (seq T) seq_eqMixin.

補題 eqseqP は手続き eqseq が述語 Equality.axiom を満たすという意味だが8,これは命題 x = y が成り立つこととは eqseq x y = true であることと,成り立たないことは eqseq x y = false と同一視できるということを述べている. SSReflect に於いては同一視できるという事実は重要な位置を占めるわけだが,その辺りを解説できるほどの知識・技量が今の私には備わっていないので割愛させていただく.

さて,この次の 2 行を経ることでようやく seq TeqType のインスタンスとみなせるようになる. とりわけ重要なのは seq_eqType だ.この型は eqType である. Canonical ではなく Definition にしてしまうと seq TeqType のインスタンスとして暗黙のうちに扱うことができなくなってしまうので注意しよう.

ちなみに seq_EqMixinCanonical で定義している理由はわからなかった. 次に treeforest に対してこれまでの流れと同じことをするわけだが,その際に CanonialDefinition に変えてみたり,そもそも定義せずに seq で例えれば

Canonical seq_eqMixin := EqMixin eqseqP.
Canonical seq_eqType := Eval hnf in EqType (seq T) seq_eqMixin.

という 2 つのコマンドを纏めてしまって

Canonical seq_eqType := Eval hnf in EqType (seq T) (EqMixin eqseqP).

に書き換えてみたりしたが,特に問題は起きなかった. 起きなかったが,ただ単に現時点で手を付けている範囲ではたまたま問題が起こらなかっただけという可能性も高いので,今は素直に真似をしておくことにしよう.

というわけでやっとのことで tree Tforest TeqType のインスタンスと見做すための作業を行う. 前置きが長いのは性だ,変えられぬ.

3.2 EqTree

seq って書いてあるところを treeforest に書き換えて,関数とかは with 使って上手い具合に相互再帰的に書いておけばよい.

この一文で終わる話をこれからダラダラとさせていただこう. 具体例があると理解のスピードも上がるよね,という話に聞き覚えがあるので,そういうポジティブな解釈をしていただければよい.

さて,まずすべきは等価性の決定手続きを定義することであった. 相互帰納的に定義された treeforest を対象とするのだから,その決定手続は相互再帰的に構成される.

Variable T: eqType.
Implicit Type t : tree T.
Implicit Type f : forest T.

Fixpoint eqtree t1 t2 :=
  match t1, t2 with
    | node x1 c1, node x2 c2 => (x1 == x2) && (eqforest c1 c2)
  end
with eqforest f1 f2 :=
  match f1, f2 with
    | leaf, leaf => true
    | sibl t1 f1, sibl t2 f2 => (eqtree t1 t2) && (eqforest f1 f2)
    | _, _ => false
  end.

そして次に行うのは eqtreeeqforestEquality.axiom を満たすこと,即ち以下の補題を証明することだ. なお,コーディングスタイルの違いはそのまま反映している.統一するのが面倒である.ついでに,引用部分とその他をなんとなく区別できてよい.

Lemma eqtreeP:
  Equality.axiom eqtree.

Lemma eqforestP:
  Equality.axiom eqforest.

このような 2 つの補題,特に相互再帰的に構成された関数について別々に命題を示そうとしているこの状況に既視感を抱いた方もおられるのではなかろうか,

というわけで,これら 2 つを次のように纏めてしまい,一つの補題として示そう.

Lemma eqtreeP_eqforestP:
  Equality.axiom eqtree)*(Equality.axiom eqforest).

さて,それでは証明してみよう.

これまでの流れを汲んで「よし,これはあれだな,相互帰納原理使って証明だな!」と勇んで tree_forest_mut_ind を適用しようとすると文句を言われる.

「あ,そっか, Equality.axiom の定義を展開しなくちゃな!」と機転を利かせて定義を展開しても,やっぱり tree_forest_mut_ind を適用しようとすると文句を言われる.

  • Q. 何故ですか.
  • A. この命題の型が Prop ではなく Type だからです.
  • Q. あなた散々定理とか補題とか宣っていたでしょう.
  • A. 証明モード使ってんだから別にいいんじゃないっすかねえ.
  • Q. は?
  • A.

というわけで tree_forest_mut_ind ではなく tree_forest_mut_rect を使わなければならない9. そして Combined Scheme コマンドでは tree_forest_mut_rect を構成できないので,直接次の型を持つ項を構成する.直接と言いつつ証明モードを使うのが手っ取り早いのでそれも含めて載せておこう.

Lemma tree_forest_mut_rect:
  forall (T: Type)(P : tree T -> Type) (Q : forest T -> Type),
    (forall (x : T) (c : forest T), Q c -> P (node x c)) ->
    Q leaf ->
    (forall t, P t -> forall f, Q f -> Q (sibl t f)) ->
    (forall t, P t) * (forall f, Q f).
Proof.
  move => T P Q IHn IHl IHs.
  exact (tree_forest_rect IHn IHl IHs, forest_tree_rect IHn IHl IHs).
Qed.

これを使えば eqtreeP_eqforestP は証明できる.こんな感じだ.

Lemma eqtreeP_eqforestP:
  (Equality.axiom eqtree)*(Equality.axiom eqforest).
Proof.
  apply: tree_forest_mut_rect
  => [x f IHf [x' f'] | [| t f] | t IHt f IHf [|t' f']] /=; try by constructor.
  - case: (x =P x') => [<- | Hneq]; last by right; case.
      by case: (IHf f') => [<- | Hneq] /=; [ left | right; case ].
  - move: (IHt t') => [<- | Hneq]; last by right; case.
      by move: (IHf f') => [<- | Hneq]; [left | right; case].
Qed.

ここまでくれば eqtreeP やら eqforestP やらは簡単に得られる. 正直なところわざわざ載せる必要もなかろうとは思うのだが,賑やかしにはなるかな,と思ったので載せておく.

Definition eqtreeP: Equality.axiom eqtree := fst eqtreeP_eqforestP.
Definition eqforestP: Equality.axiom eqforest := snd eqtreeP_eqforestP.

そろそろ,元々何がしたかったんだっけ? と記憶が薄れてきた頃であろう. tree Tforest TeqType のインスタンスとしたかったのである.

seq T に於いて Canonical ほげほげとしていたところをそのまま真似をすれば,晴れて目的は達成される.

Canonical tree_eqMixin := EqMixin eqtreeP.
Canonical tree_eqType := Eval hnf in EqType (tree T) (EqMixin eqtreeP).

Canonical forest_eqMixin := EqMixin eqforestP.
Canonical forest_eqType := Eval hnf in EqType (forest T) forest_eqMixin.

終わった.

としてしまっては味気ないので,それらしい補題を 2 つほど掲示して締めよう. 証明は恐ろしいことに 6 文字で終わる. by []. で終わる.なんということでしょう.

Lemma eqtree_node x1 x2 f1 f2:
  (x1 -: f1 == x2 -: f2) = (x1 == x2) && (f1 == f2).

Lemma eqforest_sibl t1 t2 f1 f2:
  (t1 ~+ f1 == t2 ~+ f2) = (t1 == t2) && (f1 == f2).

これらの補題はは rewrite タクティクの引数として使える.なんだか定理証明系を使っている風な,それらしい状況が出来上がったような気がしてこないだろうか.

実際に使っている場面がないとわからない? 確かにそうだ.

そしてネタバレをしてしまうと,少なくとも本稿ではこれらを使う場面はない.全くない. というわけで,出番は終わりである. そもそもこの節自体が次節で所属性判定について述べるための準備みたいなものであり,前座だ. あまり固執せずにとっとと話題を移そう.

4 所属性判定

TeqType のインスタンスであれば tree TeqType のインスタンスとなるというのが前節のお話であった. ここでは視点を変えて tree TT 型の要素を格納するコンテナと見做し,要素 x: T が木 t: tree T あるいは森 f: forest T に含まれているか否か,すなわち所属性判定を行う.

例えば l: seq TT: eqType であれば任意の x: T に対して x \in l という決定的な所属性判定ができる. \inseq T 固有の記法ではなく eqType に於ける等価性判定 @<code>==@</code> と同様に 所属性判定ができるとされた型 について共通の記法である10. これを tree Tforest T についても使えるようにしようというのが本節の目的だ.

所属性判定についても seq の真似をしよう.先人に倣うことは物事を進めるための堅実な一歩である.

4.1 EqSeq

seq の所属性判定に関する部分は等価性判定と同じく seq.vEqSeq 内にある. 該当部分を引用しておこう.

(* mem_seq and index. *)
(* mem_seq defines a predType for seq. *)

Fixpoint mem_seq (s : seq T) :=
  if s is y :: s' then xpredU1 y (mem_seq s') else xpred0.

Definition eqseq_class := seq T.
Identity Coercion seq_of_eqseq : eqseq_class >-> seq.

Coercion pred_of_eq_seq (s : eqseq_class) : pred_class := [eta mem_seq s].

Canonical seq_predType := @mkPredType T (seq T) pred_of_eq_seq.
(* The line below makes mem_seq a canonical instance of topred. *)
Canonical mem_seq_predType := mkPredType mem_seq.

まずは所属性判定関数を定義している.

Fixpoint mem_seq (s : seq T) :=
  if s is y :: s' then xpredU1 y (mem_seq s') else xpred0.

mem_seqseq T 型のデータに対する所属性判定関数だ. SSReflect を知らないと is のあたりに違和感を覚えるかもしれないが,やっていることは単純である.パターンマッチの際に この場合とそれ以外 で処理するときに少しだけ短く書けるような記法があるというだけである.しかし便利だ.

また,if 文が返す値は述語であることに注意されたい. xpredU1 y (mem_seq s') は, x: T に対して @<code>(x = y) || (mem_seq s' x)@</code> という命題を構成する述語である.述語を部分集合と見做した時,それらの和集合はまた新たな述語となる.そしてここでは一方が単集合であるから =xpredU1 という名前なのだろう.

続く 2 行で何をしているのかについては正直まだ良くわかっていない.

Definition eqseq_class := seq T.
Identity Coercion seq_of_eqseq : eqseq_class >-> seq.

だが,現時点で調べた限りでの私の推測を一応書いておこう.詳しく知っている方がいたらご教授願いたい.よろしくお願いいたします.

EqSeq に於いては T: eqType だが,基本的に seq は一般の型 T: Type に対して適用出来る.しかし,ここで定義された eqseq_classseq と同じように見えるが実際は適用出来る型が eqType のインスタンスに限られるという特徴を持つ.おそらく,この制約が predType などと関わり意味を持つのだと思う.

次の pred_of_eq_seqeqseq_class から pred_sort への coercion を与えている.

Coercion pred_of_eq_seq (s : eqseq_class) : pred_class := [eta mem_seq s].

ssrbool.v を見た限りでは, pred_sort は述語と扱うことのできる構造の career type ,日本語だと台型とでも言えばいいのだろうか,それを指すものであった. 定義から s: eqseq_class 即ち s: seq TT 上の述語と見なせるようにしているようだ. [eta f]fun x => f x だから [eta mem_seq s]fun x => mem_seq s x である.

それでは最後の 2 つに目を向けてみよう.

Canonical seq_predType := @mkPredType T (seq T) pred_of_eq_seq.
(* The line below makes mem_seq a canonical instance of topred. *)
Canonical mem_seq_predType := mkPredType mem_seq.

seq_predTypeCanonical コマンドによって tree TpretType T のインスタンスとしている.その際の変換を司るのが pred_of_eq_seq である. 続く mem_seq_predType はコメントにある通りだ.補足しておくと, predType は述語を司る台型 pred_sort と, pred_sort から pred T への変換 topred (ともう一つ意味ありげなフィールド)から構成されている.コメントにある topred とはこの topred の事であろう11

これで seq T に対して x \in s という記法が使えるようになった. コメント除いて 10 行足らずのコードに対して長々と文章を展開してきたわけだが,こうなったのは Coq のコードが持っている情報量がそれほどに多いからである.ということにしておく.

さて,準備が整ったわけであるから,やるべきことと言ったら決まっている. seq.v ではこの後に次のような補題を証明しているが,これらはあくまでもその一部である.

Lemma in_cons y s x : (x \in y :: s) = (x == y) || (x \in s).

Lemma in_nil x : (x \in [::]) = false.

Lemma mem_seq1 x y : (x \in [:: y]) = (x == y).

この後にも更に大量の補題が証明されているので,確認しておくと seq を使うときに便利だ.もしくは必要になった時に Search コマンド使いましょう. なお, Filters に入るまでの補題は大抵 1 行で終わっているので興味があればソースコードを見てみるとよい.

ようやく前置きが終わった.次だ次.

4.2 EqTree

seq って書いてあるところを treeforest に書き換えて,関数とかは with 使って上手い具合に相互再帰的に書いておけばよい.

終わらせてしまいたいが,流れを追うことにしよう.

目的は tree Tforest T についても \in を使って所属性判定ができるようにすることである. まずは判定関数を定義しよう

Fixpoint mem_tree (t: tree T): pred T :=
  match t with
    | node y f => xpredU1 y (mem_forest f)
  end
with mem_forest (f: forest T): pred T :=
  match f with
    | leaf => xpred0
    | sibl t f => xpredU (mem_tree t) (mem_forest f)
  end.

相互再帰的な定義である. xpredU は述語同士の ``和'' だ.

さて,判定関数を定義した後にすべきことは coercion を定義してカノニカるだけである. どのようにすればよいかというと, seq の該当部分を (コピー&ペースト)×2 して seqtreeforest にそれぞれ置き換えればよい12

Definition eqtree_class := tree T.
Identity Coercion tree_of_eqtree : eqtree_class >-> tree.

Coercion pred_of_eq_tree (t : eqtree_class) : pred_class := [eta mem_tree t].
Canonical tree_predType := @mkPredType T (tree T) pred_of_eq_tree.
Canonical mem_tree_predType := mkPredType mem_tree.

これが tree 版のコードで,

Definition eqforest_class := forest T.
Identity Coercion forest_of_eqforest : eqforest_class >-> forest.

Coercion pred_of_eq_forest (f : eqforest_class) : pred_class := [eta mem_forest f].
Canonical forest_predType := @mkPredType T (forest T) pred_of_eq_forest.
Canonical mem_forest_predType := mkPredType mem_forest.

これが forest 版のコードだ.本当にまるっきり同じ形をしていることが見て取れる.

\in を使えるようにするための準備はこのようにあっさり終わった. 実際にそうなっていることを確認するためにも定理証明するわけだが,実際に行ったものがこちらになります.

Lemma in_node y f x:
  (x \in node y f) = (x == y) || (x \in f).

Lemma in_leaf x:
  (x \in leaf) = false.

Lemma in_sibl x t f:
  (x \in sibl t f) = (x \in t) || (x \in f).

Lemma mem_tree1 x y:
  (x \in node y leaf) = (x == y).

証明そのものは割愛したが,概ね by []. である.

というわけで treeforest についても seq 同様に所属性判定ができるようになった.あっぱれ.

ここに至るまで,説明のための準備に長大な文章を費やし,いざ説明となった時には飽きが来てあっさりさっぱりといった具合であった. Coq で定理証明するときも大抵の場合は補題作りとその証明が時間の多くを占めているわけであるから,こうなるのもむべなるかな.

次節ではこれまでの纏めとして,ここまで定義してきたものを使ったそれらしい定理の記述(と証明)をする.

5 定理証明

Coq でやることといえば定理証明である. できることなら証明する定理がどんな意味をもつのかはわかりやすいほうがよい.

というわけで次のわかりやすい定理の証明に臨むこととしよう.

Theorem traverse_correct_pre_tree t x:
  (x \in t) == (x \in preorder_tree t).

木を走査して得られるリストはその木の要素を過不足なく含んでいるはずである. その仕様を記述したのがこの定理だ13

二度あることは三度あるので, t についての帰納法は失敗に終わる. 多くの方々に予想はついているだろうが,その予想通り,この定理の証明のためにまず示すべきは次の補題だ.

Lemma traverse_correct_pre:
  (forall t x, (x \in t) == (x \in preorder_tree t))/\
  (forall f x, (x \in f) == (x \in preorder_forest f)).

この補題の証明は相互帰納原理 tree_forest_mut_ind をゴールに適用するところから始まる. 3 つのサブゴールが生成されてそれぞれを証明していくことになるのだが,その際に必要となるのは帰納法の仮定の他は前節最後に列挙した補題のうち in_nodein_sibl の 2 つと, seq についての補題 in_consmem_cat である.等式の右辺は seq についての所属性判定なのだから,これは自然な要求であろう. 流れるままにこれらの補題を rewrite タクティクで使っていけば 証明はあっさり終わってしまう

だが,あっさり終わってしまうからといって軽く考えてはいけない. 手で証明をするときも定理証明系を使って証明をするときも,下準備をこつこつとしておくと目的の証明はあっさり進むものである. 今回であれば,等価性判定や所属性判定を seq と同じ枠組みで扱えるようにして,併せて幾つかの補題を証明してきたことがその下準備なのだ.

そして忘れてはいけないのが,更にその土台として存在している SSReflect の数多のライブラリである.これらがあってこそのあっさり感だ. これを味わうには SSReflect を実際に使う他ない. 今回は使うというか妙な部分に足を突っ込んだような気がしないでもないが,それはそれとして,である.

さて,後付の目標ではあるが纏めっぽい雰囲気を持つ定理の証明が終わったので,そろそろ締めるとしよう. 本稿に載せたコードは説明のために tree.v から一部改変しているものがある.より細かいところに興味を持った場合は,直接ソースコードを追っていくのがよいだろう.

6 次回予告

一応,書き終えた.他人の添削が入らないとこんな有り様になるという典型例の如き文章となっているだろうが,私は他人ではないのでそれを確認することはできない.皆様,いかがだったろうか.ツッコミはいつでも大歓迎である.

さて,こんな文章を書いてしまったわけではあるが,まだまだネタはある. 最後に次の題材を予告しておこう.自縄自縛必死だがそれもまた人生だ.

それでは次の題材は……おっと, eqtype のことと思ったかい?

確かに中盤から展開が苦しくなってきていたし書きながら調べつつ書きながら調べつつの繰り返しだったしその辺りを纏めたいなぁと思っているのだが,思った以上に面倒なことになりそうなので少し時間を頂きたい.

では,支配関係木かなって?

残念! 同じテーマだと 俺が飽きる から一旦別の話を挟ませてもらおう!

ということで次は計算効果の話だ!! Kleisli triple!!

Footnotes:

1

7 月ではないことがわかった.記憶とは曖昧なものだ.

2

ここでは,有向グラフ \(D\) で他の全ての頂点へ到達可能な頂点 r を持つもののことをいう.

3

非常にざっくりとした説明なので,詳しくは Google 先生や Appel の Tiger 本にお尋ね願いたい.Twitter 等で直接私に聞く場合は,用法・用量を守り正しくお使いください.

4

林と言ったりもするが,この記事では森に統一した.

5

このコマンドが使えるのは _ind に限られる. Combined Scheme コマンドは証明の自動生成を行う(と思っている)が, _rectrec で同じことをするとそれは関数の自動生成になる.あくまで私の想像だが, _rectrec の場合は証明と違って項の形も重要だから Combined Scheme が使えるのは _ind のみとしたのだろう.

6

余談だが, coercion に対応する日本語は強制型変換でよいのだろうか. これはどうにも長い気がしているのだが,いい訳語を思いつくでもなく,少々モヤモヤしている. Coq の場合は暗黙のうちに変換関数を適用する仕組みでしかなく,しかも制約がそれなりにあるので,余計にそう感じるのかもしれない.

7

少しためしてみると,どうやら Implicit Type x: T. としたあとは x だけでなく x1 とか x2 という名前の変数もその型は T だと見做される.また, Implicit Type x1: T. のようには書けなかった.単なる変数名の指定という意味ではないのだろう.リファレンスマニュアル読んできます.

8

見たままを述べているだけだ.あまりにも情報がない.

9

帰納原理は返り値の型が Prop, Set, Type のどれであるかに合わせてで ..._ind, ..._rec, ..._rect の 3 つを使い分けなければならないのであった.

10

ssrbool.vpredType 周りが重要なようだが,私自身がこの辺りに詳しくないので,説明はお預けとさせていただきたい.その仕組を理解する必要がいずれ生じるとは思うので,タイミングなど諸々の事情が噛み合えば調査レポート的なものをしたためることになると思われる.期待はしないように.

11

などと説明しているのだが,実験してみたところ seq_predTypemem_seq_predType のどちらか一方がありさえすれば問題がないのではないか,と思えてきた. tree に対して行った話ではあるが,片方をコメントアウトしても以降滞り無く進む.むしろ seq_predType を定義した後 mem_seq_predType を定義すると canonical projection を無視してるぜって警告が出るので,冗長な定義となっている可能性が高い.

12

テンプレートみたいなもんだからこそ出来る芸当だが,こういうボイラープレートを解消するために Template Vernacular 的な機能が欲しいと思った.というか,ずっと思っている.マクロでもいいから.

13

より厳密には要素の数,重複度についても言及すべきだが,本稿ではその部分は気にしないことにする.仮に重複度について考えるにしてもそれ程大変ではないと思うが.

Author: SDK@mathink

Created: 2015-06-28 Sun 02:42

Validate