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

Coq でクイックソートの検証、二回目です。コードは前回のものに追記する形で https://gist.github.com/4526374 に置いてあります。

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

今回の目標

さて、前回の最後にも触れた通り、前回定義したクイックソート qsort について、

出力が昇順になっていること

を保証することが第一の目標です。ここでは、標準ライブラリ Sorting モジュール内にある述語 Sorted を使うことにしました。Sorting.Sorted の中には、「リストが (ある関係 R に対して) 昇順である」ことを意味する述語が三種類用意されています (LocallySorted、Sorted、StronglySorted) が、これらはすべて同値です。

述語 Sorted の中身

Sorted の定義を見ると、次のようになっています。

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)

ちなみに、ここで補助的に使われている HdRel の定義は以下です。

Inductive HdRel (A : Type) (R : A -> A -> Prop) (a : A) : list A -> Prop :=
    HdRel_nil : HdRel R a nil
  | HdRel_cons : forall (b : A) (l : list A), R a b -> HdRel R a (b :: l)

自然言語で読み下せば、HdRel R a l は「a とリスト l の先頭要素との間に関係 R が成立」を意味しています。Head Relation の略でしょうね。これを考えると、Sorted は直感的には「既にソートされたリストに対して、現在の先頭要素以下のものを先頭に付け足してもソートされている」と定義されていることがわかります。

さて、ここまで来てちょっと困りました。というのも、qsort は再帰的に定義されていて、最終的な出力の先頭要素がどこから来ているのかわからないからです。こういうときに使えるのが functional induction タクティクです。

Functional Induction による証明

さて改めて確認しておくと、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.

もし人間が紙の上で「qsort の出力が昇順」を示したいとしたら、自然なのは「qsort lts とqsort ges が昇順だと仮定すると〜」というものでしょう。Coq に対してこれを伝えるタクティクが functional induction で、関数の再帰呼び出しに対して帰納法を適用することができます。実際に今回示したい定理

Theorem qsort_Sorted : forall l : list nat, Sorted le (qsort l).

に対して functional induction (qsort l) を打ち込んでみると、l = n :: l' の場合に使える仮定として「Sorted le (qsort (antifilter (leb n) l'))」および「Sorted le (qsort (filter (leb n) l'))」が追加されるはずです。

これができれば、それ以外はたいした問題はないはず。もちろん、二つの昇順リストを連結したときに結果が再び昇順になるためには、左側に小さい要素、右側に大きい要素が集まっている必要があるので、それさえ示しておけば大丈夫。定式化の方法はいろいろあると思いますが、ここでは次のような補題を使ってあります。

Lemma Sorted_app : forall (l1 l2 : list nat),
                   Sorted le l1 -> Sorted le l2 ->
                   (forall n1 n2 : nat,
                    In n1 l1 -> In n2 l2 -> n1 <= n2) ->
                   Sorted le (l1 ++ l2).

その他補足

さて、これで半分終わりました。次回は残りのもうひとつ、qsort の出力が入力の置換であることを証明する予定です。

ちなみに「置換である」という部分だけ見ると、今回補題として用いた

Lemma qsort_in : forall (l : list nat) (n : nat),
                 In n l <-> In n (qsort l).

がそのまま使えそうな気がします。がしかし、この補題は置換であることを保証しません。というのも、述語 In は「リストの中に一個以上存在する」ことしか保証せず、ダブりを考慮できないからです。置換であるためには個数まで含めて一致する必要がありますからね。

とはいえ、ライブラリを見てもらえればわかる通り、Sorting.Permutation は今回の Sorting.Sorted よりも使えそうな補題が豊富です。次回はこいつらを活用する方針で行きたいと思いますが、それはまた別の話。