Coq庵

8/29 に、Coq庵 に行ってきました。

資料等はこちら


行き道で祭りやってた。
一部道が通れなかったりして、少し迷うなど。

  • 初めてのCoq
    • 仕様記述言語
      • Prolog
      • ACL2, HOL/Light
        • 完全自動証明
        • 自動で証明してくれるが、表現力がやや低い
      • Isabelle/HOL, Coq, Agda
        • 手動証明
        • 表現力が非常に高い
    • Coq の特徴
      • 高階論理
        • 表現力最強
      • 自動証明機能 (tactic)
        • 対話的に人間が証明を与えるが、部分的に自動証明を使うこともできる
      • プログラムと連携
        • 証明したものをそのまま実行できる
        • OCaml, Haskell, Sheme に出力できる
    • Coq の中身
      • 関数型プログラム的
        • Vernacularコマンド (プログラムの文)
        • Gallina式 (プログラムの式)
          • 内部はラムダ式
      • 論理学的
        • tactic
          • 証明、証明を含む式
          • 小文字で始まって . で終わる
    • Coq のプログラム
      • Vernacular
        • 大文字で始まって . で終わる
        • Fixpoint
        • Theorem
          • 定理の宣言
          • : の後ろに Gallina 式
        • Proof
          • 特に意味はない
            • ここから証明 ってマークに使う
        • Qed
          • ここまでが定理証明
      • tactic
        • 小文字で始まって . で終わる
        • tactic 同士を ; で繋げられる
      • Gallina 式
        • match ... with ... | ...
        • x :: xs
    • Coq で書かれたプログラム
      • 大きいの
        • CAMP
        • coqtail
          • OCaml の任意精度演算モジュール
      • 小さいの
    • Coq 習得の道
      • MLやHaskellを知る
      • 書いてみる、マニュアル、Twitter、Blog
        • 分からなければマニュアル
          • Web上の Reference Manualにコマンドなどの一覧がある
          • コマンドのエイリアスがたくさんある
        • Twitter、Blogで聞いてみる
          • 第一人者的な人が答えてくれるかも
        • Blogで報告
    • 更に熟練するには
      • 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 の招待講演
    • CPS変換
      • 「継続渡し形式」ってのに変換する
        • 状態を取って処理の続きをやる関数 を引数に渡す
    • 非関数化
      • CPSで渡してた関数を、データ構造にする
    • CPS変換・非関数化の正当性
      • 正当性の証明は Coq で
        • 売ら出された喧嘩定理は買い証明しましょう
      • CPS変換の正当性の証明 (factorial)
        • ∀n∈N, fact_ds n = fact_cps n id
          • n で induction すると証明できない
            • 継続が変わっているから
          • id を一般的な形にして証明
          • ∀n∈N, k∈N → N, k (fact_ds n) = fact_cps n k
            • これは n に関する帰納法でいける
      • 非関数化の正当性の証明 (factorial)
        • 先と同様に渡すやつを一般化して帰納法で証明
          • 一部ちょっと制約付ける
    • 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)
    • 再帰制限付きたらい回し関数 (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 ⊥
            • 対称になった!
        • 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 はそれぞれ違う関数
              • 型クラスを使おう!
    • 型クラス
      • Coq 8.2 から
      • Haskell の型クラスとだいたい同じ
      • Coq の型クラスでは、関数に関する要請を指定できる
        • たとえば、Monad クラスに Monad 則を強制したり
        • 実装側でその要請を証明する必要がある
      • Coq の型クラスでは、型に対する実装に名前を付けられる
        • インスタンス定義の外で証明する場合、Defined. で証明を終了する (Qed. だとダメ)
      • 型クラスを要求するときは、型とインスタンス定義を引数に取るようにする
        • 型は省略する記法がある (インスタンス定義の型部分の型にバッククオートを使う)
      • インスタンス定義も、型のように自動推論してくれる
  • Coq でガベージコレクションの証明
    • コードはgithubに
    • マーク & スイープ GC
      • GC アルゴリズム3人衆の中で最弱
      • マークフェーズ
        • ルートから辿れるオブジェクトにマークを付ける
      • スイープフェーズ
        • マークのついてないオブジェクトを回収し、マークを外す
    • GCは完全でなければならない
      • トレース漏れ = 不良GC
        • 生存中のオブジェクトを削除してしまう (バグ)
      • アルゴリズムはホントに正しいか
      • アルゴリズムが正しくても、ちゃんと実装できているか
      • そこで Coq です!
    • Coq でプログラムを書く → 証明する → OCaml 等に変換して実行する
    • メモリのモデル化
      • Record で表現
    • Coq には3種類の集合モジュールがある
      • Ensembles, ListSet, FSet
    • ルートから辿れるオブジェクトの探索
      • 普通に書くと停止性が保証できない
      • 未探索のオブジェクトの集合を引数にもらって、停止性を保証する
        • 呼び出し毎に必ず減少するので、停止性が保証できる
    • 安全なGC
      • フリーリストと使用中のメモリに重複がない
      • 初期状態はSafety
      • SafetyなメモリをGCしてもSafety
    • Coq → OCaml
      • CoqBase を使うと、OCaml のライブラリを使ってくれる
  • ペアプルービング

最初はこんな感じで書いて、

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.

時間切れ。