Coqチュートリアル: @zakky_devさんが証明をできるようになるまで

f:id:mzp:20140629092936j:plain

先日、東京の会社から名古屋の会社に転職された@zakky_devさんの歓迎会がありました*1 。そこで、@zakky_devさんにCoqでリストの結合則を証明するチュートリアルをやってもらいました。

せっかくなので、そのときの台本を公開します。だいたい30分くらいの内容です。

Coqのインストール

ぐぐりましょう。

Coqとは

みなさん、自動化してる・してないなどの違いはあると思うんですが、プログラムを書いたらテストをすると思います。ただテストはどうしても「こういう入力があったら、こういう出力がある」というのを並べていくことになるので、どうしても有限のパターンしか確認できません。

で、これで十分なこともあるんですが、中にはものすごい信頼性がいるプログラムで、有限のパターンの保証だけではたりない場合があります。無限の入力パターンに対しての性質を保証するには数学的なテクニックを使う必要があり、それをできるのがCoqです。

あと実際、Coqで証明してる途中でバグが見つかることは少なくて、Coqで証明するために仕様を深く読んでる途中でバグを発見することも多いです。この前、見付かったOpenSSLのCCS Injectionバグもこういうパターンですね。

三段論法の証明

最初のプログラムといえばHello,worldが定番ですが、Coqでやるのは大変すぎるのでとりあえずは諦めましょう*2。

まずは、論理学のHello,worldこと三段論法を証明します。ソクラテスが死ぬやつです。

Lemma MP: forall zakky_dev 人間 死ぬ,
  (zakky_dev -> 人間) -> (人間 -> 死ぬ) -> zakky_dev -> 死ぬ.

(* zakky_dev, 人間, 死ぬはすべて変数名であり、特定の個人を指す単語ではないです。 *)

-> はimplyとか含意と呼ばれるます。とりあえず「ならば」と意味と思っておけばいいです。

これをCoqに評価させると(注: 環境によって評価方法が違うので適宜がんばる)、証明モードに突入します。

1 subgoals, subgoal 1 (ID 4)


  ============================
   forall zakky_dev 人間 死ぬ : Type,
   (zakky_dev -> 人間) -> (人間 -> 死ぬ) -> zakky_dev -> 死ぬ

さて、ここでこの表示の見方を説明します。

1 subgoals, subgoal 1 (ID 10): 証明すべきもの(goal)がいくつのsubgoalに分割されているか、また今はその何番目を表示しているか
======の上: contextとか呼ばれる。ここには使える前提が記載される。最初なので空っぽ。
======の下: 今のsubgoal。これを証明したい。最初なので定理と同じ形。

あとは前提とsubgoalを変形していって、あきらかに正しい形まで変形できれば証明完了です。あきらかに正しい形というのは、称えば、x = xみたいな右辺と左辺が等しいものや、前提にgoalがでてくるもの、前提がFalseになるものなどですね。

Coqでは前提や結論を変形するにはタクティクス(tactics)というものを使います。これは証明モードだけで使えるコマンドみたいなものです。

A -> Bを証明することと、Aという前提のもとでBが正しいことを証明するのは同じです。なので、その変形をするために introsタクティクスを使います。

1 subgoals, subgoal 1 (ID 10)

  zakky_dev : Type
  人間 : Type
  死ぬ : Type
  X : zakky_dev -> 人間
  X0 : 人間 -> 死ぬ
  X1 : zakky_dev
  ============================
   死ぬ

まずは前提をじっくり眺めます。x : Typeみたいなやつが使えることはめったにないのでとりあえず無視します。

すると使える前提は

X: ざっきーさんならば、人間である
X0: 人間であるならば、死ぬ
X1: ざっきーさんである

の3つでここから「死ぬ」という結論を導ければ証明できます。

結論から前提を導く方針と、前提から結論を導く方針があると思うんですが、とりあえず結論から前提を導きましょう。

X0から「死ぬ」という結論に至るには、まずは「人間である」という結論に至る必要があることがわかります。 A -> Bという前提を結論に適用してAに変形するにはapplyタクティクスを使います。この場合はapply X0ですね。

1 subgoals, subgoal 1 (ID 11)

  zakky_dev : Type
  人間 : Type
  死ぬ : Type
  X : zakky_dev -> 人間
  X0 : 人間 -> 死ぬ
  X1 : zakky_dev
  ============================
   人間

ちょっと進んで、「人間である」まで行けました。次はこれにX0を適用すれば「ざっきーさんである」まではいけそうです。apply Xをやってみましょう。

1 subgoals, subgoal 1 (ID 12)

  zakky_dev : Type
  人間 : Type
  死ぬ : Type
  X : zakky_dev -> 人間
  X0 : 人間 -> 死ぬ
  X1 : zakky_dev
  ============================
   zakky_dev

できましたね。よく見ると結論と同じものが前提に入っています。あとはこれを使えば証明が完了できます。apply X1もしくはtauto、exact X1あたりが使えます。

これで証明完了しました。最後はQedで締めましょう。

appendの定義

ちょっとプログラミングっぽい証明もしましょう。まずはRequire Import List.でリストを使えるようにしてappendを定義しましょう。 OCamlとかHaskell書いてれば、なんとなる分かる文法だと思います。

  Fixpoint append {A : Type} (xs : list A) (ys : list A) : list A :=
    match xs with
    | nil => ys                                                
    | x::xs =>
       x :: append xs ys                                          
    end.

とりあえず中置演算子も定義します。

Notation "x @ y" := (append x y) (right associativity, at level 60).

さて、まずはnilにappendしても変らないことを証明しましょう。

Lemma append_nil: forall A (xs : list A),
  xs @ nil = xs.

とりあえず何も考えずに、introsします。すると、証明すべきものは以下のようになります。

1 subgoals, subgoal 1 (ID 32)

  A : Type
  xs : list A
  ============================
   xs @ nil = xs

これ以上、前提を使って変形はできそうにありません。リストのように構造をもったデータを扱うときは(構造に基づく)数学的帰納法を使うと証明できることが多いです。

数学的帰納法は高校の数学で使ったと思うんですが、簡単に復習しますと

n=1に関する命題が成り立つ
n=kに関する命題が成り立つと仮定したときに、n=k+1に関する命題が成り立つ

の2つを証明すれば任意のnに対して命題が成り立つことを示せる、という証明のテクニックです。

induction xsとやるとこれができます。2つのサブゴールに分かれます。

1つめのサブゴールはこんな感じです。

2 subgoals, subgoal 1 (ID 35)

  A : Type
  ============================
   nil @ nil = nil

@の定義にしたがってちょっと変形できそうです。そういうときはsimplを使います。

2 subgoals, subgoal 1 (ID 40)

  A : Type
  ============================
   nil = nil

x = xという自明な形になりました。これはreflexivityで証明を終われます。

2つめのサブゴールはこんな感じです。IHxsに帰納法の仮定があることに注意してください。

1 subgoals, subgoal 1 (ID 39)

  A : Type
  a : A
  xs : list A
  IHxs : xs @ nil = xs
  ============================
   (a :: xs) @ nil = a :: xs

とりあえず@の定義にしたがって変形するために、simplを使います。

1 subgoals, subgoal 1 (ID 42)

  A : Type
  a : A
  xs : list A
  IHxs : xs @ nil = xs
  ============================
   a :: xs @ nil = a :: xs

さて、帰納法を使うときの常として、そろそろ帰納法の仮定を使うタイミングです。 IHxsを使ってxs@nilをxsに書き換えれそうです。このときはrewrite IHxsが使います。

1 subgoals, subgoal 1 (ID 43)

  A : Type
  a : A
  xs : list A
  IHxs : xs @ nil = xs
  ============================
   a :: xs = a :: xs

あとはreflexivityしてQedです。

結合則の証明

さて、もっと一般的な性質として、結合則を証明してみます。

結合則というのは

A op (B op C) = (A op B) op C

という法則です。

結合則を満さないものとしてはある種のかけ算*3が有名ですね。

Lemma append_assoc: forall A (xs ys zs : list A),
  xs @ (ys @ zs) = (xs @ ys) @ zs.

(あとはざっきーさんが書く)

解答例:

Lemma append_assoc: forall A (xs ys zs : list A),
  xs @ (ys @ zs) = (xs @ ys) @ zs.
Proof.
intros.
induction xs.
  simpl.
  reflexivity.

  simpl.
  rewrite IHxs.
  reflexivity. 
Qed.

OCamlプログラムへの変換

あとはいろいろな証明をしていけば、append の性質はどんどん保証されていきます。では、最後にこのappendをOCamlから使えるようにしましょう。

Extraction "my_append.ml" append.

を評価すると、my_append.mlにappendが書き出されます。*4

また出力する言語はHaskellやSchemeに切り替えれます。*5

Extraction Language Haskell.
Extraction "my_append.hs" append.

Extraction Language Scheme.
Extraction "my_append.scm" append.

*1:当日、発表者の半数以上の業務が炎上して、発表できなくなる事件がありましたが、それはまた別のお話です

*2:もちろんCoqでHello,worldをやってる人もいます。CoqでHello, world!（改） - にわとり小屋でのプログラミングブログ

*3:行列

*4:CoqIDEから使うとカレントパスが微妙なので、フルパスで指定すること。

*5:Scalaに出力する拡張もあります。ProofCafe - Coq2Scala

みずぴー日記

人間の再起動ボタンはハワイのビーチにある