coq2scalaをさわってみた

http://proofcafe.org/wiki/Coq2Scala を試してみました。

インストールはhgでソースコードとってきて、
./configure
make world
make install
でおｋ。

Extraction Language Scala. が使えちゃうCoqがインストールされます。

使ってみた

とりあえず自然数と足し算を定義してみます。

	Extraction Language Scala.
	Module ScalaTest.
	Inductive Nat := Zero | Succ : Nat -> Nat.
	Fixpoint nplus n m :=
	match n with
	| Zero => m
	| Succ n' => Succ (nplus n' m)
	end.
	Notation "n + m" := (nplus n m).
	End ScalaTest.
	Extraction "coq.scala" ScalaTest.

view raw scala.v hosted with ❤ by GitHub

吐き出されたScalaのコード。

	object CoqMain {
	object CoqModule {
	sealed abstract class Nat
	case class Zero() extends Nat
	case class Succ(x1: Nat) extends Nat
	def nat_rect[A] : (A => ((Nat => (A => A)) => (Nat => A))) = {
	(f:A) => (f0:(Nat => (A => A))) => (n:Nat) =>
	n match {
	case Zero() => f
	case Succ(n0) => f0(n0)(nat_rect(f)(f0)(n0))
	}
	}
	def nat_rec[A] : (A => ((Nat => (A => A)) => (Nat => A))) = {
	(f:A) => (f0:(Nat => (A => A))) => (n:Nat) =>
	n match {
	case Zero() => f
	case Succ(n0) => f0(n0)(nat_rec(f)(f0)(n0))
	}
	}
	def nplus : (Nat => (Nat => Nat)) = {
	(n:Nat) => (m:Nat) =>
	n match {
	case Zero() => m
	case Succ(n$prime) => Succ(nplus(n$prime)(m))
	}
	}
	}
	}

view raw coq.scala hosted with ❤ by GitHub

Notationは無視される？
パラメータとらない場合はcase object使って欲しいかも・・・・
あとインデントも付くとうれしい。

ClassとInstanceを使ってみる

Monoidを定義してみた。

私はtraitとimplicit parameterでかっこ良く変換されるのかな！？と期待。

	Class Monoid (M : Type) := {
	plus : M -> M -> M;
	zero : M
	}.
	Instance NMonid : Monoid Nat := {
	plus := nplus;
	zero := Zero
	}.

view raw monoid.v hosted with ❤ by GitHub

結果は・・・・・

	sealed abstract class Monoid[M]
	case class Build_Monoid[M](x1: (M => (M => M)), x2: M) extends Monoid[M]
	def monoid_rect[A, B] : (((A => (A => A)) => (A => B)) => (Monoid[A] => B)) = {
	(f:((A => (A => A)) => (A => B))) => (m:Monoid[A]) =>
	m match {
	case Build_Monoid(x, x0) => f(x)(x0)
	}
	}
	def monoid_rec[A, B] : (((A => (A => A)) => (A => B)) => (Monoid[A] => B)) = {
	(f:((A => (A => A)) => (A => B))) => (m:Monoid[A]) =>
	m match {
	case Build_Monoid(x, x0) => f(x)(x0)
	}
	}
	def plus[A] : (Monoid[A] => (A => (A => A))) = {
	(monoid:Monoid[A]) =>
	monoid match {
	case Build_Monoid(plus0, zero0) => plus0
	}
	}
	def zero[A] : (Monoid[A] => A) = {
	(monoid:Monoid[A]) =>
	monoid match {
	case Build_Monoid(plus0, zero0) => zero0
	}
	}
	def nMonid : Monoid[Nat] = Build_Monoid(nplus, Zero())

view raw monoid.scala hosted with ❤ by GitHub

(´・ω・｀)ｼｮﾎﾞｰﾝ
明示的にインスタンスを渡して関数を得る感じですね。
まぁ、まだまだ開発途中なのでこれからどうなるかはわかりません。

最後に証明付きコード

	Extraction Language Scala.
	Module ScalaTest.
	Inductive Nat := Zero | Succ : Nat -> Nat.
	Fixpoint nplus n m :=
	match n with
	| Zero => m
	| Succ n' => Succ (nplus n' m)
	end.
	Notation "n + m" := (nplus n m).
	Lemma nplus_assoc : forall a b c, a + (b + c) = (a + b) + c.
	intros.
	induction a.
	reflexivity.
	simpl.
	rewrite IHa.
	reflexivity.
	Qed.
	Lemma nplus_zero : forall n, n = n + Zero.
	intros.
	induction n.
	reflexivity.
	simpl.
	rewrite <- IHn.
	reflexivity.
	Qed.
	Lemma nplus_succ : forall n m, Succ (n + m) = n + (Succ m).
	intros.
	induction n.
	reflexivity.
	simpl.
	rewrite IHn.
	reflexivity.
	Qed.
	Lemma nplus_comm : forall n m, n + m = m + n.
	intros.
	induction n.
	apply nplus_zero.
	simpl.
	rewrite IHn.
	apply nplus_succ.
	Qed.
	Fixpoint nmult n m :=
	match n with
	| Zero => Zero
	| Succ n' => nplus m (nmult n' m)
	end.
	Notation "n * m" := (nmult n m).
	Lemma distr : forall a b c, a * c + b * c = (a + b) * c.
	intros.
	induction a.
	reflexivity.
	simpl.
	rewrite <- IHa.
	rewrite nplus_assoc.
	reflexivity.
	Qed.
	Lemma nmult_assoc : forall a b c, a * (b * c) = (a * b) * c.
	intros.
	induction a.
	reflexivity.
	simpl.
	rewrite IHa.
	apply distr.
	Qed.
	Lemma nmult_zero : forall n, Zero = n * Zero.
	intros.
	induction n.
	reflexivity.
	simpl.
	apply IHn.
	Qed.
	Lemma nmult_succ : forall n m, n + n * m = n * Succ m.
	intros.
	induction n.
	reflexivity.
	simpl.
	rewrite <- IHn.
	rewrite nplus_assoc.
	rewrite nplus_assoc.
	replace (n + m) with (m + n).
	reflexivity.
	apply nplus_comm.
	Qed.
	Lemma nmult_comm : forall n m, n * m = m * n.
	intros.
	induction n.
	apply nmult_zero.
	simpl.
	rewrite IHn.
	apply nmult_succ.
	Qed.
	Class Monoid (M : Type) := {
	plus : M -> M -> M;
	zero : M;
	id : forall m, plus m zero = m
	}.
	Instance NMonid : Monoid Nat := {
	plus := nplus;
	zero := Zero
	}.
	intros.
	induction m.
	reflexivity.
	simpl.
	rewrite <- nplus_zero.
	reflexivity.
	Qed.
	Eval compute in zero.
	End ScalaTest.
	Extraction "test.scala" ScalaTest.

view raw coq2scala.v hosted with ❤ by GitHub

	object CoqMain {
	object CoqModule {
	sealed abstract class Nat
	case class Zero() extends Nat
	case class Succ(x1: Nat) extends Nat
	def nat_rect[A] : (A => ((Nat => (A => A)) => (Nat => A))) = {
	(f:A) => (f0:(Nat => (A => A))) => (n:Nat) =>
	n match {
	case Zero() => f
	case Succ(n0) => f0(n0)(nat_rect(f)(f0)(n0))
	}
	}
	def nat_rec[A] : (A => ((Nat => (A => A)) => (Nat => A))) = {
	(f:A) => (f0:(Nat => (A => A))) => (n:Nat) =>
	n match {
	case Zero() => f
	case Succ(n0) => f0(n0)(nat_rec(f)(f0)(n0))
	}
	}
	def nplus : (Nat => (Nat => Nat)) = {
	(n:Nat) => (m:Nat) =>
	n match {
	case Zero() => m
	case Succ(n$prime) => Succ(nplus(n$prime)(m))
	}
	}
	def nmult : (Nat => (Nat => Nat)) = {
	(n:Nat) => (m:Nat) =>
	n match {
	case Zero() => Zero()
	case Succ(n$prime) => nplus(m)(nmult(n$prime)(m))
	}
	}
	sealed abstract class Monoid[M]
	case class Build_Monoid[M](x1: (M => (M => M)), x2: M) extends Monoid[M]
	def monoid_rect[A, B] : (((A => (A => A)) => (A => (Unit => B))) => (Monoid[A] => B)) = {
	(f:((A => (A => A)) => (A => (Unit => B)))) => (m:Monoid[A]) =>
	m match {
	case Build_Monoid(x, x0) => f(x)(x0)(())
	}
	}
	def monoid_rec[A, B] : (((A => (A => A)) => (A => (Unit => B))) => (Monoid[A] => B)) = {
	(f:((A => (A => A)) => (A => (Unit => B)))) => (m:Monoid[A]) =>
	m match {
	case Build_Monoid(x, x0) => f(x)(x0)(())
	}
	}
	def plus[A] : (Monoid[A] => (A => (A => A))) = {
	(monoid:Monoid[A]) =>
	monoid match {
	case Build_Monoid(plus0, zero0) => plus0
	}
	}
	def zero[A] : (Monoid[A] => A) = {
	(monoid:Monoid[A]) =>
	monoid match {
	case Build_Monoid(plus0, zero0) => zero0
	}
	}
	def nMonid : Monoid[Nat] = Build_Monoid(nplus, Zero())
	}
	}

view raw coq2scala.scala hosted with ❤ by GitHub

proof-editing mode楽しいです。
ScalaでPDDの時代が来るかもですね。

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、おもしろいですよ！