Coqのお勉強をしたくて出席してきました！ 非常〜にわかりやすいチュートリアルで、おかげさまで概要がわかるようになりました。やはりこういう抽象的な内容は、文章より実際にレクチャーして頂いた方が掴みやすいですね。
Coq入門(+α) / @tmiya_ さん
形式手法とは
Coq入門
- 形式手法の比較
- モデル検査: 手軽。状態爆発が起こる
- 対話的定理証明: 訓練は必要。証明出来るものすべてに利用可。実装と直結。
- Coq
- Coqを使う
- coqtopが対話環境。コマンドの最後にはピリオド。
- 空白が省略できない部分もある
- 型は推論。ただし、スコープによって2はnatか整数か変わる
- Definition, Check, Eval compute in, Inductive などなど
- ;を使うと、サブゴールすべてに対して実行できる(例:destruct b1; destructb2.)
- 練習: 3値論理のドモルガン則
- nat: peanoの自然数。0はOのこと。3は(S (S (S O)))のこと。
- 再帰関数の定義はDefinitionではなく「Fixpoint」
- 停止性の保証が必要。{struct n}。推論させることも可能。
- 定理証明系へのよくある誤解
- 「(すべてのプログラムに対して)チューリングマシンの停止性を判定することは出来ない」
- ・・・が、Coqでは停止性が保証されたプログラムのみ受理
- ライスの定理「(すべてのプログラムに対して)仕様を満たすか判定することは出来ない」
- ・・・が、Coqで仕様を満たすことが判定された物は、当然仕様を満たす
- 「(すべてのプログラムに対して)チューリングマシンの停止性を判定することは出来ない」
- Coqでは任意の割り算を定義するのは難しい (停止性の保証が難しい)
- {}で定義をすると、型推論させられる: 例: {A:Set}
- @関数名 と呼び出すと、型も明示的に指定できる(cond false 2 3 を @cond nat false 2 3 と書ける)
- @nil とかは使うらしい
- option型 : null値、Maybe のように値がないことを示す。
- sumor型 : option型と同様だが、ない理由の証明も返せる
- prod A B は A * B と書く。直積。
- (x , y , z ...) は (pair .. (pair (pair x y) z)..) のこと
- sum A Bは直和。
- cons は :: と書く
- 末尾再帰にこだわると、証明が難しくなるので注意が必要
- Coqは直観論理なので、排中律は成り立たない
- tacticを覚える必要がある(200個くらいあって結構ダブってるらしい!!)
- assumption(trivial, exact(仮定だけじゃなく既存の定理へも使える)) → 仮定から
- apply → ⊂E
- intro, intros → ⊂I
- destruct pq as [p q], split → ∧I
- destruct pq as [p|q], left, right → ∨I_L, ∨I_R
- ¬XはX→⊥なので、introする。
- elim → ¬E
- 二重否定が除去できないので、¬が入った定理は使いにくい
- Curry-Howard対応
- 証明はexactで直接与えてもよい
- Coqは型チェックをしているに過ぎない
- つまり、(命題論理であれば)Javaでも同じことができる。Coqは対話的に支援をしてくれているだけ
- 述語論理 → 量化子∃∀を用いた記述
- Coqは高階もサポート(∀P:A→Prop 述語)
- forall についてはintro
- exists についてはdestruct。exists で具体的な値を与える
- 述語eq(=) → 型が等しい、コンストラクタが等しい、コンストラクタ引数が等しい
- reflexivity → 同値の公理
- simpl → 項を展開して簡単にするが、困ることもあるので注意
- reflexivityは、内部で勝手にsimpleを呼ぶ。
- n+0 は simplで展開不可 → 帰納法の利用
- induction n as [|n']。内部的にはnat_ind という定理が使われる。
- 帰納法はlist Aなどにも利用できる
- rewrite->(rewrite),rewrite<- → 代入
- SearchAbout xxxx. → 関連する定理の検索
- 無闇にintroしない方がよい。
- forall が具体化されて、帰納法の仮定が弱くなってしまう。
- 慣れてくるとintroはしなくなる
- Lemma と Theorem は Coqでは同じ
- 引数と戻り値に条件をつけて定義 : Definition sub(m n:nat)(H:le n m) : {x:nat|x+n=m}
- 引数は n < m、戻り値xは x + n = m
- 定義すると証明が始まる。最後にDefined.とすると関数が定義される(Qed.としてはダメ)
- 仕様を満たす関数が完成する
- 利用するときは、le 2 5 というTheorem が必要
- generalize dependent → ∀E
- eapply → 自動引数を推測してapplyする
- assert → 新しいゴールを設定する
- Coqで関数と証明を扱う場合は？
- 関数を書き、定理を作って証明する
- 関数を書き、それをラップした証明付きの関数を定義する
- 証明から直接関数を定義
- refineを使って、証明を後回しにする
- 今日やらなかったとこ
- 自動証明のコマンドが楽(autoとかringとかmegaなど)
- ただし、生成される関数は複雑になる
- 各種ライブラリ
- Haskell, OCamlのコードの生成
- tacticの開発
- 型クラス、Module
- 名古屋のProofCafeとか、RubyとかJSとかSchemaとかの生成
- Coq Standard Library
- 「Twitter, MLとかで質問もらえれば、サポートします！」
- 自動証明のコマンドが楽(autoとかringとかmegaなど)
懇親会
Coqでゴルフ → Anarchy Proof
合わせて読みたい
- [Formal Methods]4/23 第15回 Formal methods 勉強会 by kencobaさん
