読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

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 とは、集合としては、等しい *)
(* その1: 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.

(* その2: 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.