Verified Programming in GURU

http://code.google.com/p/guru-lang/
Coqに強く影響を受けたとかいう、Guruという言語があります。
JVM上で動く、証明機能付きの関数型言語です。

こまかいことはともかく、"Verified Programming in GURU"(http://guru-lang.googlecode.com/svn/branches/1.0/doc/book.pdf)
の演習3をやってみます。

Include "../usr/guru-lang/lib/plus.g".
Include "../usr/guru-lang/lib/mult.g".
Include "../usr/guru-lang/lib/bool.g".

Define 3_8_1_1 := join (mult zero three) zero.
Classify 3_8_1_1.
Define 3_8_1_2 := join (lt zero three) tt.
Classify 3_8_1_2.
Define 3_8_1_3 := join (le one three) tt.
Classify 3_8_1_3.
Define 3_8_2 : Forall(x:nat). { (mult Z x) = Z } :=
  foralli(x:nat).
    join (mult Z x) Z.
Classify 3_8_2.
Define 3_8_3 : Forall(x:nat)(y:nat). { (lt Z (plus (S x) y)) = tt } :=
  foralli(x:nat)(y:nat).
    join (lt Z (plus (S x) y)) tt.
Classify 3_8_3.
Define 3_8_4 : Forall(x:bool). { (and ff x) = ff } :=
  foralli(x:bool).
    join (and ff x) ff.
Classify 3_8_4.
Define 3_8_5 : Forall(x:bool). { (and x x) = x } :=
  foralli(x:bool).
    case x with
      ff => trans cong (and * *) x_eq
            trans join (and ff ff) ff
                  symm x_eq
    | tt => trans cong (and * *) x_eq
            trans join (and tt tt) tt
                  symm x_eq
    end.
Classify 3_8_5.

join P1 P2:はP1,P2が同じnormal form（これ以上評価できない形式）を持つことを証明する。
foralliは、変数に対する帰納法かな。
caseは場合分け証明。
refl t:は{t=t}になってることを証明する。
symm P:は命題Pが{t1=t2}の時、{t2=t1}を証明する。
trans P1 P2:はP1が{t1=t2},P2が{t2=t3}の時、{t1=t3}を証明する。
cong t* P:はPが{t1=t2}の証明の時、{ t t1 = t t2 }を証明する。

うーむ、Coqの様に対話環境はないのか。だけど、考え方はわかりやすいと思う。