Coq/SSReflectで子ノード数が不定である一般の根付き木をInductiveに定義する

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

n分木に関しては別記事「[Coq/SSReflectで自然数nを引数に取ってn分木を返す型をInductiveに定義する](https://qiita.com/nekonibox/items/710eb444189417069d22)」をご覧ください。

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

```coq
  Variable (T:Type).

  Inductive tree : Type := Node of T & seq tree.
                        (* Node : T -> seq tree -> tree *)
```
`tree`型のコンストラクタは`Node`の1つのみであり、各ノードはその要素の型`T`と、その子の列`seq tree`から構成されています。

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

```coq
  Inductive btree : Type :=
  | BLeaf of T                  (* BLeaf : T -> btree *)
  | BNode of T & btree & btree. (* BNode : T -> btree -> btree -> btree *)
```

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

```coq
  Notation Leaf x := (Node x [::]).
```

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

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

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

```coq
tree_ind
    : forall P : tree -> Prop,
      (forall (x:T), (s:seq tree), P (Node x s)) ->
      forall t:tree, P t.
```

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

```coq
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`を使って直接定義されています。

```coq
(* 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`を参考にしながら定義します。

```coq
  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`を使って同様に示すことができます。

```coq
  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`を記述することができます。

```coq
  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`を掛けたものを返す関数です。
書き換えると以下のようになります。

```coq
  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`を用いて以下のように書けます。

```coq
  Definition treesize : tree -> nat := treefold (fun _ => S) addn 0.
```

##高さを調べる

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

```coq
  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`する必要があります。

```coq
  Definition height' (t:tree) : nat := (treefold (fun _ => S) maxn 0 t).-1.
```

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

```coq
  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`を示してみます。

```coq
  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で子ノード数が不定である一般の根付き木を定義し、それに関する帰納原理や定義の仕方をまとめました。