Coqはじめました。

あけましておめでとうございます。

何か新しいことをはじめようと思い、Coqに手を出しました。

まだ慣れていないけど、なかなか楽しいです。

証明楽しいとかどんな変態（褒め言葉）なんだ！

と思っていましたが、私も無事変態の仲間に入ることが出来ました。

Coqをはじめる

Coqを使い始めたきっかけは冬休みの宿題で読書感想文です。

私は選んだ本はもちろん「数学ガール」。

なかなかおもしろいのでオススメです。

数学が得意というわけでもない私は、理解の手助けとしてプログラムを書こうと思いました。

そこでCoqの登場です！

本に出てくる命題を証明していくことにしました。

Coqに関する資料は決して多くありませんが、良いチュートリアルがあるので、まずはこれらを参考にしましょう。

• http://www.iij-ii.co.jp/lab/techdoc/coqt/
• http://www.slideshare.net/tmiya/coq-tutorial

書いてみた

正の整数型を作って加算を定義し、結合法則と交換法則を証明してみました。

	Inductive P : Set :=
	I : P
	| PS : P -> P.
	Fixpoint Padd (n m : P) : P :=
	match n with
	| I => PS m
	| PS n' => PS (Padd n' m)
	end.
	Lemma Padd_assoc : forall (a b c: P), Padd a (Padd b c) = Padd (Padd a b) c.
	Proof.
	intros.
	induction a.
	reflexivity.
	simpl.
	rewrite IHa.
	reflexivity.
	Qed.
	Lemma Padd_comm : forall (n m : P), Padd n m = Padd m n.
	Proof.
	intros.
	assert (Padd I m = Padd m I).
	induction m.
	reflexivity.
	replace (PS m) with (Padd I m).
	rewrite <- Padd_assoc.
	rewrite <- IHm.
	reflexivity.
	reflexivity.
	induction n.
	rewrite H.
	reflexivity.
	replace (PS n) with (Padd I n).
	rewrite Padd_assoc.
	rewrite <- H.
	rewrite <- Padd_assoc.
	rewrite IHn.
	rewrite <- Padd_assoc.
	reflexivity.
	reflexivity.
	Qed.

view raw pos.v hosted with ❤ by GitHub

結合法則はスラスラと書けて、「うはwっwｗ楽勝ｗｗｗ」とほざいていたのですが、交換法則は丸一日かかりました・・・・・

この中で使われているタクティクは

• intros (導入)
• induction (帰納)
• reflexivity (再帰？反射？)
• simpl (簡約)
• rewrite (書き換え)
• assert (表明)
• replace (置換)

だけです。

プログラミングに慣れている人は、こういったタクティクを覚えていくだけで書けるようになると思います。

書いてみて

私はパズルを解くようなものだと感じました。

Qed. が書けたときはとても嬉しいです。

自然数の定義、自然数の加算・比較、整数の定義、ソースコードをみるだけでも勉強になります。

一度は触ってみてはどうでしょう。

Coq、おもしろいですよ！