Library Coq.Sets.Finite_sets


Require Import Ensembles.




Section Ensembles_finis.

Variable U : Type.




Inductive Finite : Ensemble U -> Prop :=

  | Empty_is_finite : Finite (Empty_set U)

  | Union_is_finite :

      forall A:Ensemble U,

        Finite A -> forall x:U, ~ In U A x -> Finite (Add U A x).




Inductive cardinal : Ensemble U -> nat -> Prop :=

  | card_empty : cardinal (Empty_set U) 0

  | card_add :

      forall (A:Ensemble U) (n:nat),

        cardinal A n -> forall x:U, ~ In U A x -> cardinal (Add U A x) (S n).




End Ensembles_finis.




Hint Resolve Empty_is_finite Union_is_finite: sets v62.

Hint Resolve card_empty card_add: sets v62.




Require Import Constructive_sets.




Section Ensembles_finis_facts.

Variable U : Type.




Lemma cardinal_invert :

 forall (X:Ensemble U) (p:nat),

   cardinal U X p ->

   match p with

   | O => X = Empty_set U

   | S n =>

        exists A : _,

         (exists x : _, X = Add U A x /\ ~ In U A x /\ cardinal U A n)

   end.

Proof.

induction 1; simpl in |- *; auto.

exists A; exists x; auto.

Qed.




Lemma cardinal_elim :

 forall (X:Ensemble U) (p:nat),

   cardinal U X p ->

   match p with

   | O => X = Empty_set U

   | S n => Inhabited U X

   end.

Proof.

intros X p C; elim C; simpl in |- *; trivial with sets.

Qed.




End Ensembles_finis_facts.
Index
This page has been generated by coqdoc