Coq/SSReflectで辞書式順序で引数が構造的に小さくなる再帰関数をFixpointで定義する

#はじめに
Coq/SSReflectで再帰関数を定義するとき、必ず停止する関数しか記述できません。特に特定の引数が必ず構造的に小さくなる場合でない場合は停止性の証明が必要になります。しかし、引数が複数あり、辞書式順序で構造的に小さくなる場合は停止性の証明を書かずに定義する方法があります。
基本的にはこちらのサイト「[停止性が明らかでない関数を定義するには](https://www.iij-ii.co.jp/activities/programming-coq/coqt7.html)」を参考にしておりますが、定義だけでなく証明に必要な補題を作るところまで説明していきます。


#辞書式順序で引数が構造的に小さくなる関数
本記事で考える関数は、以下の等式を満たす関数`myfun : X -> Y -> Z`のように、第一引数から順番に`match`で分岐して、再帰呼び出しする際の`myfun`の引数が辞書的に構造的に小さくなっているものです。[^1]

[^1]: この例は2変数関数ですが、多変数関数でも同様に考えることができます。


```coq
  myfun x y =
  match x with
  ...
  | ConXi a0 ... ak x0 ... xn (* x0 ... xn : X *)
      => match y with
         ...
         | ConYj b0 ... bl y0 ... ym (* y0 ... yn : Y *)
             => gij (myfun x0) ... (myfun xn)
                    (myfun x y0) ... (myfun x ym)
                    x y a0 ... ak b0 ... bl
              (*
                gij : (Y -> Z) -> ... -> (Y -> Z) ->
                      Z -> ... -> Z ->
                      X -> Y -> ... -> ... ->
                      Z
              *)
         ...
         end
  ...
  end.
```

返り値を計算する`gij`では`myfun`の再帰呼び出しを行いますが、第一引数が構造的に小さくなっている、すなわち`myfun x0` ... `myfun xn` であるか、第一引数が`x`のままで第二引数が構造的に小さくなっている、すなわち`myfun x y0` ... `myfun x ym`のいずれかで記述できるもののみで構成されています。

後述する解説ではこの`myfun`を用いますが、一般的な例だけだと分かりづらいので、まずは具体例を見ていきます。

##具体例
辞書式順序で引数が小さくなる再帰関数の例として以下のようなものが挙げられます。

###引数のうち、どれか1つ以上が小さくなり、他の引数は変わらない再帰関数
再帰呼び出しを行うときの引数のうちどれか1つでも小さくなる場合は辞書式順序で引数が小さくなっていると言えます。
例えばPascalの三角形の(n,m)座標の値を求める関数Pascalは以下のように定義され、再帰呼び出しする際にはどちらかの引数が固定され、もう片方の引数が小さくなっています。

```math
\operatorname{Pascal}(0,m) := 1\\
\operatorname{Pascal}(n,0) := 1\\
\operatorname{Pascal}(n+1,m+1) := \operatorname{Pascal}(n,m+1)+\operatorname{Pascal}(n+1,m)
```

Coqでこれを`pascal : nat -> nat -> nat`として実装したとき、満たすべき漸化式は以下のとおりです。

```coq
  pascal n m =
  match n with
  | 0 => 1
  | n'.+1 => match m with
           | 0 => 1
           | m'.+1 => pascal n' m + pascal n m'
           end
  end.
(*
  g11 (fn':nat -> nat) (fnm':nat) (n m:nat) : nat := fn' m + fnm'

  g11 (pascal n') (pascal n m') n m = pascal n' m + pascal n m' 
*)
```


###上記以外の辞書式順序で引数が小さくなる再帰関数
Ackermann関数は上記に当てはまらない辞書式順序で引数が小さくなる関数です。

```math
\operatorname{Ackermann}(0,m) := m+1\\
\operatorname{Ackermann}(n+1,0) := \operatorname{Ackermann}(n,1)\\
\operatorname{Ackermann}(n+1,m+1) := \operatorname{Ackermann}(n,\operatorname{Ackermann}(n+1,m))
```

これもCoqで実装したときに満たしてほしい性質は以下のとおりです。

```coq
  ackermann n m =
  match n with
  | 0 => m.+1
  | n'.+1 => match m with
            | 0 => ackermann n' 1
            | m'.+1 => ackermann n' (ackermann n m')
            end
  end.
(*
  g10 (fn':nat -> nat) (n m:nat) : nat := fn' 1
  g11 (fn':nat -> nat) (fn'm:nat) (n m:nat) : nat := fn' fnm'

  g10 (ackermann n') n m = ackermann n' 1
  g11 (ackermann n') (ackermann n m') n m = ackermann n' (ackermann n m')
*)
```

ここで挙げた`pascal`と`ackermann`のCoqでの実装は後述します。まずは一般の`myfun`の場合で説明します。

#`Fixpoint`を使って実装する

話を戻して、冒頭で説明した`myfun`を`Fixpoint`を使って定義する方法を説明していきます。

まず、そのまま定義しようとすると引数の減少性が自明でないためエラーが出ます。

```coq
Fixpoint myfun (x:X) (y:Y) : Z :=
  match x with
  ...
  | ConXi a0 ... ak x0 ... xn
      => match y with
         ...
         | ConYj b0 ... bl y0 ... ym
             => gij (myfun x0) ... (myfun xn)
                    (myfun x y0) ... (myfun x ym)
                    x y a0 ... ak b0 ... bl
         ...
         end
  ...
  end.
(* Error: Cannot guess decreasing argument of fix. *)
```

そこで、以下のような手順でこの式を書き換えます。

##手順

###1.関数名を書き換える

```coq
Fixpoint myfun_rec (x:X) (y:Y) : Z := (* 関数名変更 *)
  match x with
  ...
  | ConXi a0 ... ak x0 ... xn
      => match y with
         ...
         | ConYj b0 ... bl y0 ... ym
             => gij (myfun_rec x0) ... (myfun_rec xn)
                    (myfun_rec x y0) ... (myfun_rec x ym)
                    x y a0 ... ak b0 ... bl
                    (* 再帰呼び出し部分も関数名変更 *)
         ...
         end
  ...
  end.
```

名称変更はしなくてもいいですが、証明中`simpl`した際に式が不必要に展開されるを防ぐため、行っておくことをオススメします。

###2.`fix`文を入れる

第二引数(`y`)の`match`文の前に`let fix`を挿入してその内部式全体を返す関数(`myfun_rec'`)を定義し、返り値を今定義した関数で書き換えます。このとき、内部関数の引数は元の関数の引数と同じ型、同じ値にします。

```coq
Fixpoint myfun_rec (x:X) (y:Y) : Z :=
  match x with
  ...
  | ConXi a0 ... ak x0 ... xn
      => let fix myfun_rec' x y := (* 追加 *)
             match y with
             ...
             | ConYj b0 ... bl y0 ... ym
                 => gij (myfun_rec x0) ... (myfun_rec xn)
                        (myfun_rec x y0) ... (myfun_rec x ym)
                        x y a0 ... ak b0 ... bl
             ...
             end in
         myfun_rec' x y (* 追加 *)
  ...
  end.
```

###3.再帰呼び出し部分の変更

再帰呼び出しをしている関数のうち、第一引数が元の引数と同じもの(`x`のままのもの)を`fix`で定義した内部関数名(`myfun_rec'`)で書き換えます。

```coq
Fixpoint myfun_rec (x:X) (y:Y) : Z :=
  match x with
  ...
  | ConXi a0 ... ak x0 ... xn
      => let fix myfun_rec' x y :=
             match y with
             ...
             | ConYj b0 ... bl y0 ... ym
                 => gij (myfun_rec x0) ... (myfun_rec xn)
                        (myfun_rec' x y0) ... (myfun_rec' x ym) (* この部分 *)
                        x y a0 ... ak b0 ... bl
             ...
             end in
         myfun_rec' x y
  ...
  end.
```

この時点で`Fixpoint`の定義が通るようになります。[^2][^3]

[^2]: 内部関数`myfun_rec'`の引数`x`は実は引数として受け取る必要はないため、`x`の値は外部変数とし、`y`の値だけ受け取る1変数関数として定義してもいいです。
[^3]: `myfun_rec'`は外部で1回しか使わないため、`let fix`ではなく単に`fix`で定義してそのまま引数を渡してもいいです。

###4.元の関数を`Definition`で再定義する。

本来、関数名として付けたかった名前を`Definition`で再定義します。

```coq
Definition myfun := myfun_rec.
```

こうしておくと、証明中に`simpl`しても`myfun`が元の`myfun_rec`の定義式に分解されず、`fix`などの煩雑な式が命題中に表示されるのを防ぐことができます。


##追加で用意しておきたい補題

上記のような流れで再帰関数を`Fixpoint`で定義できますが、定義しただけでは証明する際に使いづらいので、以下のような補題を用意しておくといいと思います。


###equation
本来`myfun`を定義したかった漸化式そのものです。`Function`で定義した場合は自動生成されますが、今回の方法では自分で定義する必要があります。
この補題は、主に証明中で`simpl`の代わりに`rewrite myfun_equation.`の形で使います。
これで`myfun`の実装がどうであるかを考えずに、元の漸化式だけを考えて証明することができます。


```coq
Lemma myfun_equation x y :
  myfun x y =
  match x with
  ...
  | ConXi a0 ... ak x0 ... xn
      => match y with
         ...
         | ConYj b0 ... bl y0 ... ym
             => gij (myfun x0) ... (myfun xn)
                    (myfun x y0) ... (myfun x ym)
                    x y a0 ... ak b0 ... bl
         ...
         end
  ...
  end.
Proof.
  by case : x; case : y.
Qed.
```

`myfun_equation`自体の証明ですが、全ての引数に対して`case`を行うだけで示せるはずです。


###帰納原理

必須というわけではないですが、帰納原理も作っておくと便利です。

```coq
Lemma myfun_ind (P:X -> Y -> Prop) :
  ... ->
  (forall a0 ... ak x0 ... xn b0 ... bl y0 ... ym,
   P x0 (...) ->
   ...
   P xn (...) ->
   (*
     第二引数はgij内部のmyfun xi (...)と同じ形になるように。
     gij中に記述がない場合は仮定しなくてよい。
     場合によっては命題を(forall y, P xi y)の形にするのも可。
   *)
   P (ConXi a0 ... ak x0 ... xn) y0 ->
   ...
   P (ConXi a0 ... ak x0 ... xn) ym ->
   (* 仮定はgijの内部でmyfun x yjの記述があるものだけでよい *)
   P (ConXi a0 ... ak x0 ... xn) (ConYj b0 ... bl y0 ... ym)) ->
  ... ->
  forall x y, P x y.
Proof.
  move => ... Hij ... x y.
  elim : x =>[...|a0 ... ak x0 ... xn IHx0 ... IHxn|...] in y *;
    elim : y =>[...|b0 ... bl y0 ... ym IHy0 ... IHym|...].
  ...
  - exact : Hij.
    (*
      (Hij (IHx0 ...) ... (IHxn ...) IHy0 ... IHym)
      の形で書けるはずなのでexactで通ると思います。
     *)
  ...
Qed.
```

証明は辞書式順序で引数が減少しているので、`elim : x =>[...] in y *; elim : y.`で示せると思います。

#実用例

辞書式順序で引数が小さくなる関数の例として出したPascalの三角形とAckermann関数を例に定義してみます。

###Pascalの三角形

```coq
Fixpoint pascal_rec n m :=
  match n with
  | 0 => 1
  | n'.+1 => let fix pascal_rec' n m :=
              match m with
              | 0 => 1
              | m'.+1 => pascal_rec n' m + pascal_rec' n m'
              end in
            pascal_rec' n m
  end.

Definition pascal := pascal_rec.

Lemma pascal_equation n m:
  pascal n m =
  match n with
  | 0 => 1
  | n'.+1 => match m with
           | 0 => 1
           | m'.+1 => pascal n' m + pascal n m'
           end
  end.
Proof.
  by case : n; case : m.
Qed.

Lemma pascal_ind (P:nat -> nat -> Prop) :
  (forall m, P 0 m) ->
  (forall n, P n.+1 0) ->
  (forall n m, P n.+1 m -> P n m.+1 -> P n.+1 m.+1) ->
  forall n m, P n m.
Proof.
  move => H0m Hn0 Hnm n m.
  elim : n =>[|n IHn] in m *; elim : m =>[|m IHm]=>//.
  - exact : Hnm.
Qed.
```

ちなみに`pascal_rec`の内部関数はもう少し省略して記述できます。[^2][^3]

```coq
Fixpoint pascal2_rec n m :=
  match n with
  | 0 => 1
  | n'.+1 => (fix pascal2_rec'n m :=
              match m with
              | 0 => 1
              | m'.+1 => pascal2_rec n' m + pascal2_rec'n m'
              end) m
  end.
```

###Ackermann関数

```coq
Fixpoint ackermann_rec n m :=
  match n with
  | 0 => S m
  | n'.+1 => let fix ackermann_rec' n m :=
                match m with
                | 0 => ackermann_rec n' 1
                | m'.+1 => ackermann_rec n' (ackermann_rec' n m')
                end in
             ackermann_rec' n m
  end.

Definition ackermann := ackermann_rec.

Lemma ackermann_equation n m:
  ackermann n m =
  match n with
  | 0 => S m
  | n'.+1 => match m with
            | 0 => ackermann n' 1
            | m'.+1 => ackermann n' (ackermann n m')
            end
  end.
Proof.
    by case : n; case : m.
Qed.

Lemma ackermann_ind (P:nat -> nat -> Prop) :
  (forall m, P 0 m) ->
  (forall n, P n 1 -> P n.+1 0) ->
  (forall n m, P n.+1 m -> P n (ackermann n.+1 m) -> P n.+1 m.+1) ->
  forall n m, P n m.
Proof.
  move => H0m Hn0 Hnm n m.
  elim : n =>[|n IHn] in m *=>//; elim : m =>[|m IHm].
  - exact : Hn0.
  - exact : Hnm.
Qed.
```

`ackermann_ind`内部に`ackermann`が現れて少し気持ち悪いですが、一応これで簡単な命題は示せると思います。


#まとめ
辞書式順序で引数が構造的に小さくなる再帰関数を`Fixpoint`で定義する方法について記述しました。今回の説明は2変数関数の場合ですが、他変数関数でも同様に記述することができるので、この方法を参考にしていただければ幸いです。