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