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

  Global Instance add_subset : Proper (eq ==> subset ==> subset) add.


  Lemma subset_add a P : P [<=] add a P.

  Lemma mem_add a P : mem a (add a P).

  Global Instance add_equiv : Proper (eq ==> equiv ==> equiv) add.


  Lemma add_already_in a P : mem a P -> add a P [=] P.


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

Compatibility of subset and equiv with inclusion and same_rel.

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.

  Lemma image_add a A : image (add a A) [=] add (f a) (image A).

  Lemma image_singleton x : image (singleton x) [=] singleton (f x).

  Lemma image_union A B : image (union A B) [=] union (image A) (image B).

End image.