はじめに
2024年TPPmarkの問題の問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に関する解答を解説します。
私の解答のソースはこちら
置換に関するライブラリperm.v
mathcompには置換に関するライブラリperm.vがあります。
ここで利用する主な関数が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|であり、これらの性質が以下の定理に表れています。
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つと
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です。
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点集合の場合
Lemma porbit_card1P (p: {perm T}) (x:T):
reflect (#|porbit p x| = 1) (p x == x).
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}における位数の性質
Lemma porbit_iter (p: {perm T}) (x:T) (n:nat):
iter n p x = x -> exists k, n = k * #|porbit p x|.
ここではiter表記ですが、以下の補題が既に示されています。
Lemma permX s x n : (s ^+ n) x = iter n s x.
また、次の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における位数で抑えるのが最小値になります。
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.
その最小性も次の定理からわかります。
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には共通部分を持たないことを示しておきます。
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|)が同値になることがポイントです。
私は以下のような定義にしました。
(* 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では互換は先頭から処理していくという仕様になっているため、通常の数学の表記で互換の後ろから処理するのと逆順になることに注意してください。
Lemma permM s t x : (s × t) x = t (s x).
まずは1つの循環から互換の列へ変換してそこから置換に変換する関数toperm1を作っていきます。
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を満たす)
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と一致します。
Lemma toperm1_irtoperm1 (s:seq T):
uniq s -> toperm1 s = irtoperm1 s.
これらを循環の列に対して変換する関数が以下のtopermやirtopermです。
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を用いると次の性質が成り立ちます。
Lemma toperm_fromperm : cancel fromperm toperm.
置換から互換の列への変換
まず、与えられた列が互換の列になっていることを示す命題を作ります。
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}を以下に定義します。
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とほぼ同じで、演算子が::か*かの違いになっています。
つまり以下の定理がすぐ示せます。
Lemma toexchanges_toperm (s:seq (seq T)):
toperm s = foldr mulg 1%g (toexchanges s).
もちろん、toexchangesの出力が全てtpermの形で書けることもすぐわかります。
Lemma toexchange_isexchanges (s:seq (seq T)):
isexchanges (toexchanges s).
そこで、置換から互換の列への変換はtoexchanges \o frompermで定義できます。
問2 問1の関数の健全性、最小性
toexchanges \o frompermの健全性はその定義からすぐ示せます。
健全性
まず、この関数が互換の列を返すことは以下よりすぐ分かります。
(* toexchanges \o fromperm is valid *)
Lemma toexchange_fromperm_isexchanges (p: {perm T}):
isexchanges (toexchanges (fromperm p)).
Proof.
exact /toexchange_isexchanges.
Qed.
健全性もfrompermの健全性からすぐ示せます。
(* 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を定義します。
Definition permnorm (p: {perm T}): nat :=
\sum_(x <- fromperm p) (size x).-1.
実はこれが求めたい最小値になっています。
Lemma permnorm_size_toexchanges (p: {perm T}):
permnorm p = size (toexchanges (fromperm p)).
そして、最終的に求めたい命題は以下の通りです。
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の帰納法で、上の命題を示すことができます。
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つの定理です。
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.
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.
ここで:|:は集合の和を表しています。
この和集合の濃度ですが、どちらも上で示した
Lemma porbit_disjointP (p: {perm T}) (x y:T):
reflect [disjoint (porbit p x) & (porbit p y)] (y \notin porbit p x).
よりdisjointであることが分かるので、この和集合の濃度は元の濃度の和になります。
これさえ示れば、以下の性質が示せます。
Lemma permnorm_tperm_notin (p: {perm T}) (x y:T):
y \notin porbit p x -> (permnorm p).+1 = permnorm (tperm x y * p).
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つから最初に欲しかった
Lemma permnorm_tperm (p: {perm T}) (x y:T):
permnorm p <= (permnorm (tperm x y * p)).+1.
が示せます。
まとめ
2024年のTPPmarkの問題の問1,2について解説しました。