はじめに
Coq/SSReflectで自然数nを引数に取り、n分木の型を返す型を定義します。
子ノード数が不定の一般の木の場合は、前記事「Coq/SSReflectで子ノード数が不定である一般の根付き木をInductiveに定義する」をご覧ください。
n分木を定義する
まず、n分木がどういうコンストラクタを持てばいいのか、2分木、3分木を見ながら考察していきます。
2分木や3分木を参考にする
型Tに対する2分木bitreeや3分木tritreeを見ていきましょう。
Variable (T:Type).
Inductive bitree : Type :=
| BiLeaf of T
| BiNode of T & bitree & bitree.
(* BiNode : T -> bitree -> bitree -> bitree *)
Inductive tritree : Type :=
| TriLeaf of T
| TriNode of T & tritree & tritree & tritree.
(* TriNode : T -> tritree -> tritree -> tritree -> tritree *)
どちらも2つのコンストラクタから構成されており、それぞれBiLeaf、Trileafが葉を作るコンストラクタ、BiNode、TriNodeが枝を作るコンストラクタになっています。
葉を作るコンストラクタBiLeaf、TriLeafはそれぞれT型の変数をもらって木の型を返すものであり、両者に大きな違いはありませんが、枝を作るコンストラクタBiNode, TriNodeが大きく異なります。具体的には、どちらもT型の変数を1つもらうところは同じですが、元の木の型bitree、tritreeの引数の個数が2個、3個と異なっています。
以上のことを踏まえると、n分木を定義する場合も葉と枝を作るコンストラクタを用意して、枝を作るコンストラクタの引数の個数をn個にすることで定義できそうです。
しかしながら、2分木や3分木と同様にn分木を定義しようとするとうまくいきません。
2分木や3分木のように定義しようとすると...
2分木や3分木を参考にしながらn分木ntree : nat -> Type -> Typeを定義します。
しかしながら、n分木は自然数nに依存する型となるので、2分木や3分木のようにすんなりと定義させてもらえません。
失敗例1
n分木の引数n:natに対し、葉を作るコンストラクタの型はNLeaf : T -> ntree n、枝を作るコンストラクの型はNNode : T -> ntree n -> ... -> ntree n -> ntree nのようになればいいので、以下のように定義してみます。
(* failed *)
Inductive ntree (n:nat) (T:Type) : Type :=
| NLeaf of T
| NNode : T -> iter n (fun X:Type => ntree n T -> X) (ntree n T).
(* Error: The type of constructor nNode is not valid;
its conclusion must be "ntree" applied to its parameter. *)
iter n (fun X => ntree n T -> X) (ntree n T)の値は確かにntree n T -> ... -> ntree n T -> ntree n Tになるはずですが、Coq側でうまくマッチしてくれないみたいです。
エラー文から察するに、返り値が明確にntree n Tの形で記述されていないとダメなようです。
失敗例2
そこで、やむなく引数をuncurry化して、返り値がntree n T型になるようにtupleを引数に取る形に定義し直してみます。
(* failed *)
Inductive ntree (n:nat) (T:Type) : Type :=
| NLeaf of T
| NNode of T & n.-tuple (ntree n T).
(* NNode : T -> n.-tuple (ntree n T) -> ntree n T *)
(* Error: Non strictly positive occurrence of "ntree" in
"T -> n.-tuple (ntree n T) -> ntree n T" *)
ダメみたいです。
失敗例3
一応、tupleではなく直積の形での記述も試してみますが同様の結果になりました。
(* failed *)
Inductive ntree (n:nat) (T:Type) : Type :=
| NLeaf of T
| NNode of iter n (prod (ntree n T)) T.
(* Error: Non strictly positive occurrence of "ntree" in
"iter n (prod (ntree n T)) T -> ntree n T" *)
n個の引数を直接記述することはできないので、再帰する引数の型をiterやtupleのような、何かの関数の引数として与えなくてはなりません。
しかしながら、上記のような記述では通らないため、そもそも関数の返り値内に現れる型で再帰することはCoqでは不可能なのでしょうか？
一般の木を参考にする
前記事における一般の根付き木の定義をもう一度みてみます。
Variable (T:Type).
Inductive tree : Type := Node of T & seq tree.
一般の根付き木treeの場合、引数の個数が不定なので、それらをリストseq treeにまとめ、1つの引数としてコンストラクタNodeに取っています。
ここで、注目するべきはseq treeで、再帰する型treeを引数に取っていますが、定義が通ります。
実は、Inductiveに定義された型(この場合はseq)の引数であれば、再帰する型を取るようなものでも定義できる場合があります。1
そこで、tupleをInductiveに定義しなおし、これを引数に取ることを考えます。
n分木の型を定義する
改めてn分木を定義していきます。
n引数を表す型をInductiveに定義する
まず、n個の引数を表す型sizseqをInductiveに定義します。
Inductive sizseq (T:Type) : nat -> Type :=
| SizNil : sizseq T 0
| SizCons n : T -> (sizseq T n) -> sizseq T n.+1.
sizseqのnat型の第二引数が引数の個数を表しており、sizseq T nと記述したときn引数のT型の値を表しています。
具体的な値は、リストのそれと同様にSizConsとSizNilを用いて記述します。
Check (SizCons true (SizCons false (SizNil _))).
(* : sizseq bool 2 *)
言い換えれば、sizseqは長さの証明付きのリストだと考えることができます。
実はn.-tupleも定義の上では長さの証明付きのリストですが、こちらはリストtvalとsize tval == nの証明から構成されており、Inductiveに定義されているわけではないため、sizseqとは構成方法が異なります。
ここで、sizseq (T:Type) (n:nat) : Typeではなく、sizseq (T:Type) : nat -> Typeと定義しているのは、前者のように外部から与えてしまうと、各コンストラクタの返り値をsizseq T nに固定しなければならず、nの値を変更できないためです。実際にはコンストラクタによって異なる値を返さなければならないため、各コンストラクタの引数として後から与える形を取っています。
このように定義しておくと、証明においてs:sizseq T mに対してelimまたはcaseしたとき、それぞれのコンストラクタに対応する各ゴールにおいて、ゴールに存在する全てのmを対応する値、つまりSizNilのときは0、SizConsのときはn.+1に書き換えてくれます。言い換えれば、mは元々n.+1の形で記述できていたという事実を得ることになります。
ただし、それがmであったという情報を失うことになることに注意が必要です。
そのため、引数の順番がn分木ntree : nat -> Type -> Typeと異なるからといって、sizseq : nat -> Type -> Typeと定義してしまうと、後述するntreeの定義がうまく通らなくなります。
これは、コンストラクタに戻したときに元の型の情報、つまりntree型であったという情報を失って、ただの一般の型Tで記述することになってしまい、型が合わなくなるためです。2
Inductive sizseq' : nat -> Type -> Type :=
| SizNil' T : sizseq' 0 T
| SizCons' n T : T -> (sizseq' n T) -> sizseq' n.+1 T.
(* it can be defined, but we can not define n-ary tree using this definition *)
n分木の型
n分木を先ほどのsizseqを使って定義します。
Inductive ntree (n:nat) (T:Type) : Type :=
| NLeaf of T
| NNode of T & sizseq (ntree n T) n.
sizseqがInductiveに定義されているため、この定義が通ります。
使い方としては以下の通りです。
Check (NNode 4 (SizCons (NLeaf _ 5) (SizCons (NLeaf _ 3) (SizNil _)))).
(* : ntree 2 nat *)
これはn=2のときの要素がnat型の木で、根の値4であり、値がそれぞれ5と3の葉の子ノードを持っていることを表しています。
ただし、一般の根付き木のときのように帰納原理がうまく自動生成されないので、これを証明する必要があります。
n分木の帰納原理
n分木の帰納原理を証明する前に、帰納原理を記述するためのsizseqにおけるfold関数を定義します。
sizseqにおけるfold関数
sizseqは基本的には長さの証明付きのリストと考えられるので、fold関数sizfoldrの定義もリストに関するfoldrと同様に定義できます。
Fixpoint sizfoldr (T S:Type)
(f:T -> S -> S) (id:S) (n:nat) (i:sizseq T n) : S :=
match i with
| SizNil => id
| SizCons _ x i' => f x (sizfoldr f id i')
end.
帰納原理
n分木の帰納原理としてほしい命題は以下の通りです。
myntree_ind
: forall (n:nat) (T:Type) (P:ntree n T -> Prop),
(forall x : T, P (NLeaf n x)) ->
(forall (x:T) (s:sizseq (ntree n T) n),
sizfoldr (fun u : ntree n T => and (P u)) True s ->
P (NNode x s)) ->
forall t, P t.
Proof.
葉に対する仮定と枝に対する仮定の2つがあります。
特に枝に関して、sizfoldr (fun u => and (P u)) True sが全ての子ノードに対して、帰納法の仮定が成り立つことを表しています。
この命題の証明ですが、本記事では直接証明項を記述する方法と、Proof modeで証明する方法の2つを紹介します。
直接記述する方法
以下のように記述すれば定義できます。
Definition myntree_ind n (T:Type) (P:ntree n T -> Prop)
(Hleaf:forall x, P (NLeaf n x))
(Hnode:forall (x:T) s,
sizfoldr (fun u : ntree n T => and (P u)) True s ->
P (NNode x s)) :
forall t, P t :=
fix loop t : P t :=
match t with
| NLeaf x => Hleaf x
| NNode x s =>
let fix iter_conj (m:nat) (f:sizseq (ntree n T) m) :
sizfoldr (fun u => and (P u)) True f :=
match f with
| SizNil => Logic.I
| SizCons _ y f' => conj (loop y) (iter_conj _ f')
end in
Hnode x s (iter_conj _ s)
end.
基本的には、一般の根付き木のときと同様にfix文を用いて定義します。
ここで重要なのは、再帰関数loop内の再帰関数iter_conjの引数としてm:natを取っている点です。このmはf:sizseq (ntree n T) mの長さを表していて、再帰するたびにmが変化するため、引数として取る必要があります。
proof modeで証明する方法
以下のように証明します。
Lemma myntree_ind' n (T:Type) (P:ntree n T -> Prop) :
(forall x, P (NLeaf n x)) ->
(forall (x:T) s,
sizfoldr (fun u : ntree n T => and (P u)) True s ->
P (NNode x s)) ->
forall t, P t.
Proof.
move => Hleaf Hnode.
fix HP 1.
elim =>[x|x s].
- exact : Hleaf.
- apply : Hnode. move : (ntree n T) P HP s {Hleaf}=> X P HP.
by elim.
Qed.
fix文を用いるのは一般の根付き木の時と同じですが、ポイントは1つ目のelimでNNodeに関するゴールにおいてapply : Hnodeをしたあとです。
ここから先は木の性質ではなく、長さ証明付きリストs:sizseq (ntree n T) nに関する性質を示す場面です。
つまりsに対して帰納法を使う場面ですが、単にelim : sとしようとすると、前述の通り、ゴールにおける全てのnが任意のn0に対するn0.+1に書き換わることになります。従って型ntree n T内のnに関しても同様にn0.+1に書き変わってしまい、型が元のntree n Tと異なってしまうことから型エラーになってしまうため、そのままではelimコマンドが通りません。
そこで、一旦ntree n T型の名前をXに書き換え(ntree n T型を含む仮定P、HPも全てX型に書き直します)、nに依存しない形にしてからelimを行います。この書き換えによってntree型であるという情報を失いますが、この時点ですでにntree型に依存した仮定や関数が存在しないため、このような書き換えを行うことができます。
この操作の意味としては、一般の型Xに対してゴールの性質を示し、それをntree n T型に適用することであると考えることができます。
n分木におけるfold関数
次にn分木におけるfold関数を定義します。
fold関数によって、n分木における多くの関数が定義できます。
Definition ntreefold (T S:Type)
(fleaf:T -> S) (fnode:T -> S -> S) (op:S -> S -> S) (id:S) (n:nat)
: ntree n T -> S :=
fix loop t : S :=
match t with
| NLeaf x => fleaf x
| NNode x s =>
let fix iter_op (m:nat) (r:sizseq (ntree n T) m) : S :=
match r with
| SizNil => id
| SizCons k y r' => op (loop y) (iter_op _ r')
end in
fnode x (iter_op _ s)
end.
帰納原理を直接定義した時と同様にfix文を使って定義します。
リストのfold文と違うのは、葉のときと枝の時で処理する関数が違うところです。
葉と枝で処理を分けることによって、例えば木の高さを計算する関数nheightも以下のように定義できます。
Definition nheight (T:Type) (n:nat) (t:ntree n T) : nat :=
ntreefold (fun _ => 0) (fun _ => S) maxn 0 t.
ただ、ntreefoldはそのままでは使いづらいので、以下のような等式を示しておきます。
Lemma ntreefold_equal (T S:Type)
(fleaf:T -> S) (fnode:T -> S -> S) (op:S -> S -> S) (id:S)
(n:nat) (t:ntree n T) :
ntreefold fleaf fnode op id t =
match t with
| nLeaf x => fleaf x
| nNode x s =>
fnode x (sizfoldr (fun u => op (ntreefold fleaf fnode op id u)) id s)
end.
Proof.
elim : t =>[|x s]//=. congr(fnode _ _).
move : (ntree n T) (@ntreefold _ _ fleaf fnode op id n) s => X f.
by elim =>[|m i s /= ->].
Qed.
これもproof modeで帰納原理を示したときと同様に、一旦ntree n TをXに書き換えてから長さの証明付きリストsに関する帰納法を使っています。
ここで@ntreefold _ _ fleaf fnode op id nも書き換えているのは、ntreefoldが木を引数にとる関数であるので、これを関数fに一般化しないとntree n TをXに一般化する際に型エラーを起こすためです。
まとめ
Coq/SSReflectでn分木を定義し、それにおける帰納原理やfold関数も定義しました。
しかしながらn分木は自然数に依存する型であり、その扱いが難しいため、現実的には一般の根付き木か、素直に2分木や3分木などのように、nを具体化した木の型を個別に定義する方が使いやすいように思えました。