証明駆動開発入門(2)

証明駆動開発の最後のステップである、Extraction という機能を使って Coq のコードを他の言語のコードに変換する方法を紹介します。

8章 の続きとして、8章で定義し性質を証明した insert や insertion_sort を Extraction し、証明駆動開発での挿入ソートの実装を完成させます。

簡単な例

まずは、簡単な関数を他の言語のコードに変換してみます。標準では、Coq のコードは OCaml、Haskell、Scheme のコードに変換できます。

Coq で定義された型や関数が他の言語のコードにどう変換されるかを CoqIDE で見るには、Extraction コマンドを使います。最初は OCaml へ変換する例を挙げます。

OCaml の場合

Extraction コマンドで型または関数 example を OCaml のコードに変換したいときは、Command Pane で以下のように打ちます。

Extraction(* 左のテキストボックス *)  example(* 右のテキストボックス *)

例として List モジュールにある関数 map を変換してみましょう。Require Import List した状態で、Command Pane で以下のように打ってみてください。

Extraction  map

Result for command Extraction map . :
(** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **)

let rec map f = function
  | Nil -> Nil
  | Cons (a, t) -> Cons ((f a), (map f t))

何もエラーがなければ、このように OCaml のコードが表示されます。map の定義にはリストも定義する必要があるので、Coq の list も自動的に変換されています。変換された list の定義を見てみましょう。

Extraction  list

Result for command Extraction list . :
type 'a list =
  | Nil
  | Cons of 'a * 'a list

OCaml のリストに置き換えられるわけではないので、注意してください。

list などの帰納的に定義されたデータ型を変換先の言語に既存の型に置き換えるようにするには、Extract Inductive というコマンドを使います。

Coq の list を OCaml の list に置き換えてみます。Require Import List. の下の行に以下のように書いて読み込ませてください。

Extract Inductive list => "list" ["[]" "(::)"].

もう一度 map を Extraction させてみましょう。

Extraction  map

Result for command Extraction map . :
(** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **)

let rec map f = function
  | [] -> []
  | a::t -> (f a)::(map f t)

ちゃんと独自に定義されていたリスト型が OCaml の list に置き換えられました。

Extract Inductive は以下のように使います。

Extract Inductive (Coq の型) => (string 0) [(string 1) ... (string n)] (optstring).

こう書くことにより、(Coq の型) は (string 0) に置き換えられ、(Coq の型) のコンストラクタはそれぞれ (string 1)、...、(string n) に置き換えられます。(optstring) は list の変換では使いませんでしたが、すぐ後に扱います。

bool も帰納的に定義されているので、同じようにして OCaml の bool に置き換えられます。

Extract Inductive bool => "bool" ["true" "false"].

今度は自然数を取ってその階乗を返す関数 fact を定義して、それを Extraction させてみます。

まずは fact を定義してみます。

Fixpoint fact (n : nat) :=
  match n with
  | O => 1
  | S m => n * fact m
  end.

これを Extraction させると、以下のようになります。

Extraction  fact

Result for command Extraction fact . :
(** val fact : nat -> nat **)

let rec fact n = match n with
  | O -> S O
  | S m -> mult n (fact m)

map のときと同じように、自動的に定義された nat が fact の定義に使われています。

nat は list や bool とは違い、OCaml や Haskell にそのまま対応する型がありません。nat は整数型に置き換えたいところですが、nat と整数型はコンストラクタの対応が取れないので、パターンマッチするときに不都合になってしまいます。

このようなとき、先程使わなかった (optstring) の部分にコンストラクタごとに分岐させる関数を書くことによって、パターンマッチの代わりにその関数によって分岐するようになります。

nat の場合は以下のようになります。

Extract Inductive nat => int ["0" "succ"] "(fun fO fS n -> if n = 0 then fO () else fS (n-1))".

これを読み込ませて fact を Extraction させてみましょう。

Extraction  fact

Result for command Extraction fact . :
(** val fact : int -> int **)

let rec fact n =
  (fun fO fS n -> if n = 0 then fO () else fS (n-1))
    (fun _ -> succ 0)
    (fun m -> mult n (fact m))
    n

パターンマッチの代わりに "(fun fO fS n -> if n = 0 then fO () else fS (n-1))" で分岐するようになりました。(optstring) の部分に書いた無名関数の fO には n が O のパターンに対応する結果、つまり "(fun _ -> succ 0)" を渡し、fS には n が S m のパターンに対応する結果、つまり "(fun m -> mult n (fact m))" を渡しています。

変換された fact の定義には mult という関数が使われています。これも Coq の mult を変換して独自に定義された関数です。これを OCaml 既存の ( * ) に直すには、Extract Constant というコマンドを使います。

Extract Constant mult => "( * )".

このように書くことによって、mult は ( * ) として定義されます。

Command Pane で mult を Extraction させて見てみましょう。

Extraction  mult

Result for command Extraction mult . :
(** User defined extraction *)
(** val mult : nat -> nat -> nat **)

let rec mult = ( * )

Extract Constant コマンドは、

Extract Constant qualid => string.

と書くことにより、qualid を string で定義できます。

Haskell の場合

変換先の言語を指定するには、Extraction Language というコマンドを使います。初期では OCaml に設定されているので、OCaml の場合は何も設定せずに済んだのでした。

変換先の言語を Haskell に変えてみましょう。Coq のコードの中に次のように書いて読み込ませてみてください。

Extraction Language Haskell.

この後は同じように Extract Inductive コマンドで型を置き換え、Extraction コマンドでコードを変換させます。

Haskell に置き換える場合は、Extract Inductive コマンドを以下のように使って list、bool、nat を変換できます。

Extract Inductive list => "([])" ["[]" "(:)"].
Extract Inductive bool => "Bool" ["True" "False"].
Extract Inductive nat => Int ["0" "succ"] "(\fO fS n -> if n == 0 then fO () else fS (n-1))".

Command Pane で map や fact を Haskell のコードに Extraction させてみます。

Extraction  map

Result for command Extraction map . :
map :: (a1 -> a2) -> (([]) a1) -> ([]) a2
map f l =
  case l of
    [] -> []
    (:) a t -> (:) (f a) (map f t)

Extraction  fact

Result for command Extraction fact . :
fact :: Int -> Int
fact n =
  (\fO fS n -> if n == 0 then f0 () else fS (n-1))
    (\_ -> succ 0)
    (\m -> mult n (fact m))
    n

Scheme の場合

変換先の言語を Scheme にしたい場合も、Haskell のときと同じように Extraction Language コマンドを使い、後は同じように Extraction コマンドを使います。

Extraction Language Scheme.

map や fact を Extraction させてみます。

Extraction  map

Result for command Extraction map . :
(define map (lambdas (f l)
  (match l
    ((Nil) `(Nil))
    ((Cons a t) `(Cons ,(f a) ,(@ map f t))))))

Extraction  fact

Result for command Extraction fact . :
(define fact (lambda (n) (match n
                  ((O) `(S (O)))
                  ((S m) (@ mult n (fact m))))))

"lambdas" や "@" 、"match" は Coq Extraction to Scheme で入手できる macros_extr.scm でマクロとして定義されています。

insertion_sort の Extraction

前回定義し性質を証明した insert と insertion_sort を Extraction させてみましょう。insert や insertion_sort の定義はこうでした。

Require Import List.
Require Import Arith.

Fixpoint insert (a : nat)(l : list nat) : list nat :=
  match l with
  | nil => a :: nil
  | x :: xs => if leb a x then a :: l else x :: insert a xs
  end.

Fixpoint insertion_sort (l : list nat) : list nat :=
  match l with
  | nil => nil
  | x :: xs => insert x (insertion_sort xs)
  end.

OCaml の場合

list や bool、nat を置き換えるために、Extraction Inductive コマンドを使います。まずは OCaml に変換することを考えます。insertion_sort の定義を書いた行より下に以下のように打って読み込ませてください。

Extract Inductive list => "list" ["[]" "(::)"].
Extract Inductive bool => "bool" ["true" "false"].
Extract Inductive nat => int ["0" "succ"] "(fun fO fS n -> if n = 0 then fO () else fS (n-1))".

Command Pane で insert や insertion_sort がどのように変換されるか見てみましょう。

Extraction  insert

Result for command Extraction insert . :
(** val insert : int -> int list -> int list **)

let rec insert a l = match l with
  | [] -> a::[]
  | x::xs -> if leb a x then a::l else x::(insert a xs)

Extraction  insertion_sort

Result for command Extraction insertion_sort . :
(** val insertion_sort : int list -> int list **)

let rec insertion_sort = function
  | [] -> []
  | x::xs -> insert x (insertion_sort xs)

Haskell の場合

Extraction Language Haskell.

Extract Inductive list => "([])" ["[]" "(:)"].
Extract Inductive bool => "Bool" ["True" "False"].
Extract Inductive nat => Int ["0" "succ"] "(\fO fS n -> if n == 0 then fO () else fS (n-1))".

Extraction  insert

result for command Extraction insert . :
insert :: Int -> (([]) Int) -> ([]) Int
insert a l =
  case l of
    [] -> (:) a []
    (:) x xs ->
      (case leb a x of
         True -> (:) a l
         False -> (:) x (insert a xs))

Extraction  insertion_sort

Result for command Extraction insertion_sort . :
insertion_sort :: (([]) Int) -> ([]) Int
insertion_sort l =
  case l of
    [] -> []
    (:) x xs -> insert x (insertion_sort xs)

Haskell のコードに変換されました。

Scheme の場合

Scheme のコードに変換するときは、Command Pane で

Extraction Language  Scheme

と打ち、同じように関数を Extraction させます。

Extraction  insert

Result for command Extraction insert . :
(define insert (lambdas (a l)
  (match l
    ((Nil) `(Cons ,a (Nil)))
    ((Cons x xs)
      (match (@ leb a x)
        ((True) `(Cons ,a ,l))
        ((False) `(Cons ,x ,(@ insert a xs))))))))

Extraction  insertion_sort

Result for command Extraction insertion_sort . :
(define insertion_sort (lambda (l)
  (match l
    ((Nil) `(Nil))
    ((Cons x xs) (@ insert x (insertion_sort xs))))))

ファイルに出力する

CoqIDE 上で Coq のコードを他の言語のコードに変換できました。CoqIDE で見るだけでなく、ファイルに出力するには CoqIDE ではなく coqc を使います。

これまで書いたプログラムの最後の行に以下を書き加えます。

Extraction "insertion_sort.ml" insertion_sort.

"insertion_sort.ml" が出力されるファイル名になるので、自由に変えてもらって結構です。書き加えたら Coq のコードを名前を付けて保存します。仮に "insertion_sort.v" という名前を付けたとします。そうしたら端末上で

% coqc insertion_sort.v

と入力します。エラーが出なければ "insertion_sort.ml" というファイルが作成されており、ここに変換された OCaml のコードが出力されています。

Haskell のコードに変換したいときは Extraction "insertion_sort.ml" insertion_sort. の代わりに

Extraction Language Haskell.

Extract Inductive list => "([])" ["[]" "(:)"].
Extract Inductive bool => "Bool" ["True" "False"].
Extract Inductive nat => Int ["0" "succ"] "(\fO fS n -> if n == 0 then fO () else fS (n-1))".

Extraction "insertion_sort.hs" insertion_sort.

と書いて同じように coqc でファイルを生成します。

Scheme の場合は

Extraction Language Scheme.
Extraction "insertion_sort.scm" insertion_sort.

と書きます。

ソースコードが生成されたので、試しに ocaml で実際に動かしてみます。

% ocaml
# #use "insertion_sort.ml";;

val leb : int -> int -> bool = <fun>
val insert : int -> int list -> int list = <fun>
val insertion_sort : int list -> int list = <fun>

# insertion_sort [3; 1; 5; 2; 6; 3];;

- : int list = [1; 2; 3; 3; 5; 6]

# insertion_sort [4; 2; 9; 1; 3];;

- : int list = [1; 2; 3; 4; 9]

実際にソート関数になりました。

OCaml、Haskell、Scheme のコードが生成できました。これで証明駆動開発のステップ

をすべて終え、ソートとしての正しさが保証された挿入ソートの実装ができたことになります。少し長かったですが、お疲れさまでした!

終わりに

プログラミング Coq の連載はこれで終わりです。Coq での基本的なプログラミング、証明の仕方は以上です。

この連載を通して、少しでも Coq の使い方や証明駆動開発の概念を分かってもらえたでしょうか? 難しく感じるところも多かったかもしれませんが、プログラムでの証明というまったく新しいことに触れて楽しんでいただけていれば幸いです。

最後に、ここまで読んでくださったみなさん、ありがとうございました。楽しく証明していきましょう!