2015-09-16

Coqで命題論理の標準形

この記事はTppMark11の問題をCoqでやってみたという内容である。

問題はこちら:

docs.google.com

命題論理式と同値であることの定義

命題論理式の定義

Inductive Term :=
| Var(v : Var.T)
| Neg(t : Term)
| And(t1: Term)(t2: Term)
| Or(t1: Term)(t2: Term)
| Impl(t1: Term)(t2: Term)
| TRUE | FALSE
.

同値であることの定義

変数環境を表すctxを Var.T -> bool の関数で表現し、命題論理式のevalを次で定義した。

Fixpoint eval ctx t : bool :=
  match t with
  | Var v => ctx v
  | Neg t => negb (eval ctx t)
  | And t1 t2 => andb (eval ctx t1) (eval ctx t2)
  | Or t1 t2 => orb (eval ctx t1) (eval ctx t2)
  | Impl t1 t2 => implb (eval ctx t1)(eval ctx t2)
  | TRUE => true
  | FALSE => false
  end.

2つの命題の同値性はevalを使って次のように定義。

Definition Equiv (P Q: Term) := forall context,
  eval context P = eval context Q.

ここまではごく自然で素直な定義だと思う。

標準形の形式化と検証

問題は3.2の性質で、これを満たす標準形は私はこれまであまりみたことがなかった。

3.2 PとQが同値であれば、nf(P)とnf(Q)は形が全く等しい命題論理式である。
TPPmark-11th.docx - Google ドキュメント

例えば命題式 (P /\ P) と P は同値になるが、両者ともに連言標準形(Conjunctive normal form)であり形は等しくない。また、(P /\ Q) \/ (¬P /\ Q) と Q のように変数の数が違う命題式が同値になることもある。

これを解くために、命題論理式を真偽表へ落としこんでから復元するというアプローチを考えてみた。

真偽表への変換と正しさの証明

Definition toTable (t:Term) : TruthTable.T.
  refine ({|
    TruthTable.vars := toVars t
    ; TruthTable.map := toMap t
  |}).
  ...

Definition ofTable (table : TruthTable.T) : Term :=
  Map.elements table.(TruthTable.map)
  |> List.filter snd
  |> List.map fst
  |> List.map (fun bs => List.map2 literal table.(TruthTable.vars) bs)
  |> List.map (List.fold_right (And) TRUE)
  |> List.fold_right (Or) FALSE.

変換が正しく定義されていることを示すために次を証明した。

Lemma safe_toTable : forall context term,
  Some (eval context term) = TruthTable.eval context (toTable term).

Lemma safe_ofTable : forall context table,
  TruthTable.eval context table = Some (eval context (ofTable table)).

真偽表の最小化と一意性

以上でオッケーかと最初は考えていたけれど、実は無駄な変数があった場合、同値であっても真偽表が一意に定まらない。この問題を解決するために真偽値に影響を与えない変数を削除するという処理(elimVars)を導入した。

Definition elimVars (tbl : T) : T

そして、elimVarsの健全性(意味を変えないこと)と、一意性を証明した。

Theorem soundness : forall (x : T),
  sameSemantics x (elimVars x).
Theorem uniqueness : forall (x y: T),
  sameSemantics x y -> elimVars x == elimVars y.

標準形の定義と問題となっていた3.1, 3.2の証明

ここまでできればあとは簡単。問題にあったnfを定義と証明は以下の通り。

(** * 標準形にする関数の定義 *)
Definition nf (t : Term) : Term :=
  toTable t
  |> TruthTable.elimVars
  |> ofTable.

(** * 3.1の証明 *)
Theorem soundness_nf : forall t, Equiv t (nf t).
Proof.
 intros t. unfold Equiv. intros ctx. unfold nf, revapply.
 assert (Some (eval ctx t) = Some (eval ctx (ofTable (TruthTable.elimVars (toTable t))))).
 - rewrite <- safe_ofTable. rewrite <- TruthTable.soundness.
   now apply safe_toTable.
 - now injection H.
Qed.

(** * 3.2の証明 *)
Theorem main : forall P Q: Term, Equiv P Q -> nf P = nf Q.
Proof.
 intros. unfold nf, revapply.
 apply lem_ofTable.
 apply (TruthTable.uniqueness (toTable P) (toTable Q)).
 intro context. do 2 rewrite <- safe_toTable.
 unfold Equiv in H. now rewrite H.
Qed.

雑感

謝辞：chiguriさんに証明を一部手伝ってもらった。大変感謝。
まだ一部の小さな補題がAdmittedだけれどやればできると思っている
3日くらいでできるかと思ったけれど思ったより時間がかかった
Proof Summit で定義をいくらでもちょろまかせば簡単になると言われたけれど、ちょっといい例が思いつかない。他の人の解答に期待

Coqのコード全体はこちらから参照可能:github.com

2013-12-06

依存関係のある値のうちの一部を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.

さて、ここである変数xが 2*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.

どうやら、Hはxに依存した型をもつのに、勝手に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.

2012-12-05

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

2011-12-07

証明された証明支援器を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 ソースコードは以下で公開している。

http://proofcafe.org/wiki/Coq2Scala

ソースコードをダウンロードして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は変数名を表すメタ変数

2011-11-11

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

2011-07-24

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.

2010-09-26

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.