Coqでクイックソート (未完)
ググれば出てきそうな気もしますが、がんばってみました。しかしあえなく轟沈。(証明どころか関数さえ書けない始末…情けない。)
Coqではちゃんと停止する関数しか書けないです。これは再帰が書けないという事ではなく、再帰にはDefinitionの代わりにFixpointというキーワードを使います。関数が止まることを示すために、structural recursionで減っていく引数を明示する struct というキーワードを使ってやれば単純な例だと停止性を判定してくれるんですが、クイックソートではこれは使えなくて(filterがリストを短くしてるということを分かってくれない)、クイックソートの1ステップで引数が減るという証明が必要っぽいです。以下詳細です。
なぜか標準のリストを使わずに自前でリストを定義しているけど、こんな感じのをcoqtopに入れる。Coqをしらなくても関数型な人なら勘で読めると思います:
Inductive list(A:Set) : Set := | nil : list A | cons : A -> list A -> list A. Implicit Arguments nil[A]. Implicit Arguments cons[A]. Require Import ZArith. Fixpoint filter_gt (pivot:Z)(l:list Z) {struct l} : list Z := match l with | nil => nil | cons hd tl => match Z_le_gt_dec hd pivot with | left _ => cons hd (filter_gt pivot tl) | right _ => filter_gt pivot tl end end. Fixpoint filter_le (pivot:Z)(l:list Z) {struct l} : list Z := match l with | nil => nil | cons hd tl => match Z_le_gt_dec hd pivot with | right _ => cons hd (filter_le pivot tl) | left _ => filter_le pivot tl end end. Fixpoint append3 (l1:list Z) (a:Z) (l2:list Z){struct l1} : list Z := match l1 with | nil => cons a l2 | cons hd tl => cons hd (append3 tl a l2) end. Fixpoint qsort (l:list Z){struct l} : list Z := match l with | nil => nil | cons hd tl => append3 (qsort (filter_gt hd tl)) hd (qsort (filter_le hd tl)) end.
ここで、さいごのqsortの定義で
Recursive call to qsort has principal argument equal to "filter_gt hd tl" instead of tl
と怒られてしまいます。principal argument(structで指定したやつ)が減ってるかどうかCoqは分かってくれんのです。ああめんどい。
そこで、リストの長さに関して減少するように再帰するために、リストの長さについての述語 longer を導入する:
Fixpoint longer (A:Set)(l:list A)(m:list A){struct l} : Prop := match l,m with | _,nil => False | nil,cons _ _ => True | cons _ l1, cons _ m1 => longer A l1 m1 end.
さらに、filter_gt, filter_leが本当に引数を短くしているという証明をする:
Hypothesis filter_gt_longer : forall (hd:Z)(tl:list Z), longer (filter_gt hd tl) (cons hd tl). Hypothesis filter_le_longer : forall (hd:Z)(tl:list Z), longer (filter_le hd tl) (cons hd tl).
これが証明できれば、次の補助関数
Definition qsort_aux (l:list Z) : (forall m:list Z, longer m l -> list Z) -> list Z := match l return ((forall m:list Z, longer m l -> list Z) -> list Z) with | nil => fun _ => nil | cons hd tl => fun f => append3 (f (filter_gt hd tl) (filter_gt_longer hd tl)) hd (f (filter_le hd tl) (filter_le_longer hd tl)) end.
を、Yコンビネータみたいな関数well_founded_induction (省略) に食わせることで、やっとqsortが書ける。
しんどい。
ちなみに教科書はCoq'Artを使っていました