Coq でクイックソート (3) - チェシャ猫の消滅定理

Coq でクイックソートの検証、三回目です。今回は最後に残った部分をちょろっとだけ埋めましょう。コードは前回、前々回に追記する形で、https://gist.github.com/4526374 に置いてありますのでよかったらご参照を。

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

今回の目標

今回は、最後に残った qsort の二つ目の仕様

出力が入力の置換 (並び替え) になっていること

を証明します。モジュール Sorting.Permutation を使いましょう。前回の Sorted に比べ、Permutation はリスト操作とそれなりに相性がよく、証明済みの定理も使えそうなヤツが揃っています。

述語 Permutation の中身

Permutation の定義は以下です。

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''

特に複雑なところはないですね。要するに、空リストから始めて「同じ要素を先頭にくっつける」「先頭から二つを入れ替える」を有限回繰り返して得られるリストは互いに置換である、というわけです。

いざ、最後の証明

示したい定理を改めて掲げておきます。

Theorem qsort_Permutation : forall l : list nat,
                            Permutation (qsort l) l.

証明に使うのは前回と同じく functional induction タクティク。さらに上手いことに、ライブラリを覗いてみるとこんなのがありました。

Permutation_cons_app
     : forall (A : Type) (l l1 l2 : list A) (a : A),
       Permutation l (l1 ++ l2) -> Permutation (a :: l) (l1 ++ a :: l2)

qsort の定義が

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 の結果と antifilter の結果を append したものは、もとのリストの置換」という補題 filter_Permutation ですが、これにしたって単純な場合分けだけですぐに証明できてしまいます。

その他補足

さて、全三回に渡ってお送りしてきましたが、以上によりクイックソート qsort の仕様が証明されました。これで明日から安心してクイックソートが使えますね。めでたしめでたし。ちなみにこのナイーブな実装では遅すぎて実用性が皆無ですが、まあご愛嬌ということで。

今回の「置換であること」の定式化や証明には、この他にも方法が考えられるはずです。すぐに思いつくのは、「任意の要素に関して、二つのリストに含まれる個数が等しければ置換」というものでしょうか。形式的に書けば

Theorem Permutation_count : forall l1 l2 : list nat,
                            Permutation l1 l2 <->
                            (forall n : nat, count_occ eq_nat_dec l1 n =
                                             count_occ eq_nat_dec l2 n).

という感じでしょうかね。ただ、置換であることと述語 In とはあまり相性がよくありません。前回の補足でも述べた通り、In は重複した要素を区別することができないからです。リストが重複要素を含まないときのみ、In を使って Permutation を特徴づける補題 NoDup_Permutation も用意されていますが、使いどころは難しい気がします。

なお、ここに挙げた定理 Permutation_count はそう苦労せずに証明することができるのですが、それはまた別の話。