# Library CoLoR.Util.Set.SetUtil

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTSGHTS and LICENSE files.
• Frederic Blanqui, 2009-06-26

# Potentially infinite sets

Set Implicit Arguments.

We assume given a type A for elements.

Section S.

Context {A : Type}.

Notation eq_dec_type := (forall x y : A, {x=y}+{~x=y}).

# Type for sets of elements of type A

Definition set := A -> Prop.

# Definition of basic predicates and operations on sets

Definition mem a (P : set) := P a.

Definition subset : relation set := pointwise_relation A impl.

Infix "[<=]" := subset (at level 70).

Definition equiv : relation set := pointwise_relation A iff.

Infix "[=]" := equiv (at level 70).

Definition strict_subset P Q := P [<=] Q /\ ~Q [<=] P.

Infix "[<]" := strict_subset (at level 70).

Definition empty : set := fun _ => False.

Definition all : set := fun _ => True.

Definition add a (P : set) : set := fun x => x = a \/ mem x P.

Definition singleton a := add a empty.

Definition union (P Q : set) : set := fun x => mem x P \/ mem x Q.

Definition rem a (P : set) : set := fun x => x <> a /\ mem x P.

Definition diff (P Q : set) : set := fun x => mem x P /\ ~mem x Q.

Definition of_list l : set := fun x => In x l.

Ltac stac := intro; unfold add, rem, diff, union, of_list, mem; simpl; tauto.

Properties of subset.

Global Instance subset_preorder : PreOrder subset.

Properties of equiv.

Lemma equiv_subset2 P Q : P [=] Q <-> P [<=] Q /\ Q [<=] P.

Global Instance equiv_Equivalence : Equivalence equiv.

Global Instance subset_equiv : Proper (equiv ==> equiv ==> impl) subset.

Lemma equiv_inter_transp : equiv == inter_transp subset.

Lemma equiv_elim P Q : P [=] Q <-> P [<=] Q /\ Q [<=] P.

Properties of mem.

Global Instance mem_subset : Proper (eq ==> subset ==> impl) mem.

Global Instance mem_equiv_impl : Proper (eq ==> equiv ==> impl) mem.

Global Instance mem_equiv : Proper (eq ==> equiv ==> iff) mem.

Properties of strict_subset.
Properties of empty.

Lemma notin_empty x : ~mem x empty.

Properties of all.

Lemma subset_all P : P [<=] all.

Properties of rem.

Global Instance rem_subset : Proper (eq ==> subset ==> subset) rem.

Global Instance rem_equiv : Proper (eq ==> equiv ==> equiv) rem.

Lemma notin_rem a P : ~mem a (rem a P).

Lemma rem_notin a P : ~mem a P -> rem a P [=] P.

Lemma subset_rem a P : rem a P [<=] P.

Lemma strict_subset_rem a P : mem a P -> rem a P [<] P.

Lemma add_rem_neq a b P : a <> b -> add a (rem b P) [=] rem b (add a P).

Lemma rem_add_neq a b P : a <> b -> rem a (add b P) [=] add b (rem a P).

Lemma add_rem (eq_dec : eq_dec_type) a P : mem a P -> add a (rem a P) [=] P.

Lemma rem_add a P : ~mem a P -> rem a (add a P) [=] P.

Properties of union.

Global Instance union_subset : Proper (subset ==> subset ==> subset) union.

Global Instance union_equiv : Proper (equiv ==> equiv ==> equiv) union.

Lemma union_com P Q : union P Q [=] union Q P.

Lemma union_assoc P Q R : union (union P Q) R [=] union P (union Q R).

Lemma subset_union_l P Q : P [<=] union P Q.

Lemma subset_union_r P Q : Q [<=] union P Q.

Lemma union_empty_l P : union empty P [=] P.

Lemma union_empty_r P : union P empty [=] P.

Properties of diff.

Global Instance diff_subset : Proper (subset ==> subset --> subset) diff.

Global Instance diff_equiv : Proper (equiv ==> equiv ==> equiv) diff.

Lemma union_diff P Q (Q_dec : forall x, {Q x}+{~Q x}) :
union (diff P Q) Q [=] union P Q.

# Type for the elements of a set.

Definition elts (P : set) := sig (fun x => mem x P).

Definition elt {P x} (h : mem x P) : elts P := @exist _ P _ h.

Definition elt_val {P} (x : elts P) := proj1_sig x.

Coercion elt_val : elts >-> A.

Definition elts_subset P Q : P [<=] Q -> elts P -> elts Q.

Lemma inj_elts_subset P Q (h : P [<=] Q) : injective (elts_subset h).

Definition elts_equiv P Q : P [=] Q -> elts P -> elts Q.

Definition elts_eq {P} : relation (elts P) :=
fun x y => elt_val x = elt_val y.

Instance elts_eq_Equivalence P : Equivalence (@elts_eq P).

# Fiber (inverse image of a singleton)

Definition fiber (P : set) B (f : elts P -> B) b : set :=
fun x => exists h : mem x P, f (elt h) = b.

# Properties of of_list.

Lemma of_cons a l : of_list (a :: l) [=] add a (of_list l).

Lemma of_remove (eq_dec : eq_dec_type) a :
forall l, of_list (remove eq_dec a l) [=] rem a (of_list l).

Lemma of_app l m : of_list (l++m) [=] union (of_list l) (of_list m).

Lemma of_map_L P n (f : N n -> elts P) :
surjective f -> P [=] of_list (map (elt_val o f) (L n)).

End S.

Infix "[<=]" := subset (at level 70).
Infix "[=]" := equiv (at level 70).
Infix "[<]" := strict_subset (at level 70).

# Image of a set by a function.

Section image.

Variables (X Y : Type) (f : X -> Y).

Definition image (A : set X) : set Y := fun y => exists x, A x /\ y = f x.

Lemma image_empty : image empty [=] empty.