Definition set {A : Type} := A -> Prop.

Notation "a \in b" := (b a) (at level 25, no associativity).
Notation "{{ x | P }}" := (fun x : _ => P) (at level 0).

Definition subseteq {A : Type} (S1 : @set A) (S2 : @set A) := forall x : A, x \in S1 -> x \in S2.

Notation "a \subseteq b" := (subseteq a b) (at level 24, no associativity).

Definition seteq {A : Type} (S1 : @set A) (S2 : @set A) := S1 \subseteq S2 /\ S2 \subseteq S1.
Notation "a == b" := (seteq a b) (at level 70, no associativity).

Definition union {A : Type} (S1 : @set A) (S2 : @set A) : @set A := {{ x | x \in S1 \/ x \in S2 }}.
Definition intersect {A : Type} (S1 : @set A) (S2 : @set A) : @set A := {{ x | x \in S1 /\ x \in S2 }}.
Definition diff {A : Type} (S1 : @set A) (S2 : @set A) : @set A := {{ x | x \in S1 /\ not (x \in S2) }}.
Definition powerset {A : Type} (S1 : @set A) : @set (@set A) := {{ x | x \subseteq S1 }}.
Definition MtoN (m n : nat) : @set nat := {{ i | m <= i <= n}}.
Definition union_of_sets {A : Type} (S : @set (@set A)) : @set A := {{ x | exists s : _, s \in S /\ x \in s }}.
Definition union_of_indexed_set {A B : Type} (I : @set A) (S : A -> @set B) : @set B := {{ x | exists i : A, i \in I /\ x \in S i }}.
Definition intersect_of_sets {A : Type} (S : @set (@set A)) : @set A := {{ x | forall s : _, (s \in S) -> (x \in s) }}.
Definition intersect_of_indexed_set {A B : Type} (I : @set A) (S : A -> @set B) : @set B := {{ x | forall i : A, i \in I /\ x \in S i }}.

Definition relation {A B : Type} := @set (A * B).

Notation "a [ r ] b" := (r (a , b)) (at level 20, no associativity).

Notation "{{ [ x , y ] | P }}" := (fun pair : _ => (fun x : _ => fun y : _ => P) (fst pair) (snd pair)) (at level 0).

Definition identity {A : Type} (S : @set A) : @relation A A := {{ [x, y] | x \in S /\ x = y }}.
Definition dom {A B : Type} (r : @relation A B) : @set A := {{ x | exists x' : _, x [ r ] x' }}.
Definition ran {A B : Type} (r : @relation A B) : @set B := {{ x' | exists x : _, x [ r ] x' }}.
Definition compose {A B C : Type} (r : @relation A B) (r' : @relation B C) : @relation A C := {{ [ x , x''] | exists x' : _, x [ r ] x' /\ x' [ r' ] x'' }}.
Notation "r' `o` r" := (compose r r') (at level 20, no associativity).
Definition reflection {A B : Type} (r : @relation A B) : @relation B A := {{ [ x', x ] | x [ r ] x' }}.
Notation "r ^+" := (reflection r) (at level 20).


(* Tactics *)

Hint Unfold compose.
Hint Unfold reflection.
Hint Unfold dom.
Hint Unfold ran.
Hint Unfold iff.
Hint Unfold subseteq.
Hint Unfold seteq.
Hint Unfold identity.
Hint Unfold union.
Hint Unfold intersect.
Hint Unfold diff.
Hint Unfold powerset.
Hint Unfold union_of_sets.
Hint Unfold intersect_of_sets.
Hint Unfold union_of_indexed_set.
Hint Unfold intersect_of_indexed_set.
Hint Unfold relation.

Ltac myauto := repeat(autosimpl; intros); simpl in *;
                match goal with
                 | [ H : ex ?P |- _ ] => destruct H; myauto
                 | [ |- ?A /\ ?B ] => split; myauto
                 | [ H : ?A /\ ?B |- _ ] => destruct H; myauto
                 | [ |- ?A \/ ?B ] => solve [ left; myauto  | right; myauto ]
                 | [ H : ?A |- @ex ?A ?P ] => solve [exists H; myauto]
                 | [ H : ?A (fst ?B, snd ?B) |- ?A ?B ] => rewrite <- surjective_pairing in H; myauto
                 | [ H : ?A = ?B |- _ ] => simpl in H; solve [ rewrite <- H in *; clear H; myauto | rewrite H in *; clear H; myauto ]
                 | [ H : ?A -> ?B, H' : ?A |- _ ] => solve [ generalize (H H'); clear H; myauto ]
                 | [ H : ?A * ?B |- _ ] => destruct H; myauto
                 | [ H : (forall (X : ?A * ?B), _), H' : ?A, H'' : ?B |- _ ] => solve [ generalize (H (H', H'')); clear H; myauto ]
                 | [ H : (forall (X : ?A), _), H' : ?A |- _ ] => solve [ generalize (H H'); clear H; myauto ]
                 | [ H : _ -> ?G |- ?G ] => solve [apply H; clear H; myauto]
                 | _ => idtac
               end; eauto.