Coqによる証明駆動開発で Merge Sort プログラムをつくってみた

Coq Merge Sort Proof Driven Development 証明駆動開発 マージソート Function Functional Scheme

OCaml合宿で帰りの車の中でid:zyxwv さんにMergeSortの正しさをどうやって証明するか聞かれてとっさに証明できなかったので、合宿から帰ったあとに一生懸命証明してみた。

プログラムと証明の全体はこちら: yoshihiro503 / mergesort / source / — Bitbucket。

思ったより簡単ではなく、いろいろなテクニックが必要で非常に勉強になった。Coq初心者の人はMergeSortの問題をとりあえずの目標にして証明を頑張ると非常に効率がいいのではないかと思う。

私は、だいたい以下の流れでプログラムした。

  • Sortedという命題を作り、リストがソート済みであるという状態を定義する
  • mergesort関数があるとして、満たすべき性質(i)を定理として記述する
  • mergesort関数を定義する
    • mergesort関数に必要な補助関数 merge関数を定義して諸性質を証明する
    • mergesort関数に必要な補助関数 split関数を定義して諸性質を証明する
    • mergeとsplitを使ってmergesort関数を定義する
  • (i)を証明する


プログラムを作ろうと思ったら、実装する前にそのプログラムがどういう性質があればよいかを記述しよう。これができれば、あとはコンパイラが通るまで頑張るだけだ。コンパイラが通れば完了で、テストは必要ない。

この考えかたは証明駆動開発(Proof Driven Development)と呼ばれるらしい。

参考: d.y.d. 16:40 08/05/15 Proof Driven Development

以下、開発した手順にそって詳細を説明する。

準備

まず準備として対象とするリストの要素の型を A として、その要素上で大小比較ができることを仮定する。

型 A と A 上の大小比較演算子を\le{~}^{\prime}(小なりイコールダッシュ)とかの記号で表す。

Sortedという命題を作り、リストがソート済みであるという状態を定義する

Sortedという命題(Proposition)を次の様に定義する。

Definition Sorted (xs: list A) : Prop :=
  forall x y i j,
  i < j ->
  Some x = nth_error xs i ->
  Some y = nth_error xs j ->
    x <=' y.

nth_error関数はListモジュールにあるlistのn番目を取ってきて、オプション型で値を返す関数だ。これはだいたいi\lt jならばxs[i]\le{~}^{\prime}xs[j]であることを表現している。

Inductiveな定義で再帰的に定義する方法もあるが、今回はより一般的なかたちで定義した。ただ、それだと証明するときにちょっと大変になるのでその差を無くすために次の補題を証明しておく。

Lemma sorted_ind : forall x xs,
  Sorted xs -> (forall y, In y xs -> x <=' y) -> Sorted (x :: xs).

Lemma sorted_ind_inv : forall x xs,
  Sorted (x :: xs) -> Sorted xs /\ (forall y, In y xs -> x <=' y).

mergesort関数があるとして、満たすべき性質(i)を定理として記述する

今回の開発の目標として満たすべき性質を「任意のリストに対して、mergesortの結果が必ずsortされている」とする。それはCoqでは以下の様に記述できる。

Theorem mergesort_sorted : forall xs, Sorted (mergesort xs).

この定理を書いてコンパイルが通れば完成である。以下ではmergesortの実装と、この定理の証明を記述してコンパイルが通るようにすればいいだけだ。証明駆動開発バンザイ！

mergesort関数を定義する

mergesort関数は補助関数mergeとsplitを使って次の様に定義がしたい。

定義 merge (xs ys : list A) :=
  match (xs, ys) with
  | (nil, ys) => ys
  | (xs, nil) => xs
  | (x::xs, y::ys) =>
     if x <=?' y then
       x :: merge xs (y::ys)
     else
       y :: merge (x::xs) ys
  end.

定義 split (xs : list A) :=
  match xs with
  | nil => (nil, nil)
  | x::nil => (x::nil, nil)
  | x::y::zs =>
     match split zs with
     | (xs, ys) => (x::xs, y::ys)
     end
  end.

定義 mergesort (xs : list A) :=
  match xs with
  | nil => nil
  | x::nil => x::nil
  | x::y::zs =>
     match split (x::y::zs) with
     | (xs, ys) => merge (mergesort xs, mergesort ys)
     end
  end.

mergeもsplitもmergesortもすべて再帰的な関数である。Coqでは停止性が保証される関数しか定義することができないので、再帰的な関数はちょっとした工夫が必要だ。それぞれの関数を順番に定義していこう。

mergesort関数に必要な補助関数 merge関数を定義して諸性質を証明する

じゃあ、merge関数を定義しよう。今回この関数が一番難しかった。でもmerge関数に関する部分が本質的にかなり重要な部分なのでmergeができたら、あとはほとんどオマケと思っていいだろう。

merge関数は引数が複数有り、停止することが構造的に明らかではない。停止性が明らかでないような再帰関数の定義はFunctionというキーワードを使って定義する。Functionキーワードでmeasure指定をして定義すると、引数が何らかの意味で減少していることを後から証明すればちゃんと定義できる。ただ、減少する引数は一つである必要があるのでリストのペアを引数に取るようにした。

Functionによる関数定義でmeasure指定をした時のの構文は以下のような感じ。

"Function" <関数名> "(" (<引数名>":"<型>) ","... ")"
  "{" "measure" <メジャー関数> <減少する引数名> "}" ":" <型> ":="
  <関数の内容> "."

メジャー関数のところはだいたい大きさをはかる関数を書けば大丈夫。リストだったらlength関数、リストのペアならその合計を返す関数を書こう。

Definition pair_length (xsys: list A * list A) :=
  length (fst xsys) + length (snd xsys).

Function merge (xsys: list A * list A) {measure pair_length xsys} : list A :=
  match xsys with
  | (nil, ys) => ys
  | (xs, nil) => xs
  | (x::xs, y::ys) =>
     if x <=?' y then
       x :: merge (xs, y::ys)
     else
       y :: merge (x::xs, ys)
  end.

こう定義した時点でコンパイルすると「Error: There are pending proofs」と言われるので対話的に証明ができるチャンスだ！ coqtopでこのファイルを読み込んで対話的証明をしよう。証明する内容は「この関数の各再帰呼び出しで指定した引数のサイズが減っているということ」だ。

  $ coqtop -l MergeSort.v
Welcome to Coq 8.2pl1 (September 2009)

merge_tcc <

ここでShow.と打つと現在の示すべきことが表示される。二回の再帰呼び出しのそれぞれでリストのペアの長さの合計が減っていることを示せればOKだ。これは非常に簡単だ。

証明が完了するとめでたくmerge関数が定義できる。Functionで定義した場合はそれだけでなく、この関数の再帰呼び出しに関する帰納法ができるmerge_indも定義されるので、mergeに関する証明にガンガン使っていこう。

ただ、このmerge_indは引数がリストのペアにして定義したためちょっと使いにくい。使いやすくするために引数を複数引数にカリー化した merge_ind_curry を補助的に作ったので、以降ではこっちを使うことにする。

ここでは以下の性質を証明した。

  • mergeされたリストに含まれている要素は、もとの引数のリストのどちらかに含まれている。
Lemma merge_incl: forall xs ys x,
  In x (merge (xs,ys)) -> In x xs \/ In x ys.
  • 整列したリスト同士をmergeすると結果も整列する。
Lemma merge_ok : forall xs ys,
  Sorted xs -> Sorted ys -> Sorted (merge (xs, ys)).
mergesort関数に必要な補助関数 split関数を定義して諸性質を証明する

split関数は再起するが、停止することが構造的に明らか(再帰呼び出しがsubtermに適用される)なのでFixpointで定義できる。

Fixpoint split (xs: list A) :=
  match xs with
  | nil => (nil, nil)
  | x::nil => (x::nil, nil)
  | x::y::zs =>
     match split zs with
     | (xs, ys) => (x::xs, y::ys)
     end
  end.

ただ、Functionで定義したときの *_ind みたいなものは定義されないのでそういうときはFunctionで定義するか次の一行を書き加えよう。これでsplit_indという便利な命題が使えるようになる。

Functional Scheme split_ind := Induction for split Sort Prop.

　*_ind は普通はあんまり必要ないけれど、splitみたいに再帰呼び出しが二個前ごとに呼ばれるような関数だと便利なときがある。次のsplit関数の長さに関する補題を示すがそこでsplit_indは大活躍した。詳細が気になる人はソースコードを見てみよう。

Lemma split_length : forall zs xs ys,
  split zs = (xs, ys) -> length zs = length xs + length ys.
mergeとsplitを使ってmergesort関数を定義する

mergesort関数もやはり再帰関数だ。しかも停止性が明らかではないのでこの場合はFunctionで定義するのが有効だ。splitの結果は必ず長さが短くなるか等しいので長さに関して減ることを示す作戦でいこう。その場合はmeasureキーワードを使う。今回は引数は一つのリストなのでサイズを計る関数は単にlengthでおk。

Function mergesort (xs : list A) {measure length xs} : list A :=
  match xs with
  | nil => nil
  | x::nil => x::nil
  | x::y::zs =>
     match split (x::y::zs) with
     | (xs, ys) => merge (mergesort xs, mergesort ys)
     end
  end.

対話的証明でsplitの結果のリストがそれぞれ短くなっていることを証明できれば定義完了だ。Functionによる定義なので便利な mergesort_ind も得ることができる。

(i)を証明する

さあ、やっと目標の定理を証明すべきときがやってきた。今回のプロジェクトのラスボスだ。はりきって挑もう。

Theorem mergesort_sorted : forall xs, Sorted (mergesort xs).

ラスボスとは言いながらも実はこれまでの補題を使えば簡単にやっつけることができる。これで、今日からソートは安心して行うことができるね。よかったよかった。