[Misc] 2011 Summary

2011年を振り返ってですが、

• 今年もFormal Methods Forumが続けられた。@kencoba さん他皆様のお陰だと思います。来年も継続して行きたい。
• RegExpライブラリが書けたのは嬉しかった。2012年も上半期に何か纏まった成果を出したいなぁ。
• 数学関係の読書会に参加した。@bonotake さん、@cocoatomo さん、@erutuf13 さんのおかげです。ありがとうございます。学部時代は20年ぐらい前のはずだが、昔勉強した数学、案外忘れてないものだなー。2012年はとりあえず群環体の入門書を終わらせ、2013年以降に繋げたいな。
• ICFP 2011は、聞いた話の全部が理解出来た訳じゃないけど楽しかったー。年休とって参加した甲斐がありました。途中体調崩したのは残念というか、適宜中休み入れないと駄目か。今後も年休取れるなら学会聞きに行きたいな。
• 名古屋のProof Cafeの皆様のご協力を得て、Proof Summit 2011を開催出来ました。時間調整にかなり失敗して発表者の皆様にはかなり迷惑をおかけしましたが、結果としては充実したイベントになったかなー。
• TPP 2011を聞きに行きました。これも勉強になり楽しかったです。来年(千葉大で開催らしい)とか、何か発表出来るといいなぁ。

来年も宜しくお願いします＞皆様。

[Coq] Group defined by one operation

通常、群$G$を定義するときは、演算 $\cdot : (G \times G) \rightarrow G$, と単位元 $e:G$, 逆元 $(\cdot)^{-1}:G \rightarrow G$ から定義しますが、$x/y := xy^{-1}$ を基本的な定義として群を定義することも出来ます。（$H \subset G$ が部分群であることを示すには $\forall x,\; y \in H,\;\; x/y \in H$ を示せば良い、など計算の手間が減って都合が良い。）

演算 $x/y : (G \times G) \ni (x,y) \mapsto xy^{-1} \in G$ が下記の公理を満たすならば、

• $a/a = b/b$
• $a/(b/b) = a$
• $(a/a)/(b/c) = c/b$
• $(a/c)/(b/c) = a/b$

$G$ は群になります。というのを Coq で証明しました。コードは https://github.com/tmiya/coq/blob/master/group/group2.v にも置いてあります。
群の法則の中では、結合則を示すのに苦労しました。

(** Group defined by one operation *)
(* Operator 'x/y' means xy^{-1}.
  Probe that '/' and four axioms obout it defines a group. *)

Section Group2.
Parameter G:Set.
(* G is not an empty set. At least one element exists. *)
Parameter g0:G. 
Parameter op:G->G->G.
Notation "a / b" := (op a b).
(* Axioms for / *)
Parameter G1: forall a b, a/a = b/b.
Parameter G2: forall a b, a/(b/b) = a.
Parameter G3: forall a b c, (a/a)/(b/c) = c/b.
Parameter G4: forall a b c, (a/c)/(b/c) = a/b.

Definition e:G := g0/g0.
Notation "1" := e.
Definition mult(a b:G) := (a/(1/b)).
Notation "a * b" := (mult a b).

Lemma op_refl_1 : forall a, a/a = 1.
Proof.
intro a. unfold "1". eapply G1.
Qed.

Lemma op_1 : forall a, a/1 = a.
Proof.
intro. unfold "1". rewrite G2. auto.
Qed.

Theorem left_id : forall a, 1*a = a.
Proof.
intro. unfold "1". unfold "*".
erewrite G3. eapply op_1.
Qed.

Theorem right_id : forall a, a*1 = a.
Proof.
intro. unfold "*". erewrite op_1.
erewrite op_1. auto.
Qed.

Definition inv(a:G) := (1/a).
Notation "! a" := (inv a) (at level 91).

Theorem left_inv : forall a, (!a)*a=1.
Proof.
intros. unfold "!". unfold "*".
rewrite G4. erewrite op_1. auto.
Qed.

Lemma inv_inv : forall a, 1/(1/a) = a.
Proof.
intros.
replace (1/(1/a)) with (1/1/(1/a)).
 rewrite G3. eapply op_1.
erewrite op_1. auto.
Qed.

Theorem right_inv : forall a, a*(!a)=1.
Proof.
intros. unfold "!". unfold "*".
erewrite inv_inv. eapply op_refl_1.
Qed.

Lemma inv_op : forall a b, inv (a/b) = b/a.
Proof.
intros. unfold "!". unfold "1".
erewrite G3. auto.
Qed.

Lemma inv_idem : forall a, inv (inv a) = a.
Proof.
intros. unfold "!". eapply inv_inv.
Qed.

Lemma op_eq : forall a b c d,
 a/b = c/d -> b/a = d/c.
Proof.
intros.
replace (b/a) with (1/1/(a/b)).
 replace (d/c) with (1/1/(c/d)).
  rewrite H. auto.
 erewrite G3. auto.
erewrite G3. auto.
Qed.

Lemma op_mult : forall a b, (a/b)*b = a.
Proof.
intros. unfold "*". erewrite G4.
eapply op_1.
Qed.

Lemma rm_op_2 : forall a b c, a/c=b/c -> a=b.
Proof.
intros. assert(a/c*c = b/c*c).
 rewrite H. auto.
erewrite op_mult in H0.
erewrite op_mult in H0. auto.
Qed.

Lemma rm_op_1 : forall a b c, a/b=a/c -> b=c.
Proof.
intros. specialize(op_eq a b a c H). intro.
eapply (rm_op_2 b c a H0).
Qed.

Lemma mult_op : forall a b, (a*b)/b = a.
Proof.
intros. unfold "*".
replace (a/(1/b)/b) with (a/(1/b)/(1/(1/b))).
rewrite G4. rewrite op_1. auto.
replace (1/(1/b)) with b. auto.
erewrite inv_inv. auto.
Qed.

Lemma assoc_2 : forall a b c, a/(b/c) = a*c/b.
intros.
replace (a/(b/c)) with ((a*c)/c/(b/c)).
rewrite G4. auto.
rewrite mult_op. auto.
Qed.

Lemma assoc_3 : forall a b c, a*(c/b) = a*c/b.
intros. 
replace (a*(c/b)) with (a/(inv (c/b))).
unfold "!". replace (1/(c/b)) with (b/c).
rewrite assoc_2. auto.
replace (1/(c/b)) with (1/1/(c/b)).
rewrite G3. auto. rewrite op_1. auto.
unfold inv. unfold "*". auto.
Qed.

Lemma assoc_4 : forall a b c, a*(c*(inv b)) = a*c*(inv b).
intros. unfold inv.
replace (c*(1/b)) with (c/b).
replace (a*c*(1/b)) with (a*c/b).
eapply assoc_3.
unfold "*". rewrite inv_inv. auto.
unfold "*". rewrite inv_inv. auto.
Qed.

Theorem assoc : forall a b c, a*(b*c) = a*b*c.
intros.
replace c with (inv (inv c)).
eapply assoc_4.
eapply inv_idem.
Qed.
End Group2.

[Why3] How to Use Why3 (Theorem Prover Advent Calender)

この記事はTheorem Proving Advent Calendar 2011の16日目の記事です。（なお、Advent Calender の参加者も継続募集中です。）

前回はWhy3のインストールと動作確認を行いましたが、今回はWhy3 を使ったプログラミング検証について解説します。

素で Coq を使って手続き型的なコード(変数への破壊的代入を用いたコード)を証明する際には、Coq内DSLとして手続き的言語を実装して、Hoareトリプルを用いて言語の公理的意味論を実装して、参照や配列に関する公理ライブラリを準備して云々、という手間が必要になります。（PierceのSoftware FoundationsにImp:Simple Imperative Programsという章があります。あるいは当Advent Calenderのimunolionさんによる２日目の記事、Coqでセンター試験のBasicを解く、を参照下さい。）

Why3 を用いることで、上記の手間を省くことが出来ます。(そして運が良ければ自動証明で片が付きます。)
Why3 では、Why3ML というML系言語でプログラムを実装出来ます。その際に、コード中にアノテーションとしてHoareの事前事後条件、ループ不変条件などを記述します。Why3 は参照を用いた破壊的代入や for-loop などの手続き言語的な構文をサポートします。そして事前事後条件やループ不変条件から weakest precondition を計算してくれ、証明課題を生成します。

マニュアルのプログラム例は VSTTE 2010 の課題から取られているようで、その最初の問題を Why3 で解いてみます。 課題は

自然数 $N$ 個を格納した配列の要素の最大値 $\mathrm{max}$, 要素の和 $\mathrm{sum}$ について $\mathrm{sum} \le N \times \mathrm{max}$

が成り立つことを示せ、というものです。

■Why3ML でのプログラミング

上の問題を Why3ML 言語で実装したものです。まぁ大体読めますよね。
ref を使うことで参照を作れます。!でderefでき、:= で再代入です。refはWhy3のライブラリとして定義されているので、興味のある人は modules/ref.mlw を読むと良いでしょう。a[i] のように配列の値を参照出来ますが、array も同様に array.mlw で定義されています。
{...} は事前事後条件、invariant {...} はループ不変条件です。事後条件の部分に課題が書かれています。

% cat max_sum.mlw 
module MaxAndSum

  use import int.Int 
  use import module ref.Ref
  use import module array.Array

  let max_sum (a: array int) (n: int) =
    { 0 <= n = length a /\ forall i:int. 0 <= i < n -> a[i] >= 0 }
    let sum = ref 0 in
    let max = ref 0 in
    for i = 0 to n - 1 do
      invariant { !sum <= i * !max }
      if !max < a[i] then max := a[i];
      sum := !sum + a[i]
    done;
    (!sum, !max)
    { let (sum, max) = result in sum <= n * max }

end

ここではforループが使用されていますが、Why3MLではloop-end, while-do-done, do-done などループ構文が複数用意されています。例外処理の構文はraiseで例外を投げて、try-with-endで例外を発生する箇所をガードする形。アサーションはassert, assume, check と同じようなものが３つ。パターンマッチ構文match-with-endもあります。構文の詳細はマニュアルを参照して下さい。

■Alt-Ergoでの自動証明

これをAlt-Ergoで自動証明してみます。

% why3ml -P alt-ergo max_sum.mlw
max_sum.mlw WP MaxAndSum WP_parameter max_sum : Unknown: Unknown (0.05s)
%

が、Alt-Ergoは失敗しました。さすがに自動証明は通りませんでした。

■Coq用の証明課題生成

Coqの証明課題も生成してみます。

% mkdir max_sum
% why3ml -P coq -o max_sum max_sum.mlw
% ls max_sum
max_sum_MaxAndSum_WP_parameter_max_sum.v
% cat max_sum/max_sum_MaxAndSum_WP_parameter_max_sum.v 
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
Require Import ZArith.
Require Import Rbase.
Definition unit  := unit.

Parameter qtmark : Type.

Parameter at1: forall (a:Type), a -> qtmark -> a.

Implicit Arguments at1.

Parameter old: forall (a:Type), a -> a.

Implicit Arguments old.

Inductive ref (a:Type) :=
  | mk_ref : a -> ref a.
Implicit Arguments mk_ref.

Definition contents (a:Type)(u:(ref a)): a :=
  match u with
  | (mk_ref contents1) => contents1
  end.
Implicit Arguments contents.

Parameter map : forall (a:Type) (b:Type), Type.

Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.

Implicit Arguments get.

Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).

Implicit Arguments set.

Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
  forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
  a2) = b1).

Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
  forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
  a2) = (get m a2)).

Parameter const: forall (b:Type) (a:Type), b -> (map a b).

Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.

Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
  b1):(map a b)) a1) = b1).

Inductive array (a:Type) :=
  | mk_array : Z -> (map Z a) -> array a.
Implicit Arguments mk_array.

Definition elts (a:Type)(u:(array a)): (map Z a) :=
  match u with
  | (mk_array _ elts1) => elts1
  end.
Implicit Arguments elts.

Definition length (a:Type)(u:(array a)): Z :=
  match u with
  | (mk_array length1 _) => length1
  end.
Implicit Arguments length.

Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i).
Implicit Arguments get1.

Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) :=
  match a1 with
  | (mk_array xcl0 _) => (mk_array xcl0 (set (elts a1) i v))
  end.
Implicit Arguments set1.

(* YOU MAY EDIT THE CONTEXT BELOW *)

(* DO NOT EDIT BELOW *)

Theorem WP_parameter_max_sum : forall (a:Z), forall (n:Z), forall (a1:(map Z
  Z)), (((0%Z <= n)%Z /\ (n = a)) /\ forall (i:Z), ((0%Z <= i)%Z /\
  (i <  n)%Z) -> (0%Z <= (get a1 i))%Z) -> ((((n - 1%Z)%Z <  0%Z)%Z ->
  (0%Z <= (n * 0%Z)%Z)%Z) /\ ((0%Z <= (n - 1%Z)%Z)%Z ->
  ((0%Z <= (0%Z * 0%Z)%Z)%Z /\ forall (max:Z), forall (sum:Z), (forall (i:Z),
  ((0%Z <= i)%Z /\ (i <= (n - 1%Z)%Z)%Z) -> ((sum <= (i * max)%Z)%Z ->
  (((0%Z <= i)%Z /\ (i <  a)%Z) /\ (((max <  (get a1 i))%Z ->
  (((0%Z <= i)%Z /\ (i <  a)%Z) /\ forall (max1:Z), (max1 = (get a1 i)) ->
  (((0%Z <= i)%Z /\ (i <  a)%Z) /\ forall (sum1:Z), (sum1 = (sum + (get a1
  i))%Z) -> (sum1 <= ((i + 1%Z)%Z * max1)%Z)%Z))) /\ ((~ (max <  (get a1
  i))%Z) -> (((0%Z <= i)%Z /\ (i <  a)%Z) /\ forall (sum1:Z),
  (sum1 = (sum + (get a1 i))%Z) -> (sum1 <= ((i + 1%Z)%Z * max)%Z)%Z)))))) /\
  ((sum <= (((n - 1%Z)%Z + 1%Z)%Z * max)%Z)%Z -> (sum <= (n * max)%Z)%Z)))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.

Qed.
(* DO NOT EDIT BELOW *)

%

■生成された証明課題をCoqで証明する。

まぁこれを Coq で証明すれば OK なんですが...。
見た目、すごい定理の様になっていますが、intuition すると3つの証明課題に分離されます。それを ring, omega などを駆使して各個撃破すれば OK です。証明するとこんな感じ。

(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
Require Import Omega.
Require Import Ring.
      rewrite H8. rewrite H7.
      cut((sum <= (i*get a1 i)%Z)%Z). intro.
        replace ((i+1)%Z*get a1 i)%Z with ((i*get a1 i)%Z + get a1 i)%Z.
          omega.
        ring.
      cut(((i*max)%Z <= (i*get a1 i)%Z)%Z). intro.
        omega.
      destruct i; try omega.
        eapply Zmult_le_compat_l; try omega.
      elim H5. simpl. auto.
  rewrite H7.
    replace ((i+1)*max)%Z with (i*max + max)%Z.
      omega.
    ring.
  replace (n-1+1)%Z with n in H3. auto.
    auto.
  omega.
Qed.
(* DO NOT EDIT BELOW *)

■まとめ

Coq を使うことで課題を証明出来ました。 今回は事前条件やループ不変条件をマニュアル記載の所与のものとしましたが、実際には正しくかつ充分なそれらを書くのはそれなりに知識が必要です。
ですが、とりあえずWhy3を使用することで、最弱事前条件を自動生成してくれるので、ひたすら定理を証明すれば良く、かなり楽になります。

■その先の話

Why3の上に更にKrakatoaを使うことで、Javaプログラムの検証が出来る、という話をKrakatoa and Jessieを用いた、Javaプログラムの正当性＆安全性証明(アルゴリズムもあるよ！)という記事でqnighyさんがAdvent Calenderの記事に書いていますのでそちらもご覧下さい。Krakatoaを用いたJavaプログラムの検証の場合は、intがZ(Coqの任意桁整数)でなくJavaと同じ32bit整数で扱われるので、より実用的ですが証明が大変です。

■宣伝

毎月１回週末に、新宿にて形式手法勉強会の Formal Methods Forum を開催しています。内容は Coq を中心とした各種形式手法（定理証明系とモデル検査など）についての勉強会です。東京近隣の方はぜひご参加を。（あと来年の１、２月の平日夜にCoq講習会を計画してます。もうちょっとしたらFMFとかで告知します。）

[Blogger][LaTeX] Install MathJax

MathJax in Blogger (II) を参考にMathJaxを使える様にしてみた。

$$a^2+b^2=c^2$$

どうやら使えているみたい。

[Why3] Install of Why3 Tool (Theorem Prover Advent Calender)

この記事はTheorem Proving Advent Calendar 2011の3日目の記事です。（なお、Advent Calender の参加者も継続募集中です。）

Why3 をMacOS (Snow Leopard) に導入してみました。
Why3 は Why の後継で、Why というのはプログラム検証プラットホームです。Java や C のプログラムに注釈として事前事後条件などを書くと、why 言語という中間言語に一度処理され、Alt-Ergo などの自動証明器や Coq のような証明支援系に適した出力に変換してくれます。さらに上記を統合した GUI フロントエンドを提供します。その辺の話は昔作った発表資料(Slideshare)を参照して下さい。

■なぜ Why3 を学ぶのか
今年の11月に VSTTE 2012 Software Verification Competition という競技ソフトウェア検証イベントがありました。平日開催で忙しかったという理由もありますが、出された問題の多くが手続き型的コードの検証ということもあり、普通の Coq の証明の知識だけでは手が出ませんでした。そこで来年に活かそう、という理由で Why3 を学ぶことにしました。
実際問題として、手続き的に書かれたプログラムについて検証したいという需要は多いと思われます。（たとえ Coq などの定理証明系は純関数型的なコードと相性が良くても。）
Why3 と同様のツールに関しては CFML という OCaml コードの検証ツールについて @keigoi さんが記事をお書きになっていますので、そちらもご覧下さい --- というか CFML もいずれ動かしてみたいです。

■ Why3 導入
すでに Xcode, macports とか OCaml, Coq は導入済みと仮定します。
Why3 ダウンロードサイトよりversion 0.71のtarを入手し、適当なディレクトリで展開します。configure したら色々無いと判ったのでとりあえず導入。ocamlgraph は ports に無いので別途ここから入手。でも CoqIDE 動いてるのになんで lablgtk2 無いの？

% ./configure
略
% sudo port install lablgtk2% sudo port install caml-menhir
% sudo port install rubber
% sudo port install caml-sqlite3


ocamlgraph 導入
% cd ???/ocamlgraph-1.8.1
% ./configure
% make
% sudo make install
% sudo make install-findlib


why3 ディレクトリに戻る
% ./configure
                 Summary
-----------------------------------------
OCaml version           : 3.12.1
OCaml library path      : /opt/local/lib/ocaml
Verbose make            : no
Why IDE                 : yes
Why bench tool          : yes
Why documentation       : yes
Why plugins             : yes
Coq plugin support      : no  (not yet implemented)
TPTP parser             : yes
Menhir library          : no
hypothesis selection    : yes
profiling               : no
localdir                : no
% make


ここで why3-0.71/src/ide/gmain.ml の GSourceView2 を gSourceView2 に修正など苦労するが結局


File "gmain.ml", line 1180, characters 42-43:
Error: Syntax error: ')' expected
File "gmain.ml", line 1180, characters 25-26:
Error: This '(' might be unmatched


などのコンパイルエラーが消えず、GUIは諦めることにする。


% ./configure --disable-ide
% make clean; make
% sudo make install


各種ツールが /usr/local/bin/ に導入された。



■ 各種自動定理証明器の導入
基本的にどれかで証明出来れば良いと考えると、色々導入した方が有利なんですが、とりあえず Alt-Ergo だけ導入すれば雰囲気は味わえます。どれが一番強力な自動証明器かというのは良く解りません。

Alt-Ergo は Why3 のページから辿って、alt-ergo-0.93 の Mac 版をダウンロードするだけ (make 不要)。

CVC3 についても同様にして 64-bit Intel Mac OS X (Snow Leopard) dynamic library and executable cvc3 2.4.1 を導入。これは展開するだけ。

Yices も同様に Yices 1.0.31 をダウンロードして展開。

Gappa も同様に gappa 0.15.1 をダウンロード。INSTALL を読むと前提が GMP, MPFR, Boost なのでそれぞれダウンロードして導入。GMPは入手先サイトが無くなっていたので ports で代用し、 
% sudo port install gmp
% sudo port install mpfr
% sudo port install boost
% ./configure
GMPが見つからず失敗
% ./configure "CPPFLAGS=-I/opt/local/include" "LDFLAGS=-L/opt/local/lib"
成功
% make
% sudo make install
で代用。

■構成
インストールしたcvc3などにPATHを通して
% why3config --detect
します。なんかyicesが未サポートヴァージョン、cvc3が動かず、Alt-Ergo, Gappa, Coq だけという状況。一度構成したら
% why3 --list-provers
Known provers:
  alt-ergo (Alt-Ergo)
  coq (Coq)
  gappa (Gappa)
  yices (Yices)
と表示されます。証明器を追加したら再度同様に構成します。

■実行例
examples/に入っている

% cat hello_proof.why
theory HelloProof "My very first Why3 theory"

  goal G1 : true

  goal G2 : (true -> false) /\ (true \/ false)

  use import int.Int

  goal G3: forall x:int. x*x >= 0

end
%

を試してみましょう。ちなみにG2はそもそも間違っているので自動証明失敗して当然です。
Coq については出力先ディレクトリを予め作成しておいて、-o オプションで指定します。

% why3 -P alt-ergo hello_proof.why 
hello_proof.why HelloProof G1 : Valid (0.03s)
hello_proof.why HelloProof G2 : Unknown: Unknown (0.04s)
hello_proof.why HelloProof G3 : Valid (0.03s)
% why3 -P gappa hello_proof.why
hello_proof.why HelloProof G1 : Valid (0.00s)
hello_proof.why HelloProof G2 : Unknown: Unknown (0.00s)
hello_proof.why HelloProof G3 : Unknown: Unknown (0.00s)
% why3 -P yices hello_proof.why
hello_proof.why HelloProof G1 : Valid (0.00s)
hello_proof.why HelloProof G2 : Unknown: Unknown (0.00s)
hello_proof.why HelloProof G3 : Unknown: Unknown (0.00s) 

% mkdir hello

% why3 -P coq -o hello hello_proof.why
% ls hello
hello_proof_HelloProof_G1.v hello_proof_HelloProof_G3.v
hello_proof_HelloProof_G2.v 

% cat hello/hello_proof_HelloProof_G2.v 
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
Require Import ZArith.
Require Import Rbase.
(* YOU MAY EDIT THE CONTEXT BELOW *)

(* DO NOT EDIT BELOW *)

Theorem G2 : False.
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.

Qed.
(* DO NOT EDIT BELOW *)

% 

G2を下記の様に正しく修正すると、


% grep G2 hello_proof.why
  goal G2 : (true -> false) \/ (true \/ false)
% why3 -P alt-ergo hello_proof.why
hello_proof.why HelloProof G1 : Valid (0.03s)
hello_proof.why HelloProof G2 : Valid (0.03s)
hello_proof.why HelloProof G3 : Valid (0.03s)
%

上記の様に自動証明に成功します。 ツールの導入が終わったので、次回は Why3 を用いたプログラム開発に付いて説明します。

■宣伝
毎月１回週末に、新宿にて形式手法勉強会の Formal Methods Forum を開催しています。内容は Coq を中心とした各種形式手法（定理証明系とモデル検査など）についての勉強会です。東京近隣の方はぜひご参加を。

[Coq] TypeClass vs Record

CoqでClass/Instance (型クラス) と Record と何が違うの？、というのは私も明確に理解出来てなかったのですが、2011/11/01前後のCoq-Clubの"What are type classes?"というスレッドで色々解説されてます。

まず実装自体は "Type classes are a thin layer on top of dependent records (although some special type classes are actually not records but raw definitions)." らしく、Record の上に構文糖があるみたいなものらしい。

そして、"Type classes allow you to specify an abstract "interface" for which you want the system to *automatically* find an implementation. Hence the main difference: type class instances (terms of a record type) are registered in a special "auto" database. This database is then used to resolve the class requirements you specify in for example a lemma." ということで、抽象的な interface への操作に対しても色々 implicit な実装を自動で探してくれるということみたい。

違いが判りやすいサンプルコードは下記の様になります。

まず EqDec という decidability を持つ Class を定義し、次いで EqDec nat という具体的な instance を定義します。最後に EqDec の定義を見ると実体は単なる Record になっていることが判ります。

Class EqDec (A:Type) := {
 eq_dec: forall (x y:A), {x=y}+{x<>y}
}.
Instance EqDec_nat : EqDec nat.
constructor. decide equality.
Qed.
Print EqDec.
(* Record EqDec (A : Type) : Type := Build_EqDec
  { eq_dec : forall x y : A, {x = y} + {x <> y} } *)

同じことを Record で書きます。

Record EqDec' (A : Type) : Type := Build_EqDec'
 { eq_dec' : forall x y : A, {x = y} + {x <> y} }.
Definition EqDec'_nat : EqDec' nat.
constructor. decide equality.
Qed.

eq_dec と eq_dec' は実際、同じ型を持ちます。

Check @eq_dec.
(* eq_dec : forall A : Type, EqDec A -> forall x y : A, {x = y} + {x <> y} *)
Check @eq_dec'.
(* eq_dec' : forall A : Type, EqDec' A -> forall x y : A, {x = y} + {x <> y} *)

しかし実際に使うときの自動推論の能力に違いが出ます。

Definition eq_nat_dec :  forall (x y:nat), {x=y}+{x<>y} := @eq_dec nat _. 
Print eq_nat_dec.
(* eq_nat_dec = eq_dec : forall x y : nat, {x = y} + {x <> y} *)
Definition eq_nat_dec :  forall (x y:nat), {x=y}+{x<>y} := @eq_dec' nat _.
(* Error: Cannot infer this placeholder. *)

これを見る限り、使い方 (interface/implementationの分離にtype classを使う) とかを別にすると、実装的には単に便利な自動推論がついているだけ、ということみたいです。 あと、この発表資料はCoqにおけるType Classの良い説明かも。 http://mattam.org/research/publications/First-Class_Type_Classes-TPHOLs-200808.pdf

[Coq] Monads in Coq

社内勉強会でMonad入門の話をして、その時にCoqを用いて説明しました。
あまりHaskellに慣れてないのでCoq使ったんですが、CoqではMonad則を証明する必要があるので、実は寧ろ説明に適していました。
HaskellだとMonad則がなぜ必要なのか示すのが面倒そう（任意の関数、なんてのはQuickCheckでも作れ無さそうな気がする）ですが、CoqではそもそもMonad則を満たすことを示さないと、Monadを使えません。
サンプルコードでは、

• Maybeモナド、Listモナドについて示してあります。
• サザエさんの家族構成を用いて、MaybeやListのサンプルコードを書いています。

Class Monad (M:Type -> Type):Type := {
  return' : forall {A}, A -> M A;
  bind : forall {A B}, M A -> (A -> M B) -> M B;
  left_unit : forall A B (a:A)(f:A -> M B),
    bind (return' a) f = f a;
  right_unit : forall A (ma:M A),
    bind ma return' = ma;
  assoc : forall A B C (ma:M A)(f:A -> M B)
    (g:B -> M C), bind (bind ma f ) g =
    bind ma (fun a => bind (f a) g)
}.
Notation "m >>= f" := 
  (bind m f) (left associativity, at level 49).

Notation "'do' a <- e ; c" := 
  (e >>= (fun a => c)) 
  (at level 59, right associativity).

Instance Maybe : Monad option := {
  return' A a := Some a;
  bind A B ma f :=
    match ma with
    | None => None
    | Some a => f a
    end
}.
Proof.
  intros; auto.
  intros; destruct ma; auto.
  intros; destruct ma; [destruct (f a)|]; auto.
Defined.

Eval compute in (Some 1 >>= (fun x => return' (x + 1))).
Eval compute in (None >>= (fun x => return' (x + 1))).

Inductive Isono:Set :=
  Namihei | Fune | Masuo | Sazae | Katsuo | Wakame | Tara.

Definition father(x:Isono):option Isono :=
match x with
| Tara => Some Masuo
| Sazae | Katsuo | Wakame => Some Namihei
| _ => None
end.

Definition mother(x:Isono):option Isono :=
match x with
| Tara => Some Sazae
| Sazae | Katsuo | Wakame => Some Fune
| _ => None
end.

Definition f_of_m(s:Isono):option Isono :=
match (mother s) with
| None => None
| Some x => father x
end.

Definition f_of_m'(s:Isono):option Isono :=
  do x <- mother s;
  father x.

Eval compute in (f_of_m' Tara).
Eval compute in (f_of_m' Katsuo).

Require Import List.
Lemma flat_map_app : forall (A B:Type)(xs ys:list A)(f:A -> list B),
 flat_map f (xs++ys) = flat_map f xs ++ flat_map f ys.
Proof.
 induction xs.
   simpl. auto.
   simpl. intros. erewrite IHxs. erewrite app_ass. auto.
Qed.

Instance List : Monad list := {
  return' A x := x :: nil;
  bind A B m f := flat_map f m
}.
Proof.
(* left_unit *)
intros A B a f. simpl. erewrite <- app_nil_end. auto.
(* right_unit *)
intros A m. induction m.
 simpl. auto.
 simpl. rewrite IHm. auto.
(* assoc *)
intros A B C m f g. induction m.
 simpl. auto.
 simpl. rewrite <- IHm.
 erewrite flat_map_app. auto.
Defined.

Definition children(x:Isono):list Isono :=
match x with
| Namihei | Fune => Sazae::Katsuo::Wakame::nil
| Sazae | Masuo => Tara::nil
| _ => nil
end.

Eval compute in (children Fune).
Eval compute in (children Katsuo).

Definition grandchildren(x:Isono):list Isono :=
  do y <- children x;
     children y. 

Eval compute in (grandchildren Fune).
Eval compute in (grandchildren Katsuo).

[Coq][PFDS] How to use Module in Coq

今日のFormal Methods Forumでは、CoqでPFDS(Purely Functional Data Structure)を、というのをみんなで実施しました。参加者の誰もがMLのmodule systemになれておらず色々苦労しましたが、とりあえずこんな感じのコードになりました。 まず Exercise 2.1 の suffixes ですが、これは簡単。

Fixpoint suffixes{A:Set}(xs:list A):list (list A) :=
match xs with
| nil => nil
| _::xs' => xs :: (suffixes xs')
end.

Eval compute in (suffixes (1::2::3::4::nil)).
(* = (1 :: 2 :: 3 :: 4 :: nil)
       :: (2 :: 3 :: 4 :: nil) :: (3 :: 4 :: nil) :: (4 :: nil) :: nil
     : list (list nat) *)

consする回数を数えるヴァージョンと、回数がO(n) (というかn) である証明。

Fixpoint suffixes' {A:Set}(xs:list A)(c:nat):
  (nat * (list (list A)))%type :=
match xs with
| nil => (0,nil)
| _::xs' =>
  let (c',ys) := (suffixes' xs' c)
  in (c'+1, xs::ys)
end.
Eval compute in (suffixes' (1::2::3::4::nil) 0).

Theorem suffixes'_length : forall (A:Set)(xs:list A),
  fst (suffixes' xs 0) = length xs.
Proof.
  intros A xs.
  induction xs.
    simpl. trivial.
    simpl. destruct (suffixes' xs 0). simpl.
    simpl in IHxs. rewrite <- IHxs.  omega.
Qed. 

Coq の module の使い方はこんな感じ。 まず SET signature のモジュールを定義します。予約語回避のためあちこちに _ を追加します。

Module Type SET.
  Parameter Elem : Set.
  Parameter Set_ : Set.
  Parameter empty : Set_.
  Parameter insert : Elem -> Set_ -> Set_.
  Parameter member : Elem -> Set_ -> bool.
End SET.

次いで、ORDERED signature を定義します。

Module Type ORDERED.
  Parameter T : Set.
  Parameter eq_ : T -> T -> bool.
  Parameter lt_ : T -> T -> bool.
  Parameter gt_ : T -> T -> bool.
End ORDERED.

次が、ORDERED な型のUnbalancedSet を定義します。ElementはORDERED signatureを満たすものです。SETのsignatureを持つので<:を使って定義します。

Module Type UnbalancedSet (Element:ORDERED) <: SET.
  Definition Elem := Element.T.
  Inductive Tree :=
  | E : Tree
  | T : Tree -> Elem -> Tree -> Tree.
  Definition Set_ := Tree.
  Definition empty := E.
  Fixpoint member (x:Elem)(tr:Tree) :=
  match tr with
  | E => false
  | T a y b => 
    if (Element.lt_ x y) then (member x a)
    else (if (Element.lt_ y x) then (member x b)
          else true )
  end.
  Fixpoint insert (x:Elem)(tr:Tree) :=
  match tr with
  | E => T E x E
  | T a y b =>
    if (Element.lt_ x y) then (T (insert x a) y b)
    else (if (Element.lt_ y x) then (T a y (insert x b))
          else tr)
  end.
End UnbalancedSet.

と定義します。 ORDERED の具体例として NAT を作ります。

Fixpoint blt_nat (x y:nat):bool :=
match x,y with
| O,O => false
| O,_ => true
| _,O => false
| S x',S y' => blt_nat x' y'
end.
Eval compute in (blt_nat 2 2). (* false *)
Eval compute in (blt_nat 2 3). (* true *)
Eval compute in (blt_nat 3 2). (* false *)
Definition bgt_nat (x y:nat):bool := blt_nat y x.

Module NAT <: ORDERED.
  Definition T := nat.
  Definition eq_ := beq_nat.
  Definition lt_ := blt_nat.
  Definition gt_ := bgt_nat.
End NAT.

そして、Element:ORDERED として NAT<:ORDERED を取る UNSet を定義します。Include を使うのが大事なポイントです。

(* Unbalanced Nat Set *)
Module UNSet <: (UnbalancedSet NAT).
Include (UnbalancedSet NAT).
End UNSet.

最後にそれを使ってみます。

Definition E := UNSet.E.
Print E.
Definition T := UNSet.T.
Print T.
Print UNSet.Elem.
Print NAT.T.
Eval compute in (T E 1 E).
Eval compute in (UNSet.member 1 (T E 1 E)).
Eval compute in (UNSet.insert 2 (T E 1 E)).

[Coq] Ring in Coq

スタート代数という勉強会に参加してきました。 そこで出された宿題のうち１問を Coq で証明してみました。まぁこの程度簡単な証明なら Coq でも出来るけど、という感じです。Coq で証明するとはどんな感じかの参考になればと思います。

Section Ring.
(* R : ring *)
Axiom R:Set.
(* plus *)
Axiom plus : R -> R -> R.
Notation "a + b" := (plus a b).
Axiom plus_assoc : forall a b c:R, (a+b)+c=a+(b+c).
Axiom plus_comm : forall a b:R, a+b=b+a.
Axiom zero : R.
Notation "0" := zero.
Axiom plus_unit_l : forall a:R, 0 + a = a.
Axiom plus_unit_r : forall a:R, a + 0 = a.
Axiom minus : R -> R.
Notation "^ a" := (minus a) (at level 90).
Axiom plus_inv_l : forall a:R, (^a) + a = 0. 
Axiom plus_inv_r : forall a:R, a + (^a) = 0. 
(* mult *)
Axiom mult : R -> R -> R.
Notation "a * b" := (mult a b).
Axiom mult_assoc : forall a b c:R, (a*b)*c=a*(b*c).
Axiom one : R.
Notation "1" := one.
Axiom mult_unit_l : forall a:R, 1 * a = a.
Axiom mult_unit_r : forall a:R, a * 1 = a.
(* commutative ring *)
Axiom mult_comm : forall a b:R, a*b = b*a.
(* distributive *)
Axiom distr_l : forall a b c:R, a*(b+c) = a*b + a*c.
Axiom distr_r : forall a b c:R, (a+b)*c = a*c + b*c.

Lemma rm_plus_l : forall a b c:R, a+b=a+c -> b=c.
Proof.
  intros a b c ab_ac.
  specialize(plus_assoc (^a) a b). intro H.
  rewrite ab_ac in H.
  rewrite <- plus_assoc in H.
  rewrite plus_inv_l in H.
  repeat rewrite plus_unit_l in H.
  assumption.
Qed.
Theorem mult_a_0 : forall a:R, a * 0 = 0.
Proof.
  intro a.
  assert(H: a*(0+0) = a*0 + 0).
    rewrite plus_unit_l. rewrite plus_unit_r. reflexivity.
  rewrite distr_l in H. 
  apply(rm_plus_l (a*0) (a*0) 0). assumption.
Qed.
End Ring.

[separation logic] jStar: Bringing separation logic to Java

jStar: Bringing separation logic to Java Java Programに対してseparation logicを使って検証するというもので、事前事後条件を与えると、ループ不変条件は自動的に計算してくれるらしい（"Loop invariants are computed automatically by means of abstract interpretation. "） 論文(PDF)：jStar: Towards Practical Verification for Java チュートリアル(PDF): How to Verify Java Program with jStar: a Tutorial

[Coq] Category in Coq

先日、スタートCoqで圏論 in honor of こんさんというイベントがあり、その時に書いたコード。ConCaTというライブラリを使い、オブジェクトが２つ、その間に射が１つという圏を書いてみた、というものです。


Add LoadPath "~/coq/ConCat/ConCaT" as ConCaT.
Print LoadPath.
Require Import ConCaT.CATEGORY_THEORY.CATEGORY.Category.

Inductive Two_ob : Type := Ob_A | Ob_B.
Inductive Two_mor : Two_ob -> Two_ob -> Type :=
| Id_A : Two_mor Ob_A Ob_A
| Id_B : Two_mor Ob_B Ob_B
| Mor_AB : Two_mor Ob_A Ob_B.
Section equal_two_mor.
Variable a b:Two_ob.

Definition Equal_Two_mor(f g:Two_mor a b) := True.
Check Equal_Two_mor.
(* Two_mor a b -> Two_mor a b -> Prop *)
Lemma Equal_Two_mor_equiv : Equivalence Equal_Two_mor.
Proof.
unfold Equal_Two_mor.
apply Build_Equivalence.
unfold Reflexive. intro x. auto.
apply Build_Partial_equivalence.
unfold Transitive. intros. auto.
unfold Symmetric. intros. auto.
Qed.
Canonical Structure Two_mor_setoid : Setoid :=
Equal_Two_mor_equiv.
End equal_two_mor.
Definition Comp_Two_mor : forall a b c:Two_ob,
Two_mor_setoid a b -> Two_mor_setoid b c ->
Two_mor_setoid a c.
Proof.
intros a b c Sab Sbc.
inversion Sab.
inversion Sbc.
apply Id_A.
rewrite <- H0 in H1. discriminate H1.
apply Mor_AB.
inversion Sbc.
rewrite <- H0 in H1. discriminate H1.
apply Id_B.
rewrite <- H0 in H1. discriminate H1.
inversion Sbc.
rewrite <- H0 in H1. discriminate H1.
apply Mor_AB.
rewrite <- H0 in H1. discriminate H1.
Defined.

Lemma Comp_Two_mor_congl : Congl_law Comp_Two_mor.
Proof.
unfold Congl_law. intros. simpl.
unfold Two_mor_setoid in *.
unfold Equal_Two_mor.
auto.
Qed.

Lemma Comp_Two_mor_congr : Congr_law Comp_Two_mor.
Proof.
unfold Congr_law. intros. simpl.
unfold Two_mor_setoid in *.
unfold Equal_Two_mor.
auto.
Qed.

Definition Comp_Two :=
Build_Comp Comp_Two_mor_congl Comp_Two_mor_congr.

Lemma Assoc_Two : Assoc_law Comp_Two.
Proof.
unfold Assoc_law. intros. simpl in *.
unfold Equal_Two_mor in *. auto.
Qed.

Definition Id_Two (a:Two_ob) : Two_mor_setoid a a :=
match a as a0 return (Two_mor a0 a0) with
| Ob_A => Id_A
| Ob_B => Id_B
end.

Lemma Idl_Two : Idl_law Comp_Two Id_Two.
Proof.
unfold Idl_law; simpl.
unfold Comp_Two; unfold Id_Two; unfold Equal_Two_mor; simpl.
intros; auto.
Qed.

Lemma Idr_Two : Idr_law Comp_Two Id_Two.
Proof.
unfold Idr_law; simpl.
unfold Comp_Two; unfold Id_Two; unfold Equal_Two_mor; simpl.
intros; auto.
Qed.

Canonical Structure Two := Build_Category Assoc_Two Idl_Two Idr_Two.


[Coq] Type Class in Coq

　形式手法勉強会のFormal Methods Forum #16で、Monadを例にとってCoqでのtype-classを使い方を紹介しました。

　発表資料はhttp://www.slideshare.net/tmiya/typeclass
　練習課題の答えは、http://ideone.com/oANlm

です。

[Event][FM] Formal Methods Forum #15 on 4/23

第15回FormalMethods勉強会を 4/23(Sat) に開催します。
参加登録は下記 ATND からお願いします。
http://atnd.org/events/13673
今回は Monad 特集らしいです。

今回は Coq 関係では

• Coq の型クラスを使って Monad を実装


• Coq 未経験者向けのチュートリアルを書いたので、他の方に見て頂く
  

を予定してます。

Coq 未経験者の方は、その旨を ATND 参加時に書いて頂ければ、当日の内容を変更して対応出来る様に致します。ノートパソコン持参を推奨します。

[Coq][Formal Methods] Proof Assistant Day 2011 on 9/25(Sun)

　今年の９月は東京で ICFP 2011 が開催されることもあり、その前後の週末も公式/非公式な関数型言語イベントが多数開催される見込みです。

　我々の形式手法勉強会 Formal Methods Forum も、名古屋の ProofCafe と一緒に、昨年開催された Coq庵 と同様の定理証明系イベントを開催したいと計画しています。

　会場は新宿の豆蔵セミナールームを予定しています。（豆蔵様、会場提供ありがとうございます）

　諸々決まりましたら、また報告します。

[Coq] Formal Methods Forum 2011/03/05

　昨日はFormal Methods Forumのミーティングが行われました。

　昨年の年末から作っていたBrzozowski'sの正規表現アルゴリズム（去年の年末にLtUで話題になった正規表現の微分を使ったYacc is Deadのやつ）のCoqライブラリ化（実装がKleene代数の公理を満たす事を証明）が完成してCoqのUser contributionsに載ったので、その話をしました。（当日のプレゼン資料に一部加筆）

　もうレポート提出期限も過ぎたので、今年のGarrigue先生の授業のレポート課題をみんなで解いてみよう、というのをしました。
　私の証明はこんな感じ。最初の命題論理の証明は問題無かった様子。

Section Coq1. 
Variables P Q R : Prop. 
Theorem and_compose : (P -> Q) -> (P -> R) -> P -> Q /\ R. 
Proof.
  intros pq pr p.
  split.
    apply (pq p).
    apply (pr p).
Qed.
Theorem or_modus : P \/ (Q -> R) -> Q -> P \/ R.
Proof.
  intros p_qr q.
  destruct p_qr as [p|qr].
    left.  apply p.
    right.  apply (qr q).
Qed.
End Coq1.

次が append に関する性質で、これは解けた人が多かったです。

Section Coq2. 
Require Import List. 
Variable A : Set.
Fixpoint append (l1 l2 : list A) {struct l1} := 
match l1 with 
| nil => l2 
| a :: l => a :: append l l2
end.
Theorem append_inv_head : forall l l1 l2 : list A, 
  append l l1 = append l l2 -> l1 = l2.
Proof.
  induction l.
    intros.  simpl in H.  auto.

    intros.  simpl in H.  inversion H.
    eapply IHl.  auto.
Qed.

後半の問題は難しいみたいでした。私の解答は下記です。最初に幾つか補題を定義して目的の定理を証明しました、というのは嘘で、目的の定理を証明してる最中に欲しくなった補題を戻って証明しただけです。inversionが使えれば解ける問題だと思うので、やはりCoq初心者脱出の鍵はinversionを使える様になる、かと思う。

Lemma append_nil : forall l, append l nil = l.
Proof.
  induction l; simpl; [|erewrite IHl]; auto.
Qed.
Lemma append_l1_a_l2 : forall a l1 l2,
  append l1 (a::l2) = append (l1 ++ a::nil) l2.
Proof.
  induction l1; intros; simpl; [|erewrite IHl1]; auto.
Qed.
Lemma append_cons_not_nil : forall (a:A) l l', l ++ a::l' <> nil.
Proof.
  induction l; simpl; intros; intro; discriminate H.
Qed.
Lemma append_inv_a : forall (a:A) l1 l2,
  l1 ++ a :: nil = l2 ++ a :: nil -> l1 = l2.
Proof.
  induction l1; induction l2; simpl; intros. 
    (* l1 = nil, l2 = nil *)
    auto.
    (* l1 = nil, l2 = a0::l2 *)
    inversion H.
    specialize(append_cons_not_nil a0 l2 nil).  intros.
    rewrite <- H2 in H0.  elim H0.  auto.
    (* l1 = a::l1, l2 = nil *)
    inversion H.
    specialize(append_cons_not_nil a l1 nil).  intros.
    rewrite H2 in H0.  elim H0.  auto.
    (* l1 = a::l1, l2 = a0::l2 *)
    inversion H.
    rewrite (IHl1 l2 H2).  auto.
Qed.
Theorem append_inv_tail : forall l l1 l2 : list A, 
  append l1 l = append l2 l -> l1 = l2.
Proof.
  induction l; intros; simpl in H.
    (* l = nil *)
    repeat erewrite append_nil in H.  auto.
    (* l = a::l *)
    rewrite (append_l1_a_l2 a l1 l) in H.
    rewrite (append_l1_a_l2 a l2 l) in H.
    eapply (append_inv_a a).  eapply (IHl _ _ H).
Qed.
End Coq2.

revして前の定理に帰着せせる、という解答もありました。そっちは思いつかなかった。

　あとは、HOL-OCLというのがあるよ、とか。OCLってどの程度メジャーなんでしょうか。広く使われていて需要がありそうならIsabelleも勉強すべきかなぁ、とか。

[Coq] TAPL Chapter 8

TAPL Chap.8 の演習問題をCoqで証明しました。型があるのでChap.3より寧ろ楽かも。

http://ideone.com/ttTKY

[Coq] Sample of Setoid

先日のFormal Methods Forumで話したsetoidの話のCoqのコード。

Require Import Setoid.
Require Import Relation_Definitions.
Require Import Arith.
Require Import Compare_dec.
Require Import Omega.

Section MyZ.

(* 整数 Z' を構成するのに、nat * nat に同値関係 Z'eq を入れたものを用いる。
  (a,b) in nat*nat に対し、a-b でZ'を作る、と考えてよい。 *)

(* Z' のコンストラクタ *)
Inductive Z' : Set :=
| mkZ' : nat -> nat -> Z'.

(* 同値関係 : (a,b) =Z= (c,d) iff a+d = b+c *)
Definition Z'eq (z z':Z') : Prop :=
  let (a,b) := z in
  let (c,d) := z' in
  a + d = b + c.

Notation "a =Z= b" := (Z'eq a b) (at level 70).

(* 後々の証明で使いやすい補題 *)
Lemma Z'eq_inv : forall a b c d, (mkZ' a b) =Z= (mkZ' c d) ->
  {exists q, (a=c+q /\ b=d+q)} + {exists q, (a+q=c /\ b+q=d)}.
Proof.
  intros.  simpl in H.
  destruct (le_lt_dec a c).
    (* a <= c *)
    right.  exists (c - a).  omega.
    (* c < a *)
    left.  exists (a - c).  omega.
Qed.

(* Z'eq が同値関係であることを証明する *)
Print reflexive.
Lemma Z'eq_refl : reflexive Z' Z'eq.
Proof.
  unfold reflexive.  intros.  destruct x.
  unfold Z'eq.  omega.
Qed.

Print symmetric.
Lemma Z'eq_sym : symmetric Z' Z'eq.
Proof.
  unfold symmetric.  intros.  destruct x.  destruct y.
  unfold Z'eq in *.  omega.
Qed.

Print transitive.
Lemma Z'eq_trans : transitive Z' Z'eq.
Proof.
  unfold transitive.  intros.  destruct x. destruct y. destruct z.
  unfold Z'eq in *.  omega.
Qed.

(* Z'eq が同値関係であることが示せたので Setoid を構成する *)
Add Parametric Relation : Z' Z'eq
  reflexivity proved by Z'eq_refl
  symmetry proved by Z'eq_sym
  transitivity proved by Z'eq_trans
  as Z'_rel.

(* Z' 上の演算を定義する *)
Definition Z'plus (z z':Z') : Z' :=
  let (a,b) := z in
  let (c,d) := z' in
  mkZ' (a+c) (b+d).

Add Parametric Morphism : Z'plus with
  signature Z'eq ==> Z'eq ==> Z'eq as Z'_plus_mor.
Proof.
  (* Goal := x =Z= y -> x0 =Z= y0 -> Z'plus x x0 =Z= Z'plus y y0
  Z'plus が well-defined であることを示す必要がある *)
  intros.  destruct x; destruct y; destruct x0; destruct y0.
  unfold Z'eq in *.  unfold Z'plus.  omega.
Qed.

(* 準備 *)
Lemma Z'eq_plus_id_l : forall z a, Z'plus (mkZ' a a) z =Z= z.
Proof.
  intros.  destruct z.
  unfold Z'plus; unfold Z'eq.  omega.
Qed.

Lemma Z'eq_plus_comm : forall z z', Z'plus z z' =Z= Z'plus z' z.
Proof.
  intros.  destruct z; destruct z'.
  unfold Z'plus; unfold Z'eq.  omega.
Qed.

(* setoid_rewrite を使ってみる例 *)
Lemma Z'eq_plus_id_r : forall z a, Z'plus z (mkZ' a a) =Z= z. 
Proof.
  intros.
  setoid_rewrite (Z'eq_plus_comm z (mkZ' a a)).
  apply Z'eq_plus_id_l.
Qed.

End MyZ.

[7-Lang][Ruby] Seven Languages in Seven Weeks : Ruby Day 1

　Bruce TateのSeven Languages in Seven Weeksを読み始めました。
　最初の言語はRubyです。各言語をキャラクターに例えているのですが、Ruby = Merry Poppins らしい。
　１日目の課題はこんな感じでOKなのかしらん。

>> puts 'Hello, World!'
Hello, World!
=> nil
>> p "Hello, Ruby".index("Ruby")
7
=> nil
>> puts "@tmiya_\n"*10
@tmiya_
@tmiya_
@tmiya_
@tmiya_
@tmiya_
@tmiya_
@tmiya_
@tmiya_
@tmiya_
@tmiya_
=> nil
>> (1..10).each {|n| puts "This is sentence number #{n}" }
This is sentence number 1
This is sentence number 2
This is sentence number 3
This is sentence number 4
This is sentence number 5
This is sentence number 6
This is sentence number 7
This is sentence number 8
This is sentence number 9
This is sentence number 10
=> 1..10

% ruby numberGuess.rb
5
too large
3
too large
1
too small
2
correct!
% cat numberGuess.rb
randomNumber = rand(10)
while ((guess = gets.to_i) != randomNumber)
  if guess < randomNumber then
    puts "too small"
  else
    puts "too large"
  end
end
puts "correct!"

[Misc] Blog Design Changed

Blogのデザインをちょっといじってみました。

[Memo] How to translate LaTeX file with po4a + OmegaT

忘れない様に作業手順メモ
Mac OS X 10.5 で po4a と OmegaT で TeX 文書を翻訳を参考に。

最初にファイルを作るのは

• そもそもTutorial.v.texはTutorial.texからmake tutorialとかで作る。CoqのMakefile参照。


• ~/usr/share/perl/po4a-0.41/po4a-gettextize -f latex -m Tutorial.v.tex -p Tutorial.v.pot


• 上記が通らない場合は po4a の LaTeX.pm, TeX.pm を無理に直したりする。po4a からは platex ではなく latex が呼ばれるのでスタイルも jsbook から book にしたり、フランス人の人名を ASCII の範囲にしたりなど最初に直す。
  

あとはOmegaTを使って翻訳。

• ~/coq/coq-8.2pl1/doc/tutorial/にあるCoq_TutorialというOmegaTプロジェクトを開いて翻訳する。一段落したら訳文ファイル生成。


• cd ~/coq/coq-8.2pl1/doc/tutorial/


• cp Coq_Tutorial/target/Tutorial.v.pot ja.pot


• ~/usr/share/perl/po4a-0.41/po4a-translate -f latex -m Tutorial.v.tex -p ja.pot -l ja.tex


• フォーマットを直す場合はbookじゃなくjsbookに直す。


• platex ja.tex ; platex ja.tex ; dvipdfmx ja.dvi