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を使っていました