はじめに
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が成り立つことから示したい、つまり以下のような命題が欲しいことが本記事作成に至るきっかけです。
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では以下のように有限集合上で定義されます。
Variable (T:finType)
Definition partition (P:{set {set T}}) (D:{set T}) :=
[&& cover P == D, trivIset P & set0 \notin P].
PがDの分割であることの3つの条件はそれぞれ、被覆性、非交叉性、空集合を含まないことを表しています。
今回定義するリストに分割は後述する理由により重複要素を許すものにしたいので、被覆性と非交叉性を重複を許すように合わせた以下のような条件を満たすリストのリストとして定義します。
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として以下に定義します。
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の分割になります。
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関数の返り値が性質として嬉しくないので改良する」のmyundupに変更してもいいです。)
Definition spartition_by (X:Type) (Y:eqType) (f:X -> Y) (s:seq X) :=
subspartition_by f s (undup (map f s)).
もちろん、これが分割になっていることも上の補題からすぐ示せます。
Lemma spartition_by_sound (X Y:eqType) (f:X -> Y) s:
spartition (spartition_by f s) s.
ちなみに、最初からこれを定義すればいいように見えますが、わざわざsubspartition_byを定義したのは、spartition_by_soundを示すのに、そのままでは帰納法が回らないためです。
ちなみにtがユニークである場合には、ある種の非交叉性も成り立ちます。
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を用いて簡単に示せます。
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でリストのある種の分割に関する定義と補題を示しました。