%なぜCoqが重要か
%@yoshihiro503
%平成26年4月29日
なぜCoqが重要か
結論
- 最強のプログラム検証器
- 最強の関数型言語
最強のプログラム検証器
Coqは最強の表現力を持つ仕様記述言語を使う
- 仕様記述言語は検証したいこと を記述するための言語
- 表現力は検証器によって全然違う
- 表現できる範囲が、検証器の限界
- Coqのそれは高階述語論理 ← 最強
最強のプログラム検証器
Coqを使うためにはPhDが必要?
- 高校生でも練習すればできる (c.f. プログラミングCoq)
最強のプログラム検証器
証明を人間が与えるのが大変？
- タクティックによる自動化はOCamlでいくらでも可能
- 型チェッカはタクティックと独立なので安全
- 既にomegaなどの自動証明アルゴリズムを実装したタクティックあり
最強の関数型言語
Coqは(型の表現力が)最強の関数型言語
- 型の表現力が最強
- 型推論は完全ではない
- 停止性は保証しなければならない
注意: ここでの関数型言語とは
(ラムダ計算を基礎とした)(静的型付き)関数型(プログラミング)言語
Coqのインストール
Unix系 ソースからインストール
- OCaml, camlp5必要
- ./configure; make world; make install
Debian系
- apt-get install coq
opamユーザー
- opam install coq
Coqのインストール
Windows, Mac OS X
- バイナリ(CoqIDE付属)
- Linux VMを入れる
Coqを使う
- 拡張子は.v
- 大文字で始まるのがCoqコマンド(Vernacular)
(例: Definition, Theorem, Require Import) - 小文字で始まるのがタクティック
(例: intros, omega, destruct, rewrite)
一覧: http://coq.inria.fr/distrib/current/refman/
Coqの基本
Coqではいろんなモノが式
- 数値、文字列、if式、match式
- 関数
- 型
- 論理式(仕様)
- 証明
Coqで証明するという事
「ある論理式PをCoqで証明する」 ≡ 「(a : P)となる式aを見つける」
☆ a をPの証明と呼ぶ
Coqで証明するという事
例えば、
「任意のf, xsについて、(map f xs)の長さとxsの長さは同じ」
を証明するためには
??? : forall f xs, length (map f xs) = length xs
となる式を見つければよい。
fun (A B : Type) (f : A -> B) (xs : list A) =>
list_ind (fun xs0 : list A => length (map f xs0) = length xs0) eq_refl
(fun (_ : A) (xs0 : list A) (IHxs : length (map f xs0) = length xs0) =>
eq_ind_r (fun n : nat => S n = S (length xs0)) eq_refl IHxs) xs
Coqで証明するという事
実際はタクティックを試しながら、対話的にゴールを変形していく。
Theorem map_length: forall A B:Type f xs,
length (map f xs) = length xs.
Proof.
intros A B f xs. induction xs.
reflexivity.
simpl. rewrite IHxs. reflexivity.
Qed.