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.