Functional Programming Memo

[Coq] Coq Tutorial on 1/12, 2/2, 2/9, and 2/16

2012-01-19T16:53:00.002+09:00

イベントレポート：「Coqチュートリアル#1」 @ InfoQ

今回、豆蔵様より会場を提供していただけることになって、前々から計画していた平日夜の複数回開催のCoqチュートリアルを 1/12, 2/2, 2/9, 2/16 という予定で開催します。
参加申し込みについては上記リンクから辿って頂ければと思います。

[Coq] itoa in Coq

2012-01-05T22:40:00.002+09:00

https://github.com/tmiya/coq/blob/master/Radix/Radix.v

自然数$n$を$p \ge 2$で割って余りを求め、商をまた割って、と繰り返すことで$n$の$p$進表示を得られますが、そのencode/decodeをCoqで書きました。勿論、encodeとdecodeが逆関数になっていることも証明済みです。
encode関数を使って、C言語にあるitoa関数を書きました。これがあれば、数字を文字列に変換出来ますからFizzBuzzもCoqで書けます。
そのうちCoq user contributionに登録しよう。

[Misc] 2011 Summary

2011-12-31T21:09:00.004+09:00

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

2011-12-30T15:25:00.002+09:00

通常、群$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)

2011-12-16T07:06:00.000+09:00

この記事は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

2011-12-15T07:39:00.000+09:00

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

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

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

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

2011-12-03T01:00:00.000+09:00

この記事は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

2011-11-03T17:02:00.003+09:00

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

2011-10-28T18:24:00.000+09:00

社内勉強会で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

2011-10-10T17:07:00.001+09:00

今日の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

2011-09-04T00:43:00.001+09:00

スタート代数という勉強会に参加してきました。そこで出された宿題のうち１問を 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

2011-09-02T14:23:00.001+09:00

jStar: Bringing separation logic to JavaJava 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

2011-08-26T00:40:00.002+09:00

先日、スタート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

2011-06-04T22:55:00.002+09:00

形式手法勉強会の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

2011-04-12T07:25:00.002+09:00

第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)

2011-04-12T07:11:00.003+09:00

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

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

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

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

[Coq] Formal Methods Forum 2011/03/05

2011-03-06T07:55:00.003+09:00

昨日は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

2011-03-02T22:12:00.001+09:00

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

http://ideone.com/ttTKY

[Coq] Sample of Setoid

2011-01-31T01:04:00.002+09:00

先日の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

2011-01-10T01:23:00.002+09:00

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

2011-01-09T10:19:00.001+09:00

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

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

2011-01-09T09:30:00.004+09:00

忘れない様に作業手順メモ
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



[Coq] How to Find Unreachable Nodes
2010-12-24T22:56:00.003+09:00
不正な状態遷移を見つけるアルゴリズム @ kencobaの日記経由。

答えを出すだけならこんなのでもOK?　元の問題の規模が判らないが、この程度に小さな問題なら auto で探索出来る。

Axiom O A B C D E F G H I:Prop.
Axiom OA : O -> A.
Axiom AB : A -> B.
Axiom BC : B -> C.
Axiom CB : C -> B.
Axiom CA : C -> A.
Axiom DB : D -> B.
Axiom DH : D -> H.
Axiom HD : D -> H.
Axiom EF : E -> F.
Axiom FG : F -> G.
Axiom GF : G -> F.
Axiom GE : G -> E.
Axiom II : I -> I.

Hint Resolve OA AB BC CB CA DB DH HD EF FG GF GE II.

Goal O -> A. info auto. Qed.
Goal O -> B. info auto. Qed.
Goal O -> C. info auto. Qed.


Goal O -> D.などはauto.で証明出来ないので、path が無いと判る。


[Coq] Coq Advent Calender : reflexivity (25 of 25)
2010-12-24T00:01:00.000+09:00
Coq でよく使われる tactic の紹介も今回で最後。最終回は reflexivity を紹介します。

　reflexivity はゴールが等式で、左辺と右辺の値が等しい時に使います。内容的には apply refl_equal. と同じです。refl_equal はこんな公理。

Inductive eq (A : Type) (x : A) : A -> Prop :=  refl_equal : x = x

　左辺と右辺が全く同じ形をしていないと等式は成り立ちません（が、reflexivity は内部的に simpl を実行しているので simpl で簡単化して等しくなる物は成立します）。

　ところで、同じ形というのはどこまで同じならば = が成り立つかというのは良く解らないので色々試してみました。

Coq < Definition f : nat -> nat := fun x => x.
Coq < Definition h : nat -> nat := fun y => y .
Coq < Goal f = h.
1 subgoal
  
  ============================
   f = h

Unnamed_thm < simpl.
1 subgoal
  
  ============================
   f = h

Unnamed_thm < unfold f.
1 subgoal
  
  ============================
   (fun x : nat => x) = h

Unnamed_thm < unfold h.
1 subgoal
  
  ============================
   (fun x : nat => x) = (fun y : nat => y)

Unnamed_thm < reflexivity.
Proof completed.

Unnamed_thm < Qed.

　これを見ると、(fun x : nat => x) = (fun y : nat => y) は成立するようです。同様に、

Coq < Goal forall P:nat->Prop, (forall n, P n) = (forall m, P m).
Unnamed_thm0 < intros P.
Unnamed_thm0 < reflexivity.
Proof completed.

　これを見ると、(forall n : nat, P n) = (forall m : nat, P m) も成立。

　上記の f, h の場合はreflexivityで等しい事が示せましたが、一般には関数が等しい事を reflexivity で証明する事は出来ません。　
　f, g : nat -> nat について、f = g ⇔ ∀n:nat, f n = g n.  を以て等しいとする場合は、こんな感じで証明します。

Coq < Definition f : nat -> nat := fun x => x.

Coq < Fixpoint g(x:nat):nat :=
Coq < match x with
Coq < | O => O
Coq < | S n' => S (g n')
Coq < end.

Coq < Require Import Logic.FunctionalExtensionality.

Coq < Lemma Sample_of_reflexivity : f = g.
1 subgoal
  
  ============================
   f = g

Sample_of_reflexivity < extensionality n.
1 subgoal
  
  n : nat
  ============================
   f n = g n

Sample_of_reflexivity < unfold f.
1 subgoal
  
  n : nat
  ============================
   n = g n

Sample_of_reflexivity < induction n.
2 subgoals
  
  ============================
   0 = g 0

subgoal 2 is:
 S n = g (S n)

Sample_of_reflexivity < reflexivity.
1 subgoal
  
  n : nat
  IHn : n = g n
  ============================
   S n = g (S n)

Sample_of_reflexivity < simpl.
1 subgoal
  
  n : nat
  IHn : n = g n
  ============================
   S n = S (g n)

Sample_of_reflexivity < rewrite <- IHn.
1 subgoal
  
  n : nat
  IHn : n = g n
  ============================
   S n = S n

Sample_of_reflexivity < reflexivity.
Proof completed.

Sample_of_reflexivity < Qed.


　他にも、= を同値関係を以て定義する場合は Setoid というものを使って考える（Coqの型理論には集合論の商集合が無いので、代わりに = を同値関係で置き換えた物を使う）とか有るらしいのですが、そっちはちょっと調べきれませんでした。

ーーーーー

★後書き★

　Coq Advent Calender を始めるにあたっては、Coq Partyでのmaeda_さんの発表に有った「tactic使用例が有ると嬉しい」と「coqでの人気tactic」という話題からネタを頂きました。
　25個もあると自分では使った事の無いtacticとかもあって結構使い方を調べたり、あるいは適当な証明課題を探したりなど、それなりに大変で、何度か挫けそうになりましたがなんとか最後まで書けて良かったです。
　Coq を学ぶ人の参考になると良いなぁ。


[Coq] Coq Advent Calender : exact (24 of 25)
2010-12-23T09:38:00.002+09:00
Coq でよく使われる tactic の24番目は exact です。

　現在のゴールが、仮定のどれか、あるいは既存の定理にマッチする時に exact H?. とか exact my_theorem. とかするとゴールが証明されます。前者の場合は assumption. で済みますし、exact ではなく apply でもOKなんで、無理に使う必要は無いですが、ゴールと同じ物があったという意図を多少は示せるのかも。

　exact を使って書いてみました。

Coq < Lemma Sample_of_exact : forall n m, n + m = m + n.
1 subgoal
  
  ============================
   forall n m : nat, n + m = m + n

Sample_of_exact < intros.
1 subgoal
  
  n : nat
  m : nat
  ============================
   n + m = m + n

Sample_of_exact < induction n.
2 subgoals
  
  m : nat
  ============================
   0 + m = m + 0

subgoal 2 is:
 S n + m = m + S n

Sample_of_exact < simpl.
2 subgoals
  
  m : nat
  ============================
   m = m + 0

subgoal 2 is:
 S n + m = m + S n

Sample_of_exact < exact (plus_n_O m).
1 subgoal
  
  n : nat
  m : nat
  IHn : n + m = m + n
  ============================
   S n + m = m + S n

Sample_of_exact < simpl.
1 subgoal
  
  n : nat
  m : nat
  IHn : n + m = m + n
  ============================
   S (n + m) = m + S n

Sample_of_exact < rewrite IHn. 
1 subgoal
  
  n : nat
  m : nat
  IHn : n + m = m + n
  ============================
   S (m + n) = m + S n

Sample_of_exact < exact (plus_n_Sm m n).
Proof completed.

Sample_of_exact < Qed.



[Link] Formal Methods Forum
2010-12-22T23:35:00.003+09:00
東京でほぼ毎月開催している形式手法の勉強会、Formal Methods Forum ですが、FMFのGoogle groupに登録して頂くと開催案内や開催日程相談のメールが配信されます。
　ATNDで告知しているのですが、Google groupに登録して頂いた方がより確実だと思います。

　活動内容ですが11月分についてはkencobaさんの日記なんかも参考にして頂けるといいかと。


[Coq] Coq Advent Calender : specialize (23 of 25)
2010-12-22T00:01:00.000+09:00
Coq でよく使われる tactic の23番目は specialize です。

　公理とかライブラリにある定理とか証明済み補題とかに特定の引数を適用した物を仮定に使いたい事があります。forall n, P n. みたいな補題Lのnに特定の値 n0 を代入した P n0 が仮定にあると良いなぁ、とか。
　勿論、assert(H:P n0)とかcut (P n0)とか書いても良いのですが、specialize (L n0). と書けば cut (P n0)してapply (L n0) するのと同じになり、証明が短く判りやすくなります。

replaceの説明の時と同じ定理を、replaceを使わず、specializeとrewriteを使って証明してみます。証明の前提と成る公理は replace の回を参照して下さい。

Coq < Theorem inv_r : forall a:G, a * (inv a) = 1.
1 subgoal
  
  ============================
   forall a : G, a * inv a = 1

inv_r < intros.
1 subgoal
  
  a : G
  ============================
   a * inv a = 1

inv_r < specialize (id_l (a * inv a)).
1 subgoal
  
  a : G
  ============================
   1 * (a * inv a) = a * inv a -> a * inv a = 1

specializeすると、公理 id_l に (a * inv a) を適用した物が得られますので、intro して書き換えて消去します。あとは同様に。

inv_r < intro H; rewrite <- H; clear H.
1 subgoal
  
  a : G
  ============================
   1 * (a * inv a) = 1

inv_r < specialize (inv_l (inv a)); intro H; rewrite <- H; clear H.
1 subgoal
  
  a : G
  ============================
   inv (inv a) * inv a * (a * inv a) = inv (inv a) * inv a

inv_r < specialize (assoc (inv (inv a)) (inv a) (a * inv a)); intro H; rewrite H; clear H.
1 subgoal
  
  a : G
  ============================
   inv (inv a) * (inv a * (a * inv a)) = inv (inv a) * inv a

inv_r < specialize (assoc (inv a) a (inv a)); intro H; rewrite <- H; clear H.
1 subgoal
  
  a : G
  ============================
   inv (inv a) * (inv a * a * inv a) = inv (inv a) * inv a

inv_r < specialize (inv_l a); intro H; rewrite H; clear H.
1 subgoal
  
  a : G
  ============================
   inv (inv a) * (1 * inv a) = inv (inv a) * inv a

inv_r < specialize (id_l (inv a)); intro H; rewrite H; clear H.
1 subgoal
  
  a : G
  ============================
   inv (inv a) * inv a = inv (inv a) * inv a

inv_r < reflexivity.
Proof completed.

inv_r < Qed.



[Coq] Coq Advent Calender : left, right (21,22 of 25)
2010-12-21T04:35:00.003+09:00
Coqでよく使われる tactic の21,22番目は left と right です。
　最初に25個と決めて、でもよく考えると12/24で終了すべき。都合が良いのでここで２つ紹介して帳尻を合わせます。

　left は constructor 1 、right は constructor 2 の意味で、実は goal が A \/ B の場合に限らず、コンストラクタが２通りあってどちらかを明示的に指定したい時に使えます。
　大抵そういう場合は左右と対応している訳ですが、例えば nat とかも left が O を指すはず。同様に n:nat に対して destruct n ではなく split とかも使えるはず。単に他人に判りにくいだけですが。

　今回は sumbool について left, right を使う例です。やはり左右に対応しています。

Coq < Lemma Sample_of_left_right : forall n:nat, {n = 0} + {n <> 0}.
1 subgoal
  
  ============================
   forall n : nat, {n = 0} + {n <> 0}

Sample_of_left_right < induction n.
2 subgoals
  
  ============================
   {0 = 0} + {0 <> 0}

subgoal 2 is:
 {S n = 0} + {S n <> 0}

Sample_of_left_right < left.
2 subgoals
  
  ============================
   0 = 0

subgoal 2 is:
 {S n = 0} + {S n <> 0}

Sample_of_left_right < reflexivity.
1 subgoal
  
  n : nat
  IHn : {n = 0} + {n <> 0}
  ============================
   {S n = 0} + {S n <> 0}

Sample_of_left_right < right.
1 subgoal
  
  n : nat
  IHn : {n = 0} + {n <> 0}
  ============================
   S n <> 0

Sample_of_left_right < intro.
1 subgoal
  
  n : nat
  IHn : {n = 0} + {n <> 0}
  H : S n = 0
  ============================
   False

Sample_of_left_right < inversion H.
Proof completed.

Sample_of_left_right < Qed.



[Coq] Coq Advent Calender : generalize (20 of 25)
2010-12-20T00:54:00.000+09:00
Coqでよく使われる tactic の20番目は generalize です。

　generalize は intro の逆で、具体的な値の term を、"forall t" のような形に戻します。
　簡単な使用例は下記の様なものです。

Coq < Lemma sample_of_generalize : forall x y, 0 <= x + y + y.
1 subgoal
  
  ============================
   forall x y : nat, 0 <= x + y + y

sample_of_generalize < intros.
1 subgoal
  
  x : nat
  y : nat
  ============================
   0 <= x + y + y

sample_of_generalize < generalize (x + y + y).
1 subgoal
  
  x : nat
  y : nat
  ============================
   forall n : nat, 0 <= n

sample_of_generalize < Require Import Arith.Le.

sample_of_generalize < apply le_O_n.
Proof completed.

sample_of_generalize < Qed.


　単純に generalize で戻せない場合は、generalize dependent t のような形で使います。例えば下記の証明（TAPLの練習問題の証明）で使っています。よほど明らかな場合以外は、generalize dependentの形で使う事が多い様に思います。
　まず証明の前提の定義を幾つか。

Inductive term : Set :=
| TmTrue : term
| TmFalse : term
| TmIf : term -> term -> term -> term
| TmZero : term
| TmSucc : term -> term
| TmPred : term -> term
| TmIszero : term -> term.

Inductive nvalue : term -> Prop :=
| NvZero : nvalue TmZero
| NvSucc : forall t, nvalue t -> nvalue (TmSucc t).

Inductive bvalue : term -> Prop :=
| BvTrue : bvalue TmTrue
| BvFalse : bvalue TmFalse.

Definition value(t:term) : Prop := bvalue t \/ nvalue t.

Inductive eval : term -> term -> Prop :=
| EvIfTrue : forall t2 t3, eval (TmIf TmTrue t2 t3) t2
| EvIfFalse : forall t2 t3, eval (TmIf TmFalse t2 t3) t3
| EvIf : forall t1 t1' t2 t3, eval t1 t1' -> eval (TmIf t1 t2 t3) (TmIf t1' t2 t3)
| EvSucc : forall t1 t1', eval t1 t1' -> eval (TmSucc t1) (TmSucc t1')
| EvPred : forall t1 t1', eval t1 t1' -> eval (TmPred t1) (TmPred t1')
| EvPredZero : eval (TmPred TmZero) TmZero
| EvPredSucc : forall nv, nvalue nv -> eval (TmPred (TmSucc nv)) nv
| EvIszeroZero : eval (TmIszero TmZero) TmTrue
| EvIszeroSucc : forall nv, nvalue nv -> eval (TmIszero (TmSucc nv)) TmFalse
| EvIszero : forall t1 t1', eval t1 t1' -> eval (TmIszero t1) (TmIszero t1').

Notation "t1 --> t2" := (eval t1 t2) (at level 80, no associativity).

Definition normal_form (t : term) : Prop := ~ exists t', eval t t'.

　ここで下記の定理を証明します。intros を下記の様にすると予めdestructした形で intros 可能です。

Coq < Lemma value_is_normal_form : forall v, value v -> normal_form v.
1 subgoal
  
  ============================
   forall v : term, value v -> normal_form v

value_is_normal_form < intros v [bv|nv] [t vEt].
2 subgoals
  
  v : term
  bv : bvalue v
  t : term
  vEt : v --> t
  ============================
   False

subgoal 2 is:
 False

value_is_normal_form < destruct bv; inversion vEt.
1 subgoal
  
  v : term
  nv : nvalue v
  t : term
  vEt : v --> t
  ============================
   False

ここで t をgeneralize dependentします。（generalize t だと、forall t:term, にならずうまくいかない。）

value_is_normal_form < generalize dependent t.
1 subgoal
  
  v : term
  nv : nvalue v
  ============================
   forall t : term, v --> t -> False

value_is_normal_form < induction nv.
2 subgoals
  
  ============================
   forall t : term, TmZero --> t -> False

subgoal 2 is:
 forall t0 : term, TmSucc t --> t0 -> False

value_is_normal_form < intros t zEt.                
2 subgoals
  
  t : term
  zEt : TmZero --> t
  ============================
   False

subgoal 2 is:
 forall t0 : term, TmSucc t --> t0 -> False

value_is_normal_form < inversion zEt.
1 subgoal
  
  t : term
  nv : nvalue t
  IHnv : forall t0 : term, t --> t0 -> False
  ============================
   forall t0 : term, TmSucc t --> t0 -> False

value_is_normal_form < intros t0 stEt0.
1 subgoal
  
  t : term
  nv : nvalue t
  IHnv : forall t0 : term, t --> t0 -> False
  t0 : term
  stEt0 : TmSucc t --> t0
  ============================
   False

value_is_normal_form < inversion stEt0.
1 subgoal
  
  t : term
  nv : nvalue t
  IHnv : forall t0 : term, t --> t0 -> False
  t0 : term
  stEt0 : TmSucc t --> t0
  t1 : term
  t1' : term
  H0 : t --> t1'
  H : t1 = t
  H1 : TmSucc t1' = t0
  ============================
   False

value_is_normal_form < elim (IHnv t1').
1 subgoal
  
  t : term
  nv : nvalue t
  IHnv : forall t0 : term, t --> t0 -> False
  t0 : term
  stEt0 : TmSucc t --> t0
  t1 : term
  t1' : term
  H0 : t --> t1'
  H : t1 = t
  H1 : TmSucc t1' = t0
  ============================
   t --> t1'

value_is_normal_form < exact H0.
Proof completed.

value_is_normal_form < Qed.



[Coq] Coq Advent Calender : inversion (19 of 25)
2010-12-19T00:20:00.000+09:00
Coq でよく使われる tactic の19番目は inversion です。
　inversion は仮定に対して帰納的な定義を適用し、その仮定が成立する為の前提を導き出すか、あるいはそもそもそのような前提が存在しない（＝仮定が間違っている）ので証明終了、を導いてくれます。ある種の証明では inversion を使うと証明が非常に簡単なのですが、中で何をしているのかは簡単には説明するのは難しいです。

　inversionの使用例というと典型的にはこの関数を定義することになっています。

Coq < Inductive even : nat -> Prop :=
Coq < | EvenO : even O
Coq < | EvenSS : forall n, even n -> even (S (S n)).
even is defined
even_ind is defined

偶数である事を、上記の様に帰納的に定義します。

　では３が偶数でない事を証明しましょう。こういう定理の証明の時にはinversionが有用です。今回はinversionの中で何をしているかみたいのでinfo inversionとして使っています。

Coq < Lemma Sample_of_inversion : ~(even 3).
1 subgoal
  
  ============================
   ~ even 3

Sample_of_inversion < intro.
1 subgoal
  
  H : even 3
  ============================
   False

Sample_of_inversion < info inversion H.
 == assert (H0:3 = 3 -> False).
    refine match H in (even n) return (n = 3 -> False) with
           | EvenO => _
           | EvenSS x x0 => _ x x0
           end.
    intro H0; refine ((_:0 = 3 -> False) H0); clear H0; 
    intro H0; cut False;[intro H1|idtac].
    refine ((_:False -> False) H1); clear H1; intro H1;
       exact (False_ind False H1).
    
    exact (eq_ind 0
             (fun e : nat => match e with
                             | 0 => True
                             | S _ => False
                             end) I 3 H0).
    
    intro n; intro H0; intro H1; refine ((_:even n -> False) H0); 
    clear H0; refine ((_:S (S n) = 3 -> even n -> False) H1); 
    clear H1; intro H1;
       cut (n = 1);[intro H0|idtac].
    refine ((_:n = 1 -> even n -> False) H0); clear H0; 
    intro H0;
       refine (eq_ind 1 (fun n : nat => even n -> False) _ n _).
    clear H1; intro H1; dependent move H1 after H0.
    
    refine (sym_eq _);
       exact H0.
    
    exact (f_equal
             (fun e : nat =>
              match e with
              | 0 => n
              | 1 => n
              | S (S n) => n
              end) H1).
    
    refine (H0 _); change (3 = 3); exact (refl_equal 3).
    
1 subgoal
  
  H : even 3
  n : nat
  H1 : even 1
  H0 : n = 1
  ============================
   False

　H: even 3の前提にH1: even 1が前提である事が判りました。このH1について再度inversionを使います。

Sample_of_inversion < info inversion H1.
 == assert (H2:1 = 1 -> False).
    refine match H1 in (even n) return (n = 1 -> False) with
           | EvenO => _
           | EvenSS x x0 => _ x x0
           end.
    intro H2; refine ((_:0 = 1 -> False) H2); clear H2; 
    intro H2; cut False;[intro H3|idtac].
    refine ((_:False -> False) H3); clear H3; intro H3;
       exact (False_ind False H3).
    
    exact (eq_ind 0
             (fun e : nat => match e with
                             | 0 => True
                             | S _ => False
                             end) I 1 H2).
    
    intro n0; intro H2; intro H3; refine ((_:even n0 -> False) H2); 
    clear H2; refine ((_:S (S n0) = 1 -> even n0 -> False) H3); 
    clear H3; intro H3;
       cut False;[intro H2|idtac].
    refine ((_:False -> even n0 -> False) H2); clear H2; 
    intro H2;
       exact (False_ind (even n0 -> False) H2).
    
    exact (eq_ind (S (S n0))
             (fun e : nat =>
              match e with
              | 0 => False
              | 1 => False
              | S (S _) => True
              end) I 1 H3).
    
    refine (H2 _); change (1 = 1); exact (refl_equal 1).
    
Proof completed.

Sample_of_inversion < Qed.

H1を成立させる前提が無いので、証明完了になります。

　あと、inversionが役に立つ例というとsmall-stepの決定性の証明とかです。


Coq < Inductive term : Set :=
Coq < | TmTrue : term
Coq < | TmFalse : term
Coq < | TmIf : term -> term -> term -> term.
term is defined
term_rect is defined
term_ind is defined
term_rec is defined


Coq < Inductive eval : term -> term -> Prop :=
Coq < | EvIfTrue : forall t2 t3, eval (TmIf TmTrue t2 t3) t2 
Coq < | EvIfFalse : forall t2 t3, eval (TmIf TmFalse t2 t3) t3
Coq < | EvIf : forall t1 t1' t2 t3, eval t1 t1' ->
Coq <     eval (TmIf t1 t2 t3) (TmIf t1' t2 t3).
eval is defined
eval_ind is defined

上記の様にsmall-stepの規則を定義して、下記を証明します。

Coq < Theorem eval_deterministic : forall t t' t'', (eval t t') -> (eval t t'') -> (t' = t'').
1 subgoal
  
  ============================
   forall t t' t'' : term, eval t t' -> eval t t'' -> t' = t''

eval_deterministic < intros t t' t'' tEt' tEt''.
1 subgoal
  
  t : term
  t' : term
  t'' : term
  tEt' : eval t t'
  tEt'' : eval t t''
  ============================
   t' = t''

まず tEt' について induction で場合分けをします。

eval_deterministic < induction tEt' as [t2 t3|t2 t3|t1 t1' t2 t3 t1Et1'] in t'', tEt'' |-*.
3 subgoals
  
  t'' : term
  t2 : term
  t3 : term
  tEt'' : eval (TmIf TmTrue t2 t3) t''
  ============================
   t2 = t''

subgoal 2 is:
 t3 = t''
subgoal 3 is:
 TmIf t1' t2 t3 = t''

最初の場合は、t' = TmIf TmTrue t2 t3 の場合です。ここで tEt'' については induction ではなくinversion を使うと、tEt'' が成立するような t'' の場合分けを自動で行ってくれます。

eval_deterministic < inversion tEt'' as [t2_ t3_| t2_ t3_| t1_ t1'_ t2_ t3_ t1Et1'_].
4 subgoals
  
  t'' : term
  t2 : term
  t3 : term
  tEt'' : eval (TmIf TmTrue t2 t3) t''
  t2_ : term
  t3_ : term
  H0 : t2_ = t2
  H1 : t3_ = t3
  H2 : t2 = t''
  ============================
   t'' = t''

subgoal 2 is:
 t2 = TmIf t1'_ t2 t3
subgoal 3 is:
 t3 = t''
subgoal 4 is:
 TmIf t1' t2 t3 = t''

eval_deterministic < reflexivity.
3 subgoals
  
  t'' : term
  t2 : term
  t3 : term
  tEt'' : eval (TmIf TmTrue t2 t3) t''
  t1_ : term
  t1'_ : term
  t2_ : term
  t3_ : term
  t1Et1'_ : eval TmTrue t1'_
  H : t1_ = TmTrue
  H1 : t2_ = t2
  H2 : t3_ = t3
  H0 : TmIf t1'_ t2 t3 = t''
  ============================
   t2 = TmIf t1'_ t2 t3

subgoal 2 is:
 t3 = t''
subgoal 3 is:
 TmIf t1' t2 t3 = t''

　ここでinversion t1Et1'_を行います。TmTrueが何かにevalされる規則はevalに無いので、仮定が不成立となり、goalの証明が終わります。

eval_deterministic < inversion t1Et1'_.
2 subgoals
  
  t'' : term
  t2 : term
  t3 : term
  tEt'' : eval (TmIf TmFalse t2 t3) t''
  ============================
   t3 = t''

subgoal 2 is:
 TmIf t1' t2 t3 = t''

　t' = TmIfFalse t2 t3 の場合は同様の証明をすればOKです。

eval_deterministic < inversion tEt'' as [t2_ t3_| t2_ t3_| t1_ t1'_ t2_ t3_ t1Et1'_].
eval_deterministic < reflexivity.
eval_deterministic < inversion t1Et1'_.
1 subgoal
  
  t'' : term
  t1 : term
  t1' : term
  t2 : term
  t3 : term
  t1Et1' : eval t1 t1'
  tEt'' : eval (TmIf t1 t2 t3) t''
  IHt1Et1' : eval t1 t'' -> t1' = t''
  ============================
   TmIf t1' t2 t3 = t''

　最後は、t' = TmIf t1 t2 t3 の場合についてです。やはりtEt''についてinversionします。

eval_deterministic < inversion tEt'' as [t2_ t3_| t2_ t3_| t1_ t1'_ t2_ t3_ t1Et1'_].
3 subgoals
  
  t'' : term
  t1 : term
  t1' : term
  t2 : term
  t3 : term
  t1Et1' : eval t1 t1'
  tEt'' : eval (TmIf t1 t2 t3) t''
  IHt1Et1' : eval t1 t'' -> t1' = t''
  t2_ : term
  t3_ : term
  H0 : TmTrue = t1
  H1 : t2_ = t2
  H2 : t3_ = t3
  H3 : t2 = t''
  ============================
   TmIf t1' t'' t3 = t''

subgoal 2 is:
 TmIf t1' t2 t'' = t''
subgoal 3 is:
 TmIf t1' t2 t3 = TmIf t1'_ t2 t3

　ここでも、H0とt1Et1'から、eval TmTrue t1'を作ってinversionして仮定が成立しない事を使って証明します。

eval_deterministic < rewrite <- H0 in t1Et1'.
3 subgoals
  
  t'' : term
  t1 : term
  t1' : term
  t2 : term
  t3 : term
  t1Et1' : eval TmTrue t1'
  tEt'' : eval (TmIf t1 t2 t3) t''
  IHt1Et1' : eval t1 t'' -> t1' = t''
  t2_ : term
  t3_ : term
  H0 : TmTrue = t1
  H1 : t2_ = t2
  H2 : t3_ = t3
  H3 : t2 = t''
  ============================
   TmIf t1' t'' t3 = t''

subgoal 2 is:
 TmIf t1' t2 t'' = t''
subgoal 3 is:
 TmIf t1' t2 t3 = TmIf t1'_ t2 t3

eval_deterministic < inversion t1Et1'.
2 subgoals
  
  t'' : term
  t1 : term
  t1' : term
  t2 : term
  t3 : term
  t1Et1' : eval t1 t1'
  tEt'' : eval (TmIf t1 t2 t3) t''
  IHt1Et1' : eval t1 t'' -> t1' = t''
  t2_ : term
  t3_ : term
  H0 : TmFalse = t1
  H1 : t2_ = t2
  H2 : t3_ = t3
  H3 : t3 = t''
  ============================
   TmIf t1' t2 t'' = t''

subgoal 2 is:
 TmIf t1' t2 t3 = TmIf t1'_ t2 t3

　同様にして、TmFalse の場合も証明出来ます。

eval_deterministic < rewrite <- H0 in t1Et1'.
eval_deterministic < inversion t1Et1'.
1 subgoal
  
  t'' : term
  t1 : term
  t1' : term
  t2 : term
  t3 : term
  t1Et1' : eval t1 t1'
  tEt'' : eval (TmIf t1 t2 t3) t''
  IHt1Et1' : forall t'' : term, eval t1 t'' -> t1' = t''
  t1_ : term
  t1'_ : term
  t2_ : term
  t3_ : term
  t1Et1'_ : eval t1 t1'_
  H0 : t1_ = t1
  H1 : t2_ = t2
  H2 : t3_ = t3
  H3 : TmIf t1'_ t2 t3 = t''
  ============================
   TmIf t1' t2 t3 = TmIf t1'_ t2 t3

最後はIHt1Et1'のt''をt1'_にして、t1Et1'_と組み合わせてゴールを導きます。

eval_deterministic < rewrite (IHt1Et1' t1'_ t1Et1'_).
eval_deterministic < reflexivity.
Proof completed.

eval_deterministic < Qed.



[Coq] Coq Advent Calender : clear (18 of 25)
2010-12-18T00:12:00.001+09:00
Coq でよく使われる tactic の18番目は clear です...って使わないと思うけどなぁ。

　clear Hとすると、仮定 H が消えます。下記の様な感じです。

Coq < Lemma Sample_of_clear : forall A B C, (A->B->C)->(A->B)->A->C.
1 subgoal
  
  ============================
   forall A B C : Type, (A -> B -> C) -> (A -> B) -> A -> C

Sample_of_clear < intros A B C abc ab a.
1 subgoal
  
  A : Type
  B : Type
  C : Type
  abc : A -> B -> C
  ab : A -> B
  a : A
  ============================
   C

Sample_of_clear < apply abc; clear abc.
2 subgoals
  
  A : Type
  B : Type
  C : Type
  ab : A -> B
  a : A
  ============================
   A

subgoal 2 is:
 B

Sample_of_clear < exact a.
1 subgoal
  
  A : Type
  B : Type
  C : Type
  ab : A -> B
  a : A
  ============================
   B

Sample_of_clear < apply ab; clear ab.
1 subgoal
  
  A : Type
  B : Type
  C : Type
  a : A
  ============================
   A

Sample_of_clear < exact a.
Proof completed.

Sample_of_clear < Qed.

　使い終わって不要になった仮定をclearで消すと多少見通しが良くなる事もありますが、あまり使わないのではないかなぁ。

　むしろ、各種 tactic の中で内部的に使われる事が多い様な気がします。例えば下記の簡単な tactic の swap の中で使われています。apply して一回使った仮定は不要なので clear で消しているようです。

Ltac swap H := 
  idtac "swap is OBSOLETE: use contradict instead.";
  intro; apply H; clear H.

　これを使った証明です。

Coq < Lemma Sample_of_claer : forall P, ~~~P -> ~P.
1 subgoal
  
  ============================
   forall P : Prop, ~ ~ ~ P -> ~ P

Sample_of_claer < intros.
1 subgoal
  
  P : Prop
  H : ~ ~ ~ P
  ============================
   ~ P

Sample_of_claer < swap H.
swap is OBSOLETE: use contradict instead.
1 subgoal
  
  P : Prop
  H0 : P
  ============================
   ~ ~ P

Sample_of_claer < swap H.
swap is OBSOLETE: use contradict instead.
1 subgoal
  
  P : Prop
  H0 : P
  ============================
   P

Sample_of_claer < exact H0.
Proof completed.

Sample_of_claer < Qed.
intros.
swap H.
swap ipattern:H.
exact H0.

Sample_of_claer is defined

Coq < 



[Coq] Coq Advent Calender : elim (17 of 25)
2010-12-17T10:54:00.002+09:00
Coq でよく使われる tactic の17番目は elim です。

　elim はほとんど induction と同じ事が出来ます。例えばこんな感じ。帰納法の仮定を自分で intro する必要があるのが違います。

Coq < Lemma Sample_of_elim : forall n, n + 0 = n.
1 subgoal
  
  ============================
   forall n : nat, n + 0 = n

Sample_of_elim < intros.
1 subgoal
  
  n : nat
  ============================
   n + 0 = n

Sample_of_elim < elim n.
2 subgoals
  
  n : nat
  ============================
   0 + 0 = 0

subgoal 2 is:
 forall n0 : nat, n0 + 0 = n0 -> S n0 + 0 = S n0

Sample_of_elim < 


　ただこうやって帰納法で使うときはinductionする方が多い様にも思います。（golfだとelimが有利なのかな？）

　下記の様にゴールが False で、仮定が ~P の形をしている時は、私は習慣で他のタクティックではなく elim を使います。こんな感じ。

Coq < Lemma Sample_of_elim' : forall P, ~~(P \/ ~P).
1 subgoal
  
  ============================
   forall P : Prop, ~ ~ (P \/ ~ P)

Sample_of_elim' < intros.
1 subgoal
  
  P : Prop
  ============================
   ~ ~ (P \/ ~ P)

Sample_of_elim' < intro npnp.
1 subgoal
  
  P : Prop
  npnp : ~ (P \/ ~ P)
  ============================
   False

Sample_of_elim' < elim npnp.
1 subgoal
  
  P : Prop
  npnp : ~ (P \/ ~ P)
  ============================
   P \/ ~ P

Sample_of_elim' < right.
1 subgoal
  
  P : Prop
  npnp : ~ (P \/ ~ P)
  ============================
   ~ P

Sample_of_elim' < intro p.
1 subgoal
  
  P : Prop
  npnp : ~ (P \/ ~ P)
  p : P
  ============================
   False

Sample_of_elim' < elim npnp.
1 subgoal
  
  P : Prop
  npnp : ~ (P \/ ~ P)
  p : P
  ============================
   P \/ ~ P

Sample_of_elim' < left.
1 subgoal
  
  P : Prop
  npnp : ~ (P \/ ~ P)
  p : P
  ============================
   P

Sample_of_elim' < exact p.   
Proof completed.

Sample_of_elim' < Qed.
intros.
intro npnp.
elim npnp.
right.
intro p.
elim npnp.
left.
exact p.

Sample_of_elim' is defined

Coq < 



[Coq] Coq Advent Calender : ring (16 of 25)
2010-12-16T01:39:00.000+09:00
Coq でよく使われる tactic の16番目は ring です。

　ring は可換な半環 ( 演算 +, * があって、それぞれ単位元 0, 1 があって、それぞれ交換則と結合則が成り立って、分配法則があってな数学的構造）での計算を行ってくれます。基本的には多項式の掛け算を展開し、標準形に直して比較するようなことをします。
　使用するにはRequire Import Ring.が必要です。

　下記で色々試してみましたが、適宜 rewrite, replace なども併用しないとうまくいきませんでした。


Coq < Require Import ZArith Ring.

Coq < Open Scope Z_scope.

Coq < Lemma Sample_of_ring : forall a b:Z, a + b = 7 -> a * b = 12 -> a^2 + b^2 = 25.
1 subgoal
  
  ============================
   forall a b : Z, a + b = 7 -> a * b = 12 -> a ^ 2 + b ^ 2 = 25

Sample_of_ring < intros a b H1 H2.
1 subgoal
  
  a : Z
  b : Z
  H1 : a + b = 7
  H2 : a * b = 12
  ============================
   a ^ 2 + b ^ 2 = 25

Sample_of_ring < replace (a^2 + b^2) with ((a+b)^2 - 2*a*b) by ring.
1 subgoal
  
  a : Z
  b : Z
  H1 : a + b = 7
  H2 : a * b = 12
  ============================
   (a + b) ^ 2 - 2 * a * b = 25

Sample_of_ring < rewrite H1.
1 subgoal
  
  a : Z
  b : Z
  H1 : a + b = 7
  H2 : a * b = 12
  ============================
   7 ^ 2 - 2 * a * b = 25

Sample_of_ring < replace (2*a*b) with (2*12) by ring [H2].
1 subgoal
  
  a : Z
  b : Z
  H1 : a + b = 7
  H2 : a * b = 12
  ============================
   7 ^ 2 - 2 * 12 = 25

Sample_of_ring < reflexivity.
Proof completed.

Sample_of_ring < Qed.



[Coq] Coq Advent Calender : case (15 of 25)
2010-12-15T02:06:00.000+09:00
Coq でよく使われる tactic の15番目は case です。

　帰納的な型について自動で場合分けをしてくれるという意味では、13番目のinductionと同じですが、inductionと違って単に場合分けを行うだけで帰納法の仮定とかは作ってくれません。

　今回は３値論理を定義してみます。帰納的な bool3 という型を定義し、それらに対する否定、論理積、論理和を定義します。

Coq < Inductive bool3 : Set := yes | maybe | no.
bool3 is defined
bool3_rect is defined
bool3_ind is defined
bool3_rec is defined

Coq < Definition not3(b:bool3) :=
Coq <   match b with
Coq <   | yes => no
Coq <   | maybe => maybe
Coq <   | no => yes
Coq <   end.
not3 is defined

Coq < Definition and3(a b:bool3) :=
Coq <   match a,b with
Coq <   | yes,yes => yes
Coq <   | no, _ => no
Coq <   | _, no => no
Coq <   | _,_ => maybe
Coq <   end.
and3 is defined

Coq < Definition or3(a b:bool3) :=
Coq <   match a,b with
Coq <   | no,no => no
Coq <   | yes,_ => yes
Coq <   | _,yes => yes
Coq <   | _,_ => maybe
Coq <   end.
or3 is defined

Coq <

　では、bool3 における簡単な証明をしてみます。a, b についての場合分けを行うのに case タクティックを使用します。下記の例では case でゴールが増えるのを示したいので個別に case を使っていますが、普通は
case a; case b; reflexivity.
で一行で９通りの場合分けを実施して終了とするでしょう。

Coq < Lemma Sample_of_case : forall a b:bool3,
Coq <   not3 (or3 a b) = and3 (not3 a) (not3 b).
1 subgoal
  
  ============================
   forall a b : bool3, not3 (or3 a b) = and3 (not3 a) (not3 b)

Sample_of_case < intros a b.
1 subgoal
  
  a : bool3
  b : bool3
  ============================
   not3 (or3 a b) = and3 (not3 a) (not3 b)

Sample_of_case < case a.
3 subgoals
  
  a : bool3
  b : bool3
  ============================
   not3 (or3 yes b) = and3 (not3 yes) (not3 b)

subgoal 2 is:
 not3 (or3 maybe b) = and3 (not3 maybe) (not3 b)
subgoal 3 is:
 not3 (or3 no b) = and3 (not3 no) (not3 b)

Sample_of_case < case b.
5 subgoals
  
  a : bool3
  b : bool3
  ============================
   not3 (or3 yes yes) = and3 (not3 yes) (not3 yes)

subgoal 2 is:
 not3 (or3 yes maybe) = and3 (not3 yes) (not3 maybe)
subgoal 3 is:
 not3 (or3 yes no) = and3 (not3 yes) (not3 no)
subgoal 4 is:
 not3 (or3 maybe b) = and3 (not3 maybe) (not3 b)
subgoal 5 is:
 not3 (or3 no b) = and3 (not3 no) (not3 b)

Sample_of_case < reflexivity.
4 subgoals
  
  a : bool3
  b : bool3
  ============================
   not3 (or3 yes maybe) = and3 (not3 yes) (not3 maybe)

subgoal 2 is:
 not3 (or3 yes no) = and3 (not3 yes) (not3 no)
subgoal 3 is:
 not3 (or3 maybe b) = and3 (not3 maybe) (not3 b)
subgoal 4 is:
 not3 (or3 no b) = and3 (not3 no) (not3 b)

Sample_of_case < reflexivity.
3 subgoals
  
  a : bool3
  b : bool3
  ============================
   not3 (or3 yes no) = and3 (not3 yes) (not3 no)

subgoal 2 is:
 not3 (or3 maybe b) = and3 (not3 maybe) (not3 b)
subgoal 3 is:
 not3 (or3 no b) = and3 (not3 no) (not3 b)

Sample_of_case < reflexivity.
2 subgoals
  
  a : bool3
  b : bool3
  ============================
   not3 (or3 maybe b) = and3 (not3 maybe) (not3 b)

subgoal 2 is:
 not3 (or3 no b) = and3 (not3 no) (not3 b)

Sample_of_case < case b; reflexivity.
1 subgoal
  
  a : bool3
  b : bool3
  ============================
   not3 (or3 no b) = and3 (not3 no) (not3 b)

Sample_of_case < case b; reflexivity.
Proof completed.

Sample_of_case < Qed.



[Coq] Coq Advent Calender : split (14 of 25)
2010-12-14T04:24:00.001+09:00
Coq でよく使われる tactic の14番目は split です。...そんなに使うかなぁ？

　split はゴールが P /\ Q の形をしている時に、二つのゴール P, Q に分割します。あとはそれぞれを別々に証明すればOKです。

　簡単な例を下記に示します。

Coq < Lemma Sample_of_split : forall A B C:Prop, A /\ (B /\ C) -> (A /\ B) /\ C.
1 subgoal
  
  ============================
   forall A B C : Prop, A /\ B /\ C -> (A /\ B) /\ C

Sample_of_split < intros A B C abc.
1 subgoal
  
  A : Prop
  B : Prop
  C : Prop
  abc : A /\ B /\ C
  ============================
   (A /\ B) /\ C

Sample_of_split < destruct abc as [a [b c]].
1 subgoal
  
  A : Prop
  B : Prop
  C : Prop
  a : A
  b : B
  c : C
  ============================
   (A /\ B) /\ C

Sample_of_split < split.
2 subgoals
  
  A : Prop
  B : Prop
  C : Prop
  a : A
  b : B
  c : C
  ============================
   A /\ B

subgoal 2 is:
 C

Sample_of_split < split.
3 subgoals
  
  A : Prop
  B : Prop
  C : Prop
  a : A
  b : B
  c : C
  ============================
   A

subgoal 2 is:
 B
subgoal 3 is:
 C

Sample_of_split < assumption.
2 subgoals
  
  A : Prop
  B : Prop
  C : Prop
  a : A
  b : B
  c : C
  ============================
   B

subgoal 2 is:
 C

Sample_of_split < assumption.
1 subgoal
  
  A : Prop
  B : Prop
  C : Prop
  a : A
  b : B
  c : C
  ============================
   C

Sample_of_split < assumption.
Proof completed.

Sample_of_split < Qed.



[Coq] Coq Advent Calender : induction (13 of 25)
2010-12-13T00:15:00.000+09:00
Coq でよく使われる tactic の13番目は induction です。

　Coq は帰納的な型を定義すると、その型に対する帰納法を自動で定義してくれます。例えば

Inductive nat : Set :=  
  O : nat 
| S : nat -> nat

という自然数natに対して、

forall P : nat -> Prop, 
  P 0 -> 
  (forall n : nat, P n -> P (S n)) -> 
  forall n : nat, P n

というnat_indを定義してくれます。これを使って、自然数nについての帰納法の証明の時に、

n=0 の場合のゴール
nの時成り立つという仮定IHnと、S nの場合のゴール

を作ってくれます。同様にリストであれば、nilとconsの場合などです。

　今までにも何度か induction を使った証明を示してきましたが、今回も簡単な例を。

Coq < Lemma plus_comm : forall n m, n + m = m + n.
1 subgoal
  
  ============================
   forall n m : nat, n + m = m + n

plus_comm < induction n.
2 subgoals
  
  ============================
   forall m : nat, 0 + m = m + 0

subgoal 2 is:
 forall m : nat, S n + m = m + S n

plus_comm < intro m.
2 subgoals
  
  m : nat
  ============================
   0 + m = m + 0

subgoal 2 is:
 forall m : nat, S n + m = m + S n

plus_comm < simpl.
2 subgoals
  
  m : nat
  ============================
   m = m + 0

subgoal 2 is:
 forall m : nat, S n + m = m + S n

plus_comm < erewrite <- plus_n_O.
2 subgoals
  
  m : nat
  ============================
   m = m

subgoal 2 is:
 forall m : nat, S n + m = m + S n

plus_comm < reflexivity.
1 subgoal
  
  n : nat
  IHn : forall m : nat, n + m = m + n
  ============================
   forall m : nat, S n + m = m + S n

plus_comm < intro m.
1 subgoal
  
  n : nat
  IHn : forall m : nat, n + m = m + n
  m : nat
  ============================
   S n + m = m + S n

plus_comm < simpl.
1 subgoal
  
  n : nat
  IHn : forall m : nat, n + m = m + n
  m : nat
  ============================
   S (n + m) = m + S n

plus_comm < erewrite <- plus_n_Sm.
1 subgoal
  
  n : nat
  IHn : forall m : nat, n + m = m + n
  m : nat
  ============================
   S (n + m) = S (m + n)

plus_comm < erewrite IHn.
1 subgoal
  
  n : nat
  IHn : forall m : nat, n + m = m + n
  m : nat
  ============================
   S (m + n) = S (m + n)

plus_comm < reflexivity.
Proof completed.

plus_comm < Qed.



[Coq] Coq Advent Calender : replace (12 of 25)
2010-12-12T11:30:00.003+09:00
Coq でよく使われる tactic の12番目は replace です。

　replace t1 with t2 とすると、t2 = t1 という等式をsubgoalに追加し、t2 = t1 を用いてゴールの書き換えを行います。書き換え規則 t2 = t1 の証明を先送りにすることで本筋の証明の見通しがよくなります。また、simpl, unfold, rewriteを使う場合とかで、「ゴールのこの部分だけ書き換えたいのだが別のところも書き換えられてしまう」と悩む場面もありますが、そういうときは replace でとりあえず部分的に書き換え、あとでその箇所の書き換えを証明すると楽です。

　replace を多用するのは、等式変形を繰り返す場合です。今回はそういう例を。
　下記の様に群 G を定義してみます。

Coq < Axiom G : Set.  (* 群G *)
Coq < Axiom G_dec : forall a b:G, {a=b} + {a <> b}.  (* 単位元や逆元の一意性とかを示す時に必要 *)
Coq < Axiom mult : G -> G -> G.  (* 乗法 *)
Coq < Notation "a * b" := (mult a b).  (* 記号 * で書ける様にする *)
Coq < Axiom assoc : forall a b c:G, (a * b) * c = a * (b * c).  (* 結合則 *)
Coq < Axiom G1 : G.  (* 単位元 *)
Coq < Notation "1" := G1.  (* 記号 1 で書ける様にする *)
Coq < Axiom id_l : forall a:G, 1 * a = a.  (* 左単位元である *)
Coq < Axiom inv : G -> G.  (* 逆元 *)
Coq < Axiom inv_l : forall a:G, (inv a) * a = 1.  (* 左逆元 *)


　では、左逆元は右逆元でもあることを証明してみます。長くなるのでゴールを示すのは要所要所だけです。replaceを使うと、subgoalが増えているのが判ります。

Coq < Theorem inv_r : forall a:G, a * (inv a) = 1.
inv_r < intros.
1 subgoal
  
  a : G
  ============================
   a * inv a = 1

inv_r < replace (a * inv a) with (1 * a * inv a).
2 subgoals
  
  a : G
  ============================
   1 * a * inv a = 1

subgoal 2 is:
 1 * a * inv a = a * inv a

inv_r < replace (1 * a * inv a) with ((inv (inv a) * (inv a)) * a * inv a).
3 subgoals
  
  a : G
  ============================
   inv (inv a) * inv a * a * inv a = 1

subgoal 2 is:
 inv (inv a) * inv a * a * inv a = 1 * a * inv a
subgoal 3 is:
 1 * a * inv a = a * inv a

inv_r < replace (inv (inv a) * inv a * a * inv a) with (inv (inv a) * (inv a * a) * inv a).
4 subgoals
  
  a : G
  ============================
   inv (inv a) * (inv a * a) * inv a = 1

subgoal 2 is:
 inv (inv a) * (inv a * a) * inv a = inv (inv a) * inv a * a * inv a
subgoal 3 is:
 inv (inv a) * inv a * a * inv a = 1 * a * inv a
subgoal 4 is:
 1 * a * inv a = a * inv a

inv_r < rewrite inv_l.  (* ここからは replace を使わなくても rewrite で簡単に変形出来る *)
inv_r < rewrite assoc.
inv_r < rewrite id_l.
inv_r < rewrite inv_l.
4 subgoals
  
  a : G
  ============================
   1 = 1

subgoal 2 is:
 inv (inv a) * (inv a * a) * inv a = inv (inv a) * inv a * a * inv a
subgoal 3 is:
 inv (inv a) * inv a * a * inv a = 1 * a * inv a
subgoal 4 is:
 1 * a * inv a = a * inv a

inv_r < reflexivity.  (* メインゴールの証明完了。残りは replace の書き換えの証明 *)
3 subgoals
  
  a : G
  ============================
   inv (inv a) * (inv a * a) * inv a = inv (inv a) * inv a * a * inv a

subgoal 2 is:
 inv (inv a) * inv a * a * inv a = 1 * a * inv a
subgoal 3 is:
 1 * a * inv a = a * inv a

inv_r < rewrite <- assoc; reflexivity.
2 subgoals
  
  a : G
  ============================
   inv (inv a) * inv a * a * inv a = 1 * a * inv a

subgoal 2 is:
 1 * a * inv a = a * inv a

inv_r < erewrite inv_l; reflexivity.
1 subgoal
  
  a : G
  ============================
   1 * a * inv a = a * inv a

inv_r < rewrite assoc; rewrite id_l; reflexivity.
Proof completed.

inv_r < Qed.
intros.
replace (a * inv a) with (1 * a * inv a) .
 replace (1 * a * inv a) with (inv (inv a) * inv a * a * inv a) .
  replace (inv (inv a) * inv a * a * inv a) with
   (inv (inv a) * (inv a * a) * inv a) .
   rewrite inv_l in |- *.
   rewrite assoc in |- *.
   rewrite id_l in |- *.
   rewrite inv_l in |- *.
   reflexivity.
   
   rewrite <- assoc in |- *; reflexivity.
   
  erewrite inv_l in |- *; reflexivity.
  
 rewrite assoc in |- *; rewrite id_l in |- *; reflexivity.
 
inv_r is defined

Coq < 



[Coq] Coq Advent Calender : exists (11 of 25)
2010-12-11T03:54:00.003+09:00
Coq でよく使われる tactic の11番目は exists です。
　証明のゴールが exists x, P x とか { n:nat | isPrime n } とか、ある性質を満たす要素が存在することを求めている時に、「具体的に」その要素を与えてゴールを変形します。

　下記は exists を使う簡単な例です。mの具体的な値としてS n = n+1 を与えています。具体的なmを何か与えないとomegaでの自動証明は通りません。

Coq < Require Import Omega.

Coq < Lemma Sample_of_exists : forall n, exists m, n < m.
1 subgoal
  
  ============================
   forall n : nat, exists m : nat, n < m

Sample_of_exists < intros.
1 subgoal
  
  n : nat
  ============================
   exists m : nat, n < m

Sample_of_exists < exists (S n).
1 subgoal
  
  n : nat
  ============================
   n < S n

Sample_of_exists < omega.
Proof completed.

Sample_of_exists < Qed.
intros.
exists (S n).
omega.

Sample_of_exists is defined
Coq < 



[TAPL][OCaml] Untyped Lambda Calculus Interpreter
2010-12-10T13:31:00.003+09:00
TAPLのChap.5を読むのに型無しλ計算のインタプリタが無いかなと探していたところ下記を見つけました。（...まぁそもそもそのくらい自分で作れよ、という話はあるんだが）

http://www.cs.ru.nl/~freek/notes/lambda.ml

ページの内容を lambda.ml として保存し、

$ ocaml
# #use "lambda.ml";;

で読み込まれるので、あとは下記の様に試すだけ。

# nf "(^x.fx)a";;
- : term = term "fa"
# nf "(KISS)(KISS)";;
- : term = term "^yzz'.zz'(yzz')"
# red_gk all "SKK";;
- : term list =
[term "SKK"; term "(^yz.Kz(yz))K"; term "^z.(^y.z)(Kz)"; term "^z.z"]
# red 7 "(^x.xx)(^x.xx)";;
- : term list =
[term "(^x.xx)^x.xx"; term "(^x.xx)^x.xx"; term "(^x.xx)^x.xx";
 term "(^x.xx)^x.xx"; term "(^x.xx)^x.xx"; term "(^x.xx)^x.xx";
 term "(^x.xx)^x.xx"; term "..."]
#

手計算に自信が無い時に使うといいかなー。


[Coq] Coq Advent Calender : unfold (10 of 25)
2010-12-10T01:06:00.003+09:00
Coq でよく使われる tactic の10番目は unfold です。unfold は関数定義を展開します。
　unfold だけで使う場合も有りますが、fold と組み合わせて使う事もあります。fold は展開された関数を元に戻します。unfold して、simpl とか rewrite とかして、また fold して戻すと式が良い具合に変形されている場合があります。ここではそういう例を見てみましょう。

　まず、sum n := 1 + 2 + ... + nという関数を定義します。

Coq < Fixpoint sum n :=     
Coq <   match n with
Coq <   | O => O
Coq <   | S n' => S n' + sum n'
Coq <   end.
sum is recursively defined (decreasing on 1st argument)

　次に、sum n = 1/2 * n * (n + 1) であることを証明したいのですが、割り算が入ると面倒ですから、次の定理を証明する事にします。今回は環に関する自動証明器の ring を使いたいのでArithとRingをImportしておきます。
　nに関する帰納法で、n=0の場合はさらっと証明を流すことにします。

Coq < Require Import Arith Ring.                          

Coq < Lemma Sample_of_unfold : forall n, 2 * sum n = n * (n + 1).
1 subgoal
  
  ============================
   forall n : nat, 2 * sum n = n * (n + 1)

Sample_of_unfold < induction n.
2 subgoals
  
  ============================
   2 * sum 0 = 0 * (0 + 1)

subgoal 2 is:
 2 * sum (S n) = S n * (S n + 1)

Sample_of_unfold < reflexivity.
1 subgoal
  
  n : nat
  IHn : 2 * sum n = n * (n + 1)
  ============================
   2 * sum (S n) = S n * (S n + 1)

　ここで、sum を unfold して、fold すると式が少し変形されます。

Sample_of_unfold < unfold sum.
1 subgoal
  
  n : nat
  IHn : 2 * sum n = n * (n + 1)
  ============================
   2 *
   (S n +
    (fix sum (n0 : nat) : nat :=
       match n0 with
       | 0 => 0
       | S n' => S n' + sum n'
       end) n) = S n * (S n + 1)

Sample_of_unfold < fold sum.
1 subgoal
  
  n : nat
  IHn : 2 * sum n = n * (n + 1)
  ============================
   2 * (S n + sum n) = S n * (S n + 1)

　ここでreplaceを使ってちょっと左辺を書き換えます。書き換えて良い証明はsubgoal 2と後回しです。


Sample_of_unfold < replace (2 * (S n + sum n)) with (2 * S n + 2 * sum n).
2 subgoals
  
  n : nat
  IHn : 2 * sum n = n * (n + 1)
  ============================
   2 * S n + 2 * sum n = S n * (S n + 1)

subgoal 2 is:
 2 * S n + 2 * sum n = 2 * (S n + sum n)

　ここでIHnを用いて書き換えて式変形を ring で自動証明します。後回しにしたものもringで一発です。


Sample_of_unfold < rewrite IHn.
2 subgoals
  
  n : nat
  IHn : 2 * sum n = n * (n + 1)
  ============================
   2 * S n + n * (n + 1) = S n * (S n + 1)

subgoal 2 is:
 2 * S n + 2 * sum n = 2 * (S n + sum n)

Sample_of_unfold < ring.
1 subgoal
  
  n : nat
  IHn : 2 * sum n = n * (n + 1)
  ============================
   2 * S n + 2 * sum n = 2 * (S n + sum n)

Sample_of_unfold < ring.
Proof completed.

Sample_of_unfold < Qed.



[Coq] Coq Advent Calender : simpl (9 of 25)
2010-12-09T04:40:00.002+09:00
Coq でよく使われる tactic の９つ目は simpl です。simpl はβι簡約(beta, iota)をして式を簡単にします。βι簡約が何かについては「言語ゲーム」の記事が判りやすいです。β簡約は関数適用で、ι簡約だと再帰的に関数が適用される、と考えると良いです。

　予め、足し算の定義を示しておきます。plus を含んだ式を simpl すると、一つ目の変数 n について再帰的にパターンマッチして式を変形してくれます。

Coq < Print plus.
plus = 
fix plus (n m : nat) : nat := match n with
                              | 0 => m
                              | S p => S (plus p m)
                              end
     : nat -> nat -> nat

Argument scopes are [nat_scope nat_scope]

　では足し算を使った simpl の使用例です。

Coq < Lemma Sample_of_simpl : forall n m, n + m = m + n.
1 subgoal
  
  ============================
   forall n m : nat, n + m = m + n

Sample_of_simpl < intros n m.
1 subgoal
  
  n : nat
  m : nat
  ============================
   n + m = m + n

Sample_of_simpl < induction n.
2 subgoals
  
  m : nat
  ============================
   0 + m = m + 0

subgoal 2 is:
 S n + m = m + S n

Sample_of_simpl < simpl.
2 subgoals
  
  m : nat
  ============================
   m = m + 0

subgoal 2 is:
 S n + m = m + S n

 simpl を使うと左辺の0 + mがnに簡約されますが、右辺は変化がありません。ここは別途証明しておいた（というか標準ライブラリにはいっている）定理のplus_n_Oを使って書き換える事にします。

Sample_of_simpl < Check plus_n_O.         
plus_n_O
     : forall n : nat, n = n + 0

Sample_of_simpl < erewrite <- plus_n_O.
2 subgoals
  
  m : nat
  ============================
   m = m

subgoal 2 is:
 S n + m = m + S n

Sample_of_simpl < reflexivity.
1 subgoal
  
  n : nat
  m : nat
  IHn : n + m = m + n
  ============================
   S n + m = m + S n

帰納法の後半も simpl を使い、別の補題plus_n_Smを使います。

Sample_of_simpl < simpl.
1 subgoal
  
  n : nat
  m : nat
  IHn : n + m = m + n
  ============================
   S (n + m) = m + S n

Sample_of_simpl < Check plus_n_Sm.
plus_n_Sm
     : forall n m : nat, S (n + m) = n + S m

Sample_of_simpl < erewrite <- plus_n_Sm.
1 subgoal
  
  n : nat
  m : nat
  IHn : n + m = m + n
  ============================
   S (n + m) = S (m + n)

Sample_of_simpl < erewrite IHn.
1 subgoal
  
  n : nat
  m : nat
  IHn : n + m = m + n
  ============================
   S (m + n) = S (m + n)

Sample_of_simpl < reflexivity.
Proof completed.

Sample_of_simpl < Qed.



[Coq] Coq Advent Calender : intro (8 of 25)
2010-12-08T00:02:00.003+09:00
Coq でよく使われる tactic の８つ目は intro です。基本的には前に説明したintrosと同じで、introsと違って一度に１つしかintro出来ないのが違います。
　あと、introsと違ってintroの場合は、~Pの形のゴールを、Pという仮定と、Falseというゴールに変形出来ます。~PはP->Falseなのですが、intros.では~Pは~Pのままです。

　intro.を使った例です。

Coq < Lemma Sample_of_intro : forall P, ~~~P -> ~P.
1 subgoal
  
  ============================
   forall P : Prop, ~ ~ ~ P -> ~ P

Sample_of_intro < intro P.
1 subgoal
  
  P : Prop
  ============================
   ~ ~ ~ P -> ~ P

Sample_of_intro < intro nnnp.
1 subgoal
  
  P : Prop
  nnnp : ~ ~ ~ P
  ============================
   ~ P

Sample_of_intro < intro p.
1 subgoal
  
  P : Prop
  nnnp : ~ ~ ~ P
  p : P
  ============================
   False

Sample_of_intro < elim nnnp.
1 subgoal
  
  P : Prop
  nnnp : ~ ~ ~ P
  p : P
  ============================
   ~ ~ P

Sample_of_intro < intro np.
1 subgoal
  
  P : Prop
  nnnp : ~ ~ ~ P
  p : P
  np : ~ P
  ============================
   False

Sample_of_intro < elim np.
1 subgoal
  
  P : Prop
  nnnp : ~ ~ ~ P
  p : P
  np : ~ P
  ============================
   P

Sample_of_intro < exact p.
Proof completed.

Sample_of_intro < Qed.



[Coq] Coq Advent Calender : assert (7 of 25)
2010-12-07T05:53:00.004+09:00
Coq でよく使われる tactic の７つ目は assert です。

　１つ目のapplyのところで書いた様に、Coqの証明は最初にゴールがあって、それを仮定と逆に戻して行く格好になっています。しかし証明する人間は仮定からゴールを考える方が楽な場合、つまり証明途中で適当な補題を作りたくなる場合があります。
　補題はある程度汎用性があるならば、予め切り出して証明しておいた方が良いと思いますが、使い捨て的な補題は assert を使うと、証明内証明みたいに作る事ができます。例えば下記の例で、

Coq < Lemma Sample_of_assert : forall P Q, (P /\ P) -> (Q /\ Q) -> (P /\ Q). 
1 subgoal
  
  ============================
   forall P Q : Prop, P /\ P -> Q /\ Q -> P /\ Q

Sample_of_assert < intros P Q pp qq.
1 subgoal
  
  P : Prop
  Q : Prop
  pp : P /\ P
  qq : Q /\ Q
  ============================
   P /\ Q


　ここまで証明した段階で、forall X, X /\ X -> Xという補題があれば、ppからPを、qqからQを取り出せて便利そうだと考えました。そこでassertを使います。すると現在の証明課題より先に、まずこの補題が証明課題になります。

Sample_of_assert < assert(H: forall X, X /\ X -> X).
2 subgoals
  
  P : Prop
  Q : Prop
  pp : P /\ P
  qq : Q /\ Q
  ============================
   forall X : Prop, X /\ X -> X

subgoal 2 is:
 P /\ Q

Sample_of_assert < intros X xx.
2 subgoals
  
  P : Prop
  Q : Prop
  pp : P /\ P
  qq : Q /\ Q
  X : Prop
  xx : X /\ X
  ============================
   X

subgoal 2 is:
 P /\ Q

Sample_of_assert < destruct xx as [x _].
2 subgoals
  
  P : Prop
  Q : Prop
  pp : P /\ P
  qq : Q /\ Q
  X : Prop
  x : X
  ============================
   X

subgoal 2 is:
 P /\ Q

Sample_of_assert < exact x.
1 subgoal
  
  P : Prop
  Q : Prop
  pp : P /\ P
  qq : Q /\ Q
  H : forall X : Prop, X /\ X -> X
  ============================
   P /\ Q

　assertで設定した補題 H の証明が終わると、以後は仮定 H としてそれを使う事が出来ます。

Sample_of_assert < split.
2 subgoals
  
  P : Prop
  Q : Prop
  pp : P /\ P
  qq : Q /\ Q
  H : forall X : Prop, X /\ X -> X
  ============================
   P

subgoal 2 is:
 Q

Sample_of_assert < apply (H P).
2 subgoals
  
  P : Prop
  Q : Prop
  pp : P /\ P
  qq : Q /\ Q
  H : forall X : Prop, X /\ X -> X
  ============================
   P /\ P

subgoal 2 is:
 Q

Sample_of_assert < exact pp. 
1 subgoal
  
  P : Prop
  Q : Prop
  pp : P /\ P
  qq : Q /\ Q
  H : forall X : Prop, X /\ X -> X
  ============================
   Q

Sample_of_assert < apply (H Q).
1 subgoal
  
  P : Prop
  Q : Prop
  pp : P /\ P
  qq : Q /\ Q
  H : forall X : Prop, X /\ X -> X
  ============================
   Q /\ Q

Sample_of_assert < exact qq.
Proof completed.

Sample_of_assert < Qed.



[Coq] Coq Advent Calender : omega (6 of 25)
2010-12-06T10:06:00.003+09:00
Coq でよく使われる tactic の６つ目は omega です...ってanarchy proofは課題が数学寄りに偏っているから、順序が６つ目というのはあまり気にしないで下さい。

　omega タクティックはforallとかexistsとかを含まない形のPresburger算術 (Wikipedia)の式を自動証明してくれます。端的に言うと、

割り算無し

変数と変数の掛け算が入っているものはNG、変数と定数（2, 3などの具体的な整数）の掛け算はOK

みたいな感じの等式 or 不等式を証明します。
　Coqがよく使われる理由は、この手の数式関係の自動証明が便利に使えるからだと思います。整数の等式不等式に関する公理定理を組み合わせて証明するとか大変ですからね。

簡単な例はこんなのです。使い方は簡単で、Require Import Omega して、introsとかして、omega と入力するだけ。

Coq < Require Import Omega.

Coq < Lemma Sample_of_omega : forall x:nat, x > 1 -> 3 * x > x + 2.
1 subgoal
  
  ============================
   forall x : nat, x > 1 -> 3 * x > x + 2

Sample_of_omega < intros.
1 subgoal
  
  x : nat
  H : x > 1
  ============================
   3 * x > x + 2

Sample_of_omega < omega.
Proof completed.


　内部で実行された自動証明を見てみると、こんな感じらしい。

Sample_of_omega < Undo.
1 subgoal
  
  x : nat
  H : x > 1
  ============================
   3 * x > x + 2

Sample_of_omega < info omega.
 == refine (Decidable.dec_not_not (3 * x > x + 2) (dec_gt (3 * x) (x + 2)) _);
       intro H0;
       refine ((_:3 * x <= x + 2 -> False) (not_gt (3 * x) (x + 2) H0));
       clear H0; intro H0;
       refine ((_:(Z_of_nat x > Z_of_nat 1)%Z -> False) (inj_gt x 1 H));
       change ((Z_of_nat x > 1)%Z -> False); clear H; 
    intro H;
       refine ((_:(Z_of_nat (3 * x) <= Z_of_nat (x + 2))%Z -> False)
                 (inj_le (3 * x) (x + 2) H0));
       refine ((fun (P : Z -> Prop) (H : P (Z_of_nat 3 * Z_of_nat x)%Z) =>
                eq_ind_r P H (inj_mult 3 x))
                 (fun x0 : Z => (x0 <= Z_of_nat (x + 2))%Z -> False) _);
       change ((3 * Z_of_nat x <= Z_of_nat (x + 2))%Z -> False);
       refine ((fun (P : Z -> Prop) (H : P (Z_of_nat x + Z_of_nat 2)%Z) =>
                eq_ind_r P H (inj_plus x 2))
                 (fun x0 : Z => (3 * Z_of_nat x <= x0)%Z -> False) _);
       change ((3 * Z_of_nat x <= Z_of_nat x + 2)%Z -> False); 
    clear H0; intro H0; refine (ex_ind _ (intro_Z x)); 
    intro Zvar2; intro Omega11; refine (and_ind _ Omega11); 
    clear Omega11; intro Omega8; intro Omega11;
       refine ((_:(0 <= Z_of_nat x + -1 + - (1))%Z -> False)
                 (Zgt_left (Z_of_nat x) 1 H)); clear H;
       refine ((fun (P : Z -> Prop) (H : P Zvar2) => eq_ind_r P H Omega8)
                 (fun x : Z => (0 <= x + -1 + - (1))%Z -> False) _);
       change ((0 <= Zvar2 + -1 + -1)%Z -> False);
       refine (fast_Zplus_assoc_reverse Zvar2 (-1) 
                 (-1) (fun x : Z => (0 <= x)%Z -> False) _);
       change ((0 <= Zvar2 + -2)%Z -> False);
       refine (fast_Zred_factor0 Zvar2
                 (fun x : Z => (0 <= x + -2)%Z -> False) _); 
    intro Omega10;
       refine ((_:(0 <= Z_of_nat x + 2 + - (3 * Z_of_nat x))%Z -> False)
                 (Zle_left (3 * Z_of_nat x) (Z_of_nat x + 2) H0)); 
    clear H0;
       refine ((fun (P : Z -> Prop) (H : P Zvar2) => eq_ind_r P H Omega8)
                 (fun x0 : Z => (0 <= x0 + 2 + - (3 * Z_of_nat x))%Z -> False)
                 _);
       refine ((fun (P : Z -> Prop) (H : P Zvar2) => eq_ind_r P H Omega8)
                 (fun x : Z => (0 <= Zvar2 + 2 + - (3 * x))%Z -> False) _);
       refine (fast_Zmult_comm 3 Zvar2
                 (fun x : Z => (0 <= Zvar2 + 2 + - x)%Z -> False) _);
       refine (fast_Zopp_mult_distr_r Zvar2 3
                 (fun x : Z => (0 <= Zvar2 + 2 + x)%Z -> False) _);
       change ((0 <= Zvar2 + 2 + Zvar2 * -3)%Z -> False);
       refine (fast_Zplus_comm (Zvar2 + 2) (Zvar2 * -3)
                 (fun x : Z => (0 <= x)%Z -> False) _);
       refine (fast_Zplus_assoc (Zvar2 * -3) Zvar2 2
                 (fun x : Z => (0 <= x)%Z -> False) _);
       refine (fast_Zred_factor3 Zvar2 (-3)
                 (fun x : Z => (0 <= x + 2)%Z -> False) _);
       change ((0 <= Zvar2 * Zneg (3 - 1) + 2)%Z -> False); 
    intro Omega9;
       cut ((Zvar2 * -2 + 2)%Z = ((Zvar2 * -1 + 1) * 2 + 0)%Z);[intro H|idtac].
    refine ((_:(Zvar2 * -2 + 2)%Z = ((Zvar2 * -1 + 1) * 2 + 0)%Z -> False) H);
       clear H; intro auxiliary;
       refine ((_:(0 <= (Zvar2 * -1 + 1) * 2 + 0)%Z -> False)
                 (OMEGA1 (Zvar2 * -2 + 2) ((Zvar2 * -1 + 1) * 2 + 0)
                    auxiliary Omega9)); clear auxiliary Omega9; 
    intro Omega9;
       cut (2 > 0)%Z;[intro H|idtac].
    refine ((_:(2 > 0)%Z -> False) H); clear H;
       cut (2 > 0)%Z;[intro H|idtac].
    refine ((_:(2 > 0)%Z -> (2 > 0)%Z -> False) H); 
    clear H; intro auxiliary_1; intro auxiliary_2;
       refine ((_:(0 <= Zvar2 * -1 + 1)%Z -> False)
                 (Zmult_le_approx 2 (Zvar2 * -1 + 1) 0 auxiliary_1
                    auxiliary_2 Omega9));
       clear auxiliary_1 auxiliary_2 Omega9; intro Omega9;
       refine ((_:(0 <= Zvar2 * 1 + -2 + (Zvar2 * -1 + 1))%Z -> False)
                 (OMEGA2 (Zvar2 * 1 + -2) (Zvar2 * -1 + 1) Omega10 Omega9));
       refine (fast_OMEGA13 Zvar2 (-2) 1 1 (fun x : Z => (0 <= x)%Z -> False)
                 _); change ((0 <= Zneg (2 - 1))%Z -> False);
       change ((0 ?= Zneg (2 - 1))%Z <> Gt -> False);
       change (Gt <> Gt -> False); intro H; refine (False_ind False _);
       cut (Gt = Gt);[intro H0|idtac].
    refine ((_:Gt = Gt -> False) H0); clear H0;
       cut (Gt <> Gt);[intro H0|idtac].
    refine ((_:Gt <> Gt -> Gt = Gt -> False) H0); clear H0; 
    intro H0; intro H1; exact (H0 H1).
    
    exact H.
    
    change (Gt = Gt); exact (refl_equal Gt).
    
    change ((2 ?= 0)%Z = Gt); change (Gt = Gt); change (Gt = Gt);
       exact (refl_equal Gt).
    
    change ((2 ?= 0)%Z = Gt); change (Gt = Gt); change (Gt = Gt);
       exact (refl_equal Gt).
    
    refine (fast_OMEGA11 Zvar2 (-1) 1 0 2
              (fun x : Z => (Zvar2 * -2 + 2)%Z = x) _);
       change ((Zvar2 * -2 + 2)%Z = (Zvar2 * -2 + 2)%Z);
       change ((Zvar2 * -2 + 2)%Z = (Zvar2 * -2 + 2)%Z);
       exact (refl_equal (Zvar2 * -2 + 2)%Z).
    
Proof completed.

Sample_of_omega < 



[Coq] Coq Advent Calender : intros (5 of 25)
2010-12-05T07:11:00.000+09:00
Coq でよく使われる tactic の５つ目は intros です。

　実は過去４回の記事でも毎回 intros を使用していました。forall とかで定義された変数や -> の左の式とかを仮定に持って行く為に使います。introの複数形なので、introを必要な回数繰り返してもOKです。
　intros. だけでも勝手に適当に名前（仮定は通常 H? みたいな名前）を付けてくれますが、判りやすさを考えると自分で適切な名前を付けた方が良いと思います。

Coq < Lemma Sample_of_intros : forall A B C:Prop, (A->B->C) -> (A->B) -> A -> C.
1 subgoal
  
  ============================
   forall A B C : Prop, (A -> B -> C) -> (A -> B) -> A -> C

Sample_of_intros < intros A B C abc ab a.
1 subgoal
  
  A : Prop
  B : Prop
  C : Prop
  abc : A -> B -> C
  ab : A -> B
  a : A
  ============================
   C

Sample_of_intros < apply abc.
2 subgoals
  
  A : Prop
  B : Prop
  C : Prop
  abc : A -> B -> C
  ab : A -> B
  a : A
  ============================
   A

subgoal 2 is:
 B

Sample_of_intros < exact a.   
1 subgoal
  
  A : Prop
  B : Prop
  C : Prop
  abc : A -> B -> C
  ab : A -> B
  a : A
  ============================
   B

Sample_of_intros < apply ab; exact a.
Proof completed.

Sample_of_intros < Qed.
intros A B C abc ab a.
apply abc.
 exact a.
 
 apply ab; exact a.
 
Sample_of_intros is defined

Coq < 



[Coq] Coq Advent Calender : destruct (4 of 25)
2010-12-04T06:51:00.002+09:00
Coq でよく使われる tactic の４つ目は destruct です。

　destruct は基本的にはある項を場合分けする時使うのですが、仮定の中にある /\ とか \/ とか exists とかを分解するのに使うのに便利です。（それ以外のときは induction とか case_eq とか使う事が多い様にも思います。）
　下記の例では仮定 abc を分解して仮定 a, b, c を作っています。　


Coq < Lemma Sample_of_destruct : forall A B C:Prop,
Coq < A /\ (B /\ C) -> (A /\ B) /\ C.
1 subgoal
  
  ============================
   forall A B C : Prop, A /\ B /\ C -> (A /\ B) /\ C

Sample_of_destruct < intros A B C abc.
1 subgoal
  
  A : Prop
  B : Prop
  C : Prop
  abc : A /\ B /\ C
  ============================
   (A /\ B) /\ C

Sample_of_destruct < destruct abc as [a [b c]].
1 subgoal
  
  A : Prop
  B : Prop
  C : Prop
  a : A
  b : B
  c : C
  ============================
   (A /\ B) /\ C

Sample_of_destruct < split; [split|]; assumption.
Proof completed.

Sample_of_destruct < Qed.
intros A B C abc.
destruct abc as (a, (b, c)).
split; [ split | idtac ]; assumption.

Sample_of_destruct is defined

Coq < 



[Coq] Coq Advent Calender : rewrite (3 of 25)
2010-12-04T06:37:00.002+09:00
Coq でよく使われる tactic の３つ目は rewrite です。

　rewrite は仮定にある等式を使ってゴールを書き換えます。下記の例では、リスト xs について帰納法を用いて証明していますが、ゴールの中に含まれるlength (xs ++ ys)を、帰納法の仮定IHxsを用いてrewriteすることでlength xs + length ysに書き換えています。


Coq < Lemma Sample_of_rewrite : forall (A:Set)(xs ys:list A), 
Coq < length (xs ++ ys) = length xs + length ys.
1 subgoal
  
  ============================
   forall (A : Set) (xs ys : list A),
   length (xs ++ ys) = length xs + length ys

Sample_of_rewrite < intros A xs ys.
1 subgoal
  
  A : Set
  xs : list A
  ys : list A
  ============================
   length (xs ++ ys) = length xs + length ys

Sample_of_rewrite < induction xs.                        
2 subgoals
  
  A : Set
  ys : list A
  ============================
   length (nil ++ ys) = length nil + length ys

subgoal 2 is:
 length ((a :: xs) ++ ys) = length (a :: xs) + length ys

Sample_of_rewrite < reflexivity.       
1 subgoal
  
  A : Set
  a : A
  xs : list A
  ys : list A
  IHxs : length (xs ++ ys) = length xs + length ys
  ============================
   length ((a :: xs) ++ ys) = length (a :: xs) + length ys

Sample_of_rewrite < simpl.
1 subgoal
  
  A : Set
  a : A
  xs : list A
  ys : list A
  IHxs : length (xs ++ ys) = length xs + length ys
  ============================
   S (length (xs ++ ys)) = S (length xs + length ys)

Sample_of_rewrite < rewrite IHxs.
1 subgoal
  
  A : Set
  a : A
  xs : list A
  ys : list A
  IHxs : length (xs ++ ys) = length xs + length ys
  ============================
   S (length xs + length ys) = S (length xs + length ys)

Sample_of_rewrite < reflexivity.
Proof completed.

Sample_of_rewrite < Qed.
intros A xs ys.
induction xs.
 reflexivity.
 
 simpl in |- *.
 rewrite IHxs in |- *.
 reflexivity.
 
Sample_of_rewrite is defined

Coq < 



[Coq] Coq Advent Calender : auto (2 of 25)
2010-12-04T05:57:00.002+09:00
Coq でよく使われる tactic の２つ目は auto です。

　Coq は簡単な証明は自動的に証明してくれる機能が幾つかありますが、auto はよく使われます。autoが何をやっているか知りたい場合は、autoの代わりにinfo autoと入力すると、autoの中で何をしてるかが判ります。Coqの初学者にはinfoは便利ですよ。


Coq < Lemma Sample_of_auto : forall A B:Prop, ((((A->B)->A)->A)->B)->B.
1 subgoal
  
  ============================
   forall A B : Prop, ((((A -> B) -> A) -> A) -> B) -> B

Sample_of_auto < auto.
Proof completed.

Sample_of_auto < Qed.
auto.

Sample_of_auto is defined

Coq < 



[Coq] Coq Advent Calender : apply (1 of 25)
2010-12-04T05:26:00.004+09:00
技術的 Advent Calender という概念を知らなかったのですが、面白そうなので遅ればせながら始めてみました。という訳で12/1から開始出来なかったのはご容赦下さい。
　先日のCoq Party絡みで集計されたCoqでよく使われるtacticのリストの順に、そのtacticが使われている証明例を書いてみます。

　最初は apply です。
　「この仮定（下記の例では pq）を使うとゴール（下記の例では Q）が出て来る」という時に、apply pq とすると、ゴール Q が変化します。学校で習う普通の証明の順序と違って、Coqの証明はゴールを一歩一歩、仮定に戻して行きます。その時使うのが apply です。


Coq < Lemma Sample_of_apply : forall P Q:Prop, P -> (P->Q) -> Q.
1 subgoal
  
  ============================
   forall P Q : Prop, P -> (P -> Q) -> Q

Sample_of_apply < intros P Q p pq.
1 subgoal
  
  P : Prop
  Q : Prop
  p : P
  pq : P -> Q
  ============================
   Q

Sample_of_apply < apply pq.
1 subgoal
  
  P : Prop
  Q : Prop
  p : P
  pq : P -> Q
  ============================
   P

Sample_of_apply < exact p.  
Proof completed.

Sample_of_apply < Qed.
intros P Q p pq.
apply pq.
exact p.

Sample_of_apply is defined

Coq < 



[TAPL][Coq] Chapter 3: Boolean Expression
2010-11-01T23:09:00.001+09:00
TAPLのChapter 3のBoolean式の部分に付いてCoqで証明してみました。
コードは http://ideone.com/COzSO に公開しています。


[TAPL] Types and Programming Languages Reading at Tokyo
2010-10-12T07:55:00.003+09:00
Types and Programming Languages (通称 TAPL) の読書会の第0回が先日あったので報告。

TAPL読書会ですが、下記の様にGoogle groupが出来ました。開催情報とか流れるので興味のある方は登録をお勧めします。
http://groups.google.co.jp/group/taplreading-tokyo
次回開催は 11/3午後で、会場は同じく豆蔵オフィスです。

前回は、Chap.1はスキップ、Chap.2から読み始め、Chap.3の途中まででした。
次回はChap.3の続きから初めて、Chap.4(というか実装のChapterはこの先も)はスキップ、Chap.5を読む予定、となっています。
参加者は予習復習前提で、次回の範囲は予め読んで来ることが前提と、硬派な勉強会ということになりました。
Chap.4のような実装の箇所は各自実装したい人が自分で実装してちょっとデモをするということで。

参加者ですが、前回は総勢４名もCS専攻の大学院生の方が来てくれたのは良かったです。素人の社会人だけで勉強会してると簡単に行き詰るので。

懇親会も大変盛り上がっていたようで、大変有意義な一日でした。しかし、積読率高いですね＞TAPL。買ったけど読んでなかったとか、Chap.3までは読んだけどとか、そういう話ばっかり。


[event] Reading TAPL
2010-09-26T19:37:00.001+09:00
Types and Programming Languages ( http://www.amazon.co.jp/dp/0262162091 ) という定番の教科書を読もうという読書会です。
東京近辺の方はぜひどうぞ。

http://atnd.org/events/8291


[Scala] Fibonacci series including 7110
2010-09-20T10:26:00.002+09:00
今更ながら http://recruit.drecom.co.jp/event2010  の「7110を含むフィボナッチ数列で、初期値の組み合わせが一番小さいものをあげろ。※自然数に限る」をScalaで解いてみた。
　もうイベントは終わったから解答公開してもいいよね。

　fib が 7110以下の範囲のフォボナッチ数列を計算する関数。zipとか使って格好良く書けるかもとも思うが、判りやすさ優先で。ysのところにxs'と書けないScalaは残念な感じだ。


scala> def fib(n0:Int,n1:Int) = {                   
     |   def f(xs:List[Int]):List[Int] = xs match { 
     |     case a::b::ys if a < 7110 => f((a+b)::xs)
     |     case _ => xs                             
     |   }                                          
     |   f(n1::n0::Nil)                                    
     | }
fib: (Int,Int)List[Int]

scala> def solve = for( n1 <- (1 to 100).toList;                       
     |   n0 <- (1 to n1).toList if fib(n0,n1).head==7110               
     | ) yield {(n0,n1)}
solve: List[(Int, Int)]

scala> solve
res7: List[(Int, Int)] = List((16,70), (70,86))
scala> 



[Coq] Coq-99 : Part 1
2010-07-24T23:34:00.004+09:00
前にS-99: Ninety-Nine Scala Problemsというのを紹介しましたが、Coqでも入門者が勉強用に解く為の問題集というのを考えてみました。

　まずは命題論理の証明の課題。勿論、tautoとかで一発だと思いますが、練習問題なので入門者は自力で解こう。
　Admitted.を消して証明を書く事が期待されています。

Section Prop_Logic.
  Lemma Coq_01 : forall A B C:Prop, (A->B->C) -> (A->B) -> A -> C.
  Admitted.
  Lemma Coq_02 : forall A B C:Prop, A /\ (B /\ C) -> (A /\ B) /\ C.
  Admitted.
  Lemma Coq_03 : forall A B C D:Prop, (A -> C) /\ (B -> D) /\ A /\ B -> C /\ D.
  Admitted.
  Lemma Coq_04 : forall A : Prop, ~(A /\ ~A).
  Admitted.
  Lemma Coq_05 : forall A B C:Prop, A \/ (B \/ C) -> (A \/ B) \/ C.
  Admitted.
  Lemma Coq_06 : forall A, ~~~A -> ~A.
  Admitted.
  Lemma Coq_07 : forall A B:Prop, (A->B)->~B->~A.
  Admitted.
  Lemma Coq_08: forall A B:Prop, ((((A->B)->A)->A)->B)->B.
  Admitted.
  Lemma Coq_09 : forall A:Prop, ~~(A\/~A).
  Admitted.
End Prop_Logic.


解答例は例えばこれとか。


[Joke]Falso : HyperVerifier and HyperProver
2010-07-24T07:15:00.004+09:00
twitterで知ったジョークサイトなんだが、Falso, by Estatis Inc.があります。

　「ある公理を導入すれば」なんでも証明出来てしまう(笑)という話で、それをいかにも画期的新製品みたいな感じに仕上げているのがおかしい。

　追記：togetter: Falso 定理証明系の大革命


[FM] Maude
2010-07-19T23:33:00.003+09:00
今日はFormal Methods Forumの勉強会で、いつものCoq (CPDT)の話の他に、Maudeをちょっと触ってみた、という話をしました。

　Maudeは項書き換え系の言語で形式仕様記述やモデル検査、DSL記述などにも使える言語です。
　Coqと違って証明も出来るけどメインは仕様記述＆それ自体がプロトタイプとして動く、かなぁ。パズルとかにも役に立つかも。

　あわてて作った資料なんで完成度は低いですがこちら。
Slideshare上のプレゼン
PDF資料

　Maudeに興味のある方はコメント頂けると嬉しいです。


[Coq] CoqUn -- Summer Coq Event in Nagoya
2010-07-03T14:20:00.002+09:00
2010/08/29に名古屋でCoq庵 -- 日本の夏、証明の夏というCoqのイベントが開催されます。
　といっても、Coqユーザが集まって話をしようという比較的緩いイベントなんで、Coq初めてという人も参加すると良いのではなかろうか。入門的な話もあります。


[Coq] Puzzle from Hiyama-san's Blog
2010-07-03T13:47:00.003+09:00
檜山さんのblogに掛け算から足し算を作る（パズルとしてやってみよう）という問題が載っています。
　Coqの練習問題としてちょうど良いかと思い解いてみました。
　思ったより時間がかかってしまい、解き終わる前にネタばらしが出ちゃったのだけど、一応、解いた解答です。http://ideone.com/Staa3

　分配則は簡単だったが、交換則を思いつくまでに苦労した。交換測を思いついたらその延長で結合則もなんとか。ただ、証明はちまちまとrewriteしてるだけ。ここは本当は自動化できるんだろうなぁ。
　Coq初心者的には、inv関係の{a'|a*a'=1}みたいな記法の使い方に慣れたのが良かったか。あとAxiom eq_dec_0:forall a:G, {a=0}+{a<>0}みたいなdecide出来る公理の便利さを実感した。


[Scala] Scala 2.8 Continuation (1)
2010-06-14T22:39:00.003+09:00
root/compiler-plugins/continuations/trunk/doc/examples/continuationsに載っているサンプルコードをREPLで写経してみます。

Test0.scala

scala> import scala.util.continuations._            
import scala.util.continuations._

scala> reset {                                      
     |   2 * {                                      
     |     println("up")                            
     |     val x = shift((k:Int=>Int) => k(k(k(8))))
     |     println("down")                          
     |     x                                        
     |   }                                          
     | }
up
down
down
down
res1: Int = 64

これはdef k(i:Int):Int = {println("down"); 2*i}と考えればOK。

Test1.scala

scala> object Test1 {                                 
     |   def testThisMethod() = {                     
     |     1 + (shift((k:Int=>Int) => k(k(k(17)))))   
     |   }
     |   def testThisCallingMethod() = {              
     |     testThisMethod() * 2                       
     |   }
     |   def m() {
     |     val result = reset(testThisCallingMethod())
     |     println(result)
     |   }
     | }
defined module Test1

// ((((((17 + 1) * 2) + 1) * 2) + 1) * 2) = 150

scala> Test1.m()                                      
150

k = (_+1)*2 と考えればこれも予想通りの結果。
resetの中にshiftを書くのはOKだが、resetなしでshiftだけの関数を定義しようとすると下記の様にエラーになります。仕方が無いのでobject Test1 {...} に包みます。

scala> def testThisMethod() = {
     |   1 + (shift((k:Int=>Int) => k(k(k(17)))))
     | }
:2: error: type mismatch;
 found   : Int @scala.util.continuations.cpsSynth @scala.util.continuations.cpsParam[Int,Int]
 required: Int
object RequestResult$line4$object {
                                  ^


Test2.scala

scala> object Test2 {                             
     |   def methA() = {                          
     |     def fun(k:Int=>String) = {             
     |       for(i <- List(1,2,3,4)) println(k(i))
     |       Some("returnvalue")                  
     |     }                                      
     |     2 * shift(fun)                         
     |   }
     |   def methB() = {                          
     |     "+++ "+methA().toString()              
     |   }
     |   def m() = reset(methB())                 
     | }
defined module Test2

scala> Test2.m()
+++ 2
+++ 4
+++ 6
+++ 8
res0: Some[java.lang.String] = Some(returnvalue)

k = "+++" + (2 * _).toString() ですか。


[Scala] Scala 2.8 RC4 and continuation plugin
2010-06-13T23:03:00.005+09:00
Scala 2.8 RC4 が出ました --- が、なんかバグがあるらしく来週には RC5 が出るそうです。なんか品質安定しませんね＞Scala 2.8。

　RC4からは限定継続のコンパイラプラグインが付属される様になりました。
　使い方はこんな感じ。Scala 2.8 RC4を導入したディレクトリに居るとします。pluginにパスを通し、continuationをenableにする必要があります。

% cd ~/scala28rc4
% ./bin/scala -Xpluginsdir ./misc/scala-devel/plugins/ ¥
-Xplugin:continuations -P:continuations:enable
Welcome to Scala version 2.8.0.RC4 (Java HotSpot(TM) 64-Bit Server VM, Java 1.6.0_20).
Type in expressions to have them evaluated.
Type :help for more information.

scala> import scala.util.continuations._         
import scala.util.continuations._

scala> reset {
     |   shift { (k:Int=>Int) =>
     |     k(k(k(7)))
     |   } + 1
     | }
res0: Int = 10

scala> 


限定継続をおいおい勉強しようと思います。


[Coq] How to define complex inductions
2010-05-20T22:25:00.002+09:00
Coq の証明の書き方パターンを yoshihiro503 さんに教わったので、忘れないうちに。

自然数に関する定理を証明したい場合に、下記の様な補題が欲しかったとします。
Lemma nat2_ind : forall P:nat -> Prop, P 0 -> P 1 ->
  (forall n:nat, P n -> P (S n) -> P (S (S n))) ->
  (forall n:nat, P n).

教わったコードを元に自分なりに書いてみたのが下記の証明です。
  
  ============================
   forall P : nat -> Prop,
   P 0 ->
   P 1 ->
   (forall n : nat, P n -> P (S n) -> P (S (S n))) -> forall n : nat, P n

nat2_ind < intros P H0 H1 IH.          
1 subgoal
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ============================
   forall n : nat, P n

nat2_ind < refine (fix ll n : P n := _).     (* ここで refine を使って ll を定義するのがポイント *)
1 subgoal
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  n : nat
  ============================
   P n

(* しかしここで apply ll しても駄目。llはIHの仮定のところで使う *)

nat2_ind < induction n.
2 subgoals
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  ============================
   P 0

subgoal 2 is:
 P (S n)

nat2_ind < exact H0.  (* n=0 のケースは P 0 *)
1 subgoal
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  n : nat
  IHn : P n
  ============================
   P (S n)

nat2_ind < induction n.
2 subgoals
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  IHn : P 0
  ============================
   P 1

subgoal 2 is:
 P (S (S n))

nat2_ind < exact H1.  (* n=1 のケース *)
1 subgoal
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  n : nat
  IHn : P (S n)
  IHn0 : P n -> P (S n)
  ============================
   P (S (S n))

nat2_ind < apply IH.   (* IH を使う *)
2 subgoals
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  n : nat
  IHn : P (S n)
  IHn0 : P n -> P (S n)
  ============================
   P n

subgoal 2 is:
 P (S n)

nat2_ind < apply ll.  (* IHの仮定のところにはll を使ってOK *)
1 subgoal
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  n : nat
  IHn : P (S n)
  IHn0 : P n -> P (S n)
  ============================
   P (S n)

nat2_ind < apply IHn0.          
1 subgoal
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  n : nat
  IHn : P (S n)
  IHn0 : P n -> P (S n)
  ============================
   P n

nat2_ind < apply ll.  (* もう一度 ll を使う *)
Proof completed.

nat2_ind < Qed.

そもそもの証明のゴールをrefineを使ってllとして定義して、証明の中でllを使っているので非常に不思議なのですが、変な所（例えばrefine直後に）でapply llしてProof CompleteしてもQedしたとたんにエラーになります。エラーが出ない様にH0,H1,IHを使えば、証明が正しい事になります。

なお、同じ定理を短く書くとkikxさんの証明ゴルフみたいになるようです。すごい。


[Coq] Arithmetic in Coq : N
2010-05-15T17:41:00.004+09:00
Nは二進数で表現された自然数の型です。

Require Import NArith.すると使用出来ます。型の定義は下記の様です。
Inductive N : Set :=  N0 : N | Npos : positive -> N


positiveは下記の様に定義されています。
Inductive positive : Set :=
    xI : positive -> positive | xO : positive -> positive | xH : positive

こんな感じで正の数を表現しています。xHが最上位ビットで、xIが x -> 2x+1, xOが x -> 2x ということです。
Coq < Check (xO (xI (xO xH))).
10%positive : positive

これは(1~0~1~0)%positive.とも書けます。

natとの変換は下記で可能。
nat_of_N : N -> nat
N_of_nat : nat -> N


演算子は
Ndouble_plus_one, Ndouble : N -> N
Nsucc, Npred : N -> N
Nplus, Nminus, Nmult : N -> N -> N　。+, -, * もあり。
Ncompare : N -> N -> comparison 。Infixで ?=
  comparisonは、
  Inductive comparison : Set :=
    Eq : comparison | Lt : comparison | Gt : comparison
Nlt, Ngt, Nle, Nge : N -> N -> Prop　。Infix で <, <=, >, >=
Nmin, Nmax : N -> N -> N
Ndiv2 : N -> N


Nに関する帰納法は次の２つの好きな方を使える。Nrectを用いてNindもある。

N_ind_double
     : forall (a : N) (P : N -> Prop),
       P 0%N ->
       (forall a0 : N, P a0 -> P (Ndouble a0)) ->
       (forall a0 : N, P a0 -> P (Ndouble_plus_one a0)) -> P a
Nrect
     : forall P : N -> Type,
       P 0%N -> (forall n : N, P n -> P (Nsucc n)) -> forall n : N, P n


Require Import ZArith.ZOdiv.すれば、
Ndiv_eucl : N -> N -> N * N
Ndiv : N -> N -> N
Nmod : N -> N -> N
Theorem Ndiv_eucl_correct: forall a b,
  let (q,r) := Ndiv_eucl a b in a = (q * b + r)%N.

と除算も使える。

---
追記
ZArith.ZOdivと、ZArithの中でImportしてるZArith.Zdivとは互換性無いのだな。
ZArithを使わないことはまず無いので、ZOdivは使わないほうがよさそう。


[Coq] Arithmetic in Coq : nat
2010-05-14T23:19:00.004+09:00
Coqで大きな自然数あるいは整数を使いたくなったので調べてみました。

★nat

　Coqで自然数というと基本はnatです。natというと自分で作る物であるかの様な気すらしますが勿論標準で備わっています。
　natを使う場合Require Import Arith.すると標準ライブラリが使えます。

●基本
Init.Peanoの中で、pred, plus, mult, le, lt, ge, gtが定義されていてImport不要で使える。

●大小比較関係

- eq_nat : nat -> nat -> Prop
-- heorem eq_nat_decide : forall n m, {eq_nat n m} + {~ eq_nat n m}. が使える
- lt_eq_lt_dec n m : {n < m} + {n = m} + {m < n}. こんな感じで使う
Definition nat_compare (n m:nat) :=
  match lt_eq_lt_dec n m with 
    | inleft (left _) => Lt
    | inleft (right _) => Eq
    | inright _ => Gt
  end.
-- le_lt_dec n m : {n <= m} + {m < n}. など


●四則演算

- 末尾再帰なtail_plusというのもある
- minus : nat -> nat -> nat. n - m とかも書ける。結果が負になる場合もOを返す。
- min, max : nat -> nat -> nat.
- div2, double : nat -> nat.
- 除算は無いが、Require Import Arith.Euclid. すれば商と剰余には下記がある
-- quotient : forall n, n > 0 ->
    forall m:nat, {q : nat | exists r : nat, m = q * n + r /\ n > r}.
-- modulo : forall n, n > 0 ->
    forall m:nat, {r : nat | exists q : nat, m = q * n + r /\ n > r}.



[Coq] FoCaLize Tutorial (2)
2010-05-13T23:08:00.002+09:00
[Coq] FoCaLize Tutorial (2)の続き。

　前回のextsubset.fclに  theorem incl_remove_mem : all s : Self, all v : Val,
                            ~(v << s) -> s <: s - v
    proof = by property mem_congr, mem_remove, mem_incl ;
を追加すると自動証明が失敗するのでFoCaLizeの手動証明を試す予定なのだが...自動証明がそのまま通るみたいだ。

　が、ここは一応Tutorial通り、手動証明も試してみる事にする、証明を下記の様に直してみる。    proof = <1>1 assume s : Self, v : Val, hypothesis Hv : ~(v << s),
                 prove s <: s - v
              <2>1 assume w : Val, hypothesis Hw : w << s,
                   prove w << s - v
                <3>1 prove ~(Val!( = )(w, v)) /\ w << s
                  <4>1 prove ~(Val!( = )(w, v))
                       by property mem_congr hypothesis Hv, Hw
                  <4>2 prove w << s
                       by hypothesis Hw
                  <4>f conclude
                <3>f qed by property mem_remove step <3>1
              <2>f qed by property mem_incl step <2>1
            <1>f conclude ;

再度コンパイルするとこれでも通る。上記の様に手で証明を記述しても生成されたCoqの証明は短く分割されて読みやすくはなるもののやはり人間向けの証明とは言えない感じである。

証明に通らない例として  theorem remove_insert : all s : Self, all v : Val,
                          v << s -> s = (s - v) + v
    proof = <1>1 assume s : Self, v : Val, hypothesis Hv : v << s,
                 prove s = (s - v) + v
              <2>1 assume w : Val, hypothesis Hw : w << s,
                   prove w << (s - v) + v
                   by property mem_insert, mem_remove
              <2>2 assume w : Val, hypothesis Hw : w << (s - v) + v,
                   prove w << s
                   by property mem_insert, mem_remove, mem_congr, Val!diff_eq
              <2>f qed by property eq_incl, mem_incl step <2>1, <2>2
            <1>f conclude ;

を試すと下記の様にエラーが出る。% ~/pkg/bin/focalizec extsubset.fcl
Invoking ocamlc...
>> /Users/miyamoto/pkg/focalize-0.6.0/bin/ocamlc -I /Users/miyamoto/pkg/lib/focalizec-0.6.0 -c extsubset.ml
Invoking zvtov...
>> /Users/miyamoto/pkg/focalize-0.6.0/bin/zvtov -zenon /Users/miyamoto/pkg/focalize-0.6.0/bin/zenon -new extsubset.zv
File "extsubset.fcl", line 61, characters 19-53:                
Zenon error: could not find a proof within the memory size limit
### proof failed
%
これについてもチュートリアルに従い証明を完全に記述するとコンパイルに通る。

　なんとなくCoqに慣れてしまったので、FoCaLizeを用いて証明を記述する方が寧ろ判りにくいようにも思う。


[Coq] FoCaLize Tutorial (1)
2010-05-10T20:27:00.004+09:00
形式手法開発ツールのFoCaLizeをインストールして動かしてみました。

　FoCaLizeは言語名かつツール群の総称です。言語としては、ちょっとオブジェクト指向風（継承などの要素があったり、speciesというクラスっぽいものがある）な純粋関数型言語で、FoCaLizeという言語で書いたプログラムは、OCamlのコードが生成されると共に、（ちょっとしたヒントを人間が与える事で）Zenonという自動証明器がCoq用の証明を自動生成します。
　多分、普通のJavaプログラマとかには、素のCoqよりもFoCaLizeの方が習得しやすい思われる。逆にバリバリのOCamlerみたいな人には素のCoqを使う方が楽なんじゃなかろうか。
　開発元は例によってCoqなどと同じINRIAです。Coq界隈だけでもCoq自体に、FoCaLizeに、Ynotにとなんかツールが多過ぎて全然勉強がおいつきません。

★インストール

Downloadからtar ballをダウンロードして、
# ./configure
# make
# make install

するとOK。Coqが既に動くならそんなに大変じゃないと思う。（前提にghostscriptを要求されたり良く解らんところもあるが）

★superset.fcl

Tutorialに従い、まずはsuperset.fclをコンパイルしてみます。下記を superset.fcl として入力。文法は概ねOCaml風です。
use "basics" ;;
species Superset =
  signature ( = ) : Self -> Self -> basics#bool ;
  property eq_refl : all x : Self, x = x ;
  property eq_symm : all x y : Self, x = y -> y = x ;
  property eq_tran : all x y z : Self, x = y -> y = z -> x = z ;
  theorem eq_symmtran : all x y z : Self, x = y -> x = z -> y = z
    proof = by property eq_symm, eq_tran ;
end ;;
内容は大体見当がつくと思います。Selfというのは、OOな用語で言えば自クラスのことで、自インスタンス(Javaのthis)ではありません --- まぁ
Self -> Self -> basics#bool
を見ればそれは判るか。

% focalizec superset.fcl
でコンパイルすると、OCamlのコード (superset.ml) とかTheoremの証明 (superset.v) などが生成されます。eq_symm, eq_tran を使え、と指示するだけで自動証明されるのでCoqとかに不慣れでも使いやすいかも。ただ生成される証明が
exact(
(NNPP _ (fun zenon_G=>(zenon_notallex (fun x:abst_T=>(forall y:abst_T,(
forall z:abst_T,((Is_true (abst__equal_ x y))->((Is_true (abst__equal_
x z))->(Is_true (abst__equal_ y z))))))) (fun zenon_H2a=>(zenon_ex
abst_T (fun x:abst_T=>(~(forall y:abst_T,(forall z:abst_T,((Is_true (
   ...47行省略...
abst_eq_tran)))) zenon_H1b)) (zenon_notnot _ (refl_equal (abst__equal_
zenon_Tz_k zenon_Ty_e))) zenon_Hb)) zenon_H8 zenon_H9)) in (zenon_noteq
_ zenon_Ty_e zenon_H7)))) (fun zenon_H5=>(zenon_H6 zenon_H5)) zenon_H22)
) zenon_H23)) abst_eq_symm)) zenon_H24)) zenon_H25)) zenon_H26))
zenon_H27)) zenon_H28)) zenon_H29)) zenon_H2a)) zenon_G)))).

みたいな感じで、人間が読む証明じゃないよなー。あとNNPP : forall p : Prop, ~ ~ p -> pを使うのありなんだ、みたいな。

★subset.fcl

同様にsubset.fclを入力。
use "basics" ;;
open "superset" ;;

species Subset(Val is Superset) =
  signature ( << ) : Val -> Self -> basics#bool ;

  signature empty : Self ;
  property mem_empty : all v : Val, ~(v << empty) ;

  signature ( + ) : Self -> Val -> Self ;
  property mem_insert : all v1 v2 : Val, all s : Self,
                        v1 << s + v2 <->
                        (Val!( = )(v1, v2) \/ v1 << s) ;

  signature ( - ) : Self -> Val -> Self ;
  property mem_remove : all v1 v2 : Val, all s : Self,
                        v1 << s - v2 <->
                        (~(Val!( = )(v1, v2)) /\ v1 << s) ;
end ;;

　内容は見れば判ると思いますが<<, +, -が集合の∈、要素の追加、削除に対応します。Val!( = )とうのはValクラスの( = )メソッドを呼び出す、みたいな意味です。

★extsubset.fcl

次に継承を使う例を。ExtSubsetはSubsetを継承します。
use "basics" ;;
open "superset" ;;
open "subset" ;;

species ExtSubset(Val is Superset) =
  inherit Superset, Subset(Val) ;

  signature ( <: ) : Self -> Self -> basics#bool ;
  property mem_incl : all s1 s2 : Self,
                      s1 <: s2 <-> all v : Val, v << s1 -> v << s2 ;
  theorem incl_refl : all s : Self, s <: s
    proof = by property mem_incl ;
  theorem incl_tran : all s1 s2 s3 : Self,
                      s1 <: s2 -> s2 <: s3 -> s1 <: s3
    proof = by property mem_incl ;

  theorem incl_empty : all s : Self, empty <: s
    proof = by property mem_incl, mem_empty ;
  theorem incl_insert : all s : Self, all v : Val, s <: s + v
    proof = by property mem_insert, mem_incl ;
  theorem incl_remove : all s : Self, all v : Val, s - v <: s
    proof = by property mem_remove, mem_incl ;

  let ( = ) (s1, s2) = if (s1 <: s2) then (s2 <: s1) else false ;

  property mem_congr : all v1 v2 : Val, Val!( = ) (v1, v2) ->
                       (all s : Self, (v1 << s) <-> (v2 << s)) ;

  theorem incl_insert_mem : all s : Self, all v : Val,
                            v << s -> s + v <: s
    proof = by property mem_congr, mem_insert, mem_incl ;
end ;;


　この次には、自動証明が失敗するケースを扱います。


[Coq] ASN.1 Library is under construction
2010-05-07T00:06:00.002+09:00
この連休にCoqの練習がてら作っていたASN.1のライブラリで、全然完成してないのだがとりあえず出来たところまで公開。
　Coqdocで生成したドキュメントがTLV.htmlです。（コードが成長したら随時更新予定）

　ASN.1が何かについては、A Layman's Guide to a Subset of ASN.1, BER, and DERあたりを読んで下さい。電子証明書とかで使っているバイナリフォーマットなので、証明付きのライブラリを作りたいのだ。

　本当はInductive tlv_value : Set := 
| Primitive : string -> tlv_value 
| Structured : list tlv -> tlv_value
.
みたいに定義したかったのだが、そうするとtlv_value, tlv に関する帰納法をうまく構成出来なかった。まだCPDT Chapter 3の読み込みが足りないのだろうなぁ。
　が、とりあえず幾つかの定理も証明できたし、出だしとしてはこんなものかもとも思う。

　Coqを勉強しようと思う様なプログラマの人は、ある程度複雑な型（相互再帰的だったり再帰がネストしていたり）を定義出来ると思うが、Coqは帰納型に対して帰納法を与える関数が作れないと駄目で、しかしそこが実は難しい、というのがこの連休に得た知見だ。


[Coq] How to use Record
2010-05-05T10:45:00.004+09:00
Coq で Record を使う方法を調べました。基本的には記述を簡単にする構文糖のようです。これを使うと、事前条件を満たす証明を要求するコンストラクタを簡単に書けます。
　使い方は下記の例を見てもらうのが簡単でしょう。

　まず正の有理数を表すRat型を作りたいと考えます。符号は無視するとして、分母が０で無いことを保証したい、分子分母が既約である事を保証したい、とします。こんな感じに書けます。

Record Rat : Set := mkRat {
  numer : nat;
  denom : nat;
  denom_not_zero : denom <> O;
  irreducible : forall g n d:nat, 
    (mult g n)=numer /\ (mult g d)=denom -> g = S O
}.

Ratで 1/2 を定義したい時はこんな感じになります。まず補題を証明しないと値を作れません。

Lemma two_not_zero : 2 <> 0.
Proof.
  discriminate.
Qed.
Lemma one_two_irred : forall g n d:nat, (mult g n)=1 /\ (mult g d)=2 -> g = S O.
Admitted. (* 証明省略 *)

こうして初めて値を作れます。

Definition half : Rat := mkRat 1 2 two_not_zero one_two_irred.
Print half. (* mkRat 1 2 two_not_zero one_two_irred : Rat *)
Eval compute in (numer half). (* 1 : nat *)
Eval compute in (denom_not_zero half). (* two_not_zero *)

アクセサに見えるnumerなどは単なる関数です、従って同じ名前空間でnumerを他に定義出来ません。

Print numer.
numer = 
fun r : Rat => let (numer, denom, _, _) := r in numer
     : Rat -> nat

Ratに関する帰納法は下記の様になります。

Print Rat_ind.
(* forall P : Rat -> Prop,
       (forall (numer denom : nat) (denom_not_zero : denom <> 0)
          (irreducible : forall g n d : nat,
                         g * n = numer /\ g * d = denom -> g = 1),
        P (mkRat numer denom denom_not_zero irreducible)) ->
       forall r : Rat, P r *)



[Alloy][FM] Sample code: Addressbook
2010-05-03T13:38:00.002+09:00
[Coq][FM] Fomal Methods Forum #4でのAlloyチュートリアルの話。

　まず Alloy4 を各自インストールしておくのは前提。但し、JARファイル１つなので、JRE (Java5以上) が入っているコンピュータならば起動は難しくありません。

　表示されるWindowの左側入力欄に下記を打ち込みます。
sig Name, Addr {}
sig Book {
  addr: Name -> lone Addr
}

　sigというのは普通のOO言語のクラス定義の様なもの --- なんですが、Alloy はOOなプログラミング言語ではないのでOOとのアナロジーは時に誤解を与えるかも。どちらかというと、RDBMSに Name, Addr という表を作ったと考えるといいかも。実際、Alloy は関係代数に基づいていますし。
　OO でいうところのインスタンスはAlloyではatomと言います。Alloyでインスタンスというのは、全てのatomから構成されるモデル（モデルの中には求める反例とかも含まれます）のことを指します。用語は間違わない様に。
　また、. (ドット演算子) もOO言語の属性やメソッドを指す様に勘違いしますが、join演算子で、RDBのjoinみたいな振る舞いをします。
　Bookのatomを仮に B0, B1 と書くと、Book は {(B0), (B1)} という集合です。（ () はタプル、{}は集合を表す。）

　lone は 0 or 1 個を表す数量限定子です。他にも all (全ての)、some (１個以上)、one (１個)、no (０個) があります。lone Addr は、関数型言語的には Option Addrのようなものです。
　addr は Book の属性みたいに見えますが、これも関数型言語的には addr : Book -> Name -> Option Addr -> Prop みたいに考えると良いです。addr は (Book, Name, Addr) のタプル型の元の集合、例えば{(B0,N0,D0), (B1,N1,D1)}として表現されます。 （関係 R : R x y は (X,Y) の部分集合として表現出来る）
　Book = {(B0),(B1)} であると、ドットはjoin演算子なので（テンソルとかの添字の縮約の如く）ジョイン演算をします。Bookとaddrの共通のB0を見て(B0).(B0,N0,D1)=(N0,D0)の様に計算して、b=B0ならば、b.addr={(N0,D0)}, Book.addr={(N0,D0),(N1,D1)} となります。

　この時点で sig Book {...} の下に
pred show[] {}
run show for 3
と書いて Execute のボタンを押します。
　右側に Instance found と出るので Instance のリンクを押すと、atom 間の関係を示すダイヤグラムが表示されます。nextを押すと別のインスタンスが表示されます。
　for 3 と書いたので各 sig 毎に 3 atom づつです。

　次にモデルの性質をテストする事を考えます。addr を追加して削除すると元に戻る、という性質が成り立つ事をモデル検査で確認（＝反例が見つからない事を確認）します。
　まず追加と削除を表す述語を定義します。述語なので戻り値は真偽値を返します。
pred add[disj b,b':Book, n:Name, a:Addr] {
  b'.addr = b.addr + (n -> a)
}
pred del[disj b,b':Book, n:Name] {
  b'.addr = b.addr - (n -> Addr)
}
　Alloyは手続き型言語ではないので、b'addrに何か破壊的代入が行われる事は無く、単にbとb'の間の関係を示しているだけです。disjはbとb'とが別atomであるという意味です。

　次いでテストしたい性質を書きます。
assert delUndoesAdd {
  all b,b',b'':Book, n:Name, a:Addr |
    add[b,b',n,a] and del[b',b'',n] implies b.addr = b''.addr
}
check delUndoesAdd for 5
　|はsuch thatみたいな意味、and, implisは論理演算の記号です。

　これを追加してexecuteすると「何故か」counterexampleが見つかったと表示されます。counterexampleをじっと眺めると、bとb'が同じBookであることが判ります。
　これは元々 b に (n -> a) が含まれていた場合、b, b' が同じになるからです。（集合に既にある要素を加えても同じ）
　assertの中身を
    no n.(b.addr) and add[b,b',n,a] and del[b',b'',n] implies b.addr = b''.addr
に修正するとconterexampleが無くなります。


[Coq][FM] Fomal Methods Forum #4
2010-05-02T10:26:00.002+09:00
4/29に第4回FormalMethods勉強会を行いました。

　今回は
Alloy
　Alloyの教科書の例題（アドレス帳）を元に文法を勉強しました。大体文法は把握出来たかな。
　あとは自分で使ってみるべきなんだろうが、あまりモデリングとか仕事でやらないしなぁ。とりあえずパズルをAlloyで解く練習をするかなぁ。

CEGAR
　今回はCEGARという手法の話を聞きました。CEGARはCounterExample-Guided Abstraction Refinementの略で、モデル検査における状態数爆発を抑える為の一手法です。
　モデル検査で扱う検査の中に、到達可能性解析（エラー状態などの特定の状態にと到達するか否かの解析）があります。
　状態数を抑える方法としてモデルの抽象化（モデルの粗視化）があります。抽象化によって、エラー状態に遷移する可能性のある状態と、到達しない状態とが同一視されてしまうと、本当はエラー状態に到達しないにも関わらず、エラー状態に達すると誤って判定されます。
　CEGARは、エラー状態に到達する解に対して、解析（最弱事前条件？）を行って抽象化を修正（状態を分割）して再解析する手法です。エラー状態に達した場合にはそれが本当に達したのか、抽象化を改善して再度解析を実施します。
　原理だけ聞くと、当たり前の話と思えるのですが、実際に自動化するところを実装するのは難しそうというか見当が付かない。

Coq
　CoqはCertified Programming with Dependent TypeのChapter 1,2をざっと流して、Chapter 3を3.3まで読み終わりました。
　当日使用した資料 (PPT, Coqファイル) についてはGoogleグループ上の記事にリンクを纏めましたので、そちらから辿って下さい。
　本当はChapter 3を終わりたかったのですが終わらなかったのはちょっと残念でした。


[Coq] Tail-recursive reverse
2010-04-26T21:49:00.002+09:00
先のreverse (reverse xs) = xsで示した reverse は末尾再帰でなく、効率の悪い定義である。
　そこで末尾再帰な
Fixpoint rev' {A:Set} (xs ys:list A) :=
 match xs with
 | nil => ys
 | cons x xs' => rev' xs' (cons x ys)
 end.
Definition rev {A:Set} (xs:list A) :=
 rev' xs nil.
Eval compute in rev (cons 1 (cons 2 (cons 3 nil))).

について
Theorem reverse_rev : forall (A:Set) (xs:list A),
 reverse xs = rev xs.

が成り立つ事を示そう。まず補題
Lemma rev'_reverse : forall (A:Set) (xs ys:list A),
 rev' xs ys = reverse xs ++ ys.
Proof.
 intros A xs.
 induction xs; simpl.
   intro. reflexivity.
 intro ys'.
 rewrite (IHxs (cons a ys')).
 (* reverse xs ++ cons a ys' =
    (reverse xs ++ cons a nil) ++ ys' *)
 assert (H: cons a ys' = (cons a nil) ++ ys').
 induction ys'; simpl.
   reflexivity.
 reflexivity.
 rewrite H.
 rewrite (append_assoc A (reverse xs) (cons a nil) ys').
 reflexivity.
Qed.

である。証明の冒頭で intros A xs だけを行い、ysについては intro していないが、ys を残したまま xs の帰納法を行わないと、IHxs を apply するときにうまくいかない。「無闇に intro しない方が良い」という良い例なので、ys を一緒に intros してしまうなど自分で試行錯誤してみて欲しい。

　この補題を使えば、
Theorem reverse_rev : forall (A:Set) (xs:list A),
 reverse xs = rev xs.
Proof.
 intros.
 unfold rev.
 induction xs; simpl.
   reflexivity.
 (* reverse xs ++ cons a nil = rev' xs (cons a nil) *)
 rewrite IHxs.
 (* rev' xs nil ++ cons a nil = rev' xs (cons a nil) *)
 rewrite (rev'_reverse A xs nil).
 rewrite (rev'_reverse A xs (cons a nil)).
 assert (H: forall l:list A, l ++ nil = l).
   induction l; simpl.
     reflexivity.
   rewrite IHl.  reflexivity.
 rewrite (H (reverse xs)).
 reflexivity.
Qed.

と証明出来る。


[Coq] reverse (reverse xs) = xs
2010-04-26T20:36:00.003+09:00
先日のProofCafeでみんなで解いていた reverse (reverse xs) = xs の証明について、どんな風に解くかを解説というか自分の解答を晒すというか。

　教科書でこの問題を演習課題として解く場合は、予め必要な補題が順々に証明課題として与えられる事が多いが、現実の問題ではそういうことはまず無い。（このあたり、現実の問題と試験問題の違いにも通ずる話だ。）

　まず、ProofCafe01から必要な定義をコピーしよう。
Inductive list (A: Type) : Type :=
 | nil  : list A
 | cons : A -> list A -> list A.

Implicit Arguments nil [A].
Implicit Arguments cons [A].

Fixpoint append {A : Type} (xs ys: list A) : list A :=
 match xs with
 | nil => ys
 | cons x xs => cons x (append xs ys)
 end.
Infix "++" := append (at level 60).

Theorem append_assoc : forall (A:Type) (xs ys zs:list A),
 (xs ++ ys) ++ zs = xs ++ (ys ++ zs).
Proof.
 (* あなたの証明を書いてね *)
Qed.

定理append_assocの証明は難しく無いと思うが、判らない人はProofCafeのページを参照して欲しい。

　次いで、関数reverseを定義しよう。
　関数型言語で関数を末尾再帰で書くのに慣れている人は、ついうっかり
Fixpoint rev' {A:Set} (xs ys:list A) :=
 match xs with
 | nil => ys
 | cons x xs' => rev' xs' (cons x ys)
 end.
Definition rev {A:Set} (xs:list A) := rev' xs nil.

と書いてしまうだろう。私も実は当日そう書いてしまい嵌った。

　ここは実行効率を考えず、ひとまず素直に、
Fixpoint reverse {A:Set} (xs:list A) :=
match xs with
| nil => nil
| cons x xs' => (reverse xs') ++ (cons x nil)
end.

と定義して証明する方が簡単だ。関数を実際に動かしてみる場合は、
Eval compute in reverse (cons 1 (cons 2 (cons 3 nil))).

とか入力してみれば良い。

　ここから、どうやって証明していったか、考えた過程を示そう。
　まずはいきなり、定理を証明しようとしてみた。
Theorem reverse_reverse : forall (A:Set) (xs:list A),
  reverse (reverse xs) = xs.
Proof.
  induction xs; simpl.
    reflexivity.

最初にxsについての帰納法を試み、xs=nilのケースは簡単に証明出来た。次のゴールの
reverse (reverse xs ++ (cons a nil) = cons a xs
については、リストを ++ で繋いでreverseする、
Hypothesis reverse_append : forall (A:Set) (xs ys:list A),
 reverse (xs ++ ys) = (reverse ys) ++ (reverse xs).
という定理があれば都合が良さそうだと何となく思いつく。（なんとなく美しげな定理だし。）

　そこで、とりあえず上記のHypothesisを先に定義して、改めてreverse_reverseを証明する。
Theorem reverse_reverse : forall (A:Set) (xs:list A),
 reverse (reverse xs) = xs.
Proof.
  induction xs; simpl.
    reflexivity.
  rewrite (reverse_append A (reverse xs) (cons a nil)).
  rewrite IHxs.


　この時点でゴールが
reverse (cons a nil) ++ xs = cons a xs
となる。そこで再度
Hypothesis append_cons_nil : forall (A:Set) (a:A) (xs:list A),
 (cons a nil) ++ xs = cons a xs.
Hypothesis reverse_cons : forall (A:Set) (a:A),
 reverse (cons a nil) = cons a nil.

を追加してから、改めてreverse_reverseを証明する。
Theorem reverse_reverse : forall (A:Set) (xs:list A),
 reverse (reverse xs) = xs.
Proof.
  induction xs; simpl.
    reflexivity.
  rewrite (reverse_append A (reverse xs) (cons a nil)).
  rewrite IHxs.
  rewrite (reverse_cons A a).
  rewrite (append_cons_nil A a xs).
  reflexivity.
Qed.


　証明が出来たので、Hypothesisで誤摩化していた部分をLemma, Theoremに書き換えて証明する。
Lemma append_cons_nil : forall (A:Set) (a:A) (xs:list A),
 (cons a nil) ++ xs = cons a xs.
Lemma reverse_cons : forall (A:Set) (a:A),
 reverse (cons a nil) = cons a nil.

については難しく無いので証明してみると良いだろう。(intros, simpl, reflexivityで証明出来る。)

Theorem reverse_append : forall (A:Set) (xs ys:list A),
 reverse (xs ++ ys) = (reverse ys) ++ (reverse xs).

については、解説しよう。

Proof.
 intros A xs ys.
 induction xs; simpl.
   assert (append_nil: forall (zs:list A), zs = zs ++ nil).
     induction zs; simpl.
       reflexivity.
     rewrite <- IHzs.  reflexivity.
   apply (append_nil (reverse ys)).
 rewrite IHxs.
 rewrite (append_assoc A (reverse ys) (reverse xs) (cons a nil)).
 reflexivity.
Qed.

証明の途中でzs = zs ++ nilが使いたくなり、わざわざ補題にするまでもないと思って、途中でassertで証明している。
　この証明したreverse_appendを使って、reverse_reverseを証明すれば完成。

　全体を改めて示すとこのようになる。
Inductive list (A: Type) : Type :=
| nil : list A
| cons : A -> list A -> list A.

Implicit Arguments nil [A].
Implicit Arguments cons [A].

Fixpoint append {A : Type} (xs ys: list A) : list A :=
match xs with
| nil => ys
| cons x xs => cons x (append xs ys)
end.
Infix "++" := append (at level 60).

Theorem append_assoc : forall (A: Type) (xs ys zs : list A),
(xs ++ ys) ++ zs = xs ++ (ys ++ zs).
Proof.
  intros.
  induction xs; simpl.
    reflexivity.
  rewrite IHxs.  reflexivity.
Qed.

Fixpoint reverse {A:Set} (xs:list A) :=
match xs with
| nil => nil
| cons x xs' => (reverse xs') ++ (cons x nil)
end.

Lemma append_cons_nil : forall (A:Set) (a:A) (xs:list A),
 (cons a nil) ++ xs = cons a xs.
Proof.
  intros. simpl. reflexivity.
Qed.
Lemma reverse_cons : forall (A:Set) (a:A),
 reverse (cons a nil) = cons a nil.
Proof.
  intros. simpl. reflexivity.
Qed.

Theorem reverse_append : forall (A:Set) (xs ys:list A),
 reverse (xs ++ ys) = (reverse ys) ++ (reverse xs).
Proof.
 intros A xs ys.
 induction xs; simpl.
   assert (append_nil: forall (zs:list A), zs = zs ++ nil).
     induction zs; simpl.
       reflexivity.
     rewrite <- IHzs.  reflexivity.
   apply (append_nil (reverse ys)).
 rewrite IHxs.
 rewrite (append_assoc A (reverse ys) (reverse xs) (cons a nil)).
 reflexivity.
Qed.

Theorem reverse_reverse : forall (A:Set) (xs:list A),
 reverse (reverse xs) = xs.
Proof.
  induction xs; simpl.
    reflexivity.
  rewrite (reverse_append A (reverse xs) (cons a nil)).
  rewrite IHxs.
  rewrite (reverse_cons A a).
  rewrite (append_cons_nil A a xs).
  reflexivity.
Qed.



[Coq] Proof Cafe #01
2010-04-26T01:30:00.003+09:00
Proof Cafe (栄)に参加しました。

　当日使われた資料はyoshihiro503の日記を参照の事。

　yoshihiro503さんによるCoq最速文法マスターという感じで、僅か90分の入門講座で、（Haskellなど関数型言語の知識があるとはいえ）Coqに初めての人が
Theorem append_length : forall (A: Type) (xs ys: list A),
  length (xs ++ ys) = length xs + length ys.
を証明出来る様になるってのは、やはり説明の手際が良いよなぁ。次に入門用PPTを修正する時は是非とも参考にしよう。

　Proof Cafe自体は２時間だったんですが、その後、懇親会を実施して頂き、なんか身に余る様な歓待をして頂きました。皆さんどうもありがとうございました。Coqに限らず関数型言語とかIT業界の話とか色々楽しく話をしました。

　Proof Cafeは今後も毎月名古屋で開催されるとか、Proof CafeでもCPDTを読もうとしている、ようです。Formal Methods Forumの方でも頑張ってCPDTを読んでいきたいです。

　


[Coq] Install on NetWalker
2010-04-18T22:52:00.003+09:00
買ってあったがしばらく放置していたNetWalkerにCoq, CoqIDEをインストールしました。まぁUbuntuなんで、sudo apt-get install coq coqideでインストール出来て当然だが、なんかCoqのバージョンが古いみたい。
　ともあれ通勤途中にCoqで遊べる様になった。


[Coq][FM] Formal Methods Forum #4 on 4/29
2010-04-17T20:45:00.003+09:00
形式仕様に関する勉強会のATND - 第4回FormalMethods勉強会を4/29に行います。
　Coqに関してはCerti􏰀ed Programming with Dependent Typesという教科書を今回から読み進める予定です。この本は、関数型言語のプログラマ向けに書かれた割と実践的な教科書です。
　Coq以外の内容についてはATNDのページからFormal Methods Forumのページを辿って下さい。


[Haskell] Haskellers Meeting 2010 Spring
2010-04-17T20:26:00.003+09:00
Haskellers Meeting 2010 Springを聞きにいきました。

　和田先生の話は、まぁ割とどうでも良い昔話だった。
　メインはSimon Peyton JonesさんのSTMの話。基本的には"Beautiful Code"に載っている話で、ジョークなども比較的聞き取りやすかった。ScalaにもSTM早く欲しいなぁ。
　山本さんのHaskellでWebサーバの話は前に聞いたことのある話だった。
　山下さんの擬データの話が、実は一番興味深かった。紹介された論文「擬データを用いた対話的関数プログラミングに関する研究」（石井裕一郎）はWeb上で見つからなかったが、「擬データと関数による並行プロセス群の記述」は検索するとCiNii上で読める様だ。擬データは興味深いのだけど、Haskell以外の言語では意味が無いかなぁ。

----
追記：
山下さんの発表資料はここから入手可能。


[Coq][FM] Formal Methods Forum Meeting #3
2010-04-03T21:52:00.003+09:00
一見、キャンセル待ち状況になっている第3回FormalMethods勉強会ですが、まぁ椅子を追加して対応可能だと思うので、とりあえず名前をATNDに書いて下さい。

あと、直前に案内メールとかが流れますのでFormalMethods勉強会のGoogle groupにも登録して頂くと良いと思います。


[Coq] Coq Course Materials at Nagoya Univ.
2010-03-28T03:00:00.003+09:00
名古屋大学の2009年度後期のGarrigue先生のCoqの講義の教材が公開されているので、Coqの勉強として解いてみた。
　全部は自力では解けず、答えを参照しつつ解いた部分もある。自習用には良い教材だと思った。
　解答とかcoqdocでHTML化したんだけど...宿題は公開するとまずいよね、やはり。2009年度後期はまだ終わってないし。
　とりあえずFormal Methods Forumの勉強会用に使えるかな？


[Joke] How do you trap a programmer in the shower?
2010-02-28T23:44:00.002+09:00
redditのHow do you trap a programmer in the shower? (list.cs.brown.edu)経由。

[plt-scheme] OT: How do you trap a programmer in the shower?を翻訳してみました。

オチが判らなかった箇所が幾つかあって、それはつまり誤訳してる可能性が高いので、間違っていたら指摘して頂けると嬉しいです。

----

ある生徒が教室で１つ目のジョークを言い、この類にはもっと色々考えられる様な気がした。これは最初の試みなので批判や追加を歓迎する。代名詞の性別についてはご容赦を。男性と女性を入れ替えたりすべきかどうか自信が無いし、彼/彼女と書くのは変だし、複数形で書くと複数人でシャワーを浴びている様なニュアンスがでてしまって本意じゃないし。:-)

Todd

Schemeプログラマをシャワー室に閉じ込めるには？
シャンプーを一瓶渡せ。(Hand him a bottle of shampoo.)

Visual Basicプログラマをシャワー室に閉じ込めるには？
カーテンをオープンするウィジェットを隠せ。

BASICプログラマをシャワー室に閉じ込めるには？
彼のCommodore-64をタイルに固定する為にシリコン接着剤を使え。

アセンブラプログラマをシャワー室に閉じ込めるには？
えーと、まず彼はシャワーをビルドしないと。

Javaプログラマをシャワー室に閉じ込めるには？
どこかにexitShower()メソッドがあると彼を説得し、ドキュメント全体を精査し終わるまで笑ってやれ。

Pythonプログラマをシャワー室に閉じ込めるには？
Guidoがそこにいることを望んでいると彼に伝えろ。

Cプログラマをシャワー室に閉じ込めるには？
そんなことをするな。彼は風呂桶をオーバーフローさせて君の家のコントロールを奪うだろう。

----

以下はredditで追加された物を幾つかピックアップして紹介。

C#プログラマをシャワー室に閉じ込めるには？
> インテリセンスをオフにしろ。

PHPプログラマをシャワー室に閉じ込めるには？
1. その頃、PHPプログラマは芝生に裸で立ち、庭用ホースと驚く程沢山のアタッチメントを手にして、どうして他の全ての人がシャワーの方が良いと言っているのか理解出来ない。
2. PHPプログラマをシャワーの外に出そうとしても出来ない。全ての現実の仕事はシャワーの中でだけ起き、外でのことは単にアカデミックでエリートぶった連中のすることだと主張するだろう。
3. 必要ない。ドキュメントをチェックしないと呼ぶべきメソッドがopen_door(), door_open(), openDoor(), doorOpen() のどれなのか思い出せないから。

LISPプログラマをシャワー室に閉じ込めるには？
1. 冗談を。LISPプログラマはシャワーを浴びない。(don't _take_ showers : 副作用が無いという話？)
2. ")"キーを奪え。

Rubyプログラマをシャワー室に閉じ込めるには？
彼が中に入ったらCurtain#openメソッドにモンキーパッチを当てろ。追加で一つ引数を取る様にして、その引数が何なのかドキュメントに書いておかない。
> 彼は単に引数が不要になるモンキーパッチを当てて戻すだけだが、そのパッチは一回以上使うとsegfaultする様な代物だ。

Prologプログラマをシャワー室に閉じ込めるには？
1. Yes (ってオチが良く解らん)
2. inShower(Programmer) :- inShower(Programmer).

Haskellプログラマをシャワー室に閉じ込めるには？
1. < 圏論に関する馬鹿馬鹿しい程に長い小論を挿入せよ >
2. 何もする必要が無い。シャワーの水で洗って純粋になったならば、シャワーから出るには出力が必要だと気付くから。
3. 必要ない。彼は怠惰(lazy)なので外に出ない。

JavaScriptプログラマをシャワー室に閉じ込めるには？
1. 気にする必要は無い。同時に２つのシャワーは動作しないので、それを修正しようと時間を費やすから。
2. IE6のロゴをシャワーカーテンに張ってデバッグする様に頼め。

Erlangプログラマをシャワー室に閉じ込めるには？
出来ない。彼は自分自身をクローンして、別々のシャワーで全てのクローンに身体の別々の部位を洗わせる。もし閉じ込められたら単にそれを殺すだけだ。

C++プログラマをシャワー室に閉じ込めるには？
C++プログラマはシャワーをvoidポインタにキャストして、ドアの存在を消す。
> 「これは正しいやり方ではないがしかし...」という注釈を付けるのを忘れてるよ。

Perlプログラマをシャワー室に閉じ込めるには？
1. 彼はどうやったら自分のシャワーが動くのか思い出せない。
2. 彼の脱出用の針金の余りで、閉じたシャワーカーテンとシャワーの向きを固定しているダクトテープとをくっ付けておく。

Objective-Cプログラマをシャワー室に閉じ込めるには？
[[NSShower standardShower] addPerson:[NSObjectiveCProgrammer programmerWithRSI]];
SEL removeSelector = @selector(removePerson:);
Method removeMethod = class_getInstanceMethod([NSShower class], removeSelector);
removeMethod->method_imp = voidMethod;


[Coq][FM] Formal Methods Forum #1
2010-02-14T10:50:00.005+09:00
2010/02/08に第1回FormalMethods勉強会というのがありました。
　形式手法って、企業内の勉強会とか、あるいは有料の研修コースはあるのだけど (i.e. ビジネスになる、ということなんだろう)、無料のIT勉強会はほとんどありませんでした。
　「形式手法の勉強会欲しいよね〜」という話から勉強会を始めることになり、まず第１回は各自の持ちネタを持ち寄る感じで開催されました。
　私はCoqとWhy (INRIAで作っているプログラムの検証用ツール) の話をしました。発表資料をSlideshareに上げたので興味のある方はどうぞ。

　Coqに限らず、形式仕様記述 (B, Zとか)、あるいは各種モデル検査 (SPIN, Alloyとか)、Lightweight Formal Method (VDMとか) なんでもありの勉強会なので興味のある方はどうぞ。
　開催場所は新宿の豆蔵オフィスを利用させて頂く事が多いのではないかと思うが、Coqという意味では一度名古屋遠征したいなぁ。

Formal Methods Forum : 勉強会のGoogle group
fm-forum @ ウィキ : 勉強会のWiki


[Scala] Articles about Scala 2.8 on ITpro
2010-02-11T02:45:00.002+09:00
Scala 2.8に関する紹介記事をITproに書きました。ほぼ年末年始休暇を費やして書き、2010年の1,2月に分けて掲載。

第15回 Scala 2.8の新機能 (1)
第16回 Scala 2.8の新機能 (2) --- コレクションライブラリの再実装

　記事を書く機会を与えてくださった羽生田さんに感謝を。


[Scala] Hindley-Milner Type Inference
2010-01-31T18:29:00.003+09:00
Hindley-Milnerの型推論を理解したいと思い、とりあえずScala by Exampleに載っているコードにデバッグプリントを大量に挿入して動かしてみました。
動かした結果を、将来の自分の為にメモしたものがHM.pdf、
動かしたソースはHM.scalaにあります。

アルゴリズム自体はHindley Milner Type Inference Algorithm (PS file)とか簡潔に書かれている。が、こうやってデバッグプリントを挟んで動かしてみないとなかなか判らない...。


[Scala] Talk on scala-be's "Step by Step Scala" on 12/22
2009-12-17T12:00:00.003+09:00
東京のScala勉強会であるscale-beの、12/22開催のStep by Step Scala [vol.06]@scala-be (ATNDへのリンク)で講師をすることになりました。
　今回は主として14章の「表明と単体テスト」のScalaCheckの使い方を中心に話をしようと思っています。ScalaCheckは「満たすべき性質を記述する」ことでテストケースを自動生成してくれる面白い単体テストツールですが、従来のxUnit系テストツールとはちょっと使い方が違うというのもあって、使い方を学ぶには良いのではないかと思います。
　参加者希望者は上記のATNDのリンクから申し込みをしていただければと思います。
　今回は日程が12/22と多くの忘年会と重なる日で、割と参加者は少なそうでちょっと残念。


[Scala] Scala Style Guide
2009-11-29T22:44:00.002+09:00
Scala Style Guide (PDF)

Scalaのコーディングスタイルガイド。

[scala] Proposed Style Guideで議論されていて、Oderskyもコメントしてる。これが叩き台になって正式版が出たら訳すといいかなぁ。


[Scala][Book] Pro Scala: Monadic Design Patterns for the Web
2009-11-23T11:36:00.002+09:00
APressからPro Scala: Monadic Design Patterns for the Webという本が出る様です。
今までの職業的プログラマの視野に入っていなかったが、実は実用的にも重要である概念の、
- Monadic design patterns
- Zippers and data type differentiation
- Delimited continuations
を考察するとのこと。

「モナド＝デザインパターン」というのはあちこちで書かれていることだし、モナドに限らず圏論的視点で計算を考えようという話は檜山さんのブログで繰り返し出て来るテーマ（11/28開催のセミナーのコパスタを食べる余会はまだ空席があるようですよ）。
Delimited continuationということはScala 2.8対応だし、限定継続を一般向けに紹介した本は今までにあるのかなぁ？なんかそれだけでも価値があるよね。

なんか非常に楽しみな本ですね。


[Event] Recent Days
2009-11-23T11:17:00.002+09:00
今週は、Step by Step Scala [vol.04]@scala-beで話をしたり、Haskellナイトを見に行ったり、Scala Hack-a-thon #1に参加したり、でした。

Step-by-Step Scalaは、（少なくとも何人かの方には）Swarmについて興味を持ってもらえた様なので満足。この先の仕事の状況がまだ確定しないのだけど、また機会があればScalaの講師を出来ればなぁ、とか。

Haskellナイトは、本の話がちょっと多過ぎたかなぁとは思うのだけど、出版合わせのイベントだから仕方がないのかなぁ。もうちょっとHaskellの話を聞きたかったかも。

Scala Hackathonは存在を知った時には既に満員になっていて参加を諦めてたんですが、当日朝見たらキャンセルが大量に出たみたいで慌てて家を出た次第。yuroyoroさんの作成したテキストが良く出来ていて、みんな黙々とそれを読んでいたのかな？かつ、質問はtwitterで主として行われていたみたい。懇親会も楽しく参加させて頂きました。


[Scala] Talk on scala-be's "Step by Step Scala" in November
2009-10-25T21:17:00.004+09:00
東京のScala勉強会にscale-beというのがありまして、隔週の水曜or木曜の夜に新宿の豆蔵で開催しています。
内容はOderskyの「Scalaスケーラブルプログラミング」の章立てに沿って講師がScalaを解説するというもので、読書会の様にテキストに厳格に沿う訳ではありません。
参加者は、
出来れば該当の本を持参して下さい。本の内容を逐一全部話す訳ではないですし。
出来れば最近のScala実行系（Scala 2.7系）がインストールされたノートPCを持参して下さい。簡単な課題とか、実際に自分でインタプリタ上で動作確認したり、などがあるので。同様に、Scala APIドキュメント（JavaDoc）などをインストールしておくと良いです。（なお、会場はコンセントは利用可能ですが、インターネット接続は提供されません。）

あと、勉強会の後に懇親会も行っています。

で、11/4(Wed), 11/19(Thr)の２回は私が講師を担当する事になりました。それぞれ6,7章と8,9章の範囲について話す予定です。11/19の回にはテキストの内容からちょっと離れて最近のScalaの話題という事でSwarmの話をちょっとだけ紹介しようと思ってます。

なお、参加申し込みはATND上で行われ、ATNDへのリンクを含む開催案内は定期的にscala-be上で告知されます。
では、11月に勉強会会場でお会いしましょう。

---
追記：11/21

２回の発表で使用した資料はPDF形式でscala-be Google groupのファイル置き場で公開してます。


[Agda] Install Agda on Mac OS
2009-10-21T00:29:00.004+09:00
Mac OS 10.5 の上にAgdaをインストールしました。基本的にはAgda Wikiを参考にしたのだけど、そのままではうまく動きませんでした。


Xcodeをインストール。DVDからなり、ADCのサイトなりから。最新版は10.6用なので古いのをインストール。
Mac Portsのインストール。/opt/local/binにPATHを通す。Mac Portsの準備が済んでいる人もsudo port -v selfupdateする。
GHCはportsからインストールすると古くて駄目なので、GHC download pageよりバイナリパッケージを導入。
sudo port install hs-cabalして、sudo cabal updateして、~/.cabal/binにPATHを通す。
sudo port install darcs
sudo cabal install happyして、sudo cabal install alex
sudo cabal install Agda-executable
cd ~/.cabal/binして、./agda-mode setup
emacsは薦められるままにAquamacsを導入する。

下記を~/.emacsに追加。
(setq load-path (cons "~/.cabal/share/Agda-2.2.4/emacs-mode/" load-path)) (autoload 'agda2-mode "agda2-mode" "Major mode for Agda2 files" t) (unless (assoc "\\.agda" auto-mode-alist) (setq auto-mode-alist (nconc '(("\\.agda" . agda2-mode) ("\\.alfa" . agda2-mode)) auto-mode-alist)))
Aquamacsを起動し、~/test.agdaというファイルを作成して、
module test where data Bool : Set where true : Bool false : Bool
と書く（true, falseの前のインデント必須。単語や:の前後に空白があるのも確認。）
C-c C-lで入力内容が処理され、文字が色分けされたら、agda2-modeが動いている。

---
追記: ~/.emacsについて念のため全部掲載。haskell-modeの設定も重要らしいので。


(setq load-path (cons "‾/.cabal/share/Agda-2.2.4/emacs-mode/" load-path))
(autoload 'agda2-mode "agda2-mode" "Major mode for Agda2 files" t)
(unless (assoc "¥¥.agda" auto-mode-alist)
   (setq auto-mode-alist
   (nconc '(("¥¥.agda" . agda2-mode)
     ("¥¥.alfa" . agda2-mode)) auto-mode-alist)))
(setq load-path (cons "‾/lib/elisp/haskell" load-path))
(setq auto-mode-alist
      (append auto-mode-alist
              '(("促促.[hg]s$"  . haskell-mode)
                ("促促.hi$"     . haskell-mode)
                ("促促.l[hg]s$" . literate-haskell-mode))))
(autoload 'haskell-mode "haskell-mode"
   "Major mode for editing Haskell scripts." t)
(autoload 'literate-haskell-mode "haskell-mode"
   "Major mode for editing literate Haskell scripts." t)
(add-hook 'haskell-mode-hook 'turn-on-haskell-decl-scan)
(add-hook 'haskell-mode-hook 'turn-on-haskell-doc-mode)
(add-hook 'haskell-mode-hook 'turn-on-haskell-indent)
(add-hook 'haskell-mode-hook 'turn-on-haskell-ghci)

(setq haskell-literate-default 'latex)
(setq haskell-doc-idle-delay 0)


(load-file (let ((coding-system-for-read 'utf-8))
                (shell-command-to-string "agda-mode locate")))

[Agda] Agda Lectures at CVS

2009-10-16T00:19:00.004+09:00

産業技術総合研究所の研修コース「 Agda による仕様記述」に参加しました。

以下は私の参加した10月の回の話。もしかしたら11月は10月の参加者の反応を見て内容が変更されるかもしれません。

一言で言うと
Coq, Agda のような定理証明系とか依存型の関数型言語とかに興味のある人が、概要を知るには良い二日半のコース。参加費無料なのもポイントが高い。お薦め。（開催が大阪なんで関西周辺以外の人にはちょっと厳しいが）

もう少し詳しく説明すると
「Agdaの持つ依存型の機能を使って、仕様の制約を型として表現すれば、機械的に検証出来るよね」というところに主眼を置いているみたいです。なので、定理証明の部分は従であり、主眼は仕様を書ける様になろう、ということのようです。
とはいえ、仕様の制約をAgdaで書く以上、書いた関数が仕様を満たしていることを示す必要がある訳ですが...。

が、まぁ当たり前と言えば当たり前なんですが、二日半ではAgdaを使いこなせるようにはならなかった...。まぁJavaだってHaskellだって二日半では使える様にはならない訳で、当然というか仕方が無い。なので、「Agdaがどんなものなのかの概説を聞く」ぐらいに考えていたほうが良いです。
とはいえ、Agdaに関する日本語の資料はほとんど無い現状で、テキストの説明を聞き、判らないところを教わりつつのハンズオン実習がある訳で、価値は大きい。

参加者は結局８名。堅苦しさの無い普通のIT系勉強会のようなフレンドリーな雰囲気で、質問しまくりみたいな。逆に言うと講義内容がまだきっちりと固まっている訳では無い感じです。
にわとり小屋でのプログラミング日記のCoqな今井さんとお近づきになれたのも良かったです。数人で２日目の夜に懇親会したのですが、最初からちゃんと計画して全員（講師の方にも声をかけて）でやれば良かったと反省。
＃話に出た紫色の本は、"Handbook of Practical Logic and Automated Reasoning" (John Harrison, Cambridge Univ. Press, 2009) です＞今井さん。

とにかく私は楽しかったです。代休消化で関西旅行した価値がありました。参加させて頂き、ありがとうございました＞CVSの方々。

参加の前提について
募集要項には「プログラムを書いた経験(言語不問)、またはシステムやソフトウェアの設計に従事したことがあること。」「Emacs で文書を作成編集した経験があること。」と書いてあるんですが...。
うーむ、HaskellとかOCamlとかの類の型付き関数型言語の初歩的な知識があったほうがいいかも。モナドとか別に知らなくてもいいけど、簡単な再帰とかパターンマッチとか使って List の map とか length とかぐらい書けたほうが良いかもしれないです。そうでないと初日の演習問題でいきなり困るかも。あとはまぁ、ペアノの自然数( 3 = succ(succ(succ(zero))) みたいな話 ) も知ってた方が良いかなぁ。
ただ、参加者の関数型言語への習熟度を見て調整していたかも知れないので、11月はどうなるかは判らないです。

[Scala] sbt : simple-build-tool (1)

2009-07-25T12:11:00.004+09:00

sbt (simple-build-tool) は Scala で書かれたビルドツールです。
これもscalaで書かれたDSL的なツールであり、プロジェクトのビルドの設定などをscalaで記述する事が出来たりします。

試しに使ってみて、使い方が判ったら追記していこうと思います。

★インストール

Setupのページに従い作業します。
私は MacOS ユーザなので Unix の指示に従い作業。

まずsbt-launcher-0.5.1.jar をダウンロードして指示通り~/binに置き、~/bin/sbt ファイルを作り chmod したりします。


% ls ~/bin
sbt   sbt-launcher-0.5.1.jar
% cat ~/bin/sbt
java -Xmx256M -jar `dirname $0`/sbt-launcher-0.5.1.jar "$@"
%

★動作確認
空の (*.scala の無い) 作業ディレクトリに hw.scala を作ります。(main メソッドを探して自動で判断する都合上、無関係なソースがあると巧く動作しません。最初それで失敗しました。)


% ls
hw.scala
% cat hw.scala
object Hi { def main(args: Array[String]) { println("Hi!") } }
%

とりあえず下記の様に動きました。


[apple-3:~/work/scala/hw] miyamoto% ~/bin/sbt 
Project does not exist, create new project? (y/N/s) : s
:: loading settings :: url = jar:file:/Users/miyamoto/bin/sbt-launcher-0.5.1.jar!/org/apache/ivy/core/settings/ivysettings.xml
:: retrieving :: sbt#boot
 confs: [default]
 2 artifacts copied, 0 already retrieved (9831kB/149ms)
:: retrieving :: sbt#boot
 confs: [default]
 3 artifacts copied, 0 already retrieved (3171kB/26ms)
[info] Building project scratch 1.0 using sbt.DefaultProject
[info]    with sbt 0.5.1 and Scala 2.7.5
[info] No actions specified, interactive session started. Execute 'help' for more information.
> run
[info] 
[info] == compile ==
[info]   Source analysis: 1 new/modified, 0 indirectly invalidated, 0 removed.
[info] Compiling main sources...
[info] Compilation successful.
[info]   Post-analysis: 2 classes.
[info] == compile ==
[info] 
[info] == run ==
[info] Running Hi ...
Hi!
[info] == run ==
[success] Successful.
[info] 
[info] Total time: 2 s
> quit
[info] 
[info] Total session time: 14 s
%

この結果として下記の様にプロジェクトが生成されます。このあたりは Maven とかと同様な感じ。各プロジェクト毎にscala-compiler.jarを持ったりするのは、なんか富豪的だなぁ。


% ls -RCF
hw.scala project/ target/

./project:
boot/   build.properties

./project/boot:
scala-2.7.5/

./project/boot/scala-2.7.5:
lib/  sbt-0.5.1/ update.log

./project/boot/scala-2.7.5/lib:
scala-compiler.jar scala-library.jar

./project/boot/scala-2.7.5/sbt-0.5.1:
ivy-2.0.0.jar  jsch-0.1.31.jar  sbt_2.7.5-0.5.1.jar

./target:
analysis/ classes/

./target/analysis:
applications  external  hashes
dependencies  generated_files  tests

./target/classes:
Hi$.class Hi.class
%

[Scala] S-99: Ninety-Nine Scala Problems (P01-28)

2009-05-31T22:54:00.003+09:00

S-99: Ninety-Nine Scala ProblemsのList編(P01-P28)の抄訳です。

アスタリスクの数は難易度です。

効率も大事ですが、エレガントな回答を求めます。可能ならばより簡潔で、計算量が少なく、末尾再帰になっている回答を作りましょう。

Scalaの組み込み関数を使ってもOKです。が、使わないほうが勉強になります。

答えが知りたければ、元の英語文書の各問題のリンクをクリックして下さい。

P01 (*) リストの最後の要素を求めよ。


scala> last(List(1, 1, 2, 3, 5, 8))
res0: Int = 8

P02 (*) リストの最後から二番目の要素を求めよ。


scala> penultimate(List(1, 1, 2, 3, 5, 8))
res0: Int = 5

P03 (*) リストのn番目の要素を求めよ。但しリストの最初の要素は0番目とする。


scala> nth(2, List(1, 1, 2, 3, 5, 8))
res0: Int = 2

P04 (*) リストの要素の数を求めよ。


scala> length(List(1, 1, 2, 3, 5, 8))
res0: Int = 6

P05 (*) リストを逆順にせよ。


scala> reverse(List(1, 1, 2, 3, 5, 8))
res0: List[Int] = List(8, 5, 3, 2, 1, 1)

P06 (*) リストが回文になっているか調べよ。


scala> isPalindrome(List(1, 2, 3, 2, 1))
res0: Boolean = true

P07 (**) ネストされたリスト構造を平坦化せよ。


scala> flatten(List(List(1, 1), 2, List(3, List(5, 8))))
res0: List[Any] = List(1, 1, 2, 3, 5, 8)

P08 (**) リスト要素の連続した重複物を除去せよ。もしリストの要素で繰り返し要素が含まれていたならば要素一つに置き換えよ。要素の順序は変えてはならない。


scala> compress(List('a, 'a, 'a, 'a, 'b, 'c, 'c, 'a, 'a, 'd, 'e, 'e, 'e, 'e))
res0: List[Symbol] = List('a, 'b, 'c, 'a, 'd, 'e)

P09 (**) 連続した重複物を子リストに纏めよ。もしリストの要素が繰り返し要素ならば、別々の子リストに分割せよ。


scala> pack(List('a, 'a, 'a, 'a, 'b, 'c, 'c, 'a, 'a, 'd, 'e, 'e, 'e, 'e))
res0: List[List[Symbol]] = List(List('a, 'a, 'a, 'a), List('b), List('c, 'c), List('a, 'a), List('d), List('e, 'e, 'e, 'e))

P10 (*) リストをランレングス・エンコードせよ。P09の結果を用いていわゆるランレングス・エンコーディングによるデータ圧縮法を実装せよ。連続した重複要素はタプル(N,E)にエンコードされる。但しNは要素Eの重複数。


scala> encode(List('a, 'a, 'a, 'a, 'b, 'c, 'c, 'a, 'a, 'd, 'e, 'e, 'e, 'e))
res0: List[(Int, Symbol)] = List((4,'a), (1,'b), (2,'c), (2,'a), (1,'d), (4,'e))

P11 (*) 修正ランレングス・エンコーディング。P10の結果を修正し、もし要素に重複が無ければ単に要素を結果にコピーせよ。重複している要素だけを(N,E)の形に変換せよ。


scala> encodeModified(List('a, 'a, 'a, 'a, 'b, 'c, 'c, 'a, 'a, 'd, 'e, 'e, 'e, 'e))
res0: List[Any] = List((4,'a), 'b, (2,'c), (2,'a), 'd, (4,'e))

P12 (**) ランレングス・エンコードされたリストをデコードせよ。P10の仕様で生成されたランレングス・エンコードされたリストを元の圧縮されていないものに戻せ。


scala> decode(List((4, 'a), (1, 'b), (2, 'c), (2, 'a), (1, 'd), (4, 'e)))
res0: List[Symbol] = List('a, 'a, 'a, 'a, 'b, 'c, 'c, 'a, 'a, 'd, 'e, 'e, 'e, 'e)

P13 (**) リストのランレングス・エンコーディング（直接解法）。いわゆるランレングス・エンコーディングを直接実装せよ。すなわち（P09のpackの様な）自分で書いた他のメソッドを使ってはならない。直接書く事。


scala> encodeDirect(List('a, 'a, 'a, 'a, 'b, 'c, 'c, 'a, 'a, 'd, 'e, 'e, 'e, 'e))
res0: List[(Int, Symbol)] = List((4,'a), (1,'b), (2,'c), (2,'a), (1,'d), (4,'e))

P14 (*) リスト要素を重複させよ。


scala> duplicate(List('a, 'b, 'c, 'c, 'd))
res0: List[Symbol] = List('a, 'a, 'b, 'b, 'c, 'c, 'c, 'c, 'd, 'd)

P15 (**) 指定した個数、リスト要素を重複させよ。


scala> duplicateN(3, List('a, 'b, 'c, 'c, 'd))
res0: List[Symbol] = List('a, 'a, 'a, 'b, 'b, 'b, 'c, 'c, 'c, 'c, 'c, 'c, 'd, 'd, 'd)

P16 (**) 毎N番目の要素を除去せよ。


scala> drop(3, List('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k))
res0: List[Symbol] = List('a, 'b, 'd, 'e, 'g, 'h, 'j, 'k)

P17 (*) リストを二つに分割せよ。前半の長さは与えられるものとする。結果はタプルで返す。


scala> split(3, List('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k))
res0: (List[Symbol], List[Symbol]) = (List('a, 'b, 'c),List('d, 'e, 'f, 'g, 'h, 'i, 'j, 'k))

P18 (**) リストのスライスを抽出せよ。二つの添字 i と j が与えられたとき、スライスとは元のリストの i 番目の要素を含むが j 番目の要素を含まないリストである。要素は0番目から始まるとする。


scala> slice(3, 7, List('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k))
res0: List[Symbol] = List('d, 'e, 'f, 'g)

P19 (**) リストの要素をn個左ローテートせよ。


scala> rotate(3, List('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k))
res0: List[Symbol] = List('d, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'a, 'b, 'c)

scala> rotate(-2, List('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k))
res1: List[Symbol] = List('j, 'k, 'a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i)

P20 (*) リストのk番目の要素を除去せよ。除去されたリストと除去した要素をタプルで返せ。要素は0番目から始まるとする。


scala> removeAt(1, List('a, 'b, 'c, 'd))
res0: (List[Symbol], Symbol) = (List('a, 'c, 'd),'b)

P21 (*) リストの指定された場所に要素を追加せよ。


scala> insertAt('new, 1, List('a, 'b, 'c, 'd))
res0: List[Symbol] = List('a, 'new, 'b, 'c, 'd)

P22 (*) 与えられた範囲の整数のリストを作れ。


scala> range(4, 9)
res0: List[Int] = List(4, 5, 6, 7, 8, 9)

P23 (**) リストから指定された数だけ値をランダムに選択せよ。（ヒント：P20を使え）


scala> randomSelect(3, List('a, 'b, 'c, 'd, 'f, 'g, 'h))
res0: List[Symbol] = List('e, 'd, 'a)

P24 (*) ロト：1〜Mからn個の異なるランダムな値を選べ。


scala> lotto(6, 49)
res0: List[Int] = List(23, 1, 17, 33, 21, 37)

P25 (*) 要素のランダムな順列を作成せよ。（ヒント：P23を使え）


scala> randomPermute(List('a, 'b, 'c, 'd, 'e, 'f))
res0: List[Symbol] = List('b, 'a, 'd, 'c, 'e, 'f)

P26 (**) n要素数のリストからk個の異なるオブジェクトを取り出す組み合わせを生成せよ。12人から3人の委員会を作る方法は何通りだろうか？答えは C(12,3)=220通り（C(n,k）はよく知られた二項係数）である。数学者にとってはこれで十分であるが、我々は本当に全ての解を生成したい。


scala> combinations(3, List('a, 'b, 'c, 'd, 'e, 'f))
res0: List[List[Symbol]] = List(List('a, 'b, 'c), List('a, 'b, 'd), List('a, 'b, 'e), ...

P27 (**) 集合の要素を、互いに素な部分集合に纏めよ。
a) 9人の人をそれぞれ2,3,4人の３グループに纏める方法は何通りか？全ての組み合わせを生成する関数を書け。


scala> group3(List("Aldo", "Beat", "Carla", "David", "Evi", "Flip", "Gary", "Hugo", "Ida"))
res0: List[List[List[String]]] = List(List(List(Aldo, Beat), List(Carla, David, Evi), List(Flip, Gary, Hugo, Ida)), ...

b) 上の問題を一般化してグループの大きさのリストを与えるとグループのリストを与える様にせよ。グループメンバーの順列は求めていない、すなわち((Aldo,Beat),...)は((Beat,Aldo),...)と同じ解である。しかし、((Aldo,Beat),(Carla,David),...)は((Carla,David),(Aldo,Beat),...)と異なる解である。


scala> group(List(2, 2, 5), List("Aldo", "Beat", "Carla", "David", "Evi", "Flip", "Gary", "Hugo", "Ida"))
res0: List[List[List[String]]] = List(List(List(Aldo, Beat), List(Carla, David), List(Evi, Flip, Gary, Hugo, Ida)), ...

この組み合わせ問題に関して知りたければ離散数学の良い本で「多項係数」について調べよ。
P28 (**) リストのリストを長さでソートせよ。
a) 要素がリストであるリストを考える。そのリストの要素を長さでソートする、すなわち短いリストを前に、長いリストを後にする。


scala> lsort(List(List('a, 'b, 'c), List('d, 'e), List('f, 'g, 'h), List('d, 'e), List('i, 'j, 'k, 'l), List('m, 'n), List('o)))
res0: List[List[Symbol]] = List(List('o), List('d, 'e), List('d, 'e), List('m, 'n), List('a, 'b, 'c), List('f, 'g, 'h), List('i, 'j, 'k, 'l))

b) 次に同様にリストを長さでソートするが、今回は長さの頻度でソートする。すなわち稀な長さのものを前に、頻度の高い長さのものを後ろにする。例の場合、長さ４と１のリストはただ１度しか現れない。3番目と4番目は長さ3のリスト２つである。最後に３つの最も頻度の高い長さ２のリストが現れる。


scala> lsortFreq(List(List('a, 'b, 'c), List('d, 'e), List('f, 'g, 'h), List('d, 'e), List('i, 'j, 'k, 'l), List('m, 'n), List('o)))
res1: List[List[Symbol]] = List(List('i, 'j, 'k, 'l), List('o), List('a, 'b, 'c), List('f, 'g, 'h), List('d, 'e), List('d, 'e), List('m, 'n))

[Scala] Sudoku in Scala

2009-05-22T01:01:00.003+09:00

Scalaユーザ会5/22(金)19：00-21：00@新宿三井ビル3で話をする予定の「Scalaで数独を解く」話です。

ScalaSudoku.pdf : プレゼン資料
Sudoku.scala : ソースコード

[Joke] Translation of "A Brief, Incomplete, and Mostly Wrong History of Programming Languages"

2009-05-20T00:00:00.005+09:00

A Brief, Incomplete, and Mostly Wrong History of Programming Languagesの翻訳です。面白かったので翻訳してみました。

「簡潔で不完全でほとんど間違っているプログラミング言語の歴史」

1801 - Joseph Marie Jacquardが、織機にパンチカードで命令することで、タペストリーに「hello, world」を織り込んだ。（しかし）末尾再帰やコンカレンシーの欠如、あるいは適切に大文字が使用されていないため、当時のRedditerたちは感銘を覚え無かった。

1842 - Ada Lovelaceが最初のプログラムを書いた。その過程に於いて、コードを走らせる実際のコンピュータを持っていないという些細な困難に妨げられた。後のエンタープライズアーキテクトたちは、UMLでプログラムする為に、彼女のテクニックを再習得した。

1936 - Alan Turingが、（将来に亘る）全てのプログラミング言語を発明した。しかし彼がその特許をとる前に、英国情報部は彼を007にするために強制徴募した。

1936 - Alonzo Churchもまた、（将来に亘る）全てのプログラミング言語をさらにうまく発明した。彼のλ算法はC言語に十分似ていない為に無視された。この批判は、当時まだCが発明されていないという事実にも関わらず生じた。

1940年代 - 結線とスイッチによって様々な「コンピュータ」が「プログラム」された。「タブ vs 空白」の論戦を避けるために、技術者たちはこの方式を採用した。

1957 - John BackusとIBMがFORTRANを作った。IBMにもFORTRANにも面白いところは何も無い。青いネクタイを着用せずFORTRANを書くのは文法エラーである。

1958 - John McCarthyとPaul GrahamがLISPを発明する。戦後の戦略的括弧備蓄の枯渇による高コストの為、LISPは決してポピュラーにはならなかった[1]。ポピュラーでは無いにも関わらず、LISP (今では "Lisp" あるいは時には "Arc") は「再帰と他人を見下すことなどの重要なアルゴリズム技法」に於ける影響度の高い言語であり続けている。

1959 - L. Ron Hubbardとの賭けに負けた後に、Grace Hopperを含む何人かのサディスト達が「大文字化された定型文志向言語」 (Capitalization Of Boilerplate Oriented Language = COBOL) を発明する。後に、Hooper提督のCOBOLの業績に対する見当外れで性差別的な報復として、Rubyコンファレンスでは嫌女性的題材が取り上げられる。

1964 - John KemenyとThomas Kurtzが、非計算機科学者の為の非構造化プログラミング言語であるBASICを作った。

1965 - KemenyとKurtzはGO TO 1964.

1970 - Guy SteeleとGerald SussmanがSchemeを作った。彼らの著作は「Lambda the Ultimate」の一連の論文をもたらし、「究極の台所用品ラムダ」にその頂点を迎えた。この論文はロングランの基礎となったが、深夜のインフォマーシャルとしては究極的に失敗であった。Javaがラムダを持たないことによってラムダをポピュラーにするまでラムダは比較的目立たないところへと左遷された。

1970 - Niklaus Wirthが手続き型言語のPascalを作った。Pascalは直ちに批難されたが、"x := x + y"という構文を、より親しみやすいC的な"x = x + y"の代わりに使用したためであった。この批判は、当時まだCが発明されていないという事実にも関わらず生じた。

1972 - Dennis Ritchieは前後を同時に撃つことの出来る強力な銃を発明した。発明のもたらした多くの死者及び障害者に満足することなく、彼はCとUnixを発明した。

1972 - Alain Colmerauerは論理型言語Prologをデザインした。彼の目標は二歳児の知性を持った言語を作ることであった。全てのクエリに「No」と答えるPrologセッションを示すことによって、目標に達したことを証明した。

1973 - Robin MilnerはM&M型理論に基づく言語のMLを作った。MLの子供として形式仕様意味論を持つSMLが生まれた。形式意味論の形式意味論を質問されてMilnerの頭は爆発した。ML一家の他の良く知られた言語にはOCaml, F#, Visual Basicがある。

1980 - Alan kayはSmalltalkを作り、用語「オブジェクト指向」を発明した。その意味を聞かれると彼は「Smalltalkのプログラムは単にオブジェクトである」と答えた。オブジェクトは何から作られるのかを聞かれると彼は「オブジェクトだ」と答えた。再度質問されると彼は云った。「だからさ、下の下まで全部オブジェクトなんだってば。亀にたどり着くまでは。」

1983 - Bjarne Stroustrupは耳にしたもの全てをCにねじ止めすることでC++を作った。その結果、言語は非常に複雑になり、プログラムをSkynet人工知能でコンパイルするために未来へ送らねばならなかった。ビルド時間は犠牲となった。Skynetがサービスを提供し続けた動機は依然としてはっきりしないが、未来からの広報担当はオーストリア訛りで単調に「気にするようなことは何も無い、ベイビー」と云った。Skynetはバッファーオーバーランを飾り立てたものに過ぎないという推測もある。

1986 - Brad CoxとTom LoveがObjective-Cを作り、アナウンスした。「この言語はCのメモリ安全性とSmalltalkの素晴らしい実行速度が結びついたものです。」現代の歴史家たちは二人が失読症であったと疑っている。

1987 - Larry Wallが眠気を催し、キーボードに額をぶつけた。目を覚ましたとき、Larry Wallのモニターの上の文字列はランダムなのではなく、神が預言者Larry Wallにデザインすることを欲しているプログラミング言語のサンプルプログラムだと悟った。Perlが生まれた。

1990 - Simon Peyton-Jones, Paul Hudak, Philip Wadler, Ashton Kutcher そして「動物の倫理的扱いを求める人々の会」からなる委員会は、純粋非正格関数型言語Haskell を作った。副作用を制御するためモナドを使用する複雑さの為、Haskellは抵抗を受けた。Wadler は批判を和らげるために説明した。「モナドは自己準同系ファンクタの圏のモノイドなんだ。何か問題が？」

1991 - オランダ人プログラマのGuido van Rossumが謎の手術の為にアルゼンチンへと旅行した。頭部に大きな傷を負って帰国し、Pythonを発明し、多数の賛同者によって終身独裁者に任じられ、世界に対して「あることをするのにひとつしかやり方がない」と報じた。ポーランドは神経質になっている。

1995 - 「Mad Matz」こと、まつもとゆきひろは、漠然とした特定されない終末を避けるためにRubyを作ったが、その終末においてはオーストラリアはモヒカン戦士とティナ＝ターナーが支配する砂漠となる。その言語は後にRuby on Railsと、真の発明者David Heinemeier Hanssonによって改名された。[まつもとがRubyと呼ばれる言語を発明した云々は実際には起きておらず、この記事の次の改訂時に削除されるべきだ - DHH].

1995 - Brendan Eichはプログラミング言語設計で起きた全ての失敗について読み、自分でも幾つか発明し、LiveScriptを作成した。後にその言語は、Javaの人気に肖る為、JavaScriptと改名された。後になっても、皮膚病の人気に肖る為にECMAScriptと改名された。

1996 - James GoslingはJavaを発明した。Javaは比較的冗長で、ガベージコレクションをし、クラスベースで、静的型付けで、シングルディスパッチで、単一実装継承と複数インタフェース継承のオブジェクト指向な言語である。SunはJavaの新規性を宣伝した。

2001 - Anders HejlsbergがC#を発明した。C#は比較的冗長で、ガベージコレクションをし、クラスベースで、静的型付けで、シングルディスパッチで、単一実装継承と複数インタフェース継承のオブジェクト指向の言語である。MicrosoftはC#の新規性を宣伝した。

2003 - 酔っ払ったMartin Oderskyは誰かのピーナツバターが別の人のチョコレートにくっつくというReeseのピーナツバターカップのCMを見て着想を得た。彼はオブジェクト指向と関数型言語の作り上げたものを統合する言語Scalaを作った。これを見た両派閥とも激怒し、それぞれ直ちに聖戦を宣告した。

Footnotes

1. 計算機科学にとっては幸運なことに、中括弧と山括弧の供給は潤沢であった。
2. Catch as catch can - Verity Stob

[Scala] Jersey with Scala + Jetty

2009-05-03T22:33:00.003+09:00

Jersey は JAX-RS (Java API for RESTful Web Service)のreference実装です。
これをScalaで動かしてみます。

1. Libraries : Jetty 6.1.17. Jersey 1.0.3 を使用しました。下記をEclipseプロジェクトのreference librariesに登録

Jetty : jetty-XX.jar, jetty-util-XX.jar, servlet-api-XX.jar
Jersey : jsr311-api-XX.jar, jersey-core-XX.jar, jersey-server-XX.jar, asm-XX.jar

2. test.jersey.JerseyTest.scala : メインルーチンです


package test.jersey

import javax.servlet.ServletException
import javax.servlet.http.HttpServlet
import javax.servlet.http.HttpServletRequest
import javax.servlet.http.HttpServletResponse

import org.mortbay.jetty.Server
import org.mortbay.jetty.nio.SelectChannelConnector
import org.mortbay.jetty.servlet.Context
import org.mortbay.jetty.servlet.ServletHolder

import com.sun.jersey.spi.container.servlet.ServletContainer
  
object JerseyTest {
  def main(args: Array[String]) {
    val server = new Server(8080)
    val connector = new SelectChannelConnector()
    server.addConnector(connector)
    
    val holder:ServletHolder = new ServletHolder(classOf[ServletContainer])
    holder.setInitParameter(
      "com.sun.jersey.config.property.resourceConfigClass",
      "com.sun.jersey.api.core.PackagesResourceConfig")
    holder.setInitParameter(
      "com.sun.jersey.config.property.packages",
      "test.jersey.resource")
// URLをクラスにマッピングする為のpackage名

    val context = new Context(server, "/", Context.SESSIONS)
    context.addServlet(holder, "/*")
    
    server.start()
    server.join()
  }
}

3. test.jersey.resource : /helloworld に対応するリソース


package test.jersey.resource

import javax.ws.rs.GET
import javax.ws.rs.Produces
import javax.ws.rs.Path

@Path("/helloworld")
class HelloWorldResource {
  @GET
  @Produces(Array("text/plain"))
  def getMessage:String = "Hello, World"
}

4. テスト
Eclipseでtest.jersey.JerseyTest をアプリケーションとして実行させます。


2009-05-03 22:56:18.064::INFO:  Logging to STDERR via org.mortbay.log.StdErrLog
2009-05-03 22:56:18.123::INFO:  jetty-6.1.17
2009-05-03 22:56:18.205::INFO:  Started SocketConnector@0.0.0.0:8080
2009-05-03 22:56:18.226::INFO:  Started SelectChannelConnector@0.0.0.0:55736

次いでアクセス


% telnet localhost 8080
Trying 127.0.0.1...
Connected to localhost.
Escape character is '^]'.
GET /helloworld HTTP/1.0

HTTP/1.1 200 OK
Content-Type: text/plain
Server: Jetty(6.1.17)

Hello, WorldConnection closed by foreign host.
%


2009/05/03 22:57:08 com.sun.jersey.api.core.PackagesResourceConfig init
情報: Scanning for root resource and provider classes in the packages:
  test.jersey.resource
2009/05/03 22:57:08 com.sun.jersey.api.core.PackagesResourceConfig init
情報: Root resource classes found:
  class test.jersey.resource.HelloWorldResource
2009/05/03 22:57:08 com.sun.jersey.api.core.PackagesResourceConfig init
情報: Provider classes found:

[Scala] Scala Servlet with Jetty6

2009-05-03T02:21:00.003+09:00

Jetty + ScalaでServletを書いてみました。

1. Projectの作成
Eclipseで普通にScala Projectを作ります。
ScalaServletという名前のScala Projectを作りました。

2. Jetty6 の入手
JettyのサイトからJetty6を入手します。私がダウンロードしたのはJetty 6.1.17でした。
zipを解凍し、jetty-6.1.17.jar, jetty-util-6.1.17.jar, servlet-api-2.5-20081211.jar をプロジェクトにimportします。

3. ソースを書く
パッケージtest.jettyを作って、下記の様なJettyTest.scalaというファイルを作成します


package test.jetty

import javax.servlet.ServletException
import javax.servlet.http.HttpServlet
import javax.servlet.http.HttpServletRequest
import javax.servlet.http.HttpServletResponse

import org.mortbay.jetty.Server
import org.mortbay.jetty.nio.SelectChannelConnector
import org.mortbay.jetty.servlet.ServletHandler

object JettyTest {

  def main(args: Array[String]) {
    val server = new Server(8080)
    val connector = new SelectChannelConnector()
    server.addConnector(connector)
    
    val handler = new ServletHandler()
    handler.addServletWithMapping(HelloServlet.getClass, "/")
    server.addHandler(handler)
  
    server.start()
    server.join()
  }
}

object HelloServlet extends HttpServlet {
  override def doGet(req:HttpServletRequest, resp:HttpServletResponse) {
    val out = resp.getWriter
    resp.setContentType("text/html")
    out.println("<html><body>Hello, World!</body></html>")
  }
}

4.サーバ起動
上記のJettyTest.scalaを普通にScala Applicationとして起動します。
コンソールに下記の様に表示されます。


2009-05-03 02:20:29.316::INFO:  Logging to STDERR via org.mortbay.log.StdErrLog
2009-05-03 02:20:29.358::INFO:  jetty-6.1.17
2009-05-03 02:20:29.392::INFO:  Started SocketConnector@0.0.0.0:8080
2009-05-03 02:20:29.413::INFO:  Started SelectChannelConnector@0.0.0.0:52134

5.アクセス
ブラウザからhttp://localhost:8080/で確認してもOKですがコンソールから確認。


% telnet localhost 8080
Trying ::1...
telnet: connect to address ::1: Connection refused
Trying fe80::1...
telnet: connect to address fe80::1: Connection refused
Trying 127.0.0.1...
Connected to localhost.
Escape character is '^]'.
GET / HTTP/1.0

HTTP/1.1 200 OK
Content-Type: text/html; charset=iso-8859-1
Content-Length: 40
Server: Jetty(6.1.17)

<html><body>Hello, World!</body></html>
Connection closed by foreign host.
%

[Event] Type-Level Programming Meeting

2009-04-18T22:28:00.004+09:00

型レベルプログラミングの会

定員がすぐいっぱいになってしまって会場参加は出来ず、自宅からustreamで拝聴。
発表された皆さん、どれも興味深い話でした。ありがとうございます。

Scala : Scalaの型プログラミングの話は前にも聞かせて頂いたような気がするけど、更に話題が広がっていたような。

C++ : 定番ではありながら、私はC++は経験が少ないので興味深く聞けました。

Haskell : フォロー出来ない話も多かったですが勉強になりました。勉強すべき事、多いなぁ。

D : 型プログラミングの為のような言語ですね。興味深い。

依存型プログラミング : プレゼン資料が大変面白いというか芸達者というか。April Foolの予告のGirardの逆理の話では無かった。

G'Caml : 存在を始めて知りました。OCaml関係も色々あるなぁ。

この手の勉強会に参加すると、今まで知らなかったことがいっぱいあると判り、もっと勉強しなくちゃ、と思う。
日々の仕事は非技術的な作業ばかりが増えているので、知的好奇心の刺激の為にもこの手の勉強会に積極的に参加しないと。

[Coq] Coq'Art Chap.2

2009-04-05T19:00:00.001+09:00

Interactive Theorem Proving and Program Development; Coq'Art: The Calculus of Inductive Constructions の Chapter 2 です。

この章では概ね次の４つが語られているように見えます。

(1) Coq のコマンド

下記の様なコマンドがあります。

★Require Import library.
ライブラリをロードして environment に追加する。
libraryとしては、Arith, ZArith, Boolなどがある。

★Open Scope scope名.
Scope は notation を interprete する規則。例えばZ_scopeを指定すると各種演算子記号が Z の演算のものと判断される。

★Print Scope scope名.
Scopeで定義された notation の一覧を得る。

★Check term.
termのtypeを表示させる。

★Parameter t:A.
t:Aを environment に追加する。environmentはglobalなもの。

★Section id.

...

　End id.
localなblockを作る。

★Variable t:A.
t:Aを context に追加する。contextはlocal。なので、Section...Endの範囲内で有効。

(2) Inference Rules

様々な推論規則があります。


    (x,A)∈E∪Γ
Var ------------    x:identifier
    E,Γ |- x:A

 E,Γ|- e_1:A->B  E,Γ|- e_2:A
App ------------------------------  関数適用
    E,Γ|- e_1 e_2:B
 
  E,Γ|- e:A_1 -> A_2 -> ... -> A_n -> B   E,Γ|- e_i:A_i (i=1,...,n) 
App* -------------------------------------------------------------------
     E,Γ|- e e_1 ... e_n:B
 
 E,Γ|- t_1:A  E,Γ::(v:=t_1) |- t_2:B
Lam --------------------------------------  λ式
    E,Γ|- fun v:A => e:A->B
 
    E,Γ|- t_1:A  E,Γ::(v:=t_1) |- t_2:B
Let-in --------------------------------------  let
       E,Γ|- let v:=t_1 in t_2:B
    
      E,Γ|- A:Set  E,Γ|- B:Set
Prod-Set --------------------------
         E,Γ|- A->B:Set

  E,Γ|- t:A  E,Γ|- A ≦_{beta delta iota zeta} B
Conv --------------------------
     E,Γ|- t:B

(3) Eval

★cvb : call-by-value (cbvでなくlazyで遅延評価)

★delta-reduction : t ==> t{v/t'}。tのidentifier vをその定義t'で置換。

★beta-reduction : (fun v:T => e_1) e2 ==> e_1{v/e_2}。λ式を簡約。

★zeta-reduction : let v := e_1 in e_2 ==> e_2{v/e_1}。letを簡約。

★iota-reduction : 帰納的な処理で詳しくはChap.6でということで後回し。nat,Zは帰納的な定義なので計算する時はiota-reductionが必須。

★compute = cvb iota beta zeta delta の略

★Eval compute in (....). : ...を実際に計算する。

Reductionに関する性質

strong normalization : reductionはfinite
confluence : t |> t_1, t |> t_2 ならば、あるt_3があって、t_1 |> t_3 かつ t_2 |> t_3。

(4) Universe

typeもtermだとすると、typeのtypeがあるはず。それをsortという。
CoqではSetというデフォルトのsortが定義されている。
更にその上の無限の階層まで考えるようだが、CoqではType(i)は全部ひっくるめてTypeにしてしまう様子。


Level 0 : 具体的な項とか関数。O, S, trinomial,...
Level 1 : データの型。nat, nat->nat, ...
Level 2 : ソート。Set
Level 3 : Type(0)
   :

[Coq] Coq'Art Reading in Tokyo ?

2009-03-29T21:48:00.002+09:00

ところで東京近辺でSpringerのCoq本Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructionsに興味のある人っています？
何人かいるようならば読書会でもとか思うのですが。なお、私は素人で型理論の専門家とかではありません。なので他人に教える程の知識は無く、一緒に勉強する感じになってしまいますが。
逆に既に本を読んでいるとかで、私が参加しても構わないグループとかありましたら声をかけて下さい。

[Coq] Coq'Art Chap.1

2009-03-29T21:08:00.004+09:00

Interactive Theorem Proving and Program Development; Coq'Art: The Calculus of Inductive Constructionsを読み始める事にしました。

Chap.1ではinsertion sortを例にしてCoqの解説が行われています。そこで、Appendixのinsertion sortのコードをCoqIdeに入力してみました。実際に証明が自分で出来る様になるのは将来の課題として、とりあえずCoqでの開発の流れを追ってみます。
なお証明自体はinsertionv8.vにあります。

まず、list Zがソートされた状態を定義するsorted : list Z -> Propを定義します。こんな感じです。


Inductive sorted : list Z -> Prop :=
  | sorted0 : sorted nil
  | sorted1 : forall z:Z, sorted (z :: nil)
  | sorted2 : forall (z1 z2:Z) (l:list Z), 
       z1 <= z2 -> sorted (z2 :: l) -> sorted (z1 :: z2 :: l).

sortedは定義なのでこれ自体は証明の対象ではありません。

これを用いて、


Theorem sorted_inv : 
  forall (z:Z) (l:list Z), sorted (z :: l) -> sorted l.

を証明します。

次いで、並べ替えであることを示すequivを定義します。まず、リストのなかの出現数を示す


Fixpoint nb_occ (z:Z) (l:list Z) {struct l} : nat :=
  match l with
  | nil => 0%nat
  | (z' :: l') =>
      match Z_eq_dec z z' with
      | left _ => S (nb_occ z l')
      | right _ => nb_occ z l'
      end
  end.

を定義します。このnb_occは定義なので証明しません。

これを使って、


Definition equiv (l l':list Z) := forall z:Z, nb_occ z l = nb_occ z l'

を定義します。これ自体も証明しません。

nb_occ, equivの定義から、下記の補題を証明します。


Lemma equiv_refl : 
  forall l:list Z, equiv l l.
Lemma equiv_sym : 
  forall l l':list Z, equiv l l' -> equiv l' l.
Lemma equiv_trans : 
  forall l l' l'':list Z, equiv l l' -> equiv l' l'' -> equiv l l''.
Lemma equiv_cons : 
  forall (z:Z) (l l':list Z), equiv l l' -> equiv (z :: l) (z :: l').
Lemma equiv_perm : 
  forall (a b:Z) (l l':list Z), equiv l l' -> equiv (a :: b :: l) (b :: a :: l').

次いで、実際にinsertion sortを行う関数aux : Z -> list Z -> list Zを定義します。


Fixpoint aux (z:Z) (l:list Z) {struct l} : list Z :=
  match l with
  | nil => z :: nil
  | cons a l' =>
      match Z_le_gt_dec z a with
      | left _ =>  z :: a :: l'
      | right _ => a :: (aux z l')
      end
  end.

auxがinsertion sortの性質を持っている事を示す補題、つまりauxの結果がequivであること、sortedであることを証明します。


Lemma aux_equiv : 
  forall (l:list Z) (x:Z), equiv (x :: l) (aux x l).
Lemma aux_sorted : 
  forall (l:list Z) (x:Z), sorted l -> sorted (aux x l).

最後に、sort:list Z -> list Zを定義というか、sortされた出力の存在を証明します。


Definition sort :　forall l:list Z, {l' : list Z | equiv l l' /\ sorted l'}.

証明を追いきれてないのですが、どうもexists (aux a l')の様に、実例を示して存在を証明するみたいにauxを使っているようです。

----

sorted, nb_occ, equivは定義なので証明の対象ではありません。
aux, sortは成果物として得る、証明済みのプログラムです。sortを満たす具体的なl'の値としてauxを使った式を与えます。その値がl'の条件を満たす事はaux_equiv, aux_sortedから保証されます。

一般的に

仕様を表す様な述語(X -> Prop)を書く。仕様に関する補題も証明しておく。
解を与える様な関数を書く。
その関数の出力が仕様を満たす事を証明する。

とかすれば良い様に見えます。

----

ある程度、この本を読み終わった後で、またこのプログラムを振り返ってみたいと思います。

[Haskell][RWH] Chapter 1

2008-12-27T15:34:00.004+09:00

RWHのChapter 1を読む。

not equalは!=ではなく/=。

temporary definitionをletで。例えば、ghci> let e = exp 1とか。

ghci> :info []とかすれば、[]の情報が調べられる。

ghci> :set +tで型情報を表示する。解除は:unset +t。:type itでunsetしても簡単に調べられる。

itで前の計算結果を参照出来る。

簡単にHaskellのプログラムを書くにはinteractを使えば良いらしい。
main = interact f 但し、fはString -> Stringな関数。これで標準入力から読んで標準出力に書けば良い。


% cat WC.hs
main = interact wordCount
    where wordCount input = show (length (lines input)) + "\n"
%

Prelude> :info interact
interact :: (String -> String) -> IO ()  -- Defined in System.IO

実行は
% runghc WC.hs < quux.txt

Exerciseはとりあえずこんな感じ？


main = interact wordCount
    where wordCount input = numLines input ++ "\t" ++ numWords input ++ "\t" ++ numChars input ++ "\n"
          numLines input = show (length (lines input))
          numWords input = show (length (words input))
          numChars input = show (length input)

[Scala] map and flatMap on scala.Function1

2008-12-04T23:07:00.003+09:00

scala.Function1 lacking @ λ Tony’s blog λ

Scalaの関数の型の scala.Function1 にもっと便利な機能を、という話。
mapはともかくflatMapをこうやって定義するのか、というのはなんか勉強になったので、メモ代わりに。
同様に S combinator というのも自分ではなんか巧く使えないものなので参考になるなぁ、と。on は普通に便利かも。