にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこがちょっと違うことがあります。

依存関係のある値のうちの一部をrewriteしようとしたときの問題

この記事は「Theorem Prover Advent Calendar 2013」5日目の記事である。

最近、とある大手企業のシステムのバイナリデータを扱う処理の高速化のためにCoqを使ったのだが、ちょっとアレっと思ったことを体験したのでそれを共有したいと思う。

問題の概要は表題の通り。シンプルな問題なので、レガシーCoq (version 8.4pl2) で説明する。

簡単のため、やや人工的な例を紹介する。 まず、正の自然数を引数にとる関数fを仮定し、その関数は引数が偶数のときは、戻り値はその半分になるとする。深い意味は無いので考えてはいけない。

Variable f : forall n : nat, n > 0 -> nat.
Hypothesis h : forall (n : nat) (H : 2 * n > 0), f (2 * n) H = n.

さて、ここで ある変数x2*1 と等しいことがわかっているとき、f x H = 1 であることを証明したいとする。 仮定hから f (2*1) H = 1 なんだから、超簡単に示せそうだが、そうでもなかった。

具体的には

  eq : x = 2 * 1
  ============================
   f x H = 1

から普通に rewrite eq. しようとすると次のように怒られた。

Error: Abstracting over the term "x" leads to a term
"fun x : nat => f x H = 1" which is ill-typed.

どうやら、Hxに依存した型をもつのに、勝手にxの方だけを別のものに差し替えちゃいかんということらしい。 とりあえず generalizeタクティックでHについてゴールを一般化することで、rewriteできるようになった。

< generalize H as H.
  x : nat
  eq : x = 2 * 1
  ============================
   forall H : x > 0, f x H = 1
< rewrite eq.
  x : nat
  eq : x = 2 * 1
  ============================
   forall H : 2 * 1 > 0, f (2 * 1) H = 1

そして、あとは普通に仮定を使って証明できる。

とりあえず今回はこれでできたが、Hの部分がとても長い具体的な証明だった場合、それ全部を入力するのは大変だし、ちょっといやだ。 何かより良い方法があるものだろうか。また、依存型に定評のあるAgdaではどうなるかなども興味深い。

参考: 私の証明のコードは以下の通り

Variable f : forall n : nat, n > 0 -> nat.
Hypothesis h : forall (n : nat) (H : 2 * n > 0), f (2 * n) H = n.

Variable x : nat.
Axiom H : x > 0.

Goal x = 2*1 -> f x H = 1.
Proof.
 intro eq.
 generalize H as H.
 rewrite eq.
 intro H. rewrite h. reflexivity.
Qed.

OCamlとCoqを連携してIO処理をモナディックに扱う

この記事は OCaml Advent Calendar の5日目の記事です。

OCamlと連携して、CoqでもIO処理ができるようにするためのライブラリを作った。
http://github.com/yoshihiro503/coqio

このライブラリを使えば、例えば次のようなコードを書くことができる。

Require Import Monad IO.
Open Scope string_scope.

Definition main : IO unit :=
  do _ <- print "Hello"
  ; println ", world!".

Haskell風のdo式みたいな記法が便利だね。print関数には文字列だけでなく、Showクラスのインスタンスとなる型を持つ式ならばなんでも与えることができる*1

このコードを次のコマンドでExtractすればcoq.mlというOCamlのソースを得ることができる。

Require Import ExtrOcamlBasic ExtrOcamlString ExtrOcamlIO Hello.

Extraction "coq.ml" main.

これで、あとはOCamlでコンパイルすれば実行できる。

  $ ocamlc coq.ml
  $ ./a.out
Hello, world!

*1:Showクラスの実装についてはhttp://qiita.com/items/a6fe93ae0d867129f7b1

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

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

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

しかしながら、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という名前で参加した。

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が同じになるとき

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さんの練習問題をラムダ式で解いてみた

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変換されたフィボナッチ関数の証明をしてみた

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

http://ideone.com/3CQOn

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

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