Coq/SSReflectで自然数nを引数に取ってn分木の型を返す型をInductiveに定義する

#はじめに
Coq/SSReflectで自然数nを引数に取り、n分木の型を返す型を定義します。

子ノード数が不定の一般の木の場合は、前記事「[Coq/SSReflectで子ノード数が不定である一般の根付き木をInductiveに定義する](https://qiita.com/nekonibox/items/c2abf000e386b2a2ae33)」をご覧ください。


#n分木を定義する

まず、n分木がどういうコンストラクタを持てばいいのか、2分木、3分木を見ながら考察していきます。


##2分木や3分木を参考にする

型`T`に対する2分木`bitree`や3分木`tritree`を見ていきましょう。

```coq
  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`のようになればいいので、以下のように定義してみます。


```coq
(* 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を引数に取る形に定義し直してみます。

```coq
(* 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ではなく直積の形での記述も試してみますが同様の結果になりました。

```coq
(* 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では不可能なのでしょうか？


##一般の木を参考にする

[前記事](https://qiita.com/nekonibox/items/c2abf000e386b2a2ae33)における一般の根付き木の定義をもう一度みてみます。

```coq
  Variable (T:Type).

  Inductive tree : Type := Node of T & seq tree.
```

一般の根付き木`tree`の場合、引数の個数が不定なので、それらをリスト`seq tree`にまとめ、1つの引数としてコンストラクタ`Node`に取っています。
ここで、注目するべきは`seq tree`で、再帰する型`tree`を引数に取っていますが、定義が通ります。

実は、Inductiveに定義された型(この場合は`seq`)の引数であれば、再帰する型を取るようなものでも定義できる場合があります。[^1]
[^1]: 後述の通り、任意のInductiveな型が使えるという訳ではないので注意。

そこで、tupleをInductiveに定義しなおし、これを引数に取ることを考えます。


##n分木の型を定義する

改めてn分木を定義していきます。

###n引数を表す型をInductiveに定義する
まず、n個の引数を表す型`sizseq`をInductiveに定義します。

```coq
  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`を用いて記述します。

```coq
  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]

[^2]: それぞれ自動生成される帰納原理`sizseq_ind`と`sizseq'_ind`を比較するとわかります。`sizseq_ind`の葉に対する仮定は単に`P 0 (SizNil T)`ですが、`sizseq'_ind`は`forall T, P 0 T (SizNil' 0 T)`であり、`T:Type`が任意の型になってしまうためです。

```coq
  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`を使って定義します。

```coq
  Inductive ntree (n:nat) (T:Type) : Type :=
  | NLeaf of T
  | NNode of T & sizseq (ntree n T) n.
```

`sizseq`がInductiveに定義されているため、この定義が通ります。

使い方としては以下の通りです。

```coq
  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`と同様に定義できます。

```coq
  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分木の帰納原理としてほしい命題は以下の通りです。

```coq
  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つを紹介します。


##直接記述する方法

以下のように記述すれば定義できます。

```coq
  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.
```

基本的には、[一般の根付き木のとき](https://qiita.com/nekonibox/items/c2abf000e386b2a2ae33)と同様に`fix`文を用いて定義します。

ここで重要なのは、再帰関数`loop`内の再帰関数`iter_conj`の引数として`m:nat`を取っている点です。この`m`は`f:sizseq (ntree n T) m`の長さを表していて、再帰するたびに`m`が変化するため、引数として取る必要があります。


##proof modeで証明する方法

以下のように証明します。

```coq
  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分木における多くの関数が定義できます。

```coq
  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`も以下のように定義できます。

```coq
  Definition nheight (T:Type) (n:nat) (t:ntree n T) : nat :=
    ntreefold (fun _ => 0) (fun _ => S) maxn 0 t.
```

ただ、`ntreefold`はそのままでは使いづらいので、以下のような等式を示しておきます。

```coq
  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を具体化した木の型を個別に定義する方が使いやすいように思えました。