[Coq] Coq'Art Chap.1

Interactive Theorem Proving and Program Development; Coq'Art: The Calculus of Inductive Constructionsを読み始める事にしました。

Chap.1ではinsertion sortを例にしてCoqの解説が行われています。そこで、Appendixのinsertion sortのコードをCoqIdeに入力してみました。実際に証明が自分で出来る様になるのは将来の課題として、とりあえずCoqでの開発の流れを追ってみます。
なお証明自体はinsertionv8.vにあります。

まず、list Zがソートされた状態を定義するsorted : list Z -> Propを定義します。こんな感じです。

Inductive sorted : list Z -> Prop :=
  | sorted0 : sorted nil
  | sorted1 : forall z:Z, sorted (z :: nil)
  | sorted2 : forall (z1 z2:Z) (l:list Z), 
       z1 <= z2 -> sorted (z2 :: l) -> sorted (z1 :: z2 :: l).

sortedは定義なのでこれ自体は証明の対象ではありません。

これを用いて、

Theorem sorted_inv : 
  forall (z:Z) (l:list Z), sorted (z :: l) -> sorted l.

を証明します。

次いで、並べ替えであることを示すequivを定義します。まず、リストのなかの出現数を示す

Fixpoint nb_occ (z:Z) (l:list Z) {struct l} : nat :=
  match l with
  | nil => 0%nat
  | (z' :: l') =>
      match Z_eq_dec z z' with
      | left _ => S (nb_occ z l')
      | right _ => nb_occ z l'
      end
  end.

を定義します。このnb_occは定義なので証明しません。

これを使って、

Definition equiv (l l':list Z) := forall z:Z, nb_occ z l = nb_occ z l'

を定義します。これ自体も証明しません。

nb_occ, equivの定義から、下記の補題を証明します。

Lemma equiv_refl : 
  forall l:list Z, equiv l l.
Lemma equiv_sym : 
  forall l l':list Z, equiv l l' -> equiv l' l.
Lemma equiv_trans : 
  forall l l' l'':list Z, equiv l l' -> equiv l' l'' -> equiv l l''.
Lemma equiv_cons : 
  forall (z:Z) (l l':list Z), equiv l l' -> equiv (z :: l) (z :: l').
Lemma equiv_perm : 
  forall (a b:Z) (l l':list Z), equiv l l' -> equiv (a :: b :: l) (b :: a :: l').

次いで、実際にinsertion sortを行う関数aux : Z -> list Z -> list Zを定義します。

Fixpoint aux (z:Z) (l:list Z) {struct l} : list Z :=
  match l with
  | nil => z :: nil
  | cons a l' =>
      match Z_le_gt_dec z a with
      | left _ =>  z :: a :: l'
      | right _ => a :: (aux z l')
      end
  end.

auxがinsertion sortの性質を持っている事を示す補題、つまりauxの結果がequivであること、sortedであることを証明します。

Lemma aux_equiv : 
  forall (l:list Z) (x:Z), equiv (x :: l) (aux x l).
Lemma aux_sorted : 
  forall (l:list Z) (x:Z), sorted l -> sorted (aux x l).

最後に、sort:list Z -> list Zを定義というか、sortされた出力の存在を証明します。

Definition sort :　forall l:list Z, {l' : list Z | equiv l l' /\ sorted l'}.

証明を追いきれてないのですが、どうもexists (aux a l')の様に、実例を示して存在を証明するみたいにauxを使っているようです。

----

sorted, nb_occ, equivは定義なので証明の対象ではありません。
aux, sortは成果物として得る、証明済みのプログラムです。sortを満たす具体的なl'の値としてauxを使った式を与えます。その値がl'の条件を満たす事はaux_equiv, aux_sortedから保証されます。

一般的に

• 仕様を表す様な述語(X -> Prop)を書く。仕様に関する補題も証明しておく。
  
• 解を与える様な関数を書く。
  
• その関数の出力が仕様を満たす事を証明する。
  

とかすれば良い様に見えます。

----

ある程度、この本を読み終わった後で、またこのプログラムを振り返ってみたいと思います。