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