はじめに
CoqのSSReflectライブラリseq.vにおいて、リストの重複要素を削除するundup関数が定義されています。
しかしながら、一般にリストから重複要素を削除するアルゴリズムは複数あり、undupは返り値の性質が数学的にあまり嬉しくないと感じたため、本記事では改良した関数を考えます。
ソースはこちらです。
undup関数とは
型T:eqTypeにおけるリストの重複を削除するundup関数は以下のように定義されています。
Variable (T:eqType).
Fixpoint undup (s:seq T) :=
if s is x :: s' then if x \in s' then undup s' else x :: undup s' else [::].
要約すると、リストsの先頭要素xに対し、xが後ろs'に含まれている場合はxを取り除き、含まれていない場合はそのまま再帰します。
これにより、元のリストに同じ要素が複数含まれている場合はその最後の要素だけ残して削除していきます。
undup関数の性質
このように定義したundupは以下の性質を満たします。
Lemma undup_uniq s : uniq (undup s).
Lemma mem_undup s: undup s =i s.
1つ目は、undupの返り値には重複がないことを意味していて、2つ目は集合として等しい(=i)、つまりその構成要素に変化がないことを意味しています。
また、元の列の部分列であることも以下からわかります。
Lemma undup_subseq s : subseq (undup s) s.
しかしながら、このアルゴリズムではリストs中の要素xが初めて現れる順番(index x s)の順序が変化し、以下の性質を満たしません。
Lemma undup_leq_index x y s:
index x (undup s) <= index y (undup s) = (index x s <= index y s).
(* 一般に成り立たない *)
後述するように、任意のリストsに対して、この性質と上の3つの性質を満たすリストは一意に存在し、「リストの重複要素を削除する」ことに対する特徴付けができるのですが、残念ながらundupはこの性質を満たさず、証明する定理によってはリストの重複要素を削除する関数としてundup関数を使うのは好ましくない場合があります。
したがって、これら4つを満たすようなリストを返す新たな関数myundupを定義します。
undup関数を改良した関数myundup
undup関数を改良した関数myundupを定義する前に、関数mkallrelを定義します。
準備
型TとT上の二項関係Rとリストsに対して、sの部分列を返す関数mkallrelを以下に定義します。
Function mkallrel (R:rel T) (s:seq T) {measure size s} :=
if s is x :: s' then x :: mkallrel R (filter (R x) s') else [::].
Proof.
move => R s x s' _ /=. apply /leP.
by rewrite size_filter ltnS count_size.
Defined.
これは、特にT上の半順序Rに対し、Rが全順序になるようなsの部分列を1つ返す関数です。
具体的には、sの先頭要素xに対し、それとRで関係付くような要素のみを取り出した部分列filter (R x) s'に対して再帰します。
このアルゴリズムは再帰するリストが自明に小さくなっているわけではないので、Functionコマンドで定義します。
mkallrelの性質
関数mkallrelは以下の性質を満たします。
Lemma mkallrel_subseq R s :
subseq (mkallrel R s) s.
Lemma mkallrel_total R s x y :
subseq [:: x; y] (mkallrel R s) -> R x y.
1つ目は、元の列の部分列になることを表していて、
2つ目は、任意のmkallrel R s上の2つの要素x、yに対し、xがyよりも先頭にあるならばR x yが成り立つことを表しています。
myundupの定義
これを用いてmyundup関数を定義します。
Definition myundup := mkallrel xpredC1.
ここで、xpredC1 x y := y != xと定義されていることを考えると、先ほどの補題mkallrel_totalから、(myundup s)に重複がないことがわかります。
また、undupでは重複があった場合、先頭要素を削除していましたが、myundupの場合は先頭要素を残すので、要素がリスト中に初めて現れる順番indexの大小関係が変化しません。
ここから詳しくmyundupの性質を見ていきます。
myundupの性質
まず、このmyundupと元のundupとは以下の関係があります。
Lemma myundup_undup (s:seq T) : myundup s = rev (undup (rev s)).
つまり、myundupはsの逆列に対してundupをしたものの逆列になっています。
この補題によりundupに関する補題から以下の性質がすぐ示せます。
Lemma myundup_uniq (s:seq T) : uniq (myundup s).
Lemma mem_myundup (s:seq T) : myundup s =i s.
Lemma myundup_subseq (s:seq T) : subseq (myundup s) s.
また、undupでは一般に成立しない、要素の順序に関する以下の補題もmyundupにおいては示すことができます。
Lemma myundup_leq_index x y (s:seq T) :
index x (myundup s) <= index y (myundup s) = (index x s <= index y s).
この性質を考えると、以下のように「重複要素を削除したリスト」に対して一位性が言えます。
重複要素を削除したリストの一意性と存在性
「重複要素を削除したリスト」に関して、冒頭で記述した性質を仮定すると一意性が成り立ちます。
つまり、任意のリストs0に対し、以下を満たすリストsは一意性を満たすと言うことです。
uniq s-
s =i s0、 forall x y, index x s <= index y s = (index x s0 <= index y s0)
(冒頭では4つの性質を紹介しましたが、一意性を言うためにはsubseq s s0を仮定する必要はないです。)
さらに、s0に対し、myundup s0はこれら全てを満たすため、以下の定理が証明できます。
Lemma myundup_uniqueness (s0 s:seq T) :
uniq s ->
s =i s0 ->
(forall x y, index x s <= index y s = (index x s0 <= index y s0)) ->
s = myundup s0.
この定理により、これらの性質を満たすリストの一意性のみならず、存在性も言えます。
一意性を満たすということは、「重複要素の削除」に対する1つの特徴付けができるということです。
まとめ
Coq/SSReflectに置いて、リストの重複要素を削除するundup関数を改良した関数myundupを定義し、これに関する性質を示しました。
myundup関数の返り値は「リストの重複要素を削除」を特徴付けし、undupにはない性質として、各要素が初めて現れる順序を保存することが分かりました。