Monad

Coqのお勉強をしたくて出席してきました！ 非常〜にわかりやすいチュートリアルで、おかげさまで概要がわかるようになりました。やはりこういう抽象的な内容は、文章より実際にレクチャーして頂いた方が掴みやすいですね。

Coq入門(+α) / @tmiya_ さん

形式手法とは

• 形式手法は色々ある
  • 自然言語ではなく、機械的検証可能な記述
  • 仕様アニメーション(Lightweight FM)
  • 定理証明系 → 実装を証明する or 証明からコードを生成する
• 形式手法2.0
  • ハードの向上で、実用的に
  • 知識の普及
  • 正しさへの関心
  • スーツにもギークにも流行。組み込み系で特に。
• 定理証明系とは？
  • 正しいもの(enumや自然数、公理)+正しい組合せ規則(自然演繹)
  • カリーハワード対応。正しい定理⇔正しいプログラム
  • ユニットテストでは得られないレベルの「正しい」
• 証明はラクラク!(多少脚色ありｗ)
  • 30分程度のチュートリアルで十分
  • ユニットテストもそこまで簡単ではないよね？
  • 計算機によるレビューと考える。計算機への説明責任。
  • 定理証明系の動作は大昔より軽快
• Domain Specific Languages
  • 読み書きが楽
  • 機能制限=安全性
• DSLの正しさをCoqで証明
  • AURA : 認可・監査論理 →「誰は何をしてもよい」をコンパイル時に保証
  • 金融商品用
    • SECがPython使うって言ってるけどなんで？
    • FpMLはXML。仕様変更に弱い
    • 証明付きDSL使った方がいいじゃん
• 形式手法のまとめ
  • 最近注目を浴びている
  • 仕様検証以外にも使える

Coq入門

• 形式手法の比較
  • モデル検査: 手軽。状態爆発が起こる
  • 対話的定理証明: 訓練は必要。証明出来るものすべてに利用可。実装と直結。
• Coq
  • 対話的定理証明のための言語処理系
  • Ocamlで記述。CIC(Calculus of Inductive Construction)
  • 高階述語論理で記述。"tactic" により、証明を構成
  • 機械的検証が可能。人間も検証が可能。
  • OCaml, Haskell, Scheme のプログラムの自動生成
• 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は直観論理なので、排中律は成り立たない
  • 「a^bが有理数になるような無理数がある」の証明。排中律を使っているが、実際の値を求めることができない
  • 公理と推論規則を利用
• 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で関数と証明を扱う場合は？
  1. 関数を書き、定理を作って証明する
  2. 関数を書き、それをラップした証明付きの関数を定義する
  3. 証明から直接関数を定義
  4. refineを使って、証明を後回しにする
• 今日やらなかったとこ
  • 自動証明のコマンドが楽(autoとかringとかmegaなど)
    • ただし、生成される関数は複雑になる
  • 各種ライブラリ
  • Haskell, OCamlのコードの生成
  • tacticの開発
  • 型クラス、Module
  • 名古屋のProofCafeとか、RubyとかJSとかSchemaとかの生成
  • Coq Standard Library
  • 「Twitter, MLとかで質問もらえれば、サポートします！」

懇親会

Coqでゴルフ → Anarchy Proof

合わせて読みたい

• [Formal Methods]4/23 第15回 Formal methods 勉強会 by kencobaさん