Coq/SSReflectでリストの重複要素を削除するundup関数の返り値が性質として嬉しくないので改良する

# はじめに

CoqのSSReflectライブラリseq.vにおいて、リストの重複要素を削除する`undup`関数が定義されています。
しかしながら、一般にリストから重複要素を削除するアルゴリズムは複数あり、`undup`は返り値の性質が数学的にあまり嬉しくないと感じたため、本記事では改良した関数を考えます。

ソースは[こちら](https://github.com/nekonistyle/Qiita_example/blob/main/undup/undup.v)です。

# `undup`関数とは

型`T:eqType`におけるリストの重複を削除する`undup`関数は以下のように定義されています。

```coq
  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`は以下の性質を満たします。

```coq
  Lemma undup_uniq s : uniq (undup s).

  Lemma mem_undup s: undup s =i s.
```

1つ目は、`undup`の返り値には重複がないことを意味していて、2つ目は集合として等しい(`=i`)、つまりその構成要素に変化がないことを意味しています。

また、元の列の部分列であることも以下からわかります。
```coq
  Lemma undup_subseq s : subseq (undup s) s.
```

しかしながら、このアルゴリズムではリスト`s`中の要素`x`が初めて現れる順番`(index x s)`の順序が変化し、以下の性質を満たしません。

```coq
  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`を以下に定義します。

```coq
  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`は以下の性質を満たします。

```coq
  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`関数を定義します。

```coq
  Definition myundup := mkallrel xpredC1.
```

ここで、`xpredC1 x y := y != x`と定義されていることを考えると、先ほどの補題`mkallrel_total`から、`(myundup s)`に重複がないことがわかります。

また、`undup`では重複があった場合、先頭要素を削除していましたが、`myundup`の場合は先頭要素を残すので、要素がリスト中に初めて現れる順番`index`の大小関係が変化しません。

ここから詳しく`myundup`の性質を見ていきます。


## `myundup`の性質

まず、この`myundup`と元の`undup`とは以下の関係があります。

```coq
  Lemma myundup_undup (s:seq T) : myundup s = rev (undup (rev s)).
```

つまり、`myundup`は`s`の逆列に対して`undup`をしたものの逆列になっています。
この補題により`undup`に関する補題から以下の性質がすぐ示せます。

```coq
  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`においては示すことができます。

```coq
  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`はこれら全てを満たすため、以下の定理が証明できます。

```coq
  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`にはない性質として、各要素が初めて現れる順序を保存することが分かりました。