Pixel Pedals of Tomakomai

北海道苫小牧市出身の初老の日常

第15回FormalMethods勉強会に行ってきた

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

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

形式手法とは
  • 形式手法は色々ある
    • 自然言語ではなく、機械的検証可能な記述
    • 仕様アニメーション(Lightweight FM)
    • 定理証明系 → 実装を証明する or 証明からコードを生成する
  • 形式手法2.0
    • ハードの向上で、実用的に
    • 知識の普及
    • 正しさへの関心
    • スーツにもギークにも流行。組み込み系で特に。
  • 定理証明系とは?
    • 正しいもの(enum自然数、公理)+正しい組合せ規則(自然演繹)
    • カリーハワード対応。正しい定理⇔正しいプログラム
    • ユニットテストでは得られないレベルの「正しい」
  • 証明はラクラク!(多少脚色ありw)
    • 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

合わせて読みたい