リストの要素の内、条件に合致するものだけを抜き出す関数 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 の検証、今後これを用いてクイックソートの検証をしようという予定があったりなかったりするのですが、それはまた別の話。
