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

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

Proper (eq ==> Pf_subset ==> Pf_subset) 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.

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.