[Coq] FoCaLize Tutorial (2)

　[Coq] FoCaLize Tutorial (2)の続き。

　前回のextsubset.fclに

  theorem incl_remove_mem : all s : Self, all v : Val,
                            ~(v << s) -> s <: s - v
    proof = by property mem_congr, mem_remove, mem_incl ;

を追加すると自動証明が失敗するのでFoCaLizeの手動証明を試す予定なのだが...自動証明がそのまま通るみたいだ。

　が、ここは一応Tutorial通り、手動証明も試してみる事にする、証明を下記の様に直してみる。

    proof = <1>1 assume s : Self, v : Val, hypothesis Hv : ~(v << s),
                 prove s <: s - v
              <2>1 assume w : Val, hypothesis Hw : w << s,
                   prove w << s - v
                <3>1 prove ~(Val!( = )(w, v)) /\ w << s
                  <4>1 prove ~(Val!( = )(w, v))
                       by property mem_congr hypothesis Hv, Hw
                  <4>2 prove w << s
                       by hypothesis Hw
                  <4>f conclude
                <3>f qed by property mem_remove step <3>1
              <2>f qed by property mem_incl step <2>1
            <1>f conclude ;

再度コンパイルするとこれでも通る。上記の様に手で証明を記述しても生成されたCoqの証明は短く分割されて読みやすくはなるもののやはり人間向けの証明とは言えない感じである。

証明に通らない例として

  theorem remove_insert : all s : Self, all v : Val,
                          v << s -> s = (s - v) + v
    proof = <1>1 assume s : Self, v : Val, hypothesis Hv : v << s,
                 prove s = (s - v) + v
              <2>1 assume w : Val, hypothesis Hw : w << s,
                   prove w << (s - v) + v
                   by property mem_insert, mem_remove
              <2>2 assume w : Val, hypothesis Hw : w << (s - v) + v,
                   prove w << s
                   by property mem_insert, mem_remove, mem_congr, Val!diff_eq
              <2>f qed by property eq_incl, mem_incl step <2>1, <2>2
            <1>f conclude ;

を試すと下記の様にエラーが出る。

% ~/pkg/bin/focalizec extsubset.fcl
Invoking ocamlc...
>> /Users/miyamoto/pkg/focalize-0.6.0/bin/ocamlc -I /Users/miyamoto/pkg/lib/focalizec-0.6.0 -c extsubset.ml
Invoking zvtov...
>> /Users/miyamoto/pkg/focalize-0.6.0/bin/zvtov -zenon /Users/miyamoto/pkg/focalize-0.6.0/bin/zenon -new extsubset.zv
File "extsubset.fcl", line 61, characters 19-53:                
Zenon error: could not find a proof within the memory size limit
### proof failed
%

これについてもチュートリアルに従い証明を完全に記述するとコンパイルに通る。

　なんとなくCoqに慣れてしまったので、FoCaLizeを用いて証明を記述する方が寧ろ判りにくいようにも思う。

[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 ;;

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