証明補助coqを使ってみる

練習題材としてSTLC(Simple Typed Lambda Calculus)を使うことにした。


以下は、このSTLC.vが読めるようになるまでの布石。

まずはcoqの基本的な使い方から。
coq自体の参考は、 http://www.win.tue.nl/~fdechesn/2IF48/ にある"Coq in Hurry".


対話シェルcoqtopはコマンド履歴に対応していないので、leditかrlwrap経由で起動すると使いやすくなる。

こういうツールが複雑に見えるのは、入力コマンドに種類がいろいろあってそれが同じように使われることもひとつの理由だろう。
定義のためのコマンド、証明のためのコマンド、表示のためのコマンドなどを区別してみると少しはわかりやすくなるかも。

coqtopの頻出コマンド

  • Check 〜
    • 式の型を表示
Coq < Check True.
True
     : Prop
  • Locate パターン文字列
    • 構文糖などの展開対応を表示
Coq < Locate " <> ".
Notation            Scope
"x <> y  :> T" := not (eq x y) : type_scope
                      (default interpretation)
"x <> y" := not (eq x y)       : type_scope
                      (default interpretation)
  • Require Import ライブラリ
    • ライブラリの読み込み。パッケージだと/usr/lib/coq/theoriesあたりにいろいろ。
Coq < Require Import List.
  • Print 〜
    • 内容の表示
Coq < Print S.
Inductive nat : Set :=  O : nat | S : nat -> nat
For S: Argument scope is [nat_scope]

証明までのcoqtop対話例

Coq < Theorem ex1: forall a:Prop, a->a.
1 subgoal

  ============================
   forall a : Prop, a -> a

ex1 < auto.
Proof completed.

ex1 < Qed.
auto.
ex1 is defined

Coq < Print ex1.
ex1 = fun (a : Prop) (H : a) => H
     : forall a : Prop, a -> a


Argument scopes are [type_scope _]

Coq <


チュートリアルだと証明が中心だが、実際書く場合は、証明よりもまず型や関数の定義を書くのが普通で、いきなりやろうとするとまずそこで苦労したりする。STLCだと、型とか式とか、環境とか、パターンルールとかの部分にあたる。結局それに対して、ユニークネスとかイクオリティとかを証明していくようだ。

ファイルに保存しながら追加していく

coqtopだけで書きつづけるのはつらいので、定義とかはある程度対話でチェックしながらやって、済んだ部分はファイルに書いてそれをRequire Importしてやるといいようだ。

$ emacs Saved.v
Theorem ex1: forall a : Prop, a -> a.
auto.
Qed.

$ coqc Saved.v
$ ledit coqtop -I . -require Saved
Welcome to Coq 8.1pl3 (Dec. 2007)

Coq < Check ex1.
ex1
     : forall a : Prop, a -> a

Coq <

プログラミングとしてのcoqコーディング

一方プログラムとして証明を利用するという場合、こういった命題論理とかでの証明とは、すこし雰囲気が変わってくる。
プログラミングで利用する場合での証明の基本の例: リストやその関数の定義と、テストとしての証明

(* data MyList *)
Inductive MyList : Set
:= mynil
 | mycons (L R : MyList).

(* mylen mynil = 0; mylen (mycons l r) = 1 + (mylen l) + (mylen r) *)
Fixpoint mylen (ls : MyList) :=
match ls with
    mynil => 0
  | mycons l r => 1 + (mylen l) + (mylen r)
end.

(* Test: size of mylist *)
Theorem size_is_three:
   mylen (mycons (mycons mynil mynil) (mycons mynil mynil)) = 3.
  auto.
Qed.

プログラマー向けの解説として、こういう方面からやってくれたほうが正直ありがたいのだが、実際のところこういう感じでのチュートリアルは少ないというか見たことが無いような。証明対象はプログラム的なデータや処理。証明自体はまずautoで。成功しなかったらそこでデバッグしてくように、すこしずつtacticを広げてく、という風ならいいと思う。いろいろな名前が論理からきてるから説明自体に難がありそうだけど、そういうのはとりあえず無視でその性質の説明だけでも十分なはず。

証明戦略

真にならないコード mylen (mycons mynil mynil) = 3をTheoremにおいて、autoとやっても証明が終わらず（あたりまえだが）、つづけてQedとやるとエラーになる。

証明可能な場合でも複雑なものだと、autoで証明できないものもある。そういう場合は、個別に戦略を適用していくことで、証明できるかもしれない。つかえる戦略には、たとえば、パターンを展開したりとか、関数を適用(ベータ変換)したりとかある。(ここで初めて、チュートリアルの内容が役に立つことに。ただ、前記のようにプログラミング言語の要素に近いものから使うことになる)


LtUで宣伝されてたの。いまは教材があがってる。これはいいかも。

ほかのcoq関連情報