Library CoLoR.Util.Set.FinSet

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2014-12-11

Finite sets and their cardinal

Standard definition of set finiteness (existence of a bijection to some prefix of nat) and definition of the cardinal of a finite set (using Church's iota).

Set Implicit Arguments.

Section S.

  Variable A : Type.

  Notation set := (set A).

Definition of finiteness

  Definition finite (P : set) := exists n (f : N n -> elts P), bijective f.

Properties of finite

Finiteness is invariant by set equivalence.

  Global Instance finite_equiv : Proper (equiv ==> impl) finite.

Finiteness of sets defined by a list of elements.
A set P is finite if there is a surjection from N n to P.

  Lemma finite_surj P n (f : N n -> elts P) : surjective f -> finite P.

A set P is finite iff it can be defined by a list of elements.

  Lemma finite_eq P : finite P <-> exists l, P [=] of_list l.

Finiteness is contravariant wrt inclusion.

  Global Instance finite_subset : Proper (subset --> impl) finite.

A set P is finite iff it can be defined by a non-duplicating list of elements.

List of the elements of a finite set.

  Definition list_of_finite P : finite P -> list A.

  Lemma finite_eq_of_list P (P_fin : finite P) :
    P [=] of_list (list_of_finite P_fin).

  Lemma nodup_list_of_finite P (P_fin : finite P) :
    nodup (list_of_finite P_fin).

  Lemma In_list_of_finite x P (P_fin : finite P) :
    In x (list_of_finite P_fin) <-> P x.

Finiteness of empty.

  Lemma empty_of_list : empty [=] of_list (@nil A).

  Lemma finite_empty : finite empty.

add preserves finiteness.

  Lemma finite_add a P : finite P -> finite (add a P).

  Lemma finite_add_eq a P : finite (add a P) <-> finite P.

Finiteness of a singleton.

  Lemma finite_singleton a : finite (singleton a).

rem preserves finiteness.

  Lemma finite_rem a P : finite P -> finite (rem a P).

  Lemma finite_rem_eq a P : finite (rem a P) <-> finite P.

union preserves finiteness.

  Lemma finite_union P Q : finite P -> finite Q -> finite (union P Q).

  Lemma finite_union_eq P Q : finite (union P Q) <-> finite P /\ finite Q.

diff preserves finiteness.

  Lemma finite_diff P : finite P -> forall Q, finite (diff P Q).

Type of finite sets.

  Definition Pf := sig finite.

  Definition mk_Pf P (P_fin : finite P) : Pf := exist P_fin.

  Coercion mk_Pf : finite >-> Pf.

  Definition Pf_val (P : Pf) : set := proj1_sig P.

  Coercion Pf_val : Pf >-> SetUtil.set.

  Definition Pf_prf (P : Pf) : finite (Pf_val P) := proj2_sig P.

  Coercion Pf_prf : Pf >-> finite.

Inclusion and equivalence of finite sets.

  Definition Pf_subset (P Q : Pf) := P [<=] Q.

  Global Instance Pf_subset_preorder : PreOrder Pf_subset.

  Definition Pf_equiv (P Q : Pf) := P [=] Q.

  Infix "=f=" := Pf_equiv (at level 70).

  Global Instance Pf_equiv_Equivalence : Equivalence Pf_equiv.

  Global Instance Pf_val_subset : Proper (Pf_subset ==> subset) Pf_val.

  Global Instance Pf_val_equiv : Proper (Pf_equiv ==> equiv) Pf_val.

  Lemma Pf_equiv_of {P Q : Pf} : P [=] Q -> P =f= Q.

  Coercion Pf_equiv_of : equiv >-> Pf_equiv.

  Lemma Pf_equiv_of_gen (P Q : Pf) P_val Q_val :
    P [=] P_val -> Q [=] Q_val -> P_val [=] Q_val -> P =f= Q.

  Definition Pf_equiv_of2 {P Q : Pf} :=
    Pf_equiv_of_gen P Q (reflexivity _) (reflexivity _).

Constructors of finite sets.

  Definition Pf_of_list l : Pf := finite_of_list l.

  Definition Pf_empty : Pf := finite_empty.

  Definition Pf_add x (P : Pf) : Pf := finite_add x P.

  Global Instance Pf_add_subset :
    Proper (eq ==> Pf_subset ==> Pf_subset) Pf_add.

  Global Instance Pf_add_equiv : Proper (eq ==> Pf_equiv ==> Pf_equiv) Pf_add.

  Definition Pf_singleton x : Pf := finite_singleton x.

  Lemma Pf_singleton_eq x : Pf_singleton x =f= Pf_add x Pf_empty.

  Definition Pf_rem x (P : Pf) : Pf := finite_rem x P.

  Global Instance Pf_rem_subset :
    Proper (eq ==> Pf_subset ==> Pf_subset) Pf_rem.

  Global Instance Pf_rem_equiv : Proper (eq ==> Pf_equiv ==> Pf_equiv) Pf_rem.

  Definition Pf_union (P Q : Pf) : Pf := finite_union P Q.

  Global Instance Pf_union_subset :
    Proper (Pf_subset ==> Pf_subset ==> Pf_subset) Pf_union.

  Global Instance Pf_union_equiv :
    Proper (Pf_equiv ==> Pf_equiv ==> Pf_equiv) Pf_union.

  Definition Pf_diff (P Q : Pf) : Pf := finite_diff P Q.

  Global Instance Pf_diff_subset :
    Proper (Pf_subset ==> Pf_subset --> Pf_subset) Pf_diff.

  Global Instance Pf_diff_equiv :
    Proper (Pf_equiv ==> Pf_equiv ==> Pf_equiv) Pf_diff.

  Lemma Pf_equiv_of_list (P : Pf) : P =f= Pf_of_list (list_of_finite P).

  Lemma Pf_add_of_list a (l : list A) :
    Pf_add a (Pf_of_list l) =f= Pf_of_list (a :: l).

Induction principle on finite sets.

  Lemma Pf_ind (P : Pf -> Prop) (P_equiv : Proper (Pf_equiv ==> impl) P)
    (P0 : P Pf_empty)
    (PS : forall a (X : Pf), ~mem a X -> P X -> P (Pf_add a X)) :
    forall X, P X.

Cardinal of a finite set

  Lemma card_uniq P :
    finite P -> exists! n, exists (f : N n -> elts P), bijective f.

  Definition card : Pf -> nat.

  Global Instance card_subset : Proper (Pf_subset ==> le) card.

  Global Instance card_equiv : Proper (Pf_equiv ==> eq) card.

Induction on finite sets through their cardinals.

  Lemma card_ind (P : Pf -> Prop) (H : forall n X, card X = n -> P X) :
    forall X, P X.

Cardinal of some finite set constructors.

Cardinal of a set defined by a list of elements.
Cardinal of the empty set.

  Lemma card_empty_gen (h : finite empty) : card h = 0.

  Lemma card_empty : card Pf_empty = 0.

A set of null cardinality is empty.

  Lemma card_0 {P} : card P = 0 -> P =f= Pf_empty.

Cardinal of a set defined by a non-duplcating list of elements.
Cardinal of add.

  Lemma card_add a P :
    card (Pf_add a P) = card P + if dec (mem a P) then 0 else 1.

Cardinal of singleton.

  Lemma card_singleton a : card (Pf_singleton a) = 1.

Cardinal of rem.

  Lemma card_rem a P :
    card (Pf_rem a P) = card P - if dec (mem a P) then 1 else 0.

A set of non-null cardinality has at least one element.

  Lemma card_S {P n} : card P = S n ->
    exists a Q, P =f= Pf_add a Q /\ ~mem a Q /\ card Q = n.

Type of subsets of some cardinality.

  Section Pcard.

    Variables (P : set) (n : nat).

    Definition Pcard := { Q : Pf | Q [<=] P /\ card Q = n }.

    Definition mk_Pcard (Q : Pf) : Q [<=] P -> card Q = n -> Pcard.

    Definition Pcard_val (Q : Pcard) : Pf := proj1_sig Q.

    Definition Pcard_equiv (Q R : Pcard) := Q =f= R.

    Global Instance Pcard_equiv_Equivalence : Equivalence Pcard_equiv.

  End Pcard.

  Infix "=c=" := Pcard_equiv (at level 70).

  Definition Pcard_subset n P P' : P [<=] P' -> Pcard P n -> Pcard P' n.

  Lemma Pcard_subset_inj n R P (PR : P [<=] R) Q (QR : Q [<=] R) :
    forall (x : Pcard P n) (y : Pcard Q n),
      x [=] y -> Pcard_subset PR x =c= Pcard_subset QR y.

  Lemma Pcard_subset_equiv P Q (PQ : P [<=] Q) n R :
    forall x : Pcard P n, x [=] R -> Pcard_subset PQ x [=] R.

End S.