Coq/SSReflectで引数の長さが1短い任意の部分列で再帰呼び出しする関数を定義する

#はじめに
Coq/SSReflectで再帰関数を定義する際には停止性の証明が必要です。本記事では、リストを引数にとる再帰関数で、長さが引数より1短い任意の部分列に対して再帰呼び出しを行う関数を定義する方法を説明します。


#長さが1短い任意の部分列で再帰呼び出しする関数

該当する関数を定義する前に、まず長さが1短い任意の部分列を求める関数`pick1sub : forall T:Type, seq T -> seq (T * seq T)`を定義します。

```coq
From mathcomp Require Import all_ssreflect.

Fixpoint pick1sub_rec (T:Type) (top s:seq T) : seq (T * seq T) :=
    match s with
    | [::] => [::]
    | a :: s' => (a,top ++ s') :: sub1seqs_rec (rcons top a) s'
    end.

Definition pick1sub (T:Type) (s:seq T) := sub1seqs_rec [::] s.
```

`pick1sub`は、以下の例のように引数`s`に対し、`s`の各要素と`s`からそれを除いた部分列の組を返す関数です。`pick1sub_rec`は`pick1sub`を定義するための補助関数です。

```coq
Eval compute in pick1sub [:: 1; 2; 3; 4].
(* = [:: (1,[:: 2; 3; 4]); (2,[:: 1; 3; 4]); (3,[:: 1; 2; 4]), (4,[:: 1; 2; 3])] *)
```

これを用いて、本記事で定義したい関数`allsubrec : seq I -> R`が満たすべき漸化式`allsubrec_equation`を見ていきます。

```coq
Section Allsubrec.
  Variable R:Type.
  Variable idx:R.
  Variable op:R -> R -> R.
  Variable I:Type.
  Variable f:I -> R -> R.

  Lemma allsubrec_equation (s:seq I) :
    allsubrec s =
    foldr op idx (map (fun x => f x.1 (allsubrec x.2)) (pick1sub s)).
```

`pcik1sub s`の各要素`(x.1, x.2)`に対し、`x.2`の長さは`s`より1短いので、関数`allsubrec`は再帰するたびに引数の長さが1短くなります。一見すると常に再帰呼び出しを行う停止しない関数に見えますが、`s = [::]`のときは`foldr`の返り値が`idx`になるため停止性が言えます。

再帰呼び出しの際、リストの長さが1短くなるので、そのまま`Function allsubrec s {measure size s}`と定義したくなるのですが、残念ながらそのままではコンパイルが通りません。

```coq
(* 定義できず *)
  Function allsubrec (s:seq I) {measure size s} :=
    foldr op idx (map (fun x => f x.1 (allsubrec x.2)) (pick1sub s)).
(* the term fun x : I * seq I => f x.1 (allsubrec x.2) can not contain a recursive call to allsubrec *)
```
これは、再帰呼び出しを行う関数`allsubrec`の減少する引数が内部関数`(fun x => f x.1 (allsubrec x.2))`のローカル変数`x`に依存するためです。[^1]

それではこれを書き直して、定義が通るようにします。

[^1]: 再帰呼び出しを行う関数が内部関数の中にあっても、[こちらの記事](https://qiita.com/nekonibox/items/3d483edf4eb46adbfae7)のように、減少する引数がローカル変数に依存しない形であれば定義できます。


#再帰関数を定義する

先ほどの例では、部分列を求める`pick1sub`を外に定義し、それに対して`foldr`を行っていたため、引数の減少性が分からない状態になっていました。そこで`pick1sub`と`foldr`を1つの関数にまとめることを考えます。

```coq
  Function allsubrec_rec (s:seq I * seq I)
           {measure (fun s => measure s.1 s.2) s} : R :=
    match s.2 with
    | [::] => idx
    | a :: s' => op (f a (allsubrec_rec ([::],s.1 ++ s')))
                    (allsubrec_rec (rcons s.1 a,s'))
    end.
  Proof.
    - move =>[top s] a s' /=->. apply /ltP. exact : allsubrec_measure_lt2.
    - move =>[top s] a s' /=->. apply /ltP. exact : allsubrec_measure_lt1.
  Defined.
(* measure : seq I -> seq I -> natが定義されていて、引数の減少性がそれぞれallsubrec_measure_lt1, lt2で証明できていたとする *)

  Definition allsubrec (s:seq I) := allsubrec_rec ([::],s).
```

問題は減少性をどのように証明するかです。引数は`(size s.1 + size s.2, size s.2)`の辞書式順序で小さくなっているので、"[Coq/SSReflectで辞書式順序で引数が構成的に小さくなる再帰関数をFixpointで定義する](https://qiita.com/nekonibox/items/3d483edf4eb46adbfae7)"の手法が使えるように見えますが、`size s.1 + size s.2`の部分は構造的に小さくなるとは限らないためこの方法は使えません。そこで今回は`Function`で定義します。[^2]

[^2]: `Program Fixpoint`を使って定義する方法もありますが、`allsubrec_rec_equation`が自動生成されないため、証明するときに困ります。

`Function`で定義するためには`measure`関数が必要です。しかし、一般の辞書式順序に対し、順序を保存する自然数への写像は存在しません。[^3] しかしながら、第二引数に上界が存在する場合は順序を保存する自然数への写像を定義することができます。
今回のケースでは、再帰を行う第二引数`s.2`は最大でも`size s.1 + size s.2`以下の長さにしかなりません。すなわち、以下のような`measure : seq I -> seq I -> nat`を用いて減少性が証明できます。

[^3]: $f:\mathbb{N} * \mathbb{N} \to \mathbb{N}$が辞書式順序を保存する写像だとすると、(1,1) < x < (2,1)を満たすxは無限個あるが、f(1,1) < y < f(2,1)を満たすyは有限個しかないため矛盾する。
```coq
  Local Notation measure top s := ((size top + size s) ^ 2 + size s).

  Lemma allsubrec_measure_lt1 top (a:I) s :
    measure ([::]:seq I) (top ++ s) < measure top (a :: s).
  Proof.
    rewrite /= add0n !addnS size_cat ltnS !expnS !expn0 !muln1 mulSn -!addnA.
      by rewrite addnC leq_add // mulnS addnAC leq_addl.
  Qed.

  Lemma allsubrec_measure_lt2 top (a:I) s :
    measure (rcons top a) s < measure top (a :: s).
  Proof.
      by rewrite size_rcons addSn /= !addnS.
  Qed.
```

これで先ほどの`allsubrec_rec`及び`allsubrec`の定義が通るようになります。


##元の漸化式を満たすことの証明

元の漸化式`allsubrec_equation`を満たすことは以下の補題から分かります。

```coq
  Lemma myallsubrec_rec_equation (top s:seq I) :
    allsubrec_rec (top,s) =
    foldr op idx
          (map (fun x => f x.1 (allsubrec_rec ([::],top ++ x.2)))
               (pick1sub s)).
  Proof.
    elim : s =>[|a s IHs] in top *=>//. rewrite allsubrec_rec_equation /=.
    congr(op). rewrite IHs. congr(foldr).
    rewrite (@map_pick1sub_rec
               _ _ (fun x y => f x (allsubrec_rec ([::], top ++ y)))).
    apply : eq_map => x /=. by rewrite cat_rcons.
  Qed.
(* ただし
  Lemma map_pick1sub_rec (T S:Type) (f:T -> seq T -> S) top s :
    map (fun x => f x.1 x.2) (pick1sub_rec top s) =
    map (fun x => f x.1 (top ++ x.2)) (pick1sub s).
*)
  Lemma allsubrec_equation (s:seq I) :
    allsubrec s =
    foldr op idx (map (fun x => f x.1 (allsubrec x.2)) (pick1sub s)).
  Proof.
    exact : myallsubrec_rec_equation.
  Qed.
End Allsubrec.
```

#使用例

与えられた列の全ての置換を返す関数`mypermutations : forall T:Type, seq T -> seq (seq T)`は`allsubrec`を用いて定義できます。

```coq
Definition mypermutations (T:Type) (s:seq T) : seq (seq T) :=
  allsubrec [::] cat
            (fun a s => if s is _ :: _ then map (cons a) s else [:: [:: a]]) s.

Eval compute in mypermutations [:: 1; 2; 3].
(* = [[1; 2; 3]; [1; 3; 2]; [2; 1; 3]; [2; 3; 1]; [3; 1; 2]; [3; 2; 1]] *)
```

#応用

##可換モノイドの場合
`op:R -> R -> R`が可換モノイドの演算だった場合、`allsubrec`の返り値は引数の列は順序によらず等しくなることが分かります。これを表す命題`allsubrec_perm`を証明します。

```coq
Section Allsubrec_com.
  Variable R:eqType.
  Variable idx:R.
  Variable op:Monoid.com_law idx.
  Variable I:eqType.
  Variable f:I -> R -> R.

  Local Notation measure top s := ((size top + size s) ^ 2 + size s).

  Lemma allsubrec_rec_perm (tops topt s t:seq I) :
    perm_eq s t ->
    perm_eq tops topt ->
    allsubrec_rec idx op f (tops,s) = allsubrec_rec idx op f (topt,t).
  Proof.
    move : topt t.
    have [n] := ubnP (measure tops s).
    elim : n tops s =>[|N IHn] tops [|a s]//=; rewrite ?addnS ltnS
    => Hn topt [|b t]//; try by move =>/permP /(_ predT).
    move => Hst. move : {Hst} (perm_mem Hst a) (perm_mem Hst b) (Hst).
    rewrite !in_cons !eq_refl /= eq_sym =>/esym.
    case : (b =P a) =>[->_ _|/= Hab Ha Hb Hst Htop].
    rewrite ?perm_cons !allsubrec_rec_cons => Hst Htop.
    - congr(op (f _ _) _).
      + apply : IHn (perm_cat _ _) _=>//. apply : leq_trans Hn.
        rewrite -!addnS addnS. exact : allsubrec_measure_lt1.
      + apply : (IHn _ _ (leq_trans _ Hn));
          by rewrite ?perm_rcons2 // size_rcons addSn.
    - rewrite !allsubrec_rec_cons.
      rewrite (IHn _ s (leq_trans _ Hn) (rcons tops a) (b :: rem b s)) //;
              try exact : perm_to_rem.
      rewrite (IHn _ t (leq_trans _ Hn) (rcons topt b) (a :: rem a t)) //;
              try exact : perm_to_rem.
      rewrite !allsubrec_rec_cons Monoid.mulmCA.
      congr(op (f _ _) (op (f _ _) _));
        apply : (IHn _ _ (leq_trans _ Hn)); try exact : perm_refl.
      + apply : (leq_trans (allsubrec_measure_lt1 _ b _)).
          by rewrite -(perm_size (perm_to_rem Hb)) size_rcons addSn.
      + rewrite cat_rcons perm_cat // -(perm_cons b) (perm_trans _ Hst) //.
          by rewrite -perm_rcons /= perm_cons perm_rcons perm_sym perm_to_rem.
      + rewrite -ltnS -![(_ + size s).+1]addnS. exact : allsubrec_measure_lt1.
      + rewrite cat_rcons perm_cat // -(perm_cons a) (perm_trans Hst) //.
        rewrite perm_sym -perm_rcons /= perm_cons perm_rcons perm_sym.
        exact : perm_to_rem.
      + apply : (leq_trans (allsubrec_measure_lt2 _ _ _)).
          by rewrite -(perm_size (perm_to_rem Hb)) size_rcons addSn.
      + rewrite -(perm_cons a) (perm_trans _ (perm_to_rem Ha)) //.
        rewrite -(perm_cons b) (perm_trans _ Hst) // -perm_rcons /= perm_cons.
          by rewrite perm_rcons perm_sym perm_to_rem.
      + rewrite perm_rcons -rcons_cons perm_rcons perm_sym perm_rcons perm_cons.
          by rewrite perm_rcons perm_cons perm_sym.
      + case : (perm_size Hst) (perm_size Htop) =>->->.
          by rewrite size_rcons addSn.
      + by rewrite size_rcons addSn.
  Qed.

  Lemma allsubrec_perm s t :
    perm_eq s t -> allsubrec idx op f s = allsubrec idx op f t.
  Proof.
    move => Hst. exact : allsubrec_rec_perm.
  Qed.
```

`allsubrec_perm`を示すためには、元の関数`allsubrec_rec`に関する命題を示す必要がありますが、`allsubrec_rec`は2つ引数があり、そのそれぞれが置換であるときに返り値が等しいことを証明しています。
一見すると、片方だけが置換であったときの命題をそれぞれ示せば良さそうですが、今回のケースでは2つの引数が相互に依存するため、両方同時に証明しないと帰納法が回りませんでした。

また、帰納法ですが関数の停止性と同様、`measure`の減少性を利用した完全帰納法を使っています。具体的には"[Coq/SSReflectで{}を使わずに完全帰納法を適用する]
(https://qiita.com/nekonibox/items/8147291e9fd483e3d579)"を応用して、`have [n] := ubnP (measure top s). elim : n tops s =>[|n IHn] tops [|a s]`のように記述します。

証明の方針ですが、`perm_eq`に関する証明には"[Coq/SSReflectでperm_eqが不変条件であるような命題を証明するための帰納原理](https://qiita.com/nekonibox/items/233d23bf0fb7cad79e01)"のようにコツがあり、
`s`と`t`がそれぞれ`a :: s'`, `b :: t'`のとき、`a = b`のときは帰納法の仮定がそのまま使えば示せます。`a <> b`のときは、`b \in s'`かつ``a \in t'`のはずなので、`perm_eq s' (b :: rem b s')`かつ`perm_eq t' (a :: rem a t')`が成り立ちます。
よって、`perm_trans`より`a :: b :: rem a s'`と`b :: a :: rem b t'`に関して示せばいいので、`rem a s'`と`rem b t'`に関する帰納法の仮定を使えます。

この補題により、漸化式が以下の`allsubrec_equation_comm`のように記述できることがわかります。

```coq
  Lemma allsubrec_rec_equation_comm top s :
    allsubrec_rec idx op f (top,s) =
    foldr op idx
          (map (fun a => f a (allsubrec_rec idx op f ([::],top ++ rem a s))) s).
  Proof.
    elim : s =>[|a s IHs] in top *=>//=.
    rewrite allsubrec_rec_cons eq_refl IHs. congr(op _ (foldr _ _ _)).
    apply /eq_in_map => b Hb. congr(f). apply : allsubrec_rec_perm =>//.
    rewrite cat_rcons perm_cat ?perm_refl //.
      by case : ifP =>[/eqP->|]; rewrite ?perm_refl // perm_sym perm_to_rem.
  Qed.

  Lemma allsubrec_equation_com s:
    allsubrec idx op f s =
    foldr op idx (map (fun a => f a (allsubrec idx op f (rem a s))) s).
  Proof.
    exact : allsubrec_rec_equation_com.
  Qed.
```

`rem a s`は`s`の要素のうち、最も先頭に近い`a`を除く関数なので、重複がある場合は一般に任意の部分列を表現できません。しかし、列の順序に依存しない可換モノイドであれば、この命題が成り立つことがわかります。


#まとめ
Coq/SSReflectで引数の長さが1短い任意の部分列で再帰呼び出しする関数の定義や、補題に関して説明しました。