Coq/SSReflectで分割関数によるリストの自然な分割を定義し、証明する

# はじめに
Coq/SSReflectのライブラリであるmathcomp内にはfinset.vに有限集合の分割に関するものがありますが、リストに関するものはありません。
そこでリストのある種の分割を定義し、分割関数によるリストの自然な分割に関する定理を証明します。


# モチベーション

`X:eqType`上の適当な述語`P:pred X`が与えられていたとき、リスト`s:seq X`に対する`all p s`を示すのに、勝手な`Y:eqType`と`f:X -> Y`を与えて、任意の`y:Y`に対する`s`の部分列`filter (pred1 y \o f) s`に対して`all p`が成り立つことから示したい、つまり以下のような命題が欲しいことが本記事作成に至るきっかけです。

```coq
  Lemma all_spartition_by (X Y:eqType) (f:X -> Y) p s:
    (forall y, all p (filter (pred1 y \o f) s)) -> all p s.
```


# 本記事で定義するリストの分割

まず集合の分割の定義を見てみます。

集合の分割はmathcompでは以下のように有限集合上で定義されます。

```coq:finset.v
Variable (T:finType)

Definition partition (P:{set {set T}}) (D:{set T}) :=
  [&& cover P == D, trivIset P & set0 \notin P].
```

`P`が`D`の分割であることの3つの条件はそれぞれ、被覆性、非交叉性、空集合を含まないことを表しています。

今回定義するリストに分割は後述する理由により重複要素を許すものにしたいので、被覆性と非交叉性を重複を許すように合わせた以下のような条件を満たすリストのリストとして定義します。

```coq
  Definition spartition (X:eqType) (ss:seq (seq X)) (s:seq X) :=
    perm_eq s (flatten ss).
```

つまり、リストを重複を許す集合と捉え、順序を無視してその和の要素が元のリストの要素と等しいものとして定義し、空集合は含んでも構わないものとして定義します。

なぜこの定義をしたかというと、モチベーションにあるように、`X:Type`とリスト`s:seq X`に対し、適当な`Y:eqType`と分割関数`f:X -> Y`から、`f`によってラベル付けすることによって定義できる自然な分割を扱えるようにするためです。
つまり、任意の`y:Y`に対し、`f`の行き先が`y`になる`s`の部分リスト`filter (pred1 y \o f) s`が定義できるので、これらを全ての`y`に対して集めてきたものを分割として扱いたいということです。


# 分類関数によるリストの分割

上の分割関数から定義されるリストのリストを定義します。
リスト`t:seq Y`に対し、その各要素`y \in t`から`filter (pred1 y \o f) s`を返すリストを`s`の部分分割`subspartition_by f s t`として以下に定義します。

```coq
  Definition subspartition_by (X:Type) (Y:eqType) (f:X -> Y) (s:seq X) :=
    map (fun y => filter (pred1 y \o f) s).
```

`t`に重複要素がない場合、この`subspartition_by f s t`は`f`の行き先が`t`の要素になる`s`の部分リスト`filter (fun x => f x \in t) s`の分割になります。

```coq
  Lemma subspartition_by_sound (X Y:eqType) (f:X -> Y) s t :
    uniq t ->
    spartition (subspartition_by f s t) (filter (fun x => f x \in t) s).
  Proof.
    move => Ht. apply /permP => p.
    elim : t Ht =>[|y t IHt /=/andP[/negbTE Hy]]/= Ht.
    - by rewrite -(@eq_filter _ pred0) ?filter_pred0.
    - rewrite count_cat -IHt // !count_filter -count_predUI addnC. apply /esym.
      rewrite -(@eq_count _ pred0) ?count_pred0;
        [apply /eq_count|] => z /=; case : (p z) =>//=.
      case : (@eqP _ (f z) y) =>//->. by rewrite Hy.
  Qed.
```

この事実から、`t = undup (map f s)`のとき、`subspartition_by f s t`は`s`の分割になることがわかるので、これで分割関数`f`によるリスト`s`の分割`spartition_by f s`を定義します。
(ただしmathcompの`undup`関数は性質としてあまり嬉しくないので、「[Coq/SSReflectでリストの重複要素を削除するundup関数の返り値が性質として嬉しくないので改良する](https://qiita.com/nekonibox/items/d134c8aa92aa909a8a20)」の`myundup`に変更してもいいです。)


```coq
  Definition spartition_by (X:Type) (Y:eqType) (f:X -> Y) (s:seq X) :=
    subspartition_by f s (undup (map f s)).
```

もちろん、これが分割になっていることも上の補題からすぐ示せます。

```coq
  Lemma spartition_by_sound (X Y:eqType) (f:X -> Y) s:
    spartition (spartition_by f s) s.
```

ちなみに、最初からこれを定義すればいいように見えますが、わざわざ`subspartition_by`を定義したのは、`spartition_by_sound`を示すのに、そのままでは帰納法が回らないためです。


ちなみに`t`がユニークである場合には、ある種の非交叉性も成り立ちます。

```coq
  Lemma subspartition_by_disjoint (X Y:eqType) (f:X -> Y) s t :
    uniq t -> pairwise (allrel (fun x y => x != y)) (subspartition_by f s t).

  Lemma spartition_by_disjoint (X Y:eqType) (f:X -> Y) s :
    pairwise (allrel (fun x y => x != y)) (spartition_by f s).
```


# モチベーション部分の解消

本記事の冒頭にあったモチベーションの命題は`spartition_by`を用いて簡単に示せます。

```coq
  Lemma all_spartition_by (X:eqType) (Y:eqType) (f:X -> Y) p s:
    (forall y, all p (filter (pred1 y \o f) s)) -> all p s.
  Proof.
    rewrite (perm_all _ (spartition_by_sound f _)) => H.
      by apply /allP => t /flattenP[x /mapP[y _->]/(allP (H y))].
  Qed.
```


# まとめ
Coq/SSreflectでリストのある種の分割に関する定義と補題を示しました。