Definition set {A : Type} := A -> Prop. Notation "a \in b" := (b a) (at level 25, no associativity, only parsing). Notation "{{ x | P }}" := (fun x : _ => P) (at level 0, only parsing). 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, only parsing). 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). Definition is_function {A B : Type} (r : @relation A B) := forall x : A, forall y : B, forall z : B, x [r] y /\ x [r] z -> y = z. Definition is_relation_from_to {A B : Type} (S : @set A) (S' : @set B) (r : @relation A B) := (dom r \subseteq S) /\ (ran r \subseteq S'). Definition is_totalrelation_from_to {A B : Type} (S : @set A) (S' : @set B) (r : @relation A B) := is_relation_from_to S S' r /\ identity S \subseteq ((r^+) `o` r). Definition is_pfun_from_to {A B : Type} (S : @set A) (S' : @set B) (r : @relation A B) := is_relation_from_to S S' r /\ is_function r. Definition is_function_from_to {A B : Type} (S : @set A) (S' : @set B) (r : @relation A B) := is_function r /\ (dom r == S) /\ (ran r \subseteq S'). Definition is_surjection_from_to {A B : Type} (S : @set A) (S' : @set B) (r : @relation A B) := is_function_from_to S S' r /\ ran r == S'. Definition is_injection_from_to {A B : Type} (S : @set A) (S' : @set B) (r : @relation A B) := is_function_from_to S S' r /\ is_pfun_from_to S' S (r^+). Definition is_bijection_from_to {A B : Type} (S : @set A) (S' : @set B) (r : @relation A B) := is_function_from_to S S' r /\ is_function_from_to S' S (r^+). Definition empty_set {A : Type} : @set A := fun x => False. Definition add_element {A : Type} (a : A) (S : @set A) : @set A := fun x => x = a \/ x \in S. Notation "{{{ x , .. , y }}}" := (add_element x (.. (add_element y empty_set) ..)) (at level 0, no associativity). Definition is_transitive {A : Type} (r : @relation A A) := (r `o` r) \subseteq r. Definition is_symmetric {A : Type} (r : @relation A A) := (r^+) == r. Definition is_antisymmetric_on {A : Type} (S : @set A) (r : @relation A A) := (intersect r (r^+)) \subseteq identity S. Definition is_reflexive_on {A : Type} (S : @set A) (r : @relation A A) := identity S \subseteq r. Definition is_preorder_on {A : Type} (S : @set A) (r : @relation A A) := is_transitive r /\ is_reflexive_on S r. Definition is_partialorder_on {A : Type} (S : @set A) (r : @relation A A) := is_preorder_on S r /\ is_antisymmetric_on S r. Definition is_equivrel_on {A : Type} (S : @set A) (r : @relation A A) := is_preorder_on S r /\ is_symmetric r. Definition is_partialequivrel {A : Type} (r : @relation A A) := is_transitive r /\ is_symmetric r. Notation set_of_Type := (fun A : Type => ({{ x | True }} : @set A)). Definition is_upper_bound {A : Type} (r : @relation A A) (X : @set A) (y : A) (_ : is_partialorder_on (set_of_Type A) r) := forall x : A, x \in X -> x [r] y. Definition is_least_upper_bound {A : Type} (r : @relation A A) (X : @set A) (y : A) (pf1 : is_partialorder_on (set_of_Type A) r) := is_upper_bound r X y pf1 /\ forall x : A, is_upper_bound r X x pf1 -> y [r] x. Definition is_lower_bound {A : Type} (r : @relation A A) (X : @set A) (y : A) (_ : is_partialorder_on (set_of_Type A) r) := forall x : A, x \in X -> y [r] x. Definition is_greatest_lower_bound {A : Type} (r : @relation A A) (X : @set A) (y : A) (pf1 : is_partialorder_on (set_of_Type A) r) := is_lower_bound r X y pf1 /\ forall x : A, is_lower_bound r X x pf1 -> x [r] y. Definition relation_of_function {A B : Type} (f : A -> B) : @relation A B := {{ [n,m] | m = f n }}. (* Tactics *) Hint Unfold iff. Hint Unfold compose reflection. Hint Unfold dom ran. Hint Unfold subseteq seteq. Hint Unfold identity. Hint Unfold union intersect diff powerset. Hint Unfold union_of_sets intersect_of_sets union_of_indexed_set intersect_of_indexed_set. Hint Unfold relation. Hint Unfold empty_set add_element. Hint Unfold is_function is_relation_from_to is_totalrelation_from_to is_pfun_from_to is_function_from_to is_surjection_from_to is_injection_from_to is_bijection_from_to. Hint Unfold is_transitive is_symmetric is_antisymmetric_on is_reflexive_on is_preorder_on is_partialorder_on is_equivrel_on is_partialequivrel. Hint Unfold is_least_upper_bound is_upper_bound is_lower_bound is_greatest_lower_bound. Hint Unfold relation_of_function.