Library CoLoR.Util.Set.InfSet

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

Set Implicit Arguments.

Section S.

  Variable A : Type.

Definition of infinite sets

  Definition infinite (P : set A) := ~finite P.

Properties of infinite.

  Global Instance infinite_subset : Proper (subset ==> impl) infinite.

  Global Instance infinite_equiv : Proper (equiv ==> iff) infinite.

A set P is infinite if there is an injection from nat to P.

Set constructors preserve infiniteness.

  Lemma infinite_rem a P : infinite (rem a P) <-> infinite P.

  Lemma infinite_union P Q : infinite (union P Q) <-> infinite P \/ infinite Q.

  Lemma infinite_diff P Q : infinite (diff P Q) -> infinite P.

  Lemma infinite_diff_finite P Q (Q_dec : forall x, {Q x}+{~Q x}) :
    infinite P -> finite Q -> infinite (diff P Q).

  Lemma infinite_not_empty P : infinite P -> exists x, mem x P.

Type for infinite subsets of some set P

  Definition Pinf P := {Q | Q [<=] P /\ infinite Q}.

  Definition mk_Pinf P Q : Q [<=] P -> infinite Q -> Pinf P.

  Definition Pinf_val P (Q : Pinf P) := proj1_sig Q.

  Definition Pinf_sub P (Q : Pinf P) : Q [<=] P.

  Definition Pinf_inf P (Q : Pinf P) : infinite Q.

  Definition Pinf_subset P Q : P [<=] Q -> Pinf P -> Pinf Q.

  Definition Pinf_self P (Q : Pinf P) : Pinf Q.

An infinite set contains finite subsets of every cardinality.

  Section Pcard_of_inf.

    Variable W : set A.

    Lemma Pcard_of_inf_spec (P : Pinf W) :
      forall n, exists X : Pf A, X [<=] P /\ card X = S n.

    Definition Pcard_of_inf (P : Pinf W) n : Pcard P (S n).

  End Pcard_of_inf.

End S.