Coqで、クイックソート

（＊　注意：今回はCoq 8.1以上を使用。　＊）

今回は、らくがきえんじんで、昔 言及されていた、クイックソートに挑戦してみる。

Coqで、再帰する関数を書く場合は、Definitionコマンドではなく、Fixpointコマンドを使う。
しかし、Fixpointによる関数定義では、明らかに停止する構造を持つ必要がある。

Coqでは、必ず停止する関数のみが定義できる、という制限のため、このように再帰する関数を定義するのは難しいが、Coqで作った関数は、必ず停止して結果を返す、という性質を保っている。

しかし、Fixpointによる定義では、簡単に定義できない再帰関数もある。
例えば、次のように、クイックソートの関数を素直にかいてみると、以下のようなエラーになる。

(*  クイックソートの定義  失敗例 *)
Fixpoint qsort (l : list A) : list A :=
  match l with
  | nil => nil
  | x :: xs => qsort (filter (A_gtb compare x) xs)
                 ++ (x :: qsort (filter (A_leb compare x) xs))
  end.
(* (::) はcons, (++) はappend *)

↓

Recursive definition of qsort is ill-formed.
In environment
qsort : list A -> list A
l : list A
x : A
xs : list A
Recursive call to qsort has principal argument equal to
"filter (A_gtb compare x) xs"
instead of xs

このqsort関数は、関数の定義内で、自分自身qsortを呼び出す、再帰関数であるが、その再帰呼び出しで、(filterごにょごにょ)が、与えられており、この関数が停止するかどうか、構造的には、明らかでない形になっている。
このため、Coqからは、qsortの再帰定義が正しくない形だよ。と言われてエラーになってしまう。
この場合は、 Listのfilter関数の結果は、必ず、長さが大きくならないので、停止するはずである。

このような関数を簡単に定義する方法が、Coqの8.1から導入された。それはFunctionコマンドとmeasureキーワードである。
このコマンドによって、停止するかどうかが、簡単にはわからない再帰関数を手軽に書き表すことができ、そのあと、停止性をtacticsを使って証明することができる。

先ほどのコードにおける、Fixpoint を Function にして、measureキーワードをつけたせば、エラーにならずに、停止性の証明モードに推移する。ここでは、measureとして、listの長さを測るlength関数を指定する。

(*  クイックソートの定義  成功例 *)
Function qsort (l : list A) {measure length l} : list A :=
  match l with
  | nil => nil
  | x :: xs => qsort (filter (A_gtb compare x) xs)
                 ++ (x :: qsort (filter (A_leb compare x) xs))
  end.

↓

Coq < 2 subgoals
  
  A : Set
  compare : A -> A -> comparison
  ============================
   forall (l : list A) (x : A) (xs : list A),
   l = x :: xs -> length (filter (A_leb compare x) xs) < length (x :: xs)

subgoal 2 is:
 forall (l : list A) (x : A) (xs : list A),
 l = x :: xs -> length (filter (A_gtb compare x) xs) < length (x :: xs)

qsort_tcc <

ここで、このゴールを証明すれば、停止性が保証され、関数定義が完了するといった具合だ。
証明が終了すると、次のような応答がかえってくるはずである。

Proof completed.

qsort_tcc < Qed.

qsort_ind is defined
qsort_rec is defined
qsort_rect is defined
R_qsort_correct is defined
R_qsort_complete is defined
qsort is defined
qsort_equation is defined
qsort_terminate is defined
qsort_tcc is defined

ぱっと見た感じ、qsort以外に、いろんなものが定義されている。これらは、qsortの性質を示すために便利な項達である。
今後、停止性以外の性質を証明しようと思ったら、ふつうのlistの構造に関する帰納法ではうまく行かないことが多い。
しかし、qsort_indを使うと、qsortの定義に従った帰納法によって、証明することができる。

ここでは、qsortしても、入力と出力の要素数が変わらないことと、順番は変わるけど、要素の内容は変わらないことを証明した。

以下が、ソースコードの全体である。

Section QSort.
Require Import List.
Require Import Bool.
(* 
 * Functionキーワードによる再帰定義をうまくやるためには
 * Recdefというモジュールをインポートする必要がある
 *)
Require Import Recdef.
Variable A:Set.
Variable compare : A -> A -> comparison.

(* 停止性のための補題、filterしたら短くなるよ。 *)
Lemma filter_length : forall (A:Set)(l:list A)(p:A -> bool),
  length (filter p l) <= length l.
Proof.
intro X; induction l.
 simpl in |- *.
   auto.
simpl in |- *.
  intro p; case (p a).
 simpl in |- *.
   apply Le.le_n_S.
   apply IHl.
apply le_S.
  apply IHl.
Qed.

Definition A_gtb (compare : A -> A -> comparison) (a b : A) : bool :=
  match compare a b with | Gt => true | _ => false end.
Definition A_leb (compare : A -> A ->  comparison) (a b : A) : bool :=
  negb (A_gtb compare a b).

(*
 * qsort関数の定義 (Proof以下は停止性の証明)
 * qsort : list A -> list A
 *)
Function qsort (l : list A) {measure length l} : list A :=
  match l with
  | nil => nil
  | x :: xs => qsort (filter (A_gtb compare x) xs)
                 ++ (x :: qsort (filter (A_leb compare x) xs))
  end.
Proof.
 intros; simpl in |- *; apply Lt.le_lt_n_Sm.
   apply filter_length.
intros; simpl in |- *; apply Lt.le_lt_n_Sm.
  apply filter_length.
Qed.

(*
 * qsortの停止性の証明は無事終了
 * 以降ではqsort関数の簡単な性質について、証明するオマケレンマ
 *)

(* pでfilterしたものと~pでfilterしたものを合体させると元通りだよ *)
Lemma filter_length_not : forall (l : list A)(p q : A -> bool), 
  (forall x:A, p x = negb (q x)) ->
   length (filter p l) + length (filter q l) = length l.
Proof.
intros l p q H; induction l.
 simpl in |- *; reflexivity.
simpl in |- *.
  rewrite H in |- *.
  case (q a).
 simpl in |- *.
   rewrite <- plus_n_Sm in |- *; rewrite IHl in |- *; reflexivity.
simpl in |- *.
  rewrite IHl in |- *; reflexivity.
Qed.

(* qsortしても長さは変わらないよ *)
Lemma qsort_length : forall l: list A, length (qsort l) = length l.
Proof.
apply (qsort_ind (fun l1 l2 => length l2 = length l1)).
 intros; reflexivity.
intros l x xs H00 H1 H2.
  rewrite app_length in |- *.
  rewrite H1 in |- *.
  simpl in |- *.
  rewrite H2 in |- *.
  rewrite <- plus_n_Sm in |- *; rewrite filter_length_not in |- *.
 reflexivity.
unfold A_leb in |- *.
  intro x0; case (A_gtb compare x x0); simpl in |- *; reflexivity.
Qed.

(* l と qsort l とは、集合としては、等しい *)
(* その１: l は qsort l の部分集合 *)
Lemma qsort_In1 : forall (l:list A)(x:A), In x l -> In x (qsort l).
Proof.
apply (qsort_ind (fun l1 l2 : list A => forall x : A, In x l1 -> In x l2)).
 intros l _H x H; apply H.
intros l x xs _H IH1 IH2 a H.
  elim (in_inv H).
 intro eq; rewrite eq in |- *; apply in_or_app.
   right; apply in_eq.
intro H0.
  cut (A_gtb compare x a = true \/ A_gtb compare x a = false).
 intro tf; elim tf.
  intro t; apply in_or_app.
    left; apply IH1.
    elim (filter_In (A_gtb compare x) a xs).
    intros _H0 H1; apply H1.
    split; [ apply H0 | apply t ].
 intro f; apply in_or_app; right.
   apply in_cons; apply IH2.
   elim (filter_In (A_leb compare x) a xs).
   intros _H0 H1; apply H1.
   split; [ apply H0 | unfold A_leb in |- *; rewrite f in |- * ].
   simpl in |- *; reflexivity.
case (A_gtb compare x a); [ left; reflexivity | right; reflexivity ].
Qed.

(* その２: qsort l は l の部分集合 *)
Lemma qsort_In2 : forall (l:list A)(x:A), In x (qsort l) -> In x l.
Proof.
apply (qsort_ind (fun l ql => forall x : A, In x ql -> In x l)).
 intros l _H x H; apply H.
intros l x xs _H IH1 IH2 a.
  intro H;
   elim
    (in_app_or (qsort (filter (A_gtb compare x) xs))
       (x :: qsort (filter (A_leb compare x) xs)) a).
 intro H1; apply in_cons.
   elim (filter_In (A_gtb compare x) a xs).
   intros H2 _H0; elim H2; intros.
  apply H0.
 apply IH1; apply H1.
intro H0.
  elim (in_inv H0).
 intro eq; rewrite eq in |- *; apply in_eq.
intro H1; apply in_cons.
  elim (filter_In (A_leb compare x) a xs).
  intros H2 _H0; elim (H2 (IH2 a H1)).
  intros H3 _H1; apply H3.
apply H.
Qed.

End QSort.