トップ > coq

証明された証明支援器をScalaで書いてみた

Scala Coq coq2scala

この記事はTheorem Proving Advent Calendarの7日目の記事である。

静的型付き関数型言語は言語処理系の実装が容易であることから多くの場合、証明支援器(proof assistant)が実装されている。例えばStandard MLではIsabelle/HOL、OCamlでCoq、HaskellでAgdaが実装されている。

しかしながら、Twitter社が使っていることなどで最近有名になっている関数型言語のScalaはそのような証明支援器はあまり見受けられない。これはScalaが言語処理系だけでなく一般のアプリケーションでも効果的であることを示している。そうは言ってもScalaで証明支援器を書いてもいいんじゃないかと思ったので書いてみた。

実装に関して、証明支援器のモデルを実装したCoqのライブラリを使用した。coq2scalaを使ってこれをScalaのライブラリとして使った。*1ソースコードは以下で公開している。

ソースコードをダウンロードしてmakeしたのちに

 scala Top

と打てば対話環境が起動する。使えるコマンドは以下の6つだ。最後にピリオド"."を打つ必要があることに注意しよう。*2構文やエラーメッセージはオリジナルのOCaml版と揃えた。

Infer t.                           #項tを型チェックし、型を表示する

Check t : T.                       #項tが型Tを持つかどうかチェックする

Axiom x : T.                       #T型の変数xを公理として仮定する

List.                              #現在仮定されている公理の列を列挙する

Delete.                            #公理を削除する

Quit.                              #終了する

例えば簡単な論理式(∀P, PならばP)の証明は(λP:Prop. λH:P. H)という恒等関数で表現できるが、その証明は次のようにCheckコマンドでチェックできる。∀の式は丸括弧"()"で、λ式はカク括弧"[]"で表現している。

h2o:coqincoq_scala imai$ scala Top
Check [P:Prop][H:P]H : (P:Prop)P->P.
Correct.

「Correct.」と表示されたら成功だ。もっと複雑な論理式にも挑戦してみよう。
CCなので式の構文は項も型も同じである。その構文は以下のようなBNFで定義している。

 <expr> ::=
  | "Set" | "Prop" | "Kind"                     #定数
  | <ident>                                     #変数参照
  | "[" <idents> ":" <expr> "]" <expr>          #関数抽象(ラムダ式)
  | "let"<ident>":"<expr>"="<expr>"in"<expr>    #ローカル変数束縛
  | "(" <idents> ":" <expr> ")" <expr>          #forall型
  | <expr> "->" ... "->" <expr>                 #関数型
  | <expr> " " ... " " <expr>                   #関数適用

まとめ

  • Coq extraction pluginさえ用意すれば証明支援器が簡単にかけるよ
  • Scalaは関数型言語だからDSLも簡単に書けるよ
  • coq2scala使ってね

*1:なので実際には私はパーサーを書いただけだ

*2:t,Tは式を表し、xは変数名を表すメタ変数

VSTTE Competition - ソフトウェア検証コンテストにチームTebasakiという名前で参加した。

coq VSTTE competition

VSTTE (Verified Software: Theories, Tools and Experiments) 2012 という学会の併設イベントでソフトウェア検証コンテストというものが開催されることを前日に id:keigoi さんに教えてもらって参加してみた。日時は日本時間で11月9日の0時から48時間。初めて競技プログラミング(プルービング?)に参加したがよい経験になったと思う。

メンバーは id:mzpさん、@pirapiraさん、@hirose_golfさんの4名。チーム名は@pirapiraさんの提案で名古屋っぽいものがよいということでいろいろ候補を挙げて結局Tebasaki (手羽先) に決定。使う検証器や実装言語は何でも良い！ということだったので我々はCoqを使った。コンペ中はプライベートにしておいて後で公開するというためにソースコード管理はbitbucket.org上にリポジトリを置き、gitを使った。しかし、@pirapiraさんはオランダに引っ越したばかりでネットワーク回線がiPhoneしかなく、また、@hirose_golfさんもgitに慣れていないということで、結局私と@mzpだけがコミットした。

以下は感想:

  • 0時に開催ということで直前の22:00くらいは寝て、0時に起きて、その後5:00くらいに寝てということをやったため、生活のリズムが狂ってしまった。
  • 合宿みたいにして寝ずにやろうと思ったが、やはり集中力のために睡眠は重要なのでちゃんと家に帰って寝た方がよいと思った。
  • 難しかったけれど楽しかった。

最後に、証明器や検証器について興味があるけどなかなか手がでないという方のためにハッカソンします！ ProofのHackathonということでハッシュタグは #proofthon(命名 by mzp)です。

ProofCafe - ProofThon

fold_leftとfold_rightが同じになるとき

coq fold_left fold_right

fold_leftとfold_rightの結果が同じになるときが気になったので少し調べてみた。

例えば文字列のリストを連結して一つの文字列を生成する次の例はfold_leftでもfold_rightでも同様に定義できて同じ関数になる。Coqで書くと次のような感じ。

Definition xs := "foo" :: "bar" :: "baz" :: nil.
Eval compute in (fold_left append xs "").
Eval compute in (fold_right append "" xs).

fold_leftとfold_rightの定義はそれぞれ次のとおり

Section Fold_Left_Recursor.
  Variables A B : Type.
  Variable f : A -> B -> A.

  Fixpoint fold_left (l:list B) (a0:A) : A :=
    match l with
      | nil => a0
      | cons b t => fold_left t (f a0 b)
    end.
End Fold_Left_Recursor.

Section Fold_Right_Recursor.
  Variables A B : Type.
  Variable f : B -> A -> A.
  Variable a0 : A.

  Fixpoint fold_right (l:list B) : A :=
    match l with
      | nil => a0
      | cons b t => f b (fold_right t)
    end.
End Fold_Right_Recursor.

(a0: A)と((##): A -> A -> A)に対して次の二つの条件が成り立てばfold_leftとfold_rightの結果が同じになることを示した。

  • 任意の(x:A)に対して x ## a0 = a0 ## x
  • (##)は結合的。つまり x ## (y ## z) = (x ## y) ## z.
Require Import List.

Section Fold_LR.

Variable A : Set.
Variable op : A -> A -> A.
Variable a0 : A.

Infix "##" := op (at level 60, right associativity).

Axiom assoc : forall (x y z:A), (x ## y) ## z = x ## (y ## z).
Axiom sym_a0 : forall x:A, a0 ## x = x ## a0.

Lemma aux : forall (bs: list A) (a b1: A),
  fold_right op a (b1::bs) = fold_left op (bs ++ (a::nil)) b1.
Proof.
 induction bs; intros.
  reflexivity.

  simpl.
  rewrite <- IHbs.
  simpl.
  rewrite assoc.
  reflexivity.
Qed.

Lemma fold_left_a0_r : forall (xs: list A) (a: A),
  fold_left op (xs ++ (a0::nil)) a = fold_left op xs a ## a0.
Proof.
 induction xs; intro.
  reflexivity.

  simpl.
  rewrite IHxs.
  reflexivity.
Qed.

Lemma fold_left_a0_l: forall (xs: list A) (a: A),
  fold_left op xs (a0 ## a) = a0 ## fold_left op xs a.
Proof.
 induction xs; intros.
  reflexivity.

  simpl.
  rewrite <- IHxs.
  rewrite assoc.
  reflexivity.
Qed.

Theorem fold_lr : forall (xs: list A),
  fold_left op xs a0 = fold_right op a0 xs.
Proof.
 destruct xs.
  reflexivity.

  rewrite aux.
  simpl.
  rewrite fold_left_a0_l.
  rewrite fold_left_a0_r.
  rewrite sym_a0.
  reflexivity.
Qed.

End Fold_LR.

tmiyaさんの練習問題をラムダ式で解いてみた

Coq 練習問題

tmiyaさんがCoq入門者向けの問題をブログで紹介していたので解いてみた。
Functional Programming Memo: [Coq] Coq-99 : Part 1
この問題はCoqを使う人だけでなく論理的な思考力を鍛える良い問題ばかりなので、ぜひとも挑戦してみるとよいと思う。

このようなシンプルな直観主義的な命題論理ならばラムダ式でもシンプルな証明を与えることが出来る。HaskellやMLなどを知っている関数型プログラマやAgda2erならこちらの証明の方がわかりやすいかもしれない。

Section Prop_Logic.

  Definition Coq_01 : forall A B C:Prop, (A->B->C) -> (A->B) -> A -> C :=
    fun A B C H1 H2 H3 => (H1 H3 (H2 H3)).

  Definition Coq_02 : forall A B C:Prop, A /\ (B /\ C) -> (A /\ B) /\ C :=
    fun A B C H =>
      match H with
        | conj H1 (conj H2 H3) => conj (conj H1 H2) H3
      end.

  Definition Coq_03 : forall A B C D:Prop,
    (A -> C) /\ (B -> D) /\ A /\ B -> C /\ D :=
    fun A B C D H =>
      match H with
        | conj H1 (conj H2 (conj Ha Hb)) => conj (H1 Ha) (H2 Hb)
      end.

  Definition Coq_04 : forall A : Prop, ~(A /\ ~A) :=
    fun A H =>
      match H with
        | conj Ha Hna => Hna Ha
      end.

  Definition Coq_05 : forall A B C:Prop, A \/ (B \/ C) -> (A \/ B) \/ C :=
    fun A B C H =>
      match H with
        | or_introl Ha => or_introl _ (or_introl _ Ha)
        | or_intror (or_introl Hb) => or_introl _ (or_intror _ Hb)
        | or_intror (or_intror Hc) => or_intror _ Hc
      end.

  Definition Coq_06 : forall A, ~~~A -> ~A :=
    fun A H Ha => H (fun Hna => Hna Ha).

  Definition Coq_07 : forall A B:Prop, (A->B)->~B->~A :=
    fun A B H Hnb Ha => Hnb (H Ha).

  Definition Coq_08: forall A B:Prop, ((((A->B)->A)->A)->B)->B :=
    fun A B H => H (fun H1 => H1 (fun Ha => (H (fun _ => Ha)))).

  Definition Coq_09 : forall A:Prop, ~~(A\/~A) :=
    fun A H => H (or_intror _ (fun Ha => H (or_introl _ Ha))).

End Prop_Logic.

CPS変換されたフィボナッチ関数の証明をしてみた

Coq CPS変換 フィボナッチ

普通のフィボナッチ関数とCPS変換したフィボナッチ関数をそれぞれ定義して、それらが等価であるということを証明してみた。CPS変換についてちょっと理解できた気がする。

http://ideone.com/3CQOn

しかしfib_cps関数をもっと美しく定義できないものだろうか。

[追記 2010 09/07]
asパターンを使えばパターンマッチを入れ子にしなくても良いことがわかったので、少し実装をシンプルにして書いてみた。証明部分は ほぼ同じ。
http://ideone.com/ZFPeQ

Coqプログラマの集会、Coq庵でした

Coq Coq庵

発表者の皆さん。お手伝いいただいた皆さん。ありがとうございました。たくさんのCoqerが集まって、大変濃密な時間を過ごす事ができました。

スライドは以下から参照できます。
Coq庵 - coqグループ

掛け算から足し算を作る(足し算の一意性について)

Coq

http://d.hatena.ne.jp/kikx/20100629#1277831079 の素晴らしい足し算の存在証明を見つけたので、その存在が一意(ユニーク)であることを証明した。元々のネタはこちら http://d.hatena.ne.jp/m-hiyama/20100629/1277774676

まずは集合AとA上の掛け算とサクセッサSを仮定。この部分はid:kikxさんのコードのコピー。

Axiom A : Set.
Axiom A_eq_dec: forall a b: A, { a = b } + { a <> b }.

Axiom A_mul : A -> A -> A.
Axiom A_zero: A.
Axiom A_one: A.

Infix "*" := A_mul.
Notation "0" := A_zero.
Notation "1" := A_one.

Axiom A_mul_assoc: forall a b c, (a * b) * c = a * (b * c).
Axiom A_mul_comm: forall a b, a * b = b * a.
Axiom A_mul_1_r: forall a, a * 1 = a.
Axiom A_mul_inv_ex: forall a, a <> 0 -> { a': A | a * a' = 1 }.
Axiom A_mul_0_r: forall a, a * 0 = 0.

Lemma A_mul_1_l: forall a, 1 * a = a.
Proof.
  intros.
  rewrite (A_mul_comm 1 a).
  exact (A_mul_1_r a).
Qed.

Definition A_inv a (H: a <> 0) :=
  let (a', H) := A_mul_inv_ex a H in a'.

Axiom S: A -> A.
Axiom S_inv: A -> A.

Axiom S_inv_l: forall a, S_inv (S a) = a.
Axiom S_inv_r: forall a, S (S_inv a) = a.
Axiom S_0:  S 0 = 1.
Axiom  S_mul: forall a b (H: a <> 0),
  S (a * S (b * A_inv a H)) = a * S (S b * A_inv a H).

Lemma inv_is_inv: forall a (H: a <> 0), a * A_inv a H = 1.
Proof.
  intros.
  unfold A_inv.
  case (A_mul_inv_ex a H).
  trivial.
Qed.

ここからA上の足し算も仮定。同時に足し算が満たすべき公理も仮定。

Parameter A_add : A -> A -> A.
Infix "+" := A_add.
Hypothesis A_add_1_r_S: forall a, a + 1 = S a.
Hypothesis A_add_dist: forall a b c,  a * (b + c) = a * b + a * c.
Hypothesis A_add_0_r: forall a, a + 0 = a.
Hypothesis A_add_comm: forall a b, a+ b = b + a.
Hypothesis A_add_assoc: forall a b c, (a + b) + c = a + (b + c).
Hypothesis A_neg_ex: forall a, { a': A | a + a' = 0 }.

id:kikxさんの定義した足し算をA_kikxs_addという名前で用意し、上で仮定した抽象的な足し算A_addがA_kikxs_addと必ず等価になることを証明した。このことからA_addは一意であることが示せた。

Definition A_kikxs_add a b :=
  match A_eq_dec a 0 with
  | left _ => b
  | right H => a * S (b* A_inv a H)
  end.

Theorem uniqueness : forall a b, A_add a b = A_kikxs_add a b.
Proof.
 intros a b.
 unfold A_kikxs_add.
 case (A_eq_dec a 0).

  intro eq; rewrite eq.
  rewrite A_add_comm.
  rewrite A_add_0_r.
  reflexivity.

  intro neq.
  pattern a at 1; rewrite <- (A_mul_1_r a).
  pattern b at 1; rewrite <- (A_mul_1_l b).
  pattern 1 at 2; rewrite <- (inv_is_inv a neq).
  rewrite (A_mul_assoc).
  rewrite <- A_add_dist.
  rewrite (A_add_comm 1 _).
  rewrite A_add_1_r_S.
  rewrite (A_mul_comm _ b).
  reflexivity.
Qed.