diff options
Diffstat (limited to 'theories/Sets/Finite_sets.v')
-rw-r--r-- | theories/Sets/Finite_sets.v | 66 |
1 files changed, 33 insertions, 33 deletions
diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v index 47b41ec3..f5eae4ed 100644 --- a/theories/Sets/Finite_sets.v +++ b/theories/Sets/Finite_sets.v @@ -24,22 +24,22 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id: Finite_sets.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Finite_sets.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Import Ensembles. Section Ensembles_finis. -Variable U : Type. + Variable U : Type. -Inductive Finite : Ensemble U -> Prop := - | Empty_is_finite : Finite (Empty_set U) - | Union_is_finite : + 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 : + 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). @@ -51,31 +51,31 @@ Hint Resolve card_empty card_add: sets v62. Require Import Constructive_sets. Section Ensembles_finis_facts. -Variable U : Type. + 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_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. + 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. |