[Coq] How to define complex inductions

Coq の証明の書き方パターンを yoshihiro503 さんに教わったので、忘れないうちに。

自然数に関する定理を証明したい場合に、下記の様な補題が欲しかったとします。

Lemma nat2_ind : forall P:nat -> Prop, P 0 -> P 1 ->
  (forall n:nat, P n -> P (S n) -> P (S (S n))) ->
  (forall n:nat, P n).

教わったコードを元に自分なりに書いてみたのが下記の証明です。

  
  ============================
   forall P : nat -> Prop,
   P 0 ->
   P 1 ->
   (forall n : nat, P n -> P (S n) -> P (S (S n))) -> forall n : nat, P n

nat2_ind < intros P H0 H1 IH.          
1 subgoal
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ============================
   forall n : nat, P n

nat2_ind < refine (fix ll n : P n := _).     (* ここで refine を使って ll を定義するのがポイント *)
1 subgoal
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  n : nat
  ============================
   P n

(* しかしここで apply ll しても駄目。llはIHの仮定のところで使う *)

nat2_ind < induction n.
2 subgoals
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  ============================
   P 0

subgoal 2 is:
 P (S n)

nat2_ind < exact H0.  (* n=0 のケースは P 0 *)
1 subgoal
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  n : nat
  IHn : P n
  ============================
   P (S n)

nat2_ind < induction n.
2 subgoals
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  IHn : P 0
  ============================
   P 1

subgoal 2 is:
 P (S (S n))

nat2_ind < exact H1.  (* n=1 のケース *)
1 subgoal
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  n : nat
  IHn : P (S n)
  IHn0 : P n -> P (S n)
  ============================
   P (S (S n))

nat2_ind < apply IH.   (* IH を使う *)
2 subgoals
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  n : nat
  IHn : P (S n)
  IHn0 : P n -> P (S n)
  ============================
   P n

subgoal 2 is:
 P (S n)

nat2_ind < apply ll.  (* IHの仮定のところにはll を使ってOK *)
1 subgoal
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  n : nat
  IHn : P (S n)
  IHn0 : P n -> P (S n)
  ============================
   P (S n)

nat2_ind < apply IHn0.          
1 subgoal
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  n : nat
  IHn : P (S n)
  IHn0 : P n -> P (S n)
  ============================
   P n

nat2_ind < apply ll.  (* もう一度 ll を使う *)
Proof completed.

nat2_ind < Qed.

そもそもの証明のゴールをrefineを使ってllとして定義して、証明の中でllを使っているので非常に不思議なのですが、変な所（例えばrefine直後に）でapply llしてProof CompleteしてもQedしたとたんにエラーになります。エラーが出ない様にH0,H1,IHを使えば、証明が正しい事になります。

なお、同じ定理を短く書くとkikxさんの証明ゴルフみたいになるようです。すごい。

[Coq] Arithmetic in Coq : N

Nは二進数で表現された自然数の型です。

Require Import NArith.すると使用出来ます。型の定義は下記の様です。

Inductive N : Set :=  N0 : N | Npos : positive -> N

positiveは下記の様に定義されています。

Inductive positive : Set :=
    xI : positive -> positive | xO : positive -> positive | xH : positive

こんな感じで正の数を表現しています。xHが最上位ビットで、xIが x -> 2x+1, xOが x -> 2x ということです。

Coq < Check (xO (xI (xO xH))).
10%positive : positive

これは(1~0~1~0)%positive.とも書けます。

natとの変換は下記で可能。

nat_of_N : N -> nat
N_of_nat : nat -> N

演算子は

Ndouble_plus_one, Ndouble : N -> N
Nsucc, Npred : N -> N
Nplus, Nminus, Nmult : N -> N -> N　。+, -, * もあり。
Ncompare : N -> N -> comparison 。Infixで ?=
  comparisonは、
  Inductive comparison : Set :=
    Eq : comparison | Lt : comparison | Gt : comparison
Nlt, Ngt, Nle, Nge : N -> N -> Prop　。Infix で <, <=, >, >=
Nmin, Nmax : N -> N -> N
Ndiv2 : N -> N

Nに関する帰納法は次の２つの好きな方を使える。Nrectを用いてNindもある。

N_ind_double
     : forall (a : N) (P : N -> Prop),
       P 0%N ->
       (forall a0 : N, P a0 -> P (Ndouble a0)) ->
       (forall a0 : N, P a0 -> P (Ndouble_plus_one a0)) -> P a
Nrect
     : forall P : N -> Type,
       P 0%N -> (forall n : N, P n -> P (Nsucc n)) -> forall n : N, P n

Require Import ZArith.ZOdiv.すれば、

Ndiv_eucl : N -> N -> N * N
Ndiv : N -> N -> N
Nmod : N -> N -> N
Theorem Ndiv_eucl_correct: forall a b,
  let (q,r) := Ndiv_eucl a b in a = (q * b + r)%N.

と除算も使える。

---
追記
ZArith.ZOdivと、ZArithの中でImportしてるZArith.Zdivとは互換性無いのだな。
ZArithを使わないことはまず無いので、ZOdivは使わないほうがよさそう。

[Coq] Arithmetic in Coq : nat

Coqで大きな自然数あるいは整数を使いたくなったので調べてみました。

★nat

　Coqで自然数というと基本はnatです。natというと自分で作る物であるかの様な気すらしますが勿論標準で備わっています。
　natを使う場合Require Import Arith.すると標準ライブラリが使えます。

●基本
Init.Peanoの中で、pred, plus, mult, le, lt, ge, gtが定義されていてImport不要で使える。

●大小比較関係

- eq_nat : nat -> nat -> Prop
-- heorem eq_nat_decide : forall n m, {eq_nat n m} + {~ eq_nat n m}. が使える
- lt_eq_lt_dec n m : {n < m} + {n = m} + {m < n}. こんな感じで使う
Definition nat_compare (n m:nat) :=
  match lt_eq_lt_dec n m with 
    | inleft (left _) => Lt
    | inleft (right _) => Eq
    | inright _ => Gt
  end.
-- le_lt_dec n m : {n <= m} + {m < n}. など

●四則演算

- 末尾再帰なtail_plusというのもある
- minus : nat -> nat -> nat. n - m とかも書ける。結果が負になる場合もOを返す。
- min, max : nat -> nat -> nat.
- div2, double : nat -> nat.
- 除算は無いが、Require Import Arith.Euclid. すれば商と剰余には下記がある
-- quotient : forall n, n > 0 ->
    forall m:nat, {q : nat | exists r : nat, m = q * n + r /\ n > r}.
-- modulo : forall n, n > 0 ->
    forall m:nat, {r : nat | exists q : nat, m = q * n + r /\ n > r}.

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

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

[Coq] ASN.1 Library is under construction

　この連休にCoqの練習がてら作っていたASN.1のライブラリで、全然完成してないのだがとりあえず出来たところまで公開。
　Coqdocで生成したドキュメントがTLV.htmlです。（コードが成長したら随時更新予定）

　ASN.1が何かについては、A Layman's Guide to a Subset of ASN.1, BER, and DERあたりを読んで下さい。電子証明書とかで使っているバイナリフォーマットなので、証明付きのライブラリを作りたいのだ。

　本当は

Inductive tlv_value : Set := 
| Primitive : string -> tlv_value 
| Structured : list tlv -> tlv_value
.

みたいに定義したかったのだが、そうするとtlv_value, tlv に関する帰納法をうまく構成出来なかった。まだCPDT Chapter 3の読み込みが足りないのだろうなぁ。
　が、とりあえず幾つかの定理も証明できたし、出だしとしてはこんなものかもとも思う。

　Coqを勉強しようと思う様なプログラマの人は、ある程度複雑な型（相互再帰的だったり再帰がネストしていたり）を定義出来ると思うが、Coqは帰納型に対して帰納法を与える関数が作れないと駄目で、しかしそこが実は難しい、というのがこの連休に得た知見だ。

[Coq] How to use Record

　Coq で Record を使う方法を調べました。基本的には記述を簡単にする構文糖のようです。これを使うと、事前条件を満たす証明を要求するコンストラクタを簡単に書けます。
　使い方は下記の例を見てもらうのが簡単でしょう。

　まず正の有理数を表すRat型を作りたいと考えます。符号は無視するとして、分母が０で無いことを保証したい、分子分母が既約である事を保証したい、とします。こんな感じに書けます。

Record Rat : Set := mkRat {
  numer : nat;
  denom : nat;
  denom_not_zero : denom <> O;
  irreducible : forall g n d:nat, 
    (mult g n)=numer /\ (mult g d)=denom -> g = S O
}.

Ratで 1/2 を定義したい時はこんな感じになります。まず補題を証明しないと値を作れません。

Lemma two_not_zero : 2 <> 0.
Proof.
  discriminate.
Qed.
Lemma one_two_irred : forall g n d:nat, (mult g n)=1 /\ (mult g d)=2 -> g = S O.
Admitted. (* 証明省略 *)

こうして初めて値を作れます。

Definition half : Rat := mkRat 1 2 two_not_zero one_two_irred.
Print half. (* mkRat 1 2 two_not_zero one_two_irred : Rat *)
Eval compute in (numer half). (* 1 : nat *)
Eval compute in (denom_not_zero half). (* two_not_zero *)

アクセサに見えるnumerなどは単なる関数です、従って同じ名前空間でnumerを他に定義出来ません。

Print numer.
numer = 
fun r : Rat => let (numer, denom, _, _) := r in numer
     : Rat -> nat

Ratに関する帰納法は下記の様になります。

Print Rat_ind.
(* forall P : Rat -> Prop,
       (forall (numer denom : nat) (denom_not_zero : denom <> 0)
          (irreducible : forall g n d : nat,
                         g * n = numer /\ g * d = denom -> g = 1),
        P (mkRat numer denom denom_not_zero irreducible)) ->
       forall r : Rat, P r *)

[Alloy][FM] Sample code: Addressbook

　[Coq][FM] Fomal Methods Forum #4でのAlloyチュートリアルの話。

　まず Alloy4 を各自インストールしておくのは前提。但し、JARファイル１つなので、JRE (Java5以上) が入っているコンピュータならば起動は難しくありません。

　表示されるWindowの左側入力欄に下記を打ち込みます。

sig Name, Addr {}
sig Book {
  addr: Name -> lone Addr
}

　sigというのは普通のOO言語のクラス定義の様なもの --- なんですが、Alloy はOOなプログラミング言語ではないのでOOとのアナロジーは時に誤解を与えるかも。どちらかというと、RDBMSに Name, Addr という表を作ったと考えるといいかも。実際、Alloy は関係代数に基づいていますし。
　OO でいうところのインスタンスはAlloyではatomと言います。Alloyでインスタンスというのは、全てのatomから構成されるモデル（モデルの中には求める反例とかも含まれます）のことを指します。用語は間違わない様に。
　また、. (ドット演算子) もOO言語の属性やメソッドを指す様に勘違いしますが、join演算子で、RDBのjoinみたいな振る舞いをします。
　Bookのatomを仮に B0, B1 と書くと、Book は {(B0), (B1)} という集合です。（ () はタプル、{}は集合を表す。）

　lone は 0 or 1 個を表す数量限定子です。他にも all (全ての)、some (１個以上)、one (１個)、no (０個) があります。lone Addr は、関数型言語的には Option Addrのようなものです。
　addr は Book の属性みたいに見えますが、これも関数型言語的には addr : Book -> Name -> Option Addr -> Prop みたいに考えると良いです。addr は (Book, Name, Addr) のタプル型の元の集合、例えば{(B0,N0,D0), (B1,N1,D1)}として表現されます。 （関係 R : R x y は (X,Y) の部分集合として表現出来る）
　Book = {(B0),(B1)} であると、ドットはjoin演算子なので（テンソルとかの添字の縮約の如く）ジョイン演算をします。Bookとaddrの共通のB0を見て(B0).(B0,N0,D1)=(N0,D0)の様に計算して、b=B0ならば、b.addr={(N0,D0)}, Book.addr={(N0,D0),(N1,D1)} となります。

　この時点で sig Book {...} の下に

pred show[] {}
run show for 3

と書いて Execute のボタンを押します。
　右側に Instance found と出るので Instance のリンクを押すと、atom 間の関係を示すダイヤグラムが表示されます。nextを押すと別のインスタンスが表示されます。
　for 3 と書いたので各 sig 毎に 3 atom づつです。

　次にモデルの性質をテストする事を考えます。addr を追加して削除すると元に戻る、という性質が成り立つ事をモデル検査で確認（＝反例が見つからない事を確認）します。
　まず追加と削除を表す述語を定義します。述語なので戻り値は真偽値を返します。

pred add[disj b,b':Book, n:Name, a:Addr] {
  b'.addr = b.addr + (n -> a)
}
pred del[disj b,b':Book, n:Name] {
  b'.addr = b.addr - (n -> Addr)
}

　Alloyは手続き型言語ではないので、b'addrに何か破壊的代入が行われる事は無く、単にbとb'の間の関係を示しているだけです。disjはbとb'とが別atomであるという意味です。

　次いでテストしたい性質を書きます。

assert delUndoesAdd {
  all b,b',b'':Book, n:Name, a:Addr |
    add[b,b',n,a] and del[b',b'',n] implies b.addr = b''.addr
}
check delUndoesAdd for 5

　|はsuch thatみたいな意味、and, implisは論理演算の記号です。

　これを追加してexecuteすると「何故か」counterexampleが見つかったと表示されます。counterexampleをじっと眺めると、bとb'が同じBookであることが判ります。
　これは元々 b に (n -> a) が含まれていた場合、b, b' が同じになるからです。（集合に既にある要素を加えても同じ）
　assertの中身を

    no n.(b.addr) and add[b,b',n,a] and del[b',b'',n] implies b.addr = b''.addr

に修正するとconterexampleが無くなります。

[Coq][FM] Fomal Methods Forum #4

　4/29に第4回FormalMethods勉強会を行いました。

　今回は
Alloy
　Alloyの教科書の例題（アドレス帳）を元に文法を勉強しました。大体文法は把握出来たかな。
　あとは自分で使ってみるべきなんだろうが、あまりモデリングとか仕事でやらないしなぁ。とりあえずパズルをAlloyで解く練習をするかなぁ。

CEGAR
　今回はCEGARという手法の話を聞きました。CEGARはCounterExample-Guided Abstraction Refinementの略で、モデル検査における状態数爆発を抑える為の一手法です。
　モデル検査で扱う検査の中に、到達可能性解析（エラー状態などの特定の状態にと到達するか否かの解析）があります。
　状態数を抑える方法としてモデルの抽象化（モデルの粗視化）があります。抽象化によって、エラー状態に遷移する可能性のある状態と、到達しない状態とが同一視されてしまうと、本当はエラー状態に到達しないにも関わらず、エラー状態に達すると誤って判定されます。
　CEGARは、エラー状態に到達する解に対して、解析（最弱事前条件？）を行って抽象化を修正（状態を分割）して再解析する手法です。エラー状態に達した場合にはそれが本当に達したのか、抽象化を改善して再度解析を実施します。
　原理だけ聞くと、当たり前の話と思えるのですが、実際に自動化するところを実装するのは難しそうというか見当が付かない。

Coq
　CoqはCertified Programming with Dependent TypeのChapter 1,2をざっと流して、Chapter 3を3.3まで読み終わりました。
　当日使用した資料 (PPT, Coqファイル) についてはGoogleグループ上の記事にリンクを纏めましたので、そちらから辿って下さい。
　本当はChapter 3を終わりたかったのですが終わらなかったのはちょっと残念でした。