はじめに

Coq/SSReflectで二分木やn分木のような子ノードの数が一定の木ではなく、不定であるような一般の根付き木を定義する方法を記述します。

n分木に関しては別記事「Coq/SSReflectで自然数nを引数に取ってn分木を返す型をInductiveに定義する」をご覧ください。

根付き木を定義する

子ノード数が不定であるような根付き木の型treeは以下のように定義できます。

Variable(T:Type).Inductivetree:Type:=NodeofT&seqtree.(* Node : T -> seq tree -> tree *)

tree型のコンストラクタはNodeの1つのみであり、各ノードはその要素の型Tと、その子の列seq treeから構成されています。

ここで二分木btreeと比較してみると、

Inductivebtree:Type:=|BLeafofT(* BLeaf : T -> btree *)|BNodeofT&btree&btree.(* BNode : T -> btree -> btree -> btree *)

tree型には二分木における葉を作るコンストラクタBLeafにあたるものがないように思えます。しかしtree型では、葉は子の列が[::]の場合として定義します。

NotationLeafx:=(Nodex[::]).

つまり、一般の根付き木の場合、枝を作るコンストラクタのみで構成することが可能であるということです。

しかしながら、この定義では枝の構成に関する帰納原理がうまく自動生成されず、木に関する性質を証明するのが大変になります。そこで、木に関する帰納原理を定義します。

木に関する帰納原理

先ほどの定義でtreeに関する帰納原理tree_indが自動生成されますが、コンストラクタNodeにtree型を直接とる引数がないため、帰納法の仮定がうまく生成されません。

tree_ind:forallP:tree->Prop,(forall(x:T),(s:seqtree),P(Nodexs))->forallt:tree,Pt.

本当は、以下のような帰納法の仮定として各子ノードに全てに対して示したい命題が成り立つような命題mytree_indが欲しいです。

mytree_ind:forallP:tree->Prop,(forall(x:T)(s:seqtree),foldr(funt:tree=>and(Pt))Trues->P(Nodexs))->forallt:tree,Pt.

ここで、foldr (fun t => and (P t)) True sが、子ノードのリストsに対し、その全ての子ノードtに対してP tが成り立っていることを表しています。

帰納原理を示す

この帰納原理mytree_indを示すにはどうすればいいでしょうか？
帰納法の仮定がないtree_indは使えそうにないので、fixコマンドを使います。

mytree_indと同じ型を持つ式を直接記述する方法と、Proof modeで示す方法があるので、それぞれ紹介します。

定義式を直接記述する方法

実は、mathcompライブラリのchoice.v内に、葉が任意の型Tであって、枝がnatであるような一般の根付き木GenTree.treeが定義されています。この帰納原理GenTree.tree_indはfixを使って直接定義されています。

(* in mathcomp/choice.v *)ModuleGenTree.VariableT:Type.Inductivetree:=LeafofT|Nodeofnat&seqtree.Definitiontree_indKIH_leafIH_node:=fixloopt:Kt:Prop:=matchtwith|Leafx⇒IH_leafx|Nodenf0⇒letfixiter_conjf:foldr(funt⇒and(Kt))Truef:=iffist::f'thenconj(loopt)(iter_conjf')elseLogic.IinIH_nodenf0(iter_conjf0)end.EndGenTree.

GenTree.treeは葉GenTree.Leafと枝GenTree.Nodeの2つのコンストラクタがあり、帰納原理GenTree.tree_indでは、葉と枝、それぞれに対する帰納法の仮定IH_leafとIH_nodeを渡しています。

詳しい解説は一旦先にtreeの方の帰納原理mytree_indを定義してから、そちらを使って行います。これはGenTree.tree_indでは型が省略されているため、分かりづらいためです。

まずは帰納原理mytree_indをGenTree.tree_indを参考にしながら定義します。

Definitionmytree_ind(P:tree->Prop)(IH_node:forallxs,foldr(funt=>and(Pt))Trues->P(Nodexs)):forallt,Pt:=fixloopt:Pt:=matchtwith|Nodexs=>letfixiter_conjs:foldr(funt=>and(Pt))Trues:=ifsisu::s'thenconj(loopu)(iter_conjs')elseLogic.IinIH_nodexs(iter_conjs)end.

ここで、fix式で定義されたloop t : P tは、P tにおいて帰納法を適用していることを表しており、帰納法の仮定はloop u : P uとして内部に現れています。

実際にはloopは再帰関数で、t:treeの構造に関して再帰呼び出しを行なっています。
Coqでは停止する関数のみしか定義できないため、再起呼び出しを行うtree型の引数に対して減少性が成り立たないといけません。今回の場合、再起呼び出しを行う引数uはtをコンストラクタNodeとconsで分解して出てくるものであり、構造的に小さくなっていると言えるので、定義が通るというわけです。

Proof modeで示す方法

Proof modeでもfixを使って同様に示すことができます。

Lemmamytree_ind(P:tree->Prop):(forallxs,foldr(funt=>and(Pt))Trues->P(Nodexs))->forallt,Pt.Proof.move=>Hnode.fixHP1.elim=>[xs].apply:Hnode.byelim:s=>[|usIHs].Qed.

証明中のコマンドfix HP 1で、P tに関する帰納法を使います。このコマンドの引数のうち、HPは仮定の名前、1は第1引数に対する帰納法を表しており、 実行すると、HP : forall t, P tという仮定から、forall t, P tを示すことになります。

ゴールと同じ仮定があるように見えるので、すぐapplyしたくなりますが、残念ながらゴールは消えるものの、第1引数tの減少性が言えないため、Qedできない仕様になっています。

ここでは、子ノードに関する帰納法を使えばいいので、tを分解して子ノードのリストsを取り出し、これに関する帰納法を使えば子ノードuが現れるので、このuに対して帰納法の仮定P uを適用してやればいいです。
この証明によって、直接定義を記述するのと同じような定義の式が生成されます。

木の構造に関する再帰関数

木の構造に関する再帰関数をいくつか定義します。

fold関数を定義する

リストにおいて主な再帰関数がfoldrで記述できるように、木に関しても、全ての子ノードに対して再帰するような関数treefoldを記述することができます。

Fixpointtreefold(S:Type)(f:T->S->S)(op:S->S->S)(id:S)(t:tree):S:=matchtwith|Nodexs=>fx(foldr(funu=>op(treefoldfopidu))ids)end.

木tの各子ノードuでの再帰関数の返り値treefoldr f op id uの列に対し、foldr op idを施します。その結果と親tの要素xに対し、fを掛けたものを返す関数です。
書き換えると以下のようになります。

Lemmatreefold_equalSfop(id:S)t:treefoldfopidt=matchtwith|Nodexs=>fx(foldropid(map(treefoldfopid)s))end.Proof.case:t=>[xs]/=.byrewritefoldr_map.Qed.

例えば、木のノード数を返す関数treesizeはこのtreefoldを用いて以下のように書けます。

Definitiontreesize:tree->nat:=treefold(fun_=>S)addn0.

高さを調べる

木といえば高さを調べたくなりますが、高さを調べる関数heightはtreefoldで定義するより、直接定義したほうがいいです。

Fixpointheight(t:tree):nat:=matchtwith|Node_s=>foldr(funu=>maxn(heightu).+1)0send.

一応、treefoldを使っても高さを求める関数height'が定義できますが、tree型では葉も枝も同じコンストラクタNodeで定義されているため区別ができず、葉も枝と同じように高さとしてカウントしてしまうため、treefoldのみで定義しようとすると1大きい結果が返ってきます。つまり結果から.-1する必要があります。

Definitionheight'(t:tree):nat:=(treefold(fun_=>S)maxn0t).-1.

このように定義すると帰納法を使うときに.-1.+1が出てきますが、これを消去するためには、treefoldの返り値が0より大きいことを示す必要があります。実際には、以下の証明のrewrite prednK //; case : u.のような記述をする必要があり、証明するのが面倒になります。

Lemmaheight_equal:height=1height'.Proof.elim/mytree_ind=>[xs]/=.elim:s=>[|usIHs]//=[->/IHs->].rewrite/height'.byrewriteprednK//;case:u.Qed.

木に関する証明

上で木に関する帰納原理mytree_indと関数を定義したので、実際に使ってみます。

例として、木のノード数は高さより真に大きいことlt_height_treesizeを示してみます。

Lemmatreesize_consxus:treesize(Nodex(u::s))=treesizeu+treesize(Nodexs).Proof.byrewrite/treesize/=addnS.Qed.Lemmalt_height_treesizet:heightt<treesizet.Proof.elim/mytree_ind:t=>[xs]/=.elim:s=>[|tsIHs]//=[Ht/IHsHle].rewritetreesize_consmaxnE-addnS.apply:leq_add=>//.exact:leq_ltn_trans(leq_subr__)Hle.Qed.

基本的には、先ほどのheightとheight'が外延的等価であったことを示した時と同様に、木に関する帰納法elim /mytree_ind : t =>[x s]を使った後、子ノードを取り出すために子ノードのリストに関する帰納法elim : sを使います。

まとめ

Coq/SSReflectで子ノード数が不定である一般の根付き木を定義し、それに関する帰納原理や定義の仕方をまとめました。