はじめに
Coq/SSReflectで二分木やn分木のような子ノードの数が一定の木ではなく、不定であるような一般の根付き木を定義する方法を記述します。
n分木に関しては別記事「Coq/SSReflectで自然数nを引数に取ってn分木を返す型をInductiveに定義する」をご覧ください。
根付き木を定義する
子ノード数が不定であるような根付き木の型treeは以下のように定義できます。
Variable (T:Type).
Inductive tree : Type := Node of T & seq tree.
(* Node : T -> seq tree -> tree *)
tree型のコンストラクタはNodeの1つのみであり、各ノードはその要素の型Tと、その子の列seq treeから構成されています。
ここで二分木btreeと比較してみると、
Inductive btree : Type :=
| BLeaf of T (* BLeaf : T -> btree *)
| BNode of T & btree & btree. (* BNode : T -> btree -> btree -> btree *)
tree型には二分木における葉を作るコンストラクタBLeafにあたるものがないように思えます。しかしtree型では、葉は子の列が[::]の場合として定義します。
Notation Leaf x := (Node x [::]).
つまり、一般の根付き木の場合、枝を作るコンストラクタのみで構成することが可能であるということです。
しかしながら、この定義では枝の構成に関する帰納原理がうまく自動生成されず、木に関する性質を証明するのが大変になります。そこで、木に関する帰納原理を定義します。
木に関する帰納原理
先ほどの定義でtreeに関する帰納原理tree_indが自動生成されますが、コンストラクタNodeにtree型を直接とる引数がないため、帰納法の仮定がうまく生成されません。
tree_ind
: forall P : tree -> Prop,
(forall (x:T), (s:seq tree), P (Node x s)) ->
forall t:tree, P t.
本当は、以下のような帰納法の仮定として各子ノードに全てに対して示したい命題が成り立つような命題mytree_indが欲しいです。
mytree_ind
: forall P : tree -> Prop,
(forall (x:T) (s:seq tree),
foldr (fun t:tree => and (P t)) True s -> P (Node x s)) ->
forall t:tree, P t.
ここで、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 *)
Module GenTree.
Variable T : Type.
Inductive tree := Leaf of T | Node of nat & seq tree.
Definition tree_ind K IH_leaf IH_node :=
fix loop t : K t : Prop := match t with
| Leaf x ⇒ IH_leaf x
| Node n f0 ⇒
let fix iter_conj f : foldr (fun t ⇒ and (K t)) True f :=
if f is t :: f' then conj (loop t) (iter_conj f') else Logic.I
in IH_node n f0 (iter_conj f0)
end.
End GenTree.
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を参考にしながら定義します。
Definition mytree_ind (P:tree -> Prop)
(IH_node : forall x s,
foldr (fun t => and (P t)) True s -> P (Node x s)) :
forall t, P t :=
fix loop t : P t :=
match t with
| Node x s =>
let fix iter_conj s : foldr (fun t => and (P t)) True s :=
if s is u :: s' then conj (loop u) (iter_conj s') else Logic.I
in IH_node x s (iter_conj s)
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を使って同様に示すことができます。
Lemma mytree_ind (P:tree -> Prop) :
(forall x s, foldr (fun t => and (P t)) True s -> P (Node x s)) ->
forall t, P t.
Proof.
move => Hnode.
fix HP 1.
elim =>[x s]. apply : Hnode. by elim : s =>[|u s IHs].
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を記述することができます。
Fixpoint treefold (S:Type)
(f:T -> S -> S) (op:S -> S -> S) (id:S) (t:tree) : S :=
match t with
| Node x s => f x (foldr (fun u => op (treefold f op id u)) id s)
end.
木tの各子ノードuでの再帰関数の返り値treefoldr f op id uの列に対し、foldr op idを施します。その結果と親tの要素xに対し、fを掛けたものを返す関数です。
書き換えると以下のようになります。
Lemma treefold_equal S f op (id:S) t :
treefold f op id t =
match t with
| Node x s => f x (foldr op id (map (treefold f op id) s))
end.
Proof. case : t =>[x s]/=. by rewrite foldr_map. Qed.
例えば、木のノード数を返す関数treesizeはこのtreefoldを用いて以下のように書けます。
Definition treesize : tree -> nat := treefold (fun _ => S) addn 0.
高さを調べる
木といえば高さを調べたくなりますが、高さを調べる関数heightはtreefoldで定義するより、直接定義したほうがいいです。
Fixpoint height (t:tree) : nat :=
match t with
| Node _ s => foldr (fun u => maxn (height u).+1) 0 s
end.
一応、treefoldを使っても高さを求める関数height'が定義できますが、tree型では葉も枝も同じコンストラクタNodeで定義されているため区別ができず、葉も枝と同じように高さとしてカウントしてしまうため、treefoldのみで定義しようとすると1大きい結果が返ってきます。つまり結果から.-1する必要があります。
Definition height' (t:tree) : nat := (treefold (fun _ => S) maxn 0 t).-1.
このように定義すると帰納法を使うときに.-1.+1が出てきますが、これを消去するためには、treefoldの返り値が0より大きいことを示す必要があります。実際には、以下の証明のrewrite prednK //; case : u.のような記述をする必要があり、証明するのが面倒になります。
Lemma height_equal: height =1 height'.
Proof.
elim /mytree_ind =>[x s]/=.
elim : s =>[|u s IHs]//=[->/IHs->]. rewrite /height'.
by rewrite prednK //; case : u.
Qed.
木に関する証明
上で木に関する帰納原理mytree_indと関数を定義したので、実際に使ってみます。
例として、木のノード数は高さより真に大きいことlt_height_treesizeを示してみます。
Lemma treesize_cons x u s:
treesize (Node x (u :: s)) = treesize u + treesize (Node x s).
Proof. by rewrite /treesize /= addnS. Qed.
Lemma lt_height_treesize t: height t < treesize t.
Proof.
elim /mytree_ind : t =>[x s]/=.
elim : s =>[|t s IHs]//=[Ht /IHs Hle]. rewrite treesize_cons maxnE -addnS.
apply : leq_add =>//. exact : leq_ltn_trans (leq_subr _ _) Hle.
Qed.
基本的には、先ほどのheightとheight'が外延的等価であったことを示した時と同様に、木に関する帰納法elim /mytree_ind : t =>[x s]を使った後、子ノードを取り出すために子ノードのリストに関する帰納法elim : sを使います。
まとめ
Coq/SSReflectで子ノード数が不定である一般の根付き木を定義し、それに関する帰納原理や定義の仕方をまとめました。