[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を用いて証明を記述する方が寧ろ判りにくいようにも思う。