はじめての Coq

Coq

Coq などの定理証明系に興味を持っている人は少なくないと思うのですが、やっぱり最初の一歩を踏み出すのは大変。web 上の Coq チュートリアルは、Coq 処理系の機能を説明しているだけで、数学の素養がない人(普通の情報系の学生)が実際に関数の性質を証明するためにどうしたらいいかが書いてあるわけじゃないし。
だって「(a -> b -> c) -> (a -> b) -> a -> c" を証明してみましょう」とか言われても全然やる気にならないじゃん。そんなことを証明するために Coq を使いたいわけじゃない！

そんなわけで、ocaml-nagoya の合宿の機会を利用して id:yoshihiro503 さんと id:suer さんに、Coq をプログラミング言語として使う場合の基本を教えてもらってきました。特に id:yoshihiro503 さんは少なくとも僕から見ると Coq Master なので、そんな人が近くにいるのはとても幸運ですね。

以下はそのまとめ。あくまで僕の理解なので間違っている可能性は大いにあります。

Coq コマンド

coqtop
インタプリタ。"coqtop -l (filename)" でファイルをロードできる。
coqc
コンパイラ。使い方がわからない。
coqide
Coq の統合開発環境。macports で 入らないっぽいので使ったことがない。

Coq での関数の評価

とりあえずインタプリタである coqtop で Coq を使ってみよう。coqtop で "Eval compute in (expression)" と入力すると expression を評価できる。

$ coqtop
Welcome to Coq 8.2 (September 2009)

Coq < Require Import List.

Coq < Eval compute in ((1::nil) ++ (2::3::nil)).
     = 1 :: 2 :: 3 :: nil
     : list nat

Coq <

Coq での関数定義

Coq の文法はみんな大好き OCaml に近いので問題ないですね。Coq で関数を定義するには Definition か Fixpoint を使います。OCaml と対応させると、Definition が let 、Fixpoint が let rec です。試しにリストを連結する関数 append を Coq で定義してみます。

(* 組み込みのリストを使うので List モジュールをインポート *)
Require Import List.

Fixpoint append {A : Type} (xs : list A) (ys : list A) :=
  match xs with
    | nil => ys
    | x::xs => x :: (append xs ys)
  end.

(* append を演算子に *)
Infix "+++" := append (at level 50).

OCaml の文法とは

  • 文末には "." が必要
  • "=" じゃなくて ":="
  • "[]" じゃなくて "nil"
  • "->" じゃなくて "=>"
  • match 文は end で終わる

という点が違います。気をつけてね！

では、関数定義をもう少し詳しくみてみます。OCaml を書いたことのある人から見ると、引数の型を明示しなくてはいけないのはめんどくさいです。つまり以下のように書きたいわけです。

Fixpoint append xs ys :=
  match xs with
    | nil => ys
    | x::xs => x :: (append xs ys)
  end.

試してみます。

$ coqtop -l hoge.v
Welcome to Coq 8.2 (September 2009)
Error during initialization:
Error while reading hoge.v:
File "/Users/sho/tmp/hoge.v", line 3, characters 0-98:
Error: Cannot infer an internal placeholder of type "Type".
$

残念。Coq は型の表現力を高めたために型推論ができないそうです。素直に引数の型を書きます。

Fixpoint append (xs : list A) (ys : list A) :=
  match xs with
    | nil => ys
    | x::xs => x :: (append xs ys)
  end.

$ coqtop -l hoge.v
Welcome to Coq 8.2 (September 2009)
Error during initialization:
Error while reading hoge.v:
File "/Users/sho/tmp/hoge.v", line 3, characters 27-28:
Error: The reference a was not found in the current environment.
$

残念。A への参照が突然現れたので怒っています。そこで A を引数に取るようにします。A は型変数なので以下のようになります。

Fixpoint append (A : Type) (xs : list A) (ys : list A) :=
  match xs with
    | nil => ys
    | x::xs => x :: (append xs ys)
  end.

$ coqtop -l hoge.v
Welcome to Coq 8.2 (September 2009)
Error during initialization:
Error while reading hoge.v:
File "/Users/sho/tmp/hoge.v", line 6, characters 28-30:
Error:
In environment
append : forall (A : Type) (xs ys : list A), ?1
A : Type
xs : list A
ys : list A
x : A
xs0 : list A
The term "xs0" has type "list A" while it is expected to have type 
"Type".
$

残念。そろそろ萎えてきますね。append の引数に型を取ることにしたので、append を再帰呼び出しするときに型も渡す必要があります。つまり

Fixpoint append (A : Type) (xs : list A) (ys : list A) :=
  match xs with
    | nil => ys
    | x::xs => x :: (append A xs ys)
  end.

$ coqtop -l hoge.v
Welcome to Coq 8.2 (September 2009)

Coq < Eval compute in (append nat (1::nil) (2::3::nil)).
     = 1 :: 2 :: 3 :: nil
     : list nat

Coq <

ようやくうまくいきました。ただ、append を使うときに毎回リストの中身の型を渡してやるのはめんどくさいですね。最近の Coq では、限定的に型推論が可能だそうで、これを利用すると以下のようになります。

Fixpoint append {A : Type} (xs : list A) (ys : list A) :=
  match xs with
    | nil => ys
    | x::xs => x :: (append xs ys)
  end.

"{" と "}" で囲まれた引数は省略が可能になります。これが冒頭の append の定義です。

$ coqtop -l hoge.v
Welcome to Coq 8.2 (September 2009)

Coq < Eval compute in (append (1::nil) (2::3::nil)).    
     = 1 :: 2 :: 3 :: nil
     : list nat

Coq <

Coq での関数と証明

関数が定義できたので、次はその関数が満たすであろう性質を記述し、それを証明します。あの有名な Curry-Howard 対応によると、型とその実装は、命題とその証明に対応するんだそうな。これを利用して、Coq では証明したい性質を型で定義します。

Theorem AssociativityOfAppend :
  forall {A : Type} (x y z : list A),
  (x +++ y) +++ z = x +++ (y +++ z).

この AssociativityOfAppend は、名前と内容が ":" で区切られているので型の定義の形をしています。"AssociativityOfAppend" が変数名で、この変数は "forall ... (y+++z)."という型を持っています。ちなみに "=" 演算子の型は "forall A : Type, A -> A -> Prop" で、"forall A : Type, A -> A -> bool" ではありません。

証明は、このような型を持つ値(λ式)を記述することで行います。Coq では証明をλ式で表すので、引数に証明を取る関数を定義することもできます。こちらのほうがエレガントらしいのですが、証明と関数の定義がごちゃまぜになってしまってわかりにくくなってしまいます。少なくとも初心者のうちは、関数の実装と性質の証明を別々に行うのがいいそうです。

次の節からは coqtop による対話的な証明のやりかたについて説明します。

これまでのソースコードは以下。

Require Import List.

Fixpoint append {A : Type} (xs : list A) (ys : list A) :=
  match xs with
    | nil => ys
    | x::xs => x :: (append xs ys)
  end.
Infix "+++" := append (at level 50).

Theorem AssociativityOfAppend :
  forall {A : Type} (x y z : list A),
  (x +++ y) +++ z = x +++ (y +++ z).

coqtop で使えるコマンド

coqtop は Coq のインタプリタです。coqtop に対する命令は大文字で始まります。例えば以下のような命令があります。

Print
値の定義を出力する
Coq < Print nil.
Inductive list (A : Type) : Type :=
    nil : list A | cons : A -> list A -> list A

For nil: Argument A is implicit and maximally inserted
For cons: Argument A is implicit
For list: Argument scope is [type_scope]
For nil: Argument scope is [type_scope]
For cons: Argument scopes are [type_scope _ _]

Coq <
Check
式の型を出力する
Coq < Check 0.
0
     : nat

Coq <
Eval
式を評価する
Coq < Eval compute in 1+2.
     = 3
     : nat

Coq <
Locate
修飾子付きの名前を返す。演算子から関数の名前を調べるときにも使う
Coq < Locate nil.
Constructor Coq.Lists.List.nil

Coq < Locate "=".
Notation            Scope     
"x = y :> A" := eq x y         : type_scope
                      (default interpretation)
"x = y" := eq x y    : type_scope
                      (default interpretation)


Coq <
SearchPattern
パターンを指定してタクティックを検索する
Coq < SearchPattern (_ < S _).
Lt.le_lt_n_Sm: forall n m : nat, n <= m -> n < S m
Lt.lt_n_Sn: forall n : nat, n < S n
Lt.lt_S: forall n m : nat, n < m -> n < S m
Lt.lt_n_S: forall n m : nat, n < m -> S n < S m
Lt.lt_O_Sn: forall n : nat, 0 < S n

Coq <
Show
証明モードのときに使える命令で、証明の仮定とゴールを表示する
AssociativityOfAppend < Show.
1 subgoal
  
  ============================
   forall (A : Type) (x y z : list A), (x +++ y) +++ z = x +++ (y +++ z)

AssociativityOfAppend <
Undo
証明モードのときに使える命令で、直前の動作を取り消します。
AssociativityOfAppend < intros.
1 subgoal
  
  A : Type
  x : list A
  y : list A
  z : list A
  ============================
   (x +++ y) +++ z = x +++ (y +++ z)

AssociativityOfAppend < Undo.
1 subgoal
  
  ============================
   forall (A : Type) (x y z : list A), (x +++ y) +++ z = x +++ (y +++ z)

AssociativityOfAppend <

タクティック

coqtop にまだ証明されていない定理を記述したファイルを読み込ませると、証明モードに入ります。証明モードでは、タクティックと呼ばれる規則を使って式を変形しながら証明を行います。タクティックは小文字で始まります。以下によく使うタクティックの一部を紹介します。タクティックは数が多いので、必要に応じて調べるのが基本だそうです。

intro
ゴール(証明したいこと)から仮定を1つ取り出す
AssociativityOfAppend < Show.
1 subgoal
  
  ============================
   forall (A : Type) (x y z : list A), (x +++ y) +++ z = x +++ (y +++ z)

AssociativityOfAppend < intro H.
1 subgoal
  
  H : Type
  ============================
   forall x y z : list H, (x +++ y) +++ z = x +++ (y +++ z)

AssociativityOfAppend <
intros
intro を繰り返し実行してすべての仮定を取り出す
AssociativityOfAppend < Show.
1 subgoal
  
  ============================
   forall (A : Type) (x y z : list A), (x +++ y) +++ z = x +++ (y +++ z)

AssociativityOfAppend < intros.
1 subgoal
  
  A : Type
  x : list A
  y : list A
  z : list A
  ============================
   (x +++ y) +++ z = x +++ (y +++ z)

AssociativityOfAppend <
simpl
式をβ簡約する(評価する)。 "simple" ではないので注意
AssociativityOfAppend < Show x.
2 subgoals
  
  A : Type
  y : list A
  z : list A
  ============================
   (nil +++ y) +++ z = nil +++ (y +++ z)

subgoal 2 is:
 ((a :: x) +++ y) +++ z = (a :: x) +++ (y +++ z)

AssociativityOfAppend < simpl.
2 subgoals
  
  A : Type
  y : list A
  z : list A
  ============================
   y +++ z = y +++ z

subgoal 2 is:
 ((a :: x) +++ y) +++ z = (a :: x) +++ (y +++ z)

AssociativityOfAppend <
induction
帰納法による証明を行う。ゴールが基底と帰納の2つに増える。
AssociativityOfAppend < induction x.
2 subgoals
  
  A : Type
  y : list A
  z : list A
  ============================
   (nil +++ y) +++ z = nil +++ (y +++ z)

subgoal 2 is:
 ((a :: x) +++ y) +++ z = (a :: x) +++ (y +++ z)

AssociativityOfAppend <
apply
仮定や定理を使って式全体の書き換えを行う




rewrite


仮定や定理を使って式の一部分の書き換えを行う


AssociativityOfAppend < Show.
1 subgoal
  
  A : Type
  a : A
  x : list A
  y : list A
  z : list A
  IHx : (x +++ y) +++ z = x +++ (y +++ z)
  ============================
   a :: (x +++ y) +++ z = a :: x +++ (y +++ z)

AssociativityOfAppend < rewrite IHx.
1 subgoal
  
  A : Type
  a : A
  x : list A
  y : list A
  z : list A
  IHx : (x +++ y) +++ z = x +++ (y +++ z)
  ============================
   a :: x +++ (y +++ z) = a :: x +++ (y +++ z)

AssociativityOfAppend < 




reflexibity


式の左辺と右辺が完全に同じときに式を閉じるときに使う


AssociativityOfAppend < Show.      
1 subgoal
  
  A : Type
  a : A
  x : list A
  y : list A
  z : list A
  IHx : (x +++ y) +++ z = x +++ (y +++ z)
  ============================
   a :: x +++ (y +++ z) = a :: x +++ (y +++ z)

AssociativityOfAppend < reflexivity.
Proof completed.

AssociativityOfAppend < 





    
coqtop による対話的な証明

    
AssociativityOfAppend を証明してみよう。
まず始めに coqtop を起動します。


$ coqtop -l hoge.v
Welcome to Coq 8.2 (September 2009)
Show コマンドを使って証明すべき定理の確認をします。


AssociativityOfAppend < Show.
1 subgoal
  
  ============================
   forall (A : Type) (x y z : list A), (x +++ y) +++ z = x +++ (y +++ z)
次に Proof コマンドを実行します。 id:yoshihiro503 さんによれば、「これから証明をするぞ！」という意気込みを表現するために必ず必要なものだそうです。実は省略が可能です。


AssociativityOfAppend < Proof.
intros タクティックを使って、ゴールの式から仮定をはぎとります。


AssociativityOfAppend < intros.
1 subgoal
  
  A : Type
  x : list A
  y : list A
  z : list A
  ============================
   (x +++ y) +++ z = x +++ (y +++ z)
リストは再帰的なデータ構造なので、構造に関する帰納法が使えます。induction タクティックを使ってリスト x の構造に関する帰納法による証明を試みます。


AssociativityOfAppend < induction x.
2 subgoals
  
  A : Type
  y : list A
  z : list A
  ============================
   (nil +++ y) +++ z = nil +++ (y +++ z)

subgoal 2 is:
 ((a :: x) +++ y) +++ z = (a :: x) +++ (y +++ z)
"2 subgoals" という文字列が見えます。x の構造に関する帰納法なので、 x が nil の場合(基底)と、x が a::x の場合(帰納)の2つの場合について証明を行う必要があります。証明すべき式が2つになったので、2つめのゴールが現れました。
1つめのゴールは "(nil +++ y) +++ z = nil +++ (y +++ z)" です。 nil と y の append は簡約できそうですよね。 simpl タクティックを使ってみます。


AssociativityOfAppend < simpl.
2 subgoals
  
  A : Type
  y : list A
  z : list A
  ============================
   y +++ z = y +++ z

subgoal 2 is:
 ((a :: x) +++ y) +++ z = (a :: x) +++ (y +++ z)
append の定義から nil と y を append した結果が y になりました。同様に、nil と (y++z) を append した結果が (x++y) になりました。ゴールの左辺と右辺が明らかに同じものになったので、 reflexivity タクティックを使います。


AssociativityOfAppend < reflexivity.
1 subgoal
  
  A : Type
  a : A
  x : list A
  y : list A
  z : list A
  IHx : (x +++ y) +++ z = x +++ (y +++ z)
  ============================
   ((a :: x) +++ y) +++ z = (a :: x) +++ (y +++ z)
基底段階の証明が完了したのでゴールが1つになりました。次は帰納段階の証明を行います。帰納段階の証明なので、帰納法の仮定(IHx : Induction Hypothesis x) が仮定に増えています。
"(a :: x) +++ y" は append の簡約が行えそうなので simpl タクティックを使ってみます。


AssociativityOfAppend < simpl.
1 subgoal
  
  A : Type
  a : A
  x : list A
  y : list A
  z : list A
  IHx : (x +++ y) +++ z = x +++ (y +++ z)
  ============================
   a :: (x +++ y) +++ z = a :: x +++ (y +++ z)
a が両辺の頭にでてきました。a の後ろをよく見ると、帰納法の仮定がそのまま使えそうなことに気がつきます。rewrite タクティックを使って式の一部を書き換えます。


AssociativityOfAppend < rewrite IHx.
1 subgoal
  
  A : Type
  a : A
  x : list A
  y : list A
  z : list A
  IHx : (x +++ y) +++ z = x +++ (y +++ z)
  ============================
   a :: x +++ (y +++ z) = a :: x +++ (y +++ z)
これで両辺の式が一致しました。reflexivity タクティックを使います。


AssociativityOfAppend < reflexivity.
Proof completed.
すべてのゴールが証明されたので、無事に定理 AssociativityOfAppend の証明が完成しました。仕上げに Qed コマンドを実行して証明を出力します。


AssociativityOfAppend < Qed.
intros.
induction x.
 simpl in |- *.
 reflexivity.
 
 simpl in |- *.
 rewrite IHx in |- *.
 reflexivity.
 
AssociativityOfAppend is defined

Coq <