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の時代が来るかもですね。