チェシャ猫の消滅定理

数学にプログラミング、素敵なもの何もかも。

Coq でクイックソート (1)

以前の記事「Coq で filter 関数」の最後にちょっと触れた通り、Coq でクイックソートを扱ってみます。ひとつの記事にすると長くなりそうなので、全 3 回に分割してみました。

  1. アルゴリズムの定義 (この記事)
  2. 仕様の検証その 1
  3. 仕様の検証その 2

ちなみに、今回の分のコードは https://gist.github.com/4526374 に置いてあります。使い古されたネタではありますが、もしよろしければしばしお付き合いを。

おなじみのアルゴリズム

今更ですが、アルゴリズムの復習から始めましょう。深く考えずにクイックソートを書き下すと次のようになります。

Fixpoint qsort (l : list nat) : list nat :=
    match l with
    | nil     => nil
    | n :: l' => let lts := antifilter (leb n) l' in
                 let ges := filter (leb n) l' in
                 (qsort lts) ++ n :: (qsort ges)
    end.

前も使いましたが、antifilter は、filter と逆の (つまり false になる要素の) 抽出を行う関数として定義してあります。ここで言えば、ピボット n に対して、lts として n より小さい要素、ges として n 以上の要素が抽出されるわけです。

しかしこのコードを読み込むと、

Error:
Recursive definition of qsort is ill-formed.

と怒られてしまいます。Coq には qsort の再帰呼び出しが有限回で停止することが理解できないからです。

そこで、リストの長さが短くなっていることを明示的に教えてやりましょう。Recdef モジュールをインポートしておいて、Function コマンドで定義します。

Function qsort (l : list nat) {measure length} : list nat :=
    match l with
    | nil     => nil
    | n :: l' => let lts := antifilter (leb n) l' in
                 let ges := filter (leb n) l' in
                 (qsort lts) ++ n :: (qsort ges)
    end.

これで怒られることはなくなりましたが、その代わりリストの長さが短くなることの証明が必要です。filter 関数の検証の際に使った補題が役に立ちそうですね。

Lemma filter_sublist : forall (f : A -> bool) (l : list A),
                       sublist (filter f l) l.

Lemma antifilter_sublist : forall (f : A -> bool) (l : list A),
                           sublist (antifilter f l) l.

Lemma sublist_length : forall l1 l2 : list A,
                       sublist l1 l2 ->
                       (l1 = l2 \/ length l1 < length l2).

ソートがソートであるために

上で定義した qsort に対して、仕様の検証を行うのが今回のネタの最終目的です。 wikipedia:ソート にも書いてある通り、ソート関数の仕様として次の性質を要求します。

  1. 出力は昇順になっている。
  2. 出力は入力の置換になっている。

準備がよいことに、これらの性質は標準ライブラリ Sorting モジュールに既に準備されています。こいつを使ってやりましょう。

Inductive Sorted (A : Type) (R : A -> A -> Prop) : list A -> Prop :=
    Sorted_nil : Sorted R nil
  | Sorted_cons : forall (a : A) (l : list A),
                  Sorted R l -> HdRel R a l -> Sorted R (a :: l)

Inductive Permutation (A : Type) : list A -> list A -> Prop :=
    perm_nil : Permutation nil nil
  | perm_skip : forall (x : A) (l l' : list A),
                Permutation l l' -> Permutation (x :: l) (x :: l')
  | perm_swap : forall (x y : A) (l : list A),
                Permutation (y :: x :: l) (x :: y :: l)
  | perm_trans : forall l l' l'' : list A,
                 Permutation l l' -> Permutation l' l'' -> Permutation l l''

ちなみに有名チュートリアル プログラミング Coq では整列性の定義として、Sorted ではなく LocallySorted の方を採用しています。補題 Sorted_LocallySorted_iff によってこれら二つの性質は同値なので問題は無いはずです。

その他補足

今回は nat 型のリストに対してしか定義していないのであまり関係がありませんが、ここで定義した qsort は安定ソートになっています。「Coq で filter 関数」でも「順序を維持したままマージしたもの」という表現が出てきましたね。その代わりと言ってはなんですが、常に左端の値をピボットとして取るため、入力が整列済みの場合に計算量は最悪 O(n^2) になります。

次回はまず仕様その 1 として qsort の出力が整列していることを証明する予定です。この証明では functional induction が威力を発揮するのですが、それはまた別の話。

Coq で位相空間

前々回の記事「Coq でモジュラー束」で「群 G の部分群を述語 G -> Prop で表す」という方針を採用したところ、割と上手くいくということがわかりました。今回は他の題材として、「連結集合の連続写像による像は連結」であることを、同じ方針により証明してみます。大学の学部で習う定番問題ですね。証明付きの完全なコードは https://gist.github.com/4466805 です。

とりあえず概念を準備しよう

位相空間

「X の部分集合」の型をいちいち X -> Prop の形で書くと冗長になるため、シノニムを付けておきます。

Definition Subset (X : Set) : Type := X -> Prop.

また、開集合系の公理を記述するために必要な、X 自身、空集合、共通部分、和集合をそれぞれ定義しておきましょう。ここで、(X の) 空集合として

Definition empty (X : Set) : Subset X := fun (x : X) => x <> x.

としました。任意の x : X に対して ~ x <> x が成立することは、等号の反射性 eq_refl を用いて容易に示すことができます。また、開集合系の公理として「任意個の開集合の和集合」を表現する必要があるため、任意の添字付けに対する共通部分 bigcap と和集合 bigcup を先に定義しておき、2 個の場合 intsec と union はその特殊な場合として表しています。bigcap は今回は使い途がありませんでしたが。

以上を踏まえて、X が 位相 Open を備えた位相空間であることを、次のように表しました。

Class TopSpace (X : Set) (Open : Subset X -> Prop) := {
    TS_whole :
        Open (whole X);
    TS_empty :
        Open (empty X);
    TS_intsec :
        forall U1 U2 : Subset X,
        Open U1 -> Open U2 ->
        Open (intsec U1 U2);
    TS_union :
        forall (I : Set) (index : I -> Subset X),
        (forall i : I, Open (index i)) ->
        Open (bigcup I index)
}.
連続写像

逆像 preimage を用いて連続写像の定義を書きます。「任意の開集合の逆像が開なら連続」というやつですね。特に問題はなく、至って教科書通り。

Definition preimage {X Y : Set}
                    (f : X -> Y) (V : Subset Y) : Subset X :=
    fun (x : X) => V (f x).

Class Continuous (X : Set) (XOpen : Subset X -> Prop)
                 (Y : Set) (YOpen : Subset Y -> Prop)
                 (f : X -> Y) := {
    Conti_TopSpace_l :>
        TopSpace X XOpen;
    Conti_TopSpace_r :>
        TopSpace Y YOpen;
    Conti_preim :
        forall V : Subset Y,
        YOpen V -> XOpen (preimage f V)
}.
連結集合

さて、今回の主題である連結集合の定義です。

Class Connected (X : Set) (Open : Subset X -> Prop)
                (S : Subset X) := {
    Conn_TopSpace :>
        TopSpace X Open;
    Conn_insep :
        forall U1 U2 : Subset X,
        Open U1 -> Open U2 -> incl S (union U1 U2) ->
        (exists x1 : X, (intsec S U1) x1) ->
        (exists x2 : X, (intsec S U2) x2) ->
        exists x : X, intsec S (intsec U1 U2) x
}.

定義を書く上で、部分集合への所属を Prop で表現している関係上、否定 ~ の出現は避けたいところです。通常、連結空間の定義としては「S がふたつの (S の) 開集合の非交和として表せない」という言い回しが採用されることが多いですが、これを「S がふたつの開集合 U1 と U2 の和として表されればそれは非交和ではない」と表現することにして、さらに「共通部分が空でない」ことを「実際に元が存在する」として否定表現を回避してあります。

それから証明しよう

さて、本題の証明に入りましょう。(X, XOpen) と (Y, YOpen) を位相空間、f : X -> Y を連続写像とし、X の連結部分集合 U の像 f(U) の連結性を示します。

Variables X Y : Set.
Variable XOpen : Subset X -> Prop.
Variable YOpen : Subset Y -> Prop.
Hypothesis X_TopSpace : TopSpace X XOpen.
Hypothesis Y_TopSpace : TopSpace Y YOpen.
Variable f : X -> Y.
Hypothesis f_Continuous : Continuous X XOpen Y YOpen f.
Variable U : Subset X.
Hypothesis U_Connected : Connected X XOpen U.

Instance image_Connected : Connected Y YOpen (image f U).

ちなみに証明の中身は、次のような感じ。なんと言うか、特にひねったところもないスタンダードな証明です。

  1. V1 と V2 を、f(U) を覆う Y の開集合とする。
  2. U の連結性から、U と f^{-1} (V1) と f^{-1} (V2) の共通部分は空でなく、ここから元 x が取れる。実際、
    • f の連続性より f^{-1} (V1) と f^{-1} (V2) は開。
    • f(U) が V1 と V2 の和集合に含まれることから、U は f^{-1} (V1) と f^{-1} (V2) の和集合に含まれる。
    • f(U) と V1、V2 それぞれとの共通部分が空でないため、 U と f^{-1} (V1)、f^{-1} (V2) それぞれの共通部分も空でない。
  3. f(x) は f(U) と V1 と V2 の共通部分に属する。よってこの共通部分は空でない。

その他補足

今回の題材、本当は「コンパクト集合の連続写像による像はコンパクト」を証明しようかと思ったのですが、残念ながら上記の定式化では有限交叉性が上手く表現できません。FSet モジュール辺りが有望でしょうか。いずれこちらのネタもやってみたいものですが、それはまた別の話。

Coq で filter 関数

リストの要素の内、条件に合致するものだけを抜き出す関数 filter の仕様を Coq で証明してみました。元ネタは『ソフトウェアの基礎』の練習問題。完全なコードは https://gist.github.com/4401408 に置いてあります。

とりあえず定義の確認

List モジュールにある filter の定義を確認してみると、次のようになっています。

filter = 
fun (A : Type) (f : A -> bool) =>
fix filter (l : list A) : list A :=
      match l with
      | nil => nil
      | x :: l0 => if f x then x :: filter l0 else filter l0
      end.

要するにリストの要素を先頭から見ていって、条件 f が成り立つときだけ戻り値に反映させているわけです。実際、NPeano モジュールにある even : nat -> bool で試してみると、

Eval compute in filter even (2 :: 7 :: 3 :: 6 :: 1 :: nil).

= 2 :: 6 :: nil
: list nat

となり、確かに期待通りの動作をしていることがわかります。

さて、この filter 関数の仕様として、『ソフトウェアの基礎』では次の二種類が挙げられています。

集合 X と関数 test: X -> bool、リスト l とその型 list X を想定する。 さらに、l が二つのリスト l1 と l2 が順序を維持したままマージされたもので、 リスト l1 の要素はすべて test を満たし、 l2 の要素はすべて満たさないとすると、filter test l = l1 が成り立つ。

test の結果が true なる要素だけでできた、リスト l の すべての部分リストの中で、filter test l が最も長いリストである。

この二つを形式的に記述し、証明することを今回の目標としましょう。

なお、毎回 X と test を引数として書くのは面倒なので、これらは Variable であらかじめ宣言しておきます。

仕様の記述と filter 関数の検証

仕様その 1

一つ目の定式化から行きましょう。まず「l が二つのリスト l1 と l2 を順序を維持したままマージしたものである」ことの定義を帰納的に記述します。

Inductive merger : list X -> list X -> list X -> Prop :=
    | Merger_nil_l  : forall l : list X,
                      merger l nil l
    | Merger_nil_r  : forall l : list X,
                      merger l l nil
    | Merger_cons_l : forall (x : X) (l l1 l2 : list X),
                      merger l l1 l2 ->
                      merger (x :: l) (x :: l1) l2
    | Merger_cons_r : forall (x : X) (l l1 l2 : list X),
                      merger l l1 l2 ->
                      merger (x :: l) l1 (x :: l2).

これですべてのパターンを網羅していることになるはず。さらにこれを用いて filter が満たすべき条件を記述します。

Theorem filter_challenge : forall l l1 l2 : list X,
                           let T := fun x => test x = true  in
                           let F := fun x => test x = false in
                           merger l l1 l2 -> all T l1 -> all F l2 ->
                           filter test l = l1.

all P l は「リスト l のすべての要素が P : Prop を満たす」を意味する述語です。この部分はbool 型のまま forallb を用いて扱う手もあったのですが、もう書いてしまったのでよしとしましょう。

証明そのものは特に難しいところはないです。上に挙げた証明は似たような部分が多いので、もしかすると順番を工夫すればもっと完結にまとまるかもしれませんね。

仕様その 2

さて、二つ目。いくつか補題を用意する関係上、こちらの方が分量としては長くなりました。まず「l1 は l2 の部分リストである」ことを定義しておきます。

Inductive sublist : list X -> list X -> Prop := 
    | Sublist_nil   : forall l : list X,
                      sublist nil l
    | Sublist_cons1 : forall (x : X) (l1 l2 : list X),
                      sublist l1 l2 ->
                      sublist l1 (x :: l2)
    | Sublist_cons2 : forall (x : X) (l1 l2 : list X),
                      sublist l1 l2 ->
                      sublist (x :: l1) (x :: l2).

ちなみに書き終わった後で気がつきましたが、実はこの述語は前章で subseq として登場済みでした。今更です。そしてこれを用いた filter の仕様は以下。

Theorem filter_challenge_2 : forall l : list X,
                             let T := fun x => test x = true in
                             all T (filter test l) /\
                             sublist (filter test l) l /\
                             (forall l0 : list X,
                              all T l0 -> sublist l0 l ->
                              (l0 = filter test l \/
                               length l0 < length (filter test l))).

問題文を見てみると「filter test l が最も長い」という言い回しになっていますが、これはちょっと解釈が微妙。つまり、「長さが最大値を取る」ことだけなら length l0 <= length (filter test l) でよい (つまり、同じ長さの l0 が他にあってもよい) のですが、直感的には「すべての要素が test に対して true を返す最長の部分リスト」がただ一つしかないのは明らかです。今回は後者を採用しています。

リストの長さを直接扱うと証明が複雑になりすぎるので、「部分リストである」という関係を基本にして、次の補題を使うことで長さに関する結論を得ています。

Lemma sublist_length : forall l1 l2 : list X,
                       sublist l1 l2 ->
                       (l1 = l2 \/ length l1 < length l2).

仕様の検証

おそらく想定された解答はここまでだと思うのですが、今回はもう少し先まで進んでみましょうか。

ここまでの議論では、filter が仕様を満たすことは検証されていますが、その仕様が filter の挙動をすべて表現している保証がありません。このことは例えば、「戻り値のリストの長さが引数のリスト以下」のような性質を考えてみればわかります。filter は当然この性質を満たしますが、これを満たす関数はそれこそいくらでも構成できますね？ そこでさらに追加として、「ここで記述された仕様を満たすものは filter に限る」ことを示してみます。

仕様その 1

邪魔にならないように Section を改め、仕様その 1 を満たすような関数 f1 を宣言しておきます。

Variable f1 : list X -> list X.
Hypothesis f1_challenge : forall l l1 l2 : list X,
                          let T := fun x => test x = true  in
                          let F := fun x => test x = false in
                          merger l l1 l2 -> all T l1 -> all F l2 ->
                          f1 l = l1.

この条件だけで f1 が filter と等しいことが言えればよいわけです。

Theorem spec1_valid : forall l : list X, f1 l = filter test l.

多少トリッキーなのは、filter と逆の抽出を行う関数 antifilter を定義していること。f1 の性質について結論部分に登場するのは l1 だけなので、l から l2 に当たる部分を抽出する関数を準備しておかないと証明が進まなくなってしまいます。

Fixpoint antifilter (f : X -> bool) (l : list X) : list X :=
    match l with
    | nil => nil
    | x :: l' => if test x
                     then antifilter f l'
                     else x :: antifilter f l'
    end.

ちなみに当初の方針では、test x が false のとき true になるような antitest : X -> bool を定義していたのですが、この方法だと bool 値を反転させる関数 negb が必要になるせいで取り回しに難があるようです。

仕様その 2

f2 l と filter test l が長さについて両向きの不等号が成立することを用いて等号を示します。最大値の一意性を証明する際の常套手段ですね。これ以外にも、両向きに sublist 関係が成り立つから、という議論もできるはず。

Variable f2 : list X -> list X.
Hypothesis f2_challenge : forall l : list X,
                          let T := fun x => test x = true in
                          all T (f2 l) /\ sublist (f2 l) l /\
                          (forall l0 : list X,
                           all T l0 -> sublist l0 l ->
                           (l0 = f2 l \/
                            length l0 < length (f2 l))).

Theorem spec2_valid : forall l : list X, f2 l = filter test l.

その他補足

今回「filter と f1 や f2 が同じ関数であること」を、同じ戻り値を返すこと、いわゆる外延性によって定義しましたが、これはちょっと微妙に感じるかもしれません。実際、この意味ではすべてのソートは区別できないことになってしまい、あまりにも雑すぎるというもの。しかしまあ深入りすると危険な気がするので、プログラムの同値性についての話はこれ以上立ち入らないことにしておきましょう。

ちなみに以上の filter の検証、今後これを用いてクイックソートの検証をしようという予定があったりなかったりするのですが、それはまた別の話。

Coq でモジュラー束

この記事は LL/ML Advent Calendar の 23 日目です。

「タイトルに "LL" もしくは "ML" を含むこと」という謎ルールに従い、「群の正規部分群の全体がモジュラー束 (Modular Lattices) をなすこと」を Coq により証明してみました。なお、完全なコードは http://gist.github.com/4359976 に置いてあります。

モジュラー束を表す型クラス

数学的な定義をいちいち説明するのもアレなので wikipedia:束_(代数学) を参照。モジュラー束は分配束の条件を若干緩めたもので、今回の例は「分配性を満たさないがモジュラー性なら満たす」ような例になっています。問題はどうやって Coq で書くかですが、ちょうど Coq で群を扱う記事 Group on Setoid を見かけたので、今回はこの方を真似して「型クラス + Setoid」で書いてみました。

まずモジュラー性を要求しない、通常の束はこんな感じ。Wikipedia の表現で言えば、sup が「結び」、inf が「交わり」ですね。台となる型 L は同値関係 eq によって Setoid にする予定なので、well-definedness (L_sup_mor、L_inf_mor) も忘れずに入れておきます。ちなみに POSet は部分順序集合の型クラスです。

Class Lattice (L : Type) (eq : L -> L -> Prop)
              (le : L -> L -> Prop)
              (sup : L -> L -> L) (inf : L -> L -> L) := {
    L_POSset :>
        POSet L eq le;
    L_sup_mor :
        forall x x' : L, eq x x' ->
        forall y y' : L, eq y y' ->
        eq (sup x y) (sup x' y');
    L_inf_mor :
        forall x x' : L, eq x x' ->
        forall y y' : L, eq y y' ->
        eq (inf x y) (inf x' y');
    L_sup_l :
        forall x y : L,
        le x (sup x y);
    L_sup_r :
        forall x y : L,
        le y (sup x y);
    L_sup_min :
        forall x y z : L,
        le x z -> le y z -> le (sup x y) z;
    L_inf_l :
        forall x y : L,
        le (inf x y) x;
    L_inf_r :
        forall x y : L,
        le (inf x y) y;
    L_inf_max :
        forall x y z : L,
        le z x -> le z y -> le z (inf x y)
}.

さらにそのサブクラスとしてモジュラー束を定義します。

Class ModularLattice (L : Type) (eq : L -> L -> Prop)
                     (le : L -> L -> Prop)
                     (sup : L -> L -> L) (inf : L -> L -> L) := {
    ML_Lattice :>
        Lattice L eq le sup inf;
    ML_mod :
        forall x y z : L,
        le x z -> eq (sup x (inf y z)) (inf (sup x y) z)
}.

これで、示したい結論は「群の正規部分群の全体は、型クラス ModularLattice のインスタンスとなること」と表現できました。さて、次の問題は「正規部分群」をどう書くか、です。

正規部分群を表す型クラス

まず前提として、G を群の型クラス Group のインスタンスにしておきます。台 G の上に同値関係 Geq が入っていて、Gop、Gunit、Ginv がそれぞれ群としての演算、単位元、逆元になっています。

Variable G : Type.
Variable Geq : G -> G -> Prop.
Variable Gop : G -> G -> G.
Variable Gunit : G.
Variable Ginv : G -> G.
Hypothesis G_Group : Group G Geq Gop Gunit Ginv.

さらにここで忘れちゃいけないのが、Gop、Ginv が Setoid としての Morphism になるということを Add Prametric Morphism で Coq に教えておくこと。面倒ですが、これをやっておかないと Setoid に対して rewrite タクティクが機能しません。

埋め込みによる方法

真っ先に思いつくのは、G の部分群 H を「群 H と H から G への単射準同型の組」として定義する方法です。しかし、最終的には G の正規部分群たちに同値関係を入れて Setoid にする必要があったことを思い出しましょう。この埋め込みによる方法では、「二つの部分群が等しい」と書きたいときにハマる予感がします。という訳でこの方針は却下。

特性関数による方法

そこで今回は、集合を型として直接扱うのではなく、それを表現する論理式と同一視して扱う方針を取ってみました。つまり、「G の元 x が正規部分群 N に属する」という述語 G -> Prop たちの全体にモジュラー束としての構造を入れます。

以下が対応する型クラスです。G が Setoid なので、同値関係 Geq に対する well-definedness (SS_mor) も忘れずに要求しておきます。正規部分群の定義については wikipedia:正規部分群 あたりをよろしく。

Class Subsetoid {X : Type} {eq : X -> X -> Prop}
                (S : X -> Prop) := {
    SS_mor :
        forall x x' : X,
        eq x x' -> (S x <-> S x')
}.

Class Subgroup {G : Type} {eq : G -> G -> Prop}
               {op : G -> G -> G} {unit : G} {inv : G -> G}
               (H : G -> Prop) := {
    SG_outer_Group :>
        Group G eq op unit inv;
    SG_Subsetoid :>
        @Subsetoid G eq H; 
    SG_unit_in :
        H unit;
    SG_op_clo :
        forall x y : G,
        H x -> H y -> H (op x y);
    SG_inv_clo :
        forall x : G,
        H x -> H (inv x)
}.

Class NormalSubgroup  {G : Type} {eq : G -> G -> Prop}
                      {op : G -> G -> G} {unit : G} {inv : G -> G}
                      (H : G -> Prop) := {
    NSG_Subgroup :>
        @Subgroup G eq op unit inv H;
    NSG_normal :
        forall x y : G,
        H x -> H (op (op y x) (inv y))
}.

ちなみに今回の証明には幸い登場しませんが、「x は N に属さない」という主張が必要になるとこの方針では詰むかもしれません。

束としての構造

さて、とりあえず準備はできました。最終的な台集合となる G の正規部分集合の全体 NSG を、依存積を使って書いておきます。

Definition CF : Type := G -> Prop.

Definition NSG : Type :=
    {N : CF | @NormalSubgroup G Geq Gop Gunit Ginv N}.

NSG 上の順序 NSGle は集合としての包含関係、交わり NSGinf は共通部分をとればよいのですが、注意が必要なのは結び NSGsup の定義。前述の Wikipedia には書いてありませんが、今回欲しかった「モジュラー束だが分配束にならない」例を作るためには、以下を用いて結びを定義する必要があります。

Definition CFprod (S1 S2 : CF) : CF :=
    fun x => exists s1 : G, exists s2 : G,
             S1 s1 /\ S2 s2 /\ x |=| s1 |*| s2.

直感的に言えば、「S1 の元と S2 の元の積の全体」が CFprod S2 S2 ですね。これに正規性の証明を付け加えたものが NSGsup になります。正規部分群の結びが再び正規部分群になる、という部分が今回の証明中で最も重い部分でしょうか。難しいわけではないのですが、書き換えが多くて手数が掛かります。

後は証明するだけ。やっていることは基本的に正規部分群としての性質を使った書き換えのみです。先にも触れましたが、最終的な結論はコードの一番最後で登場する以下の一文です。

Instance NSG_ModularLattice : ModularLattice NSG NSGeq NSGle
                                             NSGsup NSGinf.

その他補足

我ながら駆け足過ぎますね。しかしまあ Advent Calendar 担当者としての義務は果たしたのでよしとしましょう。もしよかったら実際のコードも覗いてやって下さい。

ちなみに題材自体に特に深い意味はなく、頭文字が ML になるからというだけの話です。当初は、分配束の型クラスを作って「分配束ならばモジュラー束」を証明するというプランもあったのですが、今考えるとそっちの方がよかったかもしれません。

また、束に関する面白い性質として、今回のような順序による定義の他、結びと交わりを先に与えることによっても結果的に同じものを定義することができます。この点についても Coq で書いた証明があるのですが、それはまた別の話。