Coq庵
8/29 に、Coq庵 に行ってきました。
資料等はこちら。
行き道で祭りやってた。
一部道が通れなかったりして、少し迷うなど。
- 初めてのCoq
- 仕様記述言語
- Coq の特徴
- Coq の中身
- 関数型プログラム的
- Vernacularコマンド (プログラムの文)
- Gallina式 (プログラムの式)
- 内部はラムダ式
- 論理学的
- tactic
- 証明、証明を含む式
- 小文字で始まって . で終わる
- tactic
- 関数型プログラム的
- Coq のプログラム
- Coq で書かれたプログラム
- Coq 習得の道
- 更に熟練するには
- CPDT (Certified Program with Dependent Types)
- Coq'Art
- その他 Curry-Howard 対応や型理論など
- 勉強会会に参加しよう
- ProofCafe(栄)
- Formal Method 勉強会
- Coq による暗号アルゴリズムの実装の暗号学的安全性検証
- 暗号プログラムの安全性検証の必要
- 暗号学的安全性の検証は行われていない
- 不具合が発見された場合の社会的・経済的影響が大きい
- → 暗号アルゴリズムの安全性検証とプログラム(実装)の検証
- 疑似乱数生成期 BBS (Blum Blum Shub) の実装の安全性検証
- ゲーム列による安全性証明
- システムと攻撃者の挑戦としてモデル化
- 実装の正しさの検証
- ホーア論理、操作的意味論、etc.
- Coqを用いた形式化
- Inductive 内の :> は展開になる
- 暗号プログラムの安全性検証の必要
- にわとりかんさつにっき in お茶大
- 浅井先生の研究室のお話
- Coq 使い多い (8人中 6人)
- Coq ゼミ
- 2008年にあった
- http://pllab.is.ocha.ac.jp/lab.html
- 「型 = 命題、プログラム = 証明」
- Coq 楽しそう
- プログラム書いてテストケース通っても、それがちゃんと正しいかは分からない
- Coq で 証明したら一応安心できるかな
- プログラム書いてテストケース通っても、それがちゃんと正しいかは分からない
- 証明に良さそう
- 手で書く証明よりも間違いがなくて良さそう
- ICFP 2009 B.C.Pierce の招待講演
- http://www.cis.upenn.edu/~bcpierce/sf/
- 基礎から、いろいろまである
- 全部やろうとすると 2 ヶ月くらい Coq 漬けになる
- http://www.cis.upenn.edu/~bcpierce/sf/
- CPS変換
- 「継続渡し形式」ってのに変換する
- 状態を取って処理の続きをやる関数 を引数に渡す
- 「継続渡し形式」ってのに変換する
- 非関数化
- CPSで渡してた関数を、データ構造にする
- CPS変換・非関数化の正当性
- CPS変換 + 非関数化の正当性 (fibonacci)
- 結構複雑になる
- shift/reset
- 継続のオペレータ
- 浅井先生の研究室のお話
- 一般たらいまわし関数の停止性を証明する
- たらい回し関数の定義
- t(x,y,z) := if x <= y then y else t(t(x-1,y,z), t(y-1, z, x), t(z-1, x, y))
- 複雑な再帰
- 停止性が問題
- 深さ制限付きたらい回し関数
- カウントを付ける
- t_n(x,y,z) := if x <= y then y else t_{n-1}(t_{n-1}(x-1,y,z), t_{n-1}(y-1, z, x), t_{n-1}(z-1, x, y))
- t_0(x,y,z) = ⊥ (bottom)
- 停止性
- 整数 x, y, z に対して停止する : ∃n, t_n(x, y, z) ≠ ⊥
- 一般たらいまわし関数
- 引数が増える
- Coq で表現
- ⊥を加えた整数型
- option Z で表現
- Some x が計算完了 (以下 Vx)
- None が 未完了 (以下 B)
- ⊥を加えた整数型
- 深さ制限付き再帰
- 皆さんよく知ってる Y コンビネータ
- Yn O init recur = init
- Yn (S n) init recur = recur (Yn n init recur)
- 普通の Y は、Y f = f (Y f)
- 皆さんよく知ってる Y コンビネータ
- 再帰制限付きたらい回し関数 (ntarai)
- ntarai n v = Yn n ntarai_init ntarai_recur
- ntarai_init x = B
- ntarai_recur f (Vx Vy v) = ...
- ntarai_recur f _ = B
- 最初に証明したいこと
- 深さ n で停止したら、n 以上の m でも n で停止する
- forall n m v x, ntarai n v = V x -> n <= m -> ntarai m v = V x
- bottom が出てきた場合、計算経過が異なることが
- bottom を値に書き換えても結果は変わらないことを証明
- f ⊥ = V a -> ∀x, f x = V a
- 美しくない
- x = y ∨ x = ⊥ -> f x = f y ∨ f x = f ⊥
- 対称になった!
- f ⊥ = V a -> ∀x, f x = V a
- R x y := x = y ∨ x = ⊥ とすると、R は半順序 (x ≪ y)
- 証明したいこと:x ≪ y -> f x ≪ f y
- f は単調増加
- 多変数関数の場合
- [xi] ≪ [yi] <-> forall i, xi ≪ yi
- リストで与える
- 連続な関数の合成は連続
- Coq で順序を定義する
- le を定義
- dZ, list dZ, list (list dZ) の le はそれぞれ違う関数
- 型クラスを使おう!
- dZ, list dZ, list (list dZ) の le はそれぞれ違う関数
- le を定義
- 型クラス
- たらい回し関数の定義
- Coq でガベージコレクションの証明
- コードはgithubに
- マーク & スイープ GC
- GC アルゴリズム3人衆の中で最弱
- マークフェーズ
- ルートから辿れるオブジェクトにマークを付ける
- スイープフェーズ
- マークのついてないオブジェクトを回収し、マークを外す
- GCは完全でなければならない
- トレース漏れ = 不良GC
- 生存中のオブジェクトを削除してしまう (バグ)
- アルゴリズムはホントに正しいか
- アルゴリズムが正しくても、ちゃんと実装できているか
- そこで Coq です!
- トレース漏れ = 不良GC
- Coq でプログラムを書く → 証明する → OCaml 等に変換して実行する
- メモリのモデル化
- Record で表現
- Coq には3種類の集合モジュールがある
- Ensembles, ListSet, FSet
- ルートから辿れるオブジェクトの探索
- 普通に書くと停止性が保証できない
- 未探索のオブジェクトの集合を引数にもらって、停止性を保証する
- 呼び出し毎に必ず減少するので、停止性が保証できる
- 安全なGC
- フリーリストと使用中のメモリに重複がない
- 初期状態はSafety
- SafetyなメモリをGCしてもSafety
- Coq → OCaml
- ペアプルービング
- anarchy proof
- bleis と youku_s と 3 人でトリオプルーピング
- Require Import Definitions. で迷うなど
最初はこんな感じで書いて、
Theorem Modus_ponens: forall (P Q: Prop), (P -> Q) -> P -> Q. Proof. intros P Q. (* forall のところの P Q が Prop だよってのを前提へ *) intro H. (* (P -> Q) -> P -> Q の (P -> Q) を H として前提へ *) intro p. (* P -> Q の P を p をして前提へ *) apply H. (* ゴール Q、前提 H (P -> Q) から、ゴールを P に *) exact p. (* ゴール P 、それは前提 p にある *) Admitted.
2人にまったりと解説のようなものをしてみる。
で、auto ってのがあるよって、
Theorem Modus_ponens: forall (P Q: Prop), (P -> Q) -> P -> Q. Proof. auto. (*`・ω・´*) Admitted.
Require Import Classical. Theorem Peirce: forall (P Q: Prop), ((P -> Q) -> P) -> P. Proof. intros P Q. intro H0. elim (classic P). intros p. exact p. intro p1. apply H0. intro p2. elim p1. exact p2. Admitted.
classic ってのが、Coq.Logic.Classical_Prop にあって、
Axiom classic : forall P:Prop, P \/ ~ P.
こんな感じになってる。
古典論理の排中律。
Theorem sqrt_2: forall (n m:nat), n*n = 2*m*m -> m = 0. Proof. intros n m H0. destruct m. reflexivity. (*´・ω・`*) Admitted.
こういうのって Coq だと難しめ?
まだ自分には分からなかった (´・ω・`)
Axiom Falso: False. Fixpoint pow a n := match n with | O => 1 | S m => a * pow a m end. Theorem Fermat's_Last_Theorem: forall (a b c n: nat), n > 2 -> pow a n + pow b n = pow c n -> a = 0 /\ b = 0 /\ c = 0. Proof. elimtype False. exact Falso. Admitted.
elimtype False. でゴールを False にできるらしい。
(他の人の見ると apply False_ind. が普通?)
てか、この場合前提に False があるので、case Falso. でいいらしい。
Theorem Fermat's_Last_Theorem: forall (a b c n: nat), n > 2 -> pow a n + pow b n = pow c n -> a = 0 /\ b = 0 /\ c = 0. Proof. case Falso. Admitted.
(Coq 証明事例集: 前提が……のとき 参考にさせてもらいました)
Axiom Peirce: forall (P Q: Prop), ((P -> Q) -> P) -> P. Theorem Excluded_Middle: forall (P: Prop), P \/ ~P. Proof. intro P. (*Д*) Admitted.
時間切れ。
- ToDo 的な
- あなぷる 4. Converse Peirce の続き
- Software Foundations 読む
- Introduction to generalized type systems 読む (ラムダキューブ、*:□)
- Coq りさん再挑戦