置換を最小の互換の列に変換する関数の健全性、最小性をCoq/SSReflectで証明する(2024年TPPmark問1,2の解答)

# はじめに

[2024年TPPmarkの問題](https://www.math.nagoya-u.ac.jp/~garrigue/tpp2024/)の問1,2におけるCoq/SSReflectによる解答の解説をします。

問題は以下の通りです。

> 今年のTPPmarkは互換による整列をテーマにしています．この場合，整列のコ ストは比較の数ではなく，整列するのに必要な互換の数です．
> 例えば，リスト [5, 9, 1, 3, 7] を整列するには，すなわちリスト [1, 3, 5, 7, 9] に変えるには，3つの互換を適用すればいい．まず位置1と3を交換し， 次に2と4を交換し，しまいに4と5を交換すればいい(ただし位置を1から数えた 場合)． 別の見方をすれば，置換 [1 → 3, 2 → 5, 3 → 1, 4 → 2, 5 → 4] を適用する必要がある．線形代数の講義を思い出すと，置換はまず循環に分解 できる．ここでは (1 3) と (2 5 4) である (循環内に各位置が次のものにな り，最後の位置が最初のものになる)．そして循環がまた互換に分解される． 長さmの循環が(m-1)互換で実現できるので，最適なアルゴリズムが (要素の数 - 循環の数) 個の互換で整列を完成させる．

> タスクは以下のとおりである．

> 1, 置換をその置換を実現する最小の互換の列に変換する関数を書きなさい．
> 2, この関数の正しさ，そして列の最小性を証明せよ． この際，置換に関する理論が必要だろう．
> 3, 重複のない自然数のリストを与えられたら，それを整列する最小の互換列を返す関数 を書きなさい．正しさと列の最小性を証明せよ．
> 4, 重複のありうる自然数のリストを与えられたら，それを整列する最小の互換列を返す関数 を書きなさい．正しさと列の最小性を証明せよ．
> 位置を0から始めてもよい．

これの問1,2に関する解答を解説します。

私の解答のソースは[こちら](https://github.com/nekonistyle/Qiita_example/blob/main/TPPmark2024/tppmark2024.v)


# 置換に関するライブラリperm.v

mathcompには置換に関するライブラリ[perm.v](https://math-comp.github.io/htmldoc_2_2_0/mathcomp.fingroup.perm.html)があります。

ここで利用する主な関数が`porbit`と`tperm`です。

### `porbit`

`porbit`は有限集合`T:finType`における置換`p:{perm T}`と`x:T`に対し、`porbit p x`が$< x >_p := \\{ p^n x \mid n \in \mathbb{N} \\}$つまり`x`の`p`における軌跡を表しています。

この有限列が`traject p x #|porbit p x|`であり、これらの性質が以下の定理に表れています。

```coq:perm.v
Lemma porbit_traject s x : porbit s x =i traject s x #|porbit s x|.

Lemma porbitP s x y :
  reflect (∃ i, y = (s ^+ i) x) (y \in porbit s x).
```

### `tperm`

有限集合`T:finType`とその要素`x y:T`に対し、`tperm x y : {perm T}`が互換$(x,y)$になります。

ここでよく使う定理は以下の3つと

```coq:perm.v
Lemma tpermL x y : tperm x y x = y.

Lemma tpermR x y : tperm x y y = x.

Lemma tpermD x y z : x != z → y != z → tperm x y z = z.
```

`ifP`のように、ゴールに`tperm x y z`が出てきた時に場合分けできるようにした`tpermP`です。

```coq:perm.v
Variant tperm_spec x y z : T → Type :=
  | TpermFirst of z = x : tperm_spec x y z y
  | TpermSecond of z = y : tperm_spec x y z x
  | TpermNone of z <> x & z <> y : tperm_spec x y z z.

Lemma tpermP x y z : tperm_spec x y z (tperm x y z).
```


# perm.vにはない置換に関する汎用的な定理

上記のperm.vだと置換に関する定理が足りないので、重要な定理だけ先に示しておきます。

### `porbit p x`が1点集合の場合

```coq
  Lemma porbit_card1P (p: {perm T}) (x:T):
    reflect (#|porbit p x| = 1) (p x == x).
```

```coq
  Lemma mem_porbit_card1P (p: {perm T}) (x:T):
    p x == x -> forall (y:T), reflect (y = x) (y \in porbit p x).
```

### `x:T`の`p:{perm T}`における位数の性質

```coq
  Lemma porbit_iter (p: {perm T}) (x:T) (n:nat):
    iter n p x = x -> exists k, n = k * #|porbit p x|.
```

ここでは`iter`表記ですが、以下の補題が既に示されています。

```coq:perm.v
Lemma permX s x n : (s ^+ n) x = iter n s x.
```

また、次のperm.vの定理は実は最小性を満たさないので、再証明します。

```coq:perm.v
Lemma porbitPmin s x y :
  y \in porbit s x → exists2 i, i < #[s] & y = (s ^+ i) x.
  (* `i` is not always minimam *)
```

この命題のように`s`の位数ではなく、次のように`x`の`s`における位数で抑えるのが最小値になります。

```coq
  Lemma my_porbitPmin' (p: {perm T}) (x y:T):
    y \in porbit p x -> exists2 i, i < #|porbit p x| & y = (p ^+ i)%g x.
```

その最小性も次の定理からわかります。

```coq
  Lemma my_porbitPmin (p: {perm T}) (x y:T):
    y \in porbit p x ->
          exists2 i,
          i < #|porbit p x| /\ (forall k, k < i -> (p ^+ k)%g x != y)
                            & y = (p ^+ i)%g x.
```

### `porbit p`による分割

もう一つ重要な性質は、`porbit p`は`T`における同値類を定義できるという性質です。
特に、異なる`porbit p x`と`porbit p y`には共通部分を持たないことを示しておきます。

```coq
  Lemma porbit_disjointP (p: {perm T}) (x y:T):
    reflect [disjoint (porbit p x) & (porbit p y)] (y \notin porbit p x).
```


# 問1 置換から互換の列への変換関数

有限集合`T:finType`を固定します。
まず、置換`p:{perm T}`から循環の列へ変換関数を定義します。

## 置換から循環の列への変換

循環`[:: x_0; ...; x_n]`は任意の`i`に対し`x_i`から`x_{i+1}`へ, `x_n`から`x_0`への変換を表しています。

ここで定義する関数`fromperm`の型は`{perm T} -> seq (seq T)`になります。

任意の`x:T`に対し、`traject p x #|porbit p x|`は`x`の`p`における軌跡が1つの循環になります。
この軌跡を任意の`x:T`に対して`rot`したものを同一視して集めてきたものが出力として欲しい循環の列になります。
ここで、任意の`x y:T`に対して`y \in traject p x #|porbit p x|`と`exists n, traject p x #|porbit p x| = rot n (traject p y #|porbit p y|)`が同値になることがポイントです。
私は以下のような定義にしました。

```coq
  (* perm -> cycles *)
  Fixpoint fromperm_rec (p: {perm T}) (r:seq (seq T)) (s:seq T) :
    seq (seq T) :=
    if s is x :: s'
    then if has (mem^~ x) r then fromperm_rec p r s'
         else if p x == x then fromperm_rec p r s'
              else fromperm_rec p (traject p x #|porbit p x| :: r) s'
    else r.

  Definition fromperm (p: {perm T}) : seq (seq T) :=
    fromperm_rec p [::] (enum T).
```

補助関数`fromperm_rec`の第二引数`r:seq (seq T)`は今まで作った軌跡のリストを保存しておく引数になります。
また、長さ1の軌跡を残しておく必要がないので、これも削除します。


### 循環の列への変換の健全性

`fromperm`の健全性を見るためにこれを置換に戻す関数`toperm : seq (seq T) -> {perm T}`を定義します。

ここで、以下の定理から分かる通り、**perm.vでは互換は先頭から処理していく**という仕様になっているため、通常の数学の表記で互換の後ろから処理するのと逆順になることに注意してください。

```coq:perm.v
Lemma permM s t x : (s × t) x = t (s x).
```


まずは1つの循環から互換の列へ変換してそこから置換に変換する関数`toperm1`を作っていきます。

```coq
  Fixpoint toperm1_rec (x0:T) (s:seq T) : {perm T} :=
    if s is x :: s' then tperm x0 x * toperm1_rec x0 s' else 1.

  Fixpoint toperm1 (s:seq T) : {perm T} :=
    if s is x0 :: s' then toperm1_rec x0 s' else 1.
```

循環`[:: x_0; ...; x_n]`はCoqの定義における計算順序を考慮すると`tperm x_0 x_1 * tperm x_0 x_2 * ... * tperm x_0 x_n`という互換の積で表せるので、このような定義になっています。
しかしながら後の`traject`に関する性質の証明で隣り合う要素同士の互換の方が扱いやすいので、次の定義を使います。(`traject p x n.+1 = [:: x_0; ...; x_n]`のとき、任意の`i`に対して`x_{i+1} = p x_i`を満たす)

```coq
  Fixpoint irtoperm1_rec (x0:T) (s:seq T) : {perm T} :=
    if s is x :: s' then irtoperm1_rec x s' * tperm x0 x else 1.

  Fixpoint irtoperm1 (s:seq T) : {perm T} :=
    if s is x0 :: s' then irtoperm1_rec x0 s' else 1.
```

これは循環循環`[:: x_0; ...; x_n]`を`tperm x_{n-1} x_n * ... * tperm x_0 x_1`に変換した形になります。

これは入力`s`が`uniq`ならば元の`toperm1`と一致します。

```coq
  Lemma toperm1_irtoperm1 (s:seq T):
    uniq s -> toperm1 s = irtoperm1 s.
```

これらを循環の列に対して変換する関数が以下の`toperm`や`irtoperm`です。

```coq
  Definition toperm (s:seq (seq T)) : {perm T} :=
    foldr (mulg \o toperm1) 1%g s.
  Definition irtoperm (s:seq (seq T)) : {perm T} :=
    foldr (mulg \o irtoperm1) 1%g s.
```

### `fromperm`の健全性の証明

この`toperm`を用いると次の性質が成り立ちます。

```coq
  Lemma toperm_fromperm : cancel fromperm toperm.
```


## 置換から互換の列への変換

まず、与えられた列が互換の列になっていることを示す命題を作ります。

```coq
  Definition istperm : pred {perm T} :=
    fun p => [exists x, [exists y, p == tperm x y]].

  Definition isexchanges : pred (seq {perm T}) := all istperm.
```

上の`fromperm`を用いると置換から循環に変換できるので、これを互換の列に変換する関数`toexchanges : seq (seq T) -> seq {perm T}`を以下に定義します。

```coq
Fixpoint toexchanges1_rec (x0:T) (s:seq T) : seq {perm T} :=
    if s is x :: s' then tperm x0 x :: toexchanges1_rec x0 s' else [::].

  Definition toexchanges1 (s:seq T) : seq {perm T} :=
    if s is x0 :: s' then toexchanges1_rec x0 s' else [::].

  Definition toexchanges (s:seq (seq T)) : seq {perm T} :=
    flatten (map toexchanges1 s).
```

特に`toexchanges_rec`は上の`toperm1_rec`とほぼ同じで、演算子が`::`か`*`かの違いになっています。

つまり以下の定理がすぐ示せます。

```coq
  Lemma toexchanges_toperm (s:seq (seq T)):
    toperm s = foldr mulg 1%g (toexchanges s).
```

もちろん、`toexchanges`の出力が全て`tperm`の形で書けることもすぐわかります。

```coq
  Lemma toexchange_isexchanges (s:seq (seq T)):
    isexchanges (toexchanges s).
```

そこで、置換から互換の列への変換は`toexchanges \o fromperm`で定義できます。


# 問2 問1の関数の健全性、最小性

`toexchanges \o fromperm`の健全性はその定義からすぐ示せます。


## 健全性

まず、この関数が互換の列を返すことは以下よりすぐ分かります。

```coq
  (* toexchanges \o fromperm is valid *)
  Lemma toexchange_fromperm_isexchanges (p: {perm T}):
    isexchanges (toexchanges (fromperm p)).
  Proof.
    exact /toexchange_isexchanges.
  Qed.
```

健全性も`fromperm`の健全性からすぐ示せます。

```coq
  (* soundness of toexchanges \o fromperm *)
  Lemma toexchanges_fromperm: cancel (toexchanges \o fromperm) (foldr mulg 1%g).
  Proof.
    move => p /=. by rewrite -toexchanges_toperm toperm_fromperm.
  Qed.
```


## 最小性

まず、置換`p:{perm T}`に対して、あるノルム`permnorm : {perm T} -> nat`を定義します。

```coq
  Definition permnorm (p: {perm T}): nat :=
    \sum_(x <- fromperm p) (size x).-1.
```

実はこれが求めたい最小値になっています。

```coq
  Lemma permnorm_size_toexchanges (p: {perm T}):
    permnorm p = size (toexchanges (fromperm p)).
```

そして、最終的に求めたい命題は以下の通りです。

```coq
  Lemma toexchanges_min (p: {perm T}) (s:seq {perm T}):
    isexchanges s -> foldr mulg 1%g s = p ->
    size (toexchanges (fromperm p)) <= size s.
```

今、`size (toexchanges (fromperm p)) = permnorm p`であり、次の命題
を示すことができれば、リスト`s`の帰納法で、上の命題を示すことができます。

```coq
  Lemma permnorm_tperm (p: {perm T}) (x y:T):
    permnorm p <= (permnorm (tperm x y * p)).+1.
```

ですので、この`permnorm_perm`を示すのが目標です。
そのためには`tperm x y * p`に関する性質を示していきます。


### `tperm x y * p`に関する性質

`permnorm`は`fromperm`で定義されており、その返り値は全て`traject p x #|porbit p x|`の形になっています。最終的にはこの`size`を求めるのですが、
`size (traject p x #|porbit p x|) = #|porbit p x|`より、`porbit`に関する性質を示せばいいです。

そこで`porbit (tperm x y * p)`と`porbit p`の間の関係を示していきます。

ここで重要になるのは以下の2つの定理です。

```coq
  Lemma porbit_tperm_notin (p: {perm T}) (x y:T):
    y \notin porbit p x ->
    porbit (tperm x y * p)%g x = porbit p x :|: porbit p y.
```

```coq
  Lemma porbit_tperm_in (p: {perm T}) (x y:T):
    y \in porbit p x ->
          porbit (tperm x y * p)%g x :|: porbit (tperm x y * p) y = porbit p x.
```

ここで`:|:`は集合の和を表しています。

この和集合の濃度ですが、どちらも上で示した

```coq
  Lemma porbit_disjointP (p: {perm T}) (x y:T):
    reflect [disjoint (porbit p x) & (porbit p y)] (y \notin porbit p x).
```

より`disjoint`であることが分かるので、この和集合の濃度は元の濃度の和になります。


これさえ示れば、以下の性質が示せます。

```coq
  Lemma permnorm_tperm_notin (p: {perm T}) (x y:T):
    y \notin porbit p x -> (permnorm p).+1 = permnorm (tperm x y * p).
```

```coq
  Lemma permnorm_tperm_in (p: {perm T}) (x y:T):
    y != x -> y \in porbit p x -> permnorm p = (permnorm (tperm x y * p)).+1.
```

この2つから最初に欲しかった

```coq
  Lemma permnorm_tperm (p: {perm T}) (x y:T):
    permnorm p <= (permnorm (tperm x y * p)).+1.
```

が示せます。


# まとめ

2024年のTPPmarkの問題の問1,2について解説しました。