[Coq][Alloy] Proof of Alloy Example

本日の Formal Methods Forum で扱った Alloy の問題で、

assert union {
  all s:set univ, p,q : univ -> univ |
    s.(p + q) = s.p + s.q
}
check union for 4

で Counterexample が見つからない、従ってこの関係式は正しい、というのを確認する問題があった。
しかし、正しさを確認するには証明が必要であろう。

Coq で集合を扱うライブラリSets.Ensemblesというのもあるがここでは自前で集合演算などを定義して証明してみた。集合 S とは univ -> Prop というmembershipを表す述語であり、二項関係 xRy というのも univ -> univ -> Prop という述語であると言う点に注意すれば、あとは単に定義を述語論理で記述するだけである。

Section Alloy_Ex.

(* univ *)
Variable univ : Set.
(* relation *)
Definition Rel1 := univ -> Prop. (* arity=1 *)
Definition Rel2 := univ -> univ -> Prop. (* arity=2 *)

(* set = Rel1 *)
(* x is an element of s *)
Definition In1 (s:Rel1)(x:univ):Prop := s x.
(* A is a subset of B *)
Definition subset1 (A B:Rel1):Prop :=
 forall x:univ, In1 A x -> In1 B x.
(* A = B iff A includes B and B includes A *)
Definition eq1 (A B:Rel1):Prop :=
 (subset1 A B) /\ (subset1 B A).

(* join operation *)
Definition join12 (s:Rel1)(p:Rel2):Rel1 :=
 fun y:univ => (exists x:univ, In1 s x /\ p x y).

(* union *)
Definition union1 (p q:Rel1):Rel1 :=
 fun x:univ => (p x \/ q x).
Definition union2 (p q:Rel2):Rel2 :=
 fun x:univ => fun y:univ => (p x y \/ q x y).

Theorem alloy_ex_union : forall (s:Rel1)(p q:Rel2),
 eq1 (join12 s (union2 p q)) (union1 (join12 s p) (join12 s q)).
Proof.
intros s p q. unfold eq1. split.
 unfold subset1. intros x H.
 unfold In1 in *. unfold join12 in *.
 destruct H as [x0 [H1 H2]]. unfold union2 in H2.
 unfold union1.
 destruct H2; [left|right]; exists x0; split; auto.
unfold subset1. intros x H.
unfold In1 in *. unfold union1 in H.
unfold join12. unfold union2.
destruct H; unfold join12 in H; destruct H as [x0 [H1 H2]];
exists x0; split; auto.
Qed.

[Coq][Alloy] Properties of Relation

先日のFormal Methods Forum勉強会にて、Alloy本の演習問題を皆で解いた。Alloyとしての課題は、関係 r について各種性質（推移律とか単射とか）を Alloy の関係演算記法で書かれたものについて検討した後に、述語論理っぽく同等の性質を書き下し、同等性を Alloy でチェックする、というものだった。
その課題については kencoba さんの日記に回答が示されている。

同じことを Coq を用いて行ってみた。
Coq では univ を U:Set として現し、その上の関係 univ -> univ は U -> U -> Prop として表現できる。後は、関係に対する join などの演算子を定義すれば、同等性の証明を Coq で確認することが出来る。

証明してみた結果、これらの等価性を示すには U_dec: forall u u':U, {u=u'}+{u<>u'} や、Uが有限集合であることなどの性質を使わなくても等価であることが判る。

Section Alloy1.

(* See "Software Abstraction" Alloy Tutorial *)
(* http://d.hatena.ne.jp/kencoba/20120212 *)

(* univ *)
Parameter U:Set.
(* relation *)
Definition relation := U -> U -> Prop.

Definition JOIN(R S:relation):relation :=
 fun x => (fun z => (exists y:U, R x y /\ S y z)).

Definition INV(R:relation):relation :=
 fun x => (fun y => (R y x)).

Definition IN(R S:relation):Prop :=
 forall x y:U, R x y -> S x y.

Definition IDEN:relation :=
 fun x => (fun y => (x=y)).

Definition AND(R S:relation):relation :=
 fun x => (fun y => R x y /\ S x y).

Definition NO(R:relation):Prop :=
 forall x y, ~(R x y).

Definition SOME(R:relation):Prop :=
 exists x, exists y, R x y.

Lemma NonEmpty : forall r:relation,
 (SOME r) <->
 (exists x, exists y, r x y).
Proof.
intros. split.
 unfold SOME. intro. assumption.
intros. unfold SOME. assumption.
Qed.

Lemma Transitive : forall r:relation,
 (IN (JOIN r r) r) <->
 (forall x y z, r x y -> r y z -> r x z).
Proof.
intros. split.
 intros. unfold IN in H. unfold JOIN in H.
 specialize (H x z). eapply H.
 exists y. split; assumption.
intros. unfold IN. unfold JOIN.
intros x z H0. destruct H0 as [y [H1 H2]].
eapply (H x y z).
exact H1. exact H2.
Qed.

Lemma Irreflexive : forall r:relation,
 (NO (AND IDEN r)) <->
 (forall x, ~r x x).
Proof.
intros. split.
 intros. unfold NO in H. unfold AND in H.
 unfold IDEN in H. specialize(H x x).
 intro. elim H. split.
  reflexivity.
 assumption.
intros. unfold NO. unfold AND.
unfold IDEN. intros. intro. destruct H0.
rewrite <- H0 in *. elim (H x). assumption.
Qed.

Lemma Symmetric : forall r:relation,
 (IN (INV r) r) <->
 (forall x y, r x y -> r y x).
Proof.
intros. split.
 intros. unfold IN in H. unfold INV in H.
 eapply H. assumption.
intros. unfold IN. unfold INV.
intros. eapply H. assumption.
Qed.

Lemma Functional : forall r:relation,
 (IN (JOIN (INV r) r) IDEN) <->
 (forall x y1 y2, r x y1 -> r x y2 -> y1 = y2).
Proof.
intros. split.
 intros. unfold IN in H. unfold JOIN in H.
 unfold INV in H. unfold IDEN in H.
 specialize (H y1 y2). eapply H.
 exists x. split; assumption.
intros. unfold IN. unfold JOIN.
unfold INV. unfold IDEN.
intros. destruct H0. destruct H0.
eapply (H x0 x y); assumption.
Qed.

Lemma Injective : forall r:relation,
 (IN (JOIN r (INV r)) IDEN) <->
 (forall x1 x2 y, r x1 y -> r x2 y -> x1=x2).
Proof.
intros. split.
 intros. unfold IN in H. unfold JOIN in H.
 unfold INV in H. unfold IDEN in H.
 specialize(H x1 x2). eapply H.
 exists y. split; assumption.
intros. unfold IN. unfold JOIN.
unfold INV. unfold IDEN. intros.
destruct H0. destruct H0. 
eapply (H x y x0); assumption.
Qed.

Definition set := U -> Prop.

Definition SIN(R S:set):Prop :=
 forall x:U, R x -> S x.

Definition UNIV:set :=
 fun x:U => True.

Definition JOIN_SR(S:set)(R:relation):set :=
 fun y => (exists x:U, S x /\ R x y).

Definition JOIN_RS(R:relation)(S:set):set :=
 fun x => (exists y:U, R x y /\ S y).

Lemma Total : forall r:relation,
 (SIN UNIV (JOIN_RS r UNIV)) <->
 (forall x, exists y, r x y).
Proof.
intros. split.
 intros. unfold SIN in H. unfold JOIN_RS in H.
 unfold UNIV in H. specialize (H x).
 specialize(H I). destruct H. destruct H.
 exists x0. assumption.
intros. unfold SIN. unfold JOIN_RS.
unfold UNIV. intros. specialize(H x).
destruct H. exists x0. split; auto.
Qed.

Lemma Surjective : forall r:relation,
 (SIN UNIV (JOIN_SR UNIV r)) <->
 (forall y, exists x, r x y).
Proof.
intros. split.
 intros. unfold SIN in H. unfold JOIN_SR in H.
 unfold UNIV in H. specialize(H y).
 specialize(H I). destruct H. destruct H.
 exists x. auto.
intros. unfold SIN. unfold JOIN_SR.
unfold UNIV. intros. specialize(H x).
destruct H. exists x0. split; auto.
Qed.

End Alloy1.

[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が無くなります。