[Coq] FoCaLize Tutorial (1)

　形式手法開発ツールの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 ;;

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