summaryrefslogtreecommitdiff
path: root/theories/Sets
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Sets')
-rw-r--r--theories/Sets/Classical_sets.v189
-rw-r--r--theories/Sets/Constructive_sets.v231
-rw-r--r--theories/Sets/Cpo.v105
-rw-r--r--theories/Sets/Ensembles.v103
-rw-r--r--theories/Sets/Finite_sets.v66
-rw-r--r--theories/Sets/Finite_sets_facts.v583
-rw-r--r--theories/Sets/Image.v322
-rw-r--r--theories/Sets/Infinite_sets.v388
-rw-r--r--theories/Sets/Integers.v223
-rw-r--r--theories/Sets/Multiset.v306
-rw-r--r--theories/Sets/Partial_Order.v116
-rw-r--r--theories/Sets/Permut.v144
-rw-r--r--theories/Sets/Powerset_Classical_facts.v578
-rw-r--r--theories/Sets/Powerset_facts.v436
14 files changed, 1874 insertions, 1916 deletions
diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v
index 382b5d72..e6755898 100644
--- a/theories/Sets/Classical_sets.v
+++ b/theories/Sets/Classical_sets.v
@@ -24,109 +24,104 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Classical_sets.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Classical_sets.v 9245 2006-10-17 12:53:34Z notin $ i*)
Require Export Ensembles.
Require Export Constructive_sets.
Require Export Classical_Type.
-(* Hints Unfold not . *)
-
Section Ensembles_classical.
-Variable U : Type.
-
-Lemma not_included_empty_Inhabited :
- forall A:Ensemble U, ~ Included U A (Empty_set U) -> Inhabited U A.
-Proof.
-intros A NI.
-elim (not_all_ex_not U (fun x:U => ~ In U A x)).
-intros x H; apply Inhabited_intro with x.
-apply NNPP; auto with sets.
-red in |- *; intro.
-apply NI; red in |- *.
-intros x H'; elim (H x); trivial with sets.
-Qed.
-Hint Resolve not_included_empty_Inhabited.
-
-Lemma not_empty_Inhabited :
- forall A:Ensemble U, A <> Empty_set U -> Inhabited U A.
-Proof.
-intros; apply not_included_empty_Inhabited.
-red in |- *; auto with sets.
-Qed.
-
-Lemma Inhabited_Setminus :
- forall X Y:Ensemble U,
- Included U X Y -> ~ Included U Y X -> Inhabited U (Setminus U Y X).
-Proof.
-intros X Y I NI.
-elim (not_all_ex_not U (fun x:U => In U Y x -> In U X x) NI).
-intros x YX.
-apply Inhabited_intro with x.
-apply Setminus_intro.
-apply not_imply_elim with (In U X x); trivial with sets.
-auto with sets.
-Qed.
-Hint Resolve Inhabited_Setminus.
-
-Lemma Strict_super_set_contains_new_element :
- forall X Y:Ensemble U,
- Included U X Y -> X <> Y -> Inhabited U (Setminus U Y X).
-Proof.
-auto 7 with sets.
-Qed.
-Hint Resolve Strict_super_set_contains_new_element.
-
-Lemma Subtract_intro :
- forall (A:Ensemble U) (x y:U), In U A y -> x <> y -> In U (Subtract U A x) y.
-Proof.
-unfold Subtract at 1 in |- *; auto with sets.
-Qed.
-Hint Resolve Subtract_intro.
-
-Lemma Subtract_inv :
- forall (A:Ensemble U) (x y:U), In U (Subtract U A x) y -> In U A y /\ x <> y.
-Proof.
-intros A x y H'; elim H'; auto with sets.
-Qed.
-
-Lemma Included_Strict_Included :
- forall X Y:Ensemble U, Included U X Y -> Strict_Included U X Y \/ X = Y.
-Proof.
-intros X Y H'; try assumption.
-elim (classic (X = Y)); auto with sets.
-Qed.
-
-Lemma Strict_Included_inv :
- forall X Y:Ensemble U,
- Strict_Included U X Y -> Included U X Y /\ Inhabited U (Setminus U Y X).
-Proof.
-intros X Y H'; red in H'.
-split; [ tauto | idtac ].
-elim H'; intros H'0 H'1; try exact H'1; clear H'.
-apply Strict_super_set_contains_new_element; auto with sets.
-Qed.
-
-Lemma not_SIncl_empty :
- forall X:Ensemble U, ~ Strict_Included U X (Empty_set U).
-Proof.
-intro X; red in |- *; intro H'; try exact H'.
-lapply (Strict_Included_inv X (Empty_set U)); auto with sets.
-intro H'0; elim H'0; intros H'1 H'2; elim H'2; clear H'0.
-intros x H'0; elim H'0.
-intro H'3; elim H'3.
-Qed.
-
-Lemma Complement_Complement :
- forall A:Ensemble U, Complement U (Complement U A) = A.
-Proof.
-unfold Complement in |- *; intros; apply Extensionality_Ensembles;
- auto with sets.
-red in |- *; split; auto with sets.
-red in |- *; intros; apply NNPP; auto with sets.
-Qed.
+ Variable U : Type.
+
+ Lemma not_included_empty_Inhabited :
+ forall A:Ensemble U, ~ Included U A (Empty_set U) -> Inhabited U A.
+ Proof.
+ intros A NI.
+ elim (not_all_ex_not U (fun x:U => ~ In U A x)).
+ intros x H; apply Inhabited_intro with x.
+ apply NNPP; auto with sets.
+ red in |- *; intro.
+ apply NI; red in |- *.
+ intros x H'; elim (H x); trivial with sets.
+ Qed.
+
+ Lemma not_empty_Inhabited :
+ forall A:Ensemble U, A <> Empty_set U -> Inhabited U A.
+ Proof.
+ intros; apply not_included_empty_Inhabited.
+ red in |- *; auto with sets.
+ Qed.
+
+ Lemma Inhabited_Setminus :
+ forall X Y:Ensemble U,
+ Included U X Y -> ~ Included U Y X -> Inhabited U (Setminus U Y X).
+ Proof.
+ intros X Y I NI.
+ elim (not_all_ex_not U (fun x:U => In U Y x -> In U X x) NI).
+ intros x YX.
+ apply Inhabited_intro with x.
+ apply Setminus_intro.
+ apply not_imply_elim with (In U X x); trivial with sets.
+ auto with sets.
+ Qed.
+
+ Lemma Strict_super_set_contains_new_element :
+ forall X Y:Ensemble U,
+ Included U X Y -> X <> Y -> Inhabited U (Setminus U Y X).
+ Proof.
+ auto 7 using Inhabited_Setminus with sets.
+ Qed.
+
+ Lemma Subtract_intro :
+ forall (A:Ensemble U) (x y:U), In U A y -> x <> y -> In U (Subtract U A x) y.
+ Proof.
+ unfold Subtract at 1 in |- *; auto with sets.
+ Qed.
+ Hint Resolve Subtract_intro : sets.
+
+ Lemma Subtract_inv :
+ forall (A:Ensemble U) (x y:U), In U (Subtract U A x) y -> In U A y /\ x <> y.
+ Proof.
+ intros A x y H'; elim H'; auto with sets.
+ Qed.
+
+ Lemma Included_Strict_Included :
+ forall X Y:Ensemble U, Included U X Y -> Strict_Included U X Y \/ X = Y.
+ Proof.
+ intros X Y H'; try assumption.
+ elim (classic (X = Y)); auto with sets.
+ Qed.
+
+ Lemma Strict_Included_inv :
+ forall X Y:Ensemble U,
+ Strict_Included U X Y -> Included U X Y /\ Inhabited U (Setminus U Y X).
+ Proof.
+ intros X Y H'; red in H'.
+ split; [ tauto | idtac ].
+ elim H'; intros H'0 H'1; try exact H'1; clear H'.
+ apply Strict_super_set_contains_new_element; auto with sets.
+ Qed.
+
+ Lemma not_SIncl_empty :
+ forall X:Ensemble U, ~ Strict_Included U X (Empty_set U).
+ Proof.
+ intro X; red in |- *; intro H'; try exact H'.
+ lapply (Strict_Included_inv X (Empty_set U)); auto with sets.
+ intro H'0; elim H'0; intros H'1 H'2; elim H'2; clear H'0.
+ intros x H'0; elim H'0.
+ intro H'3; elim H'3.
+ Qed.
+
+ Lemma Complement_Complement :
+ forall A:Ensemble U, Complement U (Complement U A) = A.
+ Proof.
+ unfold Complement in |- *; intros; apply Extensionality_Ensembles;
+ auto with sets.
+ red in |- *; split; auto with sets.
+ red in |- *; intros; apply NNPP; auto with sets.
+ Qed.
End Ensembles_classical.
-Hint Resolve Strict_super_set_contains_new_element Subtract_intro
- not_SIncl_empty: sets v62. \ No newline at end of file
+ Hint Resolve Strict_super_set_contains_new_element Subtract_intro
+ not_SIncl_empty: sets v62.
diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v
index 7e4471a0..ad81316d 100644
--- a/theories/Sets/Constructive_sets.v
+++ b/theories/Sets/Constructive_sets.v
@@ -24,136 +24,123 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Constructive_sets.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Constructive_sets.v 9245 2006-10-17 12:53:34Z notin $ i*)
Require Export Ensembles.
Section Ensembles_facts.
-Variable U : Type.
-
-Lemma Extension : forall B C:Ensemble U, B = C -> Same_set U B C.
-Proof.
-intros B C H'; rewrite H'; auto with sets.
-Qed.
-
-Lemma Noone_in_empty : forall x:U, ~ In U (Empty_set U) x.
-Proof.
-red in |- *; destruct 1.
-Qed.
-Hint Resolve Noone_in_empty.
-
-Lemma Included_Empty : forall A:Ensemble U, Included U (Empty_set U) A.
-Proof.
-intro; red in |- *.
-intros x H; elim (Noone_in_empty x); auto with sets.
-Qed.
-Hint Resolve Included_Empty.
-
-Lemma Add_intro1 :
- forall (A:Ensemble U) (x y:U), In U A y -> In U (Add U A x) y.
-Proof.
-unfold Add at 1 in |- *; auto with sets.
-Qed.
-Hint Resolve Add_intro1.
-
-Lemma Add_intro2 : forall (A:Ensemble U) (x:U), In U (Add U A x) x.
-Proof.
-unfold Add at 1 in |- *; auto with sets.
-Qed.
-Hint Resolve Add_intro2.
-
-Lemma Inhabited_add : forall (A:Ensemble U) (x:U), Inhabited U (Add U A x).
-Proof.
-intros A x.
-apply Inhabited_intro with (x := x); auto with sets.
-Qed.
-Hint Resolve Inhabited_add.
-
-Lemma Inhabited_not_empty :
- forall X:Ensemble U, Inhabited U X -> X <> Empty_set U.
-Proof.
-intros X H'; elim H'.
-intros x H'0; red in |- *; intro H'1.
-absurd (In U X x); auto with sets.
-rewrite H'1; auto with sets.
-Qed.
-Hint Resolve Inhabited_not_empty.
-
-Lemma Add_not_Empty : forall (A:Ensemble U) (x:U), Add U A x <> Empty_set U.
-Proof.
-auto with sets.
-Qed.
-Hint Resolve Add_not_Empty.
-
-Lemma not_Empty_Add : forall (A:Ensemble U) (x:U), Empty_set U <> Add U A x.
-Proof.
-intros; red in |- *; intro H; generalize (Add_not_Empty A x); auto with sets.
-Qed.
-Hint Resolve not_Empty_Add.
-
-Lemma Singleton_inv : forall x y:U, In U (Singleton U x) y -> x = y.
-Proof.
-intros x y H'; elim H'; trivial with sets.
-Qed.
-Hint Resolve Singleton_inv.
-
-Lemma Singleton_intro : forall x y:U, x = y -> In U (Singleton U x) y.
-Proof.
-intros x y H'; rewrite H'; trivial with sets.
-Qed.
-Hint Resolve Singleton_intro.
-
-Lemma Union_inv :
- forall (B C:Ensemble U) (x:U), In U (Union U B C) x -> In U B x \/ In U C x.
-Proof.
-intros B C x H'; elim H'; auto with sets.
-Qed.
-
-Lemma Add_inv :
- forall (A:Ensemble U) (x y:U), In U (Add U A x) y -> In U A y \/ x = y.
-Proof.
-intros A x y H'; elim H'; auto with sets.
-Qed.
-
-Lemma Intersection_inv :
- forall (B C:Ensemble U) (x:U),
- In U (Intersection U B C) x -> In U B x /\ In U C x.
-Proof.
-intros B C x H'; elim H'; auto with sets.
-Qed.
-Hint Resolve Intersection_inv.
-
-Lemma Couple_inv : forall x y z:U, In U (Couple U x y) z -> z = x \/ z = y.
-Proof.
-intros x y z H'; elim H'; auto with sets.
-Qed.
-Hint Resolve Couple_inv.
-
-Lemma Setminus_intro :
- forall (A B:Ensemble U) (x:U),
- In U A x -> ~ In U B x -> In U (Setminus U A B) x.
-Proof.
-unfold Setminus at 1 in |- *; red in |- *; auto with sets.
-Qed.
-Hint Resolve Setminus_intro.
+ Variable U : Type.
+
+ Lemma Extension : forall B C:Ensemble U, B = C -> Same_set U B C.
+ Proof.
+ intros B C H'; rewrite H'; auto with sets.
+ Qed.
+
+ Lemma Noone_in_empty : forall x:U, ~ In U (Empty_set U) x.
+ Proof.
+ red in |- *; destruct 1.
+ Qed.
+
+ Lemma Included_Empty : forall A:Ensemble U, Included U (Empty_set U) A.
+ Proof.
+ intro; red in |- *.
+ intros x H; elim (Noone_in_empty x); auto with sets.
+ Qed.
+
+ Lemma Add_intro1 :
+ forall (A:Ensemble U) (x y:U), In U A y -> In U (Add U A x) y.
+ Proof.
+ unfold Add at 1 in |- *; auto with sets.
+ Qed.
+
+ Lemma Add_intro2 : forall (A:Ensemble U) (x:U), In U (Add U A x) x.
+ Proof.
+ unfold Add at 1 in |- *; auto with sets.
+ Qed.
+
+ Lemma Inhabited_add : forall (A:Ensemble U) (x:U), Inhabited U (Add U A x).
+ Proof.
+ intros A x.
+ apply Inhabited_intro with (x := x); auto using Add_intro2 with sets.
+ Qed.
+
+ Lemma Inhabited_not_empty :
+ forall X:Ensemble U, Inhabited U X -> X <> Empty_set U.
+ Proof.
+ intros X H'; elim H'.
+ intros x H'0; red in |- *; intro H'1.
+ absurd (In U X x); auto with sets.
+ rewrite H'1; auto using Noone_in_empty with sets.
+ Qed.
+
+ Lemma Add_not_Empty : forall (A:Ensemble U) (x:U), Add U A x <> Empty_set U.
+ Proof.
+ intros A x; apply Inhabited_not_empty; apply Inhabited_add.
+ Qed.
+
+ Lemma not_Empty_Add : forall (A:Ensemble U) (x:U), Empty_set U <> Add U A x.
+ Proof.
+ intros; red in |- *; intro H; generalize (Add_not_Empty A x); auto with sets.
+ Qed.
+
+ Lemma Singleton_inv : forall x y:U, In U (Singleton U x) y -> x = y.
+ Proof.
+ intros x y H'; elim H'; trivial with sets.
+ Qed.
+
+ Lemma Singleton_intro : forall x y:U, x = y -> In U (Singleton U x) y.
+ Proof.
+ intros x y H'; rewrite H'; trivial with sets.
+ Qed.
+
+ Lemma Union_inv :
+ forall (B C:Ensemble U) (x:U), In U (Union U B C) x -> In U B x \/ In U C x.
+ Proof.
+ intros B C x H'; elim H'; auto with sets.
+ Qed.
+
+ Lemma Add_inv :
+ forall (A:Ensemble U) (x y:U), In U (Add U A x) y -> In U A y \/ x = y.
+ Proof.
+ intros A x y H'; induction H'.
+ left; assumption.
+ right; apply Singleton_inv; assumption.
+ Qed.
+
+ Lemma Intersection_inv :
+ forall (B C:Ensemble U) (x:U),
+ In U (Intersection U B C) x -> In U B x /\ In U C x.
+ Proof.
+ intros B C x H'; elim H'; auto with sets.
+ Qed.
+
+ Lemma Couple_inv : forall x y z:U, In U (Couple U x y) z -> z = x \/ z = y.
+ Proof.
+ intros x y z H'; elim H'; auto with sets.
+ Qed.
+
+ Lemma Setminus_intro :
+ forall (A B:Ensemble U) (x:U),
+ In U A x -> ~ In U B x -> In U (Setminus U A B) x.
+ Proof.
+ unfold Setminus at 1 in |- *; red in |- *; auto with sets.
+ Qed.
-Lemma Strict_Included_intro :
- forall X Y:Ensemble U, Included U X Y /\ X <> Y -> Strict_Included U X Y.
-Proof.
-auto with sets.
-Qed.
-Hint Resolve Strict_Included_intro.
-
-Lemma Strict_Included_strict : forall X:Ensemble U, ~ Strict_Included U X X.
-Proof.
-intro X; red in |- *; intro H'; elim H'.
-intros H'0 H'1; elim H'1; auto with sets.
-Qed.
-Hint Resolve Strict_Included_strict.
+ Lemma Strict_Included_intro :
+ forall X Y:Ensemble U, Included U X Y /\ X <> Y -> Strict_Included U X Y.
+ Proof.
+ auto with sets.
+ Qed.
+
+ Lemma Strict_Included_strict : forall X:Ensemble U, ~ Strict_Included U X X.
+ Proof.
+ intro X; red in |- *; intro H'; elim H'.
+ intros H'0 H'1; elim H'1; auto with sets.
+ Qed.
End Ensembles_facts.
Hint Resolve Singleton_inv Singleton_intro Add_intro1 Add_intro2
Intersection_inv Couple_inv Setminus_intro Strict_Included_intro
Strict_Included_strict Noone_in_empty Inhabited_not_empty Add_not_Empty
- not_Empty_Add Inhabited_add Included_Empty: sets v62. \ No newline at end of file
+ not_Empty_Add Inhabited_add Included_Empty: sets v62.
diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v
index 0b2cf3e3..1e1b70d5 100644
--- a/theories/Sets/Cpo.v
+++ b/theories/Sets/Cpo.v
@@ -24,86 +24,87 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Cpo.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Cpo.v 9245 2006-10-17 12:53:34Z notin $ i*)
Require Export Ensembles.
Require Export Relations_1.
Require Export Partial_Order.
Section Bounds.
-Variable U : Type.
-Variable D : PO U.
+ Variable U : Type.
+ Variable D : PO U.
-Let C := Carrier_of U D.
+ Let C := Carrier_of U D.
+
+ Let R := Rel_of U D.
-Let R := Rel_of U D.
-
-Inductive Upper_Bound (B:Ensemble U) (x:U) : Prop :=
+ Inductive Upper_Bound (B:Ensemble U) (x:U) : Prop :=
Upper_Bound_definition :
- In U C x -> (forall y:U, In U B y -> R y x) -> Upper_Bound B x.
+ In U C x -> (forall y:U, In U B y -> R y x) -> Upper_Bound B x.
-Inductive Lower_Bound (B:Ensemble U) (x:U) : Prop :=
+ Inductive Lower_Bound (B:Ensemble U) (x:U) : Prop :=
Lower_Bound_definition :
- In U C x -> (forall y:U, In U B y -> R x y) -> Lower_Bound B x.
-
-Inductive Lub (B:Ensemble U) (x:U) : Prop :=
+ In U C x -> (forall y:U, In U B y -> R x y) -> Lower_Bound B x.
+
+ Inductive Lub (B:Ensemble U) (x:U) : Prop :=
Lub_definition :
- Upper_Bound B x -> (forall y:U, Upper_Bound B y -> R x y) -> Lub B x.
+ Upper_Bound B x -> (forall y:U, Upper_Bound B y -> R x y) -> Lub B x.
-Inductive Glb (B:Ensemble U) (x:U) : Prop :=
+ Inductive Glb (B:Ensemble U) (x:U) : Prop :=
Glb_definition :
- Lower_Bound B x -> (forall y:U, Lower_Bound B y -> R y x) -> Glb B x.
+ Lower_Bound B x -> (forall y:U, Lower_Bound B y -> R y x) -> Glb B x.
-Inductive Bottom (bot:U) : Prop :=
+ Inductive Bottom (bot:U) : Prop :=
Bottom_definition :
- In U C bot -> (forall y:U, In U C y -> R bot y) -> Bottom bot.
-
-Inductive Totally_ordered (B:Ensemble U) : Prop :=
+ In U C bot -> (forall y:U, In U C y -> R bot y) -> Bottom bot.
+
+ Inductive Totally_ordered (B:Ensemble U) : Prop :=
Totally_ordered_definition :
- (Included U B C ->
- forall x y:U, Included U (Couple U x y) B -> R x y \/ R y x) ->
- Totally_ordered B.
+ (Included U B C ->
+ forall x y:U, Included U (Couple U x y) B -> R x y \/ R y x) ->
+ Totally_ordered B.
-Definition Compatible : Relation U :=
- fun x y:U =>
- In U C x ->
- In U C y -> exists z : _, In U C z /\ Upper_Bound (Couple U x y) z.
-
-Inductive Directed (X:Ensemble U) : Prop :=
- Definition_of_Directed :
- Included U X C ->
- Inhabited U X ->
- (forall x1 x2:U,
- Included U (Couple U x1 x2) X ->
- exists x3 : _, In U X x3 /\ Upper_Bound (Couple U x1 x2) x3) ->
- Directed X.
+ Definition Compatible : Relation U :=
+ fun x y:U =>
+ In U C x ->
+ In U C y -> exists z : _, In U C z /\ Upper_Bound (Couple U x y) z.
-Inductive Complete : Prop :=
+ Inductive Directed (X:Ensemble U) : Prop :=
+ Definition_of_Directed :
+ Included U X C ->
+ Inhabited U X ->
+ (forall x1 x2:U,
+ Included U (Couple U x1 x2) X ->
+ exists x3 : _, In U X x3 /\ Upper_Bound (Couple U x1 x2) x3) ->
+ Directed X.
+
+ Inductive Complete : Prop :=
Definition_of_Complete :
- (exists bot : _, Bottom bot) ->
- (forall X:Ensemble U, Directed X -> exists bsup : _, Lub X bsup) ->
- Complete.
+ (exists bot : _, Bottom bot) ->
+ (forall X:Ensemble U, Directed X -> exists bsup : _, Lub X bsup) ->
+ Complete.
-Inductive Conditionally_complete : Prop :=
+ Inductive Conditionally_complete : Prop :=
Definition_of_Conditionally_complete :
- (forall X:Ensemble U,
- Included U X C ->
- (exists maj : _, Upper_Bound X maj) ->
- exists bsup : _, Lub X bsup) -> Conditionally_complete.
+ (forall X:Ensemble U,
+ Included U X C ->
+ (exists maj : _, Upper_Bound X maj) ->
+ exists bsup : _, Lub X bsup) -> Conditionally_complete.
End Bounds.
+
Hint Resolve Totally_ordered_definition Upper_Bound_definition
Lower_Bound_definition Lub_definition Glb_definition Bottom_definition
Definition_of_Complete Definition_of_Complete
Definition_of_Conditionally_complete.
Section Specific_orders.
-Variable U : Type.
-
-Record Cpo : Type := Definition_of_cpo
- {PO_of_cpo : PO U; Cpo_cond : Complete U PO_of_cpo}.
-
-Record Chain : Type := Definition_of_chain
- {PO_of_chain : PO U;
- Chain_cond : Totally_ordered U PO_of_chain (Carrier_of U PO_of_chain)}.
+ Variable U : Type.
+
+ Record Cpo : Type := Definition_of_cpo
+ {PO_of_cpo : PO U; Cpo_cond : Complete U PO_of_cpo}.
+
+ Record Chain : Type := Definition_of_chain
+ {PO_of_chain : PO U;
+ Chain_cond : Totally_ordered U PO_of_chain (Carrier_of U PO_of_chain)}.
End Specific_orders. \ No newline at end of file
diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v
index d71c96b0..c38a2fe1 100644
--- a/theories/Sets/Ensembles.v
+++ b/theories/Sets/Ensembles.v
@@ -24,72 +24,71 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Ensembles.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Ensembles.v 9245 2006-10-17 12:53:34Z notin $ i*)
Section Ensembles.
-Variable U : Type.
-
-Definition Ensemble := U -> Prop.
-
-Definition In (A:Ensemble) (x:U) : Prop := A x.
-
-Definition Included (B C:Ensemble) : Prop := forall x:U, In B x -> In C x.
-
-Inductive Empty_set : Ensemble :=.
-
-Inductive Full_set : Ensemble :=
+ Variable U : Type.
+
+ Definition Ensemble := U -> Prop.
+
+ Definition In (A:Ensemble) (x:U) : Prop := A x.
+
+ Definition Included (B C:Ensemble) : Prop := forall x:U, In B x -> In C x.
+
+ Inductive Empty_set : Ensemble :=.
+
+ Inductive Full_set : Ensemble :=
Full_intro : forall x:U, In Full_set x.
(** NB: The following definition builds-in equality of elements in [U] as
- Leibniz equality.
+ Leibniz equality.
- This may have to be changed if we replace [U] by a Setoid on [U]
- with its own equality [eqs], with
- [In_singleton: (y: U)(eqs x y) -> (In (Singleton x) y)]. *)
+ This may have to be changed if we replace [U] by a Setoid on [U]
+ with its own equality [eqs], with
+ [In_singleton: (y: U)(eqs x y) -> (In (Singleton x) y)]. *)
-Inductive Singleton (x:U) : Ensemble :=
+ Inductive Singleton (x:U) : Ensemble :=
In_singleton : In (Singleton x) x.
-Inductive Union (B C:Ensemble) : Ensemble :=
- | Union_introl : forall x:U, In B x -> In (Union B C) x
- | Union_intror : forall x:U, In C x -> In (Union B C) x.
-
-Definition Add (B:Ensemble) (x:U) : Ensemble := Union B (Singleton x).
+ Inductive Union (B C:Ensemble) : Ensemble :=
+ | Union_introl : forall x:U, In B x -> In (Union B C) x
+ | Union_intror : forall x:U, In C x -> In (Union B C) x.
-Inductive Intersection (B C:Ensemble) : Ensemble :=
+ Definition Add (B:Ensemble) (x:U) : Ensemble := Union B (Singleton x).
+
+ Inductive Intersection (B C:Ensemble) : Ensemble :=
Intersection_intro :
- forall x:U, In B x -> In C x -> In (Intersection B C) x.
-
-Inductive Couple (x y:U) : Ensemble :=
- | Couple_l : In (Couple x y) x
- | Couple_r : In (Couple x y) y.
-
-Inductive Triple (x y z:U) : Ensemble :=
- | Triple_l : In (Triple x y z) x
- | Triple_m : In (Triple x y z) y
- | Triple_r : In (Triple x y z) z.
-
-Definition Complement (A:Ensemble) : Ensemble := fun x:U => ~ In A x.
-
-Definition Setminus (B C:Ensemble) : Ensemble :=
- fun x:U => In B x /\ ~ In C x.
-
-Definition Subtract (B:Ensemble) (x:U) : Ensemble := Setminus B (Singleton x).
-
-Inductive Disjoint (B C:Ensemble) : Prop :=
+ forall x:U, In B x -> In C x -> In (Intersection B C) x.
+
+ Inductive Couple (x y:U) : Ensemble :=
+ | Couple_l : In (Couple x y) x
+ | Couple_r : In (Couple x y) y.
+
+ Inductive Triple (x y z:U) : Ensemble :=
+ | Triple_l : In (Triple x y z) x
+ | Triple_m : In (Triple x y z) y
+ | Triple_r : In (Triple x y z) z.
+
+ Definition Complement (A:Ensemble) : Ensemble := fun x:U => ~ In A x.
+
+ Definition Setminus (B C:Ensemble) : Ensemble :=
+ fun x:U => In B x /\ ~ In C x.
+
+ Definition Subtract (B:Ensemble) (x:U) : Ensemble := Setminus B (Singleton x).
+
+ Inductive Disjoint (B C:Ensemble) : Prop :=
Disjoint_intro : (forall x:U, ~ In (Intersection B C) x) -> Disjoint B C.
-Inductive Inhabited (B:Ensemble) : Prop :=
+ Inductive Inhabited (B:Ensemble) : Prop :=
Inhabited_intro : forall x:U, In B x -> Inhabited B.
+
+ Definition Strict_Included (B C:Ensemble) : Prop := Included B C /\ B <> C.
+
+ Definition Same_set (B C:Ensemble) : Prop := Included B C /\ Included C B.
+
+ (** Extensionality Axiom *)
-Definition Strict_Included (B C:Ensemble) : Prop := Included B C /\ B <> C.
-
-Definition Same_set (B C:Ensemble) : Prop := Included B C /\ Included C B.
-
-(** Extensionality Axiom *)
-
-Axiom Extensionality_Ensembles : forall A B:Ensemble, Same_set A B -> A = B.
-Hint Resolve Extensionality_Ensembles.
+ Axiom Extensionality_Ensembles : forall A B:Ensemble, Same_set A B -> A = B.
End Ensembles.
@@ -98,4 +97,4 @@ Hint Unfold In Included Same_set Strict_Included Add Setminus Subtract: sets
Hint Resolve Union_introl Union_intror Intersection_intro In_singleton
Couple_l Couple_r Triple_l Triple_m Triple_r Disjoint_intro
- Extensionality_Ensembles: sets v62. \ No newline at end of file
+ Extensionality_Ensembles: sets v62.
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.
diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v
index ddbf62e4..91717f9e 100644
--- a/theories/Sets/Finite_sets_facts.v
+++ b/theories/Sets/Finite_sets_facts.v
@@ -24,7 +24,7 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Finite_sets_facts.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Finite_sets_facts.v 9245 2006-10-17 12:53:34Z notin $ i*)
Require Export Finite_sets.
Require Export Constructive_sets.
@@ -37,311 +37,308 @@ Require Export Gt.
Require Export Lt.
Section Finite_sets_facts.
-Variable U : Type.
+ Variable U : Type.
-Lemma finite_cardinal :
- forall X:Ensemble U, Finite U X -> exists n : nat, cardinal U X n.
-Proof.
-induction 1 as [| A _ [n H]].
-exists 0; auto with sets.
-exists (S n); auto with sets.
-Qed.
+ Lemma finite_cardinal :
+ forall X:Ensemble U, Finite U X -> exists n : nat, cardinal U X n.
+ Proof.
+ induction 1 as [| A _ [n H]].
+ exists 0; auto with sets.
+ exists (S n); auto with sets.
+ Qed.
-Lemma cardinal_finite :
- forall (X:Ensemble U) (n:nat), cardinal U X n -> Finite U X.
-Proof.
-induction 1; auto with sets.
-Qed.
+ Lemma cardinal_finite :
+ forall (X:Ensemble U) (n:nat), cardinal U X n -> Finite U X.
+ Proof.
+ induction 1; auto with sets.
+ Qed.
-Theorem Add_preserves_Finite :
- forall (X:Ensemble U) (x:U), Finite U X -> Finite U (Add U X x).
-Proof.
-intros X x H'.
-elim (classic (In U X x)); intro H'0; auto with sets.
-rewrite (Non_disjoint_union U X x); auto with sets.
-Qed.
-Hint Resolve Add_preserves_Finite.
+ Theorem Add_preserves_Finite :
+ forall (X:Ensemble U) (x:U), Finite U X -> Finite U (Add U X x).
+ Proof.
+ intros X x H'.
+ elim (classic (In U X x)); intro H'0; auto with sets.
+ rewrite (Non_disjoint_union U X x); auto with sets.
+ Qed.
-Theorem Singleton_is_finite : forall x:U, Finite U (Singleton U x).
-Proof.
-intro x; rewrite <- (Empty_set_zero U (Singleton U x)).
-change (Finite U (Add U (Empty_set U) x)) in |- *; auto with sets.
-Qed.
-Hint Resolve Singleton_is_finite.
+ Theorem Singleton_is_finite : forall x:U, Finite U (Singleton U x).
+ Proof.
+ intro x; rewrite <- (Empty_set_zero U (Singleton U x)).
+ change (Finite U (Add U (Empty_set U) x)) in |- *; auto with sets.
+ Qed.
-Theorem Union_preserves_Finite :
- forall X Y:Ensemble U, Finite U X -> Finite U Y -> Finite U (Union U X Y).
-Proof.
-intros X Y H'; elim H'.
-rewrite (Empty_set_zero U Y); auto with sets.
-intros A H'0 H'1 x H'2 H'3.
-rewrite (Union_commutative U (Add U A x) Y).
-rewrite <- (Union_add U Y A x).
-rewrite (Union_commutative U Y A); auto with sets.
-Qed.
+ Theorem Union_preserves_Finite :
+ forall X Y:Ensemble U, Finite U X -> Finite U Y -> Finite U (Union U X Y).
+ Proof.
+ intros X Y H; induction H as [|A Fin_A Hind x].
+ rewrite (Empty_set_zero U Y). trivial.
+ intros.
+ rewrite (Union_commutative U (Add U A x) Y).
+ rewrite <- (Union_add U Y A x).
+ rewrite (Union_commutative U Y A).
+ apply Add_preserves_Finite.
+ apply Hind. assumption.
+ Qed.
-Lemma Finite_downward_closed :
- forall A:Ensemble U,
- Finite U A -> forall X:Ensemble U, Included U X A -> Finite U X.
-Proof.
-intros A H'; elim H'; auto with sets.
-intros X H'0.
-rewrite (less_than_empty U X H'0); auto with sets.
-intros; elim Included_Add with U X A0 x; auto with sets.
-destruct 1 as [A' [H5 H6]].
-rewrite H5; auto with sets.
-Qed.
+ Lemma Finite_downward_closed :
+ forall A:Ensemble U,
+ Finite U A -> forall X:Ensemble U, Included U X A -> Finite U X.
+ Proof.
+ intros A H'; elim H'; auto with sets.
+ intros X H'0.
+ rewrite (less_than_empty U X H'0); auto with sets.
+ intros; elim Included_Add with U X A0 x; auto with sets.
+ destruct 1 as [A' [H5 H6]].
+ rewrite H5; auto with sets.
+ Qed.
-Lemma Intersection_preserves_finite :
- forall A:Ensemble U,
- Finite U A -> forall X:Ensemble U, Finite U (Intersection U X A).
-Proof.
-intros A H' X; apply Finite_downward_closed with A; auto with sets.
-Qed.
+ Lemma Intersection_preserves_finite :
+ forall A:Ensemble U,
+ Finite U A -> forall X:Ensemble U, Finite U (Intersection U X A).
+ Proof.
+ intros A H' X; apply Finite_downward_closed with A; auto with sets.
+ Qed.
+
+ Lemma cardinalO_empty :
+ forall X:Ensemble U, cardinal U X 0 -> X = Empty_set U.
+ Proof.
+ intros X H; apply (cardinal_invert U X 0); trivial with sets.
+ Qed.
-Lemma cardinalO_empty :
- forall X:Ensemble U, cardinal U X 0 -> X = Empty_set U.
-Proof.
-intros X H; apply (cardinal_invert U X 0); trivial with sets.
-Qed.
-Hint Resolve cardinalO_empty.
+ Lemma inh_card_gt_O :
+ forall X:Ensemble U, Inhabited U X -> forall n:nat, cardinal U X n -> n > 0.
+ Proof.
+ induction 1 as [x H'].
+ intros n H'0.
+ elim (gt_O_eq n); auto with sets.
+ intro H'1; generalize H'; generalize H'0.
+ rewrite <- H'1; intro H'2.
+ rewrite (cardinalO_empty X); auto with sets.
+ intro H'3; elim H'3.
+ Qed.
-Lemma inh_card_gt_O :
- forall X:Ensemble U, Inhabited U X -> forall n:nat, cardinal U X n -> n > 0.
-Proof.
-induction 1 as [x H'].
-intros n H'0.
-elim (gt_O_eq n); auto with sets.
-intro H'1; generalize H'; generalize H'0.
-rewrite <- H'1; intro H'2.
-rewrite (cardinalO_empty X); auto with sets.
-intro H'3; elim H'3.
-Qed.
+ Lemma card_soustr_1 :
+ forall (X:Ensemble U) (n:nat),
+ cardinal U X n ->
+ forall x:U, In U X x -> cardinal U (Subtract U X x) (pred n).
+ Proof.
+ intros X n H'; elim H'.
+ intros x H'0; elim H'0.
+ clear H' n X.
+ intros X n H' H'0 x H'1 x0 H'2.
+ elim (classic (In U X x0)).
+ intro H'4; rewrite (add_soustr_xy U X x x0).
+ elim (classic (x = x0)).
+ intro H'5.
+ absurd (In U X x0); auto with sets.
+ rewrite <- H'5; auto with sets.
+ intro H'3; try assumption.
+ cut (S (pred n) = pred (S n)).
+ intro H'5; rewrite <- H'5.
+ apply card_add; auto with sets.
+ red in |- *; intro H'6; elim H'6.
+ intros H'7 H'8; try assumption.
+ elim H'1; auto with sets.
+ unfold pred at 2 in |- *; symmetry in |- *.
+ apply S_pred with (m := 0).
+ change (n > 0) in |- *.
+ apply inh_card_gt_O with (X := X); auto with sets.
+ apply Inhabited_intro with (x := x0); auto with sets.
+ red in |- *; intro H'3.
+ apply H'1.
+ elim H'3; auto with sets.
+ rewrite H'3; auto with sets.
+ elim (classic (x = x0)).
+ intro H'3; rewrite <- H'3.
+ cut (Subtract U (Add U X x) x = X); auto with sets.
+ intro H'4; rewrite H'4; auto with sets.
+ intros H'3 H'4; try assumption.
+ absurd (In U (Add U X x) x0); auto with sets.
+ red in |- *; intro H'5; try exact H'5.
+ lapply (Add_inv U X x x0); tauto.
+ Qed.
-Lemma card_soustr_1 :
- forall (X:Ensemble U) (n:nat),
- cardinal U X n ->
- forall x:U, In U X x -> cardinal U (Subtract U X x) (pred n).
-Proof.
-intros X n H'; elim H'.
-intros x H'0; elim H'0.
-clear H' n X.
-intros X n H' H'0 x H'1 x0 H'2.
-elim (classic (In U X x0)).
-intro H'4; rewrite (add_soustr_xy U X x x0).
-elim (classic (x = x0)).
-intro H'5.
-absurd (In U X x0); auto with sets.
-rewrite <- H'5; auto with sets.
-intro H'3; try assumption.
-cut (S (pred n) = pred (S n)).
-intro H'5; rewrite <- H'5.
-apply card_add; auto with sets.
-red in |- *; intro H'6; elim H'6.
-intros H'7 H'8; try assumption.
-elim H'1; auto with sets.
-unfold pred at 2 in |- *; symmetry in |- *.
-apply S_pred with (m := 0).
-change (n > 0) in |- *.
-apply inh_card_gt_O with (X := X); auto with sets.
-apply Inhabited_intro with (x := x0); auto with sets.
-red in |- *; intro H'3.
-apply H'1.
-elim H'3; auto with sets.
-rewrite H'3; auto with sets.
-elim (classic (x = x0)).
-intro H'3; rewrite <- H'3.
-cut (Subtract U (Add U X x) x = X); auto with sets.
-intro H'4; rewrite H'4; auto with sets.
-intros H'3 H'4; try assumption.
-absurd (In U (Add U X x) x0); auto with sets.
-red in |- *; intro H'5; try exact H'5.
-lapply (Add_inv U X x x0); tauto.
-Qed.
+ Lemma cardinal_is_functional :
+ forall (X:Ensemble U) (c1:nat),
+ cardinal U X c1 ->
+ forall (Y:Ensemble U) (c2:nat), cardinal U Y c2 -> X = Y -> c1 = c2.
+ Proof.
+ intros X c1 H'; elim H'.
+ intros Y c2 H'0; elim H'0; auto with sets.
+ intros A n H'1 H'2 x H'3 H'5.
+ elim (not_Empty_Add U A x); auto with sets.
+ clear H' c1 X.
+ intros X n H' H'0 x H'1 Y c2 H'2.
+ elim H'2.
+ intro H'3.
+ elim (not_Empty_Add U X x); auto with sets.
+ clear H'2 c2 Y.
+ intros X0 c2 H'2 H'3 x0 H'4 H'5.
+ elim (classic (In U X0 x)).
+ intro H'6; apply f_equal with nat.
+ apply H'0 with (Y := Subtract U (Add U X0 x0) x).
+ elimtype (pred (S c2) = c2); auto with sets.
+ apply card_soustr_1; auto with sets.
+ rewrite <- H'5.
+ apply Sub_Add_new; auto with sets.
+ elim (classic (x = x0)).
+ intros H'6 H'7; apply f_equal with nat.
+ apply H'0 with (Y := X0); auto with sets.
+ apply Simplify_add with (x := x); auto with sets.
+ pattern x at 2 in |- *; rewrite H'6; auto with sets.
+ intros H'6 H'7.
+ absurd (Add U X x = Add U X0 x0); auto with sets.
+ clear H'0 H' H'3 n H'5 H'4 H'2 H'1 c2.
+ red in |- *; intro H'.
+ lapply (Extension U (Add U X x) (Add U X0 x0)); auto with sets.
+ clear H'.
+ intro H'; red in H'.
+ elim H'; intros H'0 H'1; red in H'0; clear H' H'1.
+ absurd (In U (Add U X0 x0) x); auto with sets.
+ lapply (Add_inv U X0 x0 x); [ intuition | apply (H'0 x); apply Add_intro2 ].
+ Qed.
-Lemma cardinal_is_functional :
- forall (X:Ensemble U) (c1:nat),
- cardinal U X c1 ->
- forall (Y:Ensemble U) (c2:nat), cardinal U Y c2 -> X = Y -> c1 = c2.
-Proof.
-intros X c1 H'; elim H'.
-intros Y c2 H'0; elim H'0; auto with sets.
-intros A n H'1 H'2 x H'3 H'5.
-elim (not_Empty_Add U A x); auto with sets.
-clear H' c1 X.
-intros X n H' H'0 x H'1 Y c2 H'2.
-elim H'2.
-intro H'3.
-elim (not_Empty_Add U X x); auto with sets.
-clear H'2 c2 Y.
-intros X0 c2 H'2 H'3 x0 H'4 H'5.
-elim (classic (In U X0 x)).
-intro H'6; apply f_equal with nat.
-apply H'0 with (Y := Subtract U (Add U X0 x0) x).
-elimtype (pred (S c2) = c2); auto with sets.
-apply card_soustr_1; auto with sets.
-rewrite <- H'5.
-apply Sub_Add_new; auto with sets.
-elim (classic (x = x0)).
-intros H'6 H'7; apply f_equal with nat.
-apply H'0 with (Y := X0); auto with sets.
-apply Simplify_add with (x := x); auto with sets.
-pattern x at 2 in |- *; rewrite H'6; auto with sets.
-intros H'6 H'7.
-absurd (Add U X x = Add U X0 x0); auto with sets.
-clear H'0 H' H'3 n H'5 H'4 H'2 H'1 c2.
-red in |- *; intro H'.
-lapply (Extension U (Add U X x) (Add U X0 x0)); auto with sets.
-clear H'.
-intro H'; red in H'.
-elim H'; intros H'0 H'1; red in H'0; clear H' H'1.
-absurd (In U (Add U X0 x0) x); auto with sets.
-lapply (Add_inv U X0 x0 x); [ intuition | apply (H'0 x); apply Add_intro2 ].
-Qed.
+ Lemma cardinal_Empty : forall m:nat, cardinal U (Empty_set U) m -> 0 = m.
+ Proof.
+ intros m Cm; generalize (cardinal_invert U (Empty_set U) m Cm).
+ elim m; auto with sets.
+ intros; elim H0; intros; elim H1; intros; elim H2; intros.
+ elim (not_Empty_Add U x x0 H3).
+ Qed.
-Lemma cardinal_Empty : forall m:nat, cardinal U (Empty_set U) m -> 0 = m.
-Proof.
-intros m Cm; generalize (cardinal_invert U (Empty_set U) m Cm).
-elim m; auto with sets.
-intros; elim H0; intros; elim H1; intros; elim H2; intros.
-elim (not_Empty_Add U x x0 H3).
-Qed.
+ Lemma cardinal_unicity :
+ forall (X:Ensemble U) (n:nat),
+ cardinal U X n -> forall m:nat, cardinal U X m -> n = m.
+ Proof.
+ intros; apply cardinal_is_functional with X X; auto with sets.
+ Qed.
+
+ Lemma card_Add_gen :
+ forall (A:Ensemble U) (x:U) (n n':nat),
+ cardinal U A n -> cardinal U (Add U A x) n' -> n' <= S n.
+ Proof.
+ intros A x n n' H'.
+ elim (classic (In U A x)).
+ intro H'0.
+ rewrite (Non_disjoint_union U A x H'0).
+ intro H'1; cut (n = n').
+ intro E; rewrite E; auto with sets.
+ apply cardinal_unicity with A; auto with sets.
+ intros H'0 H'1.
+ cut (n' = S n).
+ intro E; rewrite E; auto with sets.
+ apply cardinal_unicity with (Add U A x); auto with sets.
+ Qed.
-Lemma cardinal_unicity :
- forall (X:Ensemble U) (n:nat),
- cardinal U X n -> forall m:nat, cardinal U X m -> n = m.
-Proof.
-intros; apply cardinal_is_functional with X X; auto with sets.
-Qed.
+ Lemma incl_st_card_lt :
+ forall (X:Ensemble U) (c1:nat),
+ cardinal U X c1 ->
+ forall (Y:Ensemble U) (c2:nat),
+ cardinal U Y c2 -> Strict_Included U X Y -> c2 > c1.
+ Proof.
+ intros X c1 H'; elim H'.
+ intros Y c2 H'0; elim H'0; auto with sets arith.
+ intro H'1.
+ elim (Strict_Included_strict U (Empty_set U)); auto with sets arith.
+ clear H' c1 X.
+ intros X n H' H'0 x H'1 Y c2 H'2.
+ elim H'2.
+ intro H'3; elim (not_SIncl_empty U (Add U X x)); auto with sets arith.
+ clear H'2 c2 Y.
+ intros X0 c2 H'2 H'3 x0 H'4 H'5; elim (classic (In U X0 x)).
+ intro H'6; apply gt_n_S.
+ apply H'0 with (Y := Subtract U (Add U X0 x0) x).
+ elimtype (pred (S c2) = c2); auto with sets arith.
+ apply card_soustr_1; auto with sets arith.
+ apply incl_st_add_soustr; auto with sets arith.
+ elim (classic (x = x0)).
+ intros H'6 H'7; apply gt_n_S.
+ apply H'0 with (Y := X0); auto with sets arith.
+ apply sincl_add_x with (x := x0).
+ rewrite <- H'6; auto with sets arith.
+ pattern x0 at 1 in |- *; rewrite <- H'6; trivial with sets arith.
+ intros H'6 H'7; red in H'5.
+ elim H'5; intros H'8 H'9; try exact H'8; clear H'5.
+ red in H'8.
+ generalize (H'8 x).
+ intro H'5; lapply H'5; auto with sets arith.
+ intro H; elim Add_inv with U X0 x0 x; auto with sets arith.
+ intro; absurd (In U X0 x); auto with sets arith.
+ intro; absurd (x = x0); auto with sets arith.
+ Qed.
-Lemma card_Add_gen :
- forall (A:Ensemble U) (x:U) (n n':nat),
- cardinal U A n -> cardinal U (Add U A x) n' -> n' <= S n.
-Proof.
-intros A x n n' H'.
-elim (classic (In U A x)).
-intro H'0.
-rewrite (Non_disjoint_union U A x H'0).
-intro H'1; cut (n = n').
-intro E; rewrite E; auto with sets.
-apply cardinal_unicity with A; auto with sets.
-intros H'0 H'1.
-cut (n' = S n).
-intro E; rewrite E; auto with sets.
-apply cardinal_unicity with (Add U A x); auto with sets.
-Qed.
+ Lemma incl_card_le :
+ forall (X Y:Ensemble U) (n m:nat),
+ cardinal U X n -> cardinal U Y m -> Included U X Y -> n <= m.
+ Proof.
+ intros; elim Included_Strict_Included with U X Y; auto with sets arith; intro.
+ cut (m > n); auto with sets arith.
+ apply incl_st_card_lt with (X := X) (Y := Y); auto with sets arith.
+ generalize H0; rewrite <- H2; intro.
+ cut (n = m).
+ intro E; rewrite E; auto with sets arith.
+ apply cardinal_unicity with X; auto with sets arith.
+ Qed.
+
+ Lemma G_aux :
+ forall P:Ensemble U -> Prop,
+ (forall X:Ensemble U,
+ Finite U X ->
+ (forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
+ P (Empty_set U).
+ Proof.
+ intros P H'; try assumption.
+ apply H'; auto with sets.
+ clear H'; auto with sets.
+ intros Y H'; try assumption.
+ red in H'.
+ elim H'; intros H'0 H'1; try exact H'1; clear H'.
+ lapply (less_than_empty U Y); [ intro H'3; try exact H'3 | assumption ].
+ elim H'1; auto with sets.
+ Qed.
-Lemma incl_st_card_lt :
- forall (X:Ensemble U) (c1:nat),
- cardinal U X c1 ->
- forall (Y:Ensemble U) (c2:nat),
- cardinal U Y c2 -> Strict_Included U X Y -> c2 > c1.
-Proof.
-intros X c1 H'; elim H'.
-intros Y c2 H'0; elim H'0; auto with sets arith.
-intro H'1.
-elim (Strict_Included_strict U (Empty_set U)); auto with sets arith.
-clear H' c1 X.
-intros X n H' H'0 x H'1 Y c2 H'2.
-elim H'2.
-intro H'3; elim (not_SIncl_empty U (Add U X x)); auto with sets arith.
-clear H'2 c2 Y.
-intros X0 c2 H'2 H'3 x0 H'4 H'5; elim (classic (In U X0 x)).
-intro H'6; apply gt_n_S.
-apply H'0 with (Y := Subtract U (Add U X0 x0) x).
-elimtype (pred (S c2) = c2); auto with sets arith.
-apply card_soustr_1; auto with sets arith.
-apply incl_st_add_soustr; auto with sets arith.
-elim (classic (x = x0)).
-intros H'6 H'7; apply gt_n_S.
-apply H'0 with (Y := X0); auto with sets arith.
-apply sincl_add_x with (x := x0).
-rewrite <- H'6; auto with sets arith.
-pattern x0 at 1 in |- *; rewrite <- H'6; trivial with sets arith.
-intros H'6 H'7; red in H'5.
-elim H'5; intros H'8 H'9; try exact H'8; clear H'5.
-red in H'8.
-generalize (H'8 x).
-intro H'5; lapply H'5; auto with sets arith.
-intro H; elim Add_inv with U X0 x0 x; auto with sets arith.
-intro; absurd (In U X0 x); auto with sets arith.
-intro; absurd (x = x0); auto with sets arith.
-Qed.
+ Lemma Generalized_induction_on_finite_sets :
+ forall P:Ensemble U -> Prop,
+ (forall X:Ensemble U,
+ Finite U X ->
+ (forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
+ forall X:Ensemble U, Finite U X -> P X.
+ Proof.
+ intros P H'0 X H'1.
+ generalize P H'0; clear H'0 P.
+ elim H'1.
+ intros P H'0.
+ apply G_aux; auto with sets.
+ clear H'1 X.
+ intros A H' H'0 x H'1 P H'3.
+ cut (forall Y:Ensemble U, Included U Y (Add U A x) -> P Y); auto with sets.
+ generalize H'1.
+ apply H'0.
+ intros X K H'5 L Y H'6; apply H'3; auto with sets.
+ apply Finite_downward_closed with (A := Add U X x); auto with sets.
+ intros Y0 H'7.
+ elim (Strict_inclusion_is_transitive_with_inclusion U Y0 Y (Add U X x));
+ auto with sets.
+ intros H'2 H'4.
+ elim (Included_Add U Y0 X x);
+ [ intro H'14
+ | intro H'14; elim H'14; intros A' E; elim E; intros H'15 H'16; clear E H'14
+ | idtac ]; auto with sets.
+ elim (Included_Strict_Included U Y0 X); auto with sets.
+ intro H'9; apply H'5 with (Y := Y0); auto with sets.
+ intro H'9; rewrite H'9.
+ apply H'3; auto with sets.
+ intros Y1 H'8; elim H'8.
+ intros H'10 H'11; apply H'5 with (Y := Y1); auto with sets.
+ elim (Included_Strict_Included U A' X); auto with sets.
+ intro H'8; apply H'5 with (Y := A'); auto with sets.
+ rewrite <- H'15; auto with sets.
+ intro H'8.
+ elim H'7.
+ intros H'9 H'10; apply H'10 || elim H'10; try assumption.
+ generalize H'6.
+ rewrite <- H'8.
+ rewrite <- H'15; auto with sets.
+ Qed.
-Lemma incl_card_le :
- forall (X Y:Ensemble U) (n m:nat),
- cardinal U X n -> cardinal U Y m -> Included U X Y -> n <= m.
-Proof.
-intros; elim Included_Strict_Included with U X Y; auto with sets arith; intro.
-cut (m > n); auto with sets arith.
-apply incl_st_card_lt with (X := X) (Y := Y); auto with sets arith.
-generalize H0; rewrite <- H2; intro.
-cut (n = m).
-intro E; rewrite E; auto with sets arith.
-apply cardinal_unicity with X; auto with sets arith.
-Qed.
-
-Lemma G_aux :
- forall P:Ensemble U -> Prop,
- (forall X:Ensemble U,
- Finite U X ->
- (forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
- P (Empty_set U).
-Proof.
-intros P H'; try assumption.
-apply H'; auto with sets.
-clear H'; auto with sets.
-intros Y H'; try assumption.
-red in H'.
-elim H'; intros H'0 H'1; try exact H'1; clear H'.
-lapply (less_than_empty U Y); [ intro H'3; try exact H'3 | assumption ].
-elim H'1; auto with sets.
-Qed.
-
-Hint Unfold not.
-
-Lemma Generalized_induction_on_finite_sets :
- forall P:Ensemble U -> Prop,
- (forall X:Ensemble U,
- Finite U X ->
- (forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
- forall X:Ensemble U, Finite U X -> P X.
-Proof.
-intros P H'0 X H'1.
-generalize P H'0; clear H'0 P.
-elim H'1.
-intros P H'0.
-apply G_aux; auto with sets.
-clear H'1 X.
-intros A H' H'0 x H'1 P H'3.
-cut (forall Y:Ensemble U, Included U Y (Add U A x) -> P Y); auto with sets.
-generalize H'1.
-apply H'0.
-intros X K H'5 L Y H'6; apply H'3; auto with sets.
-apply Finite_downward_closed with (A := Add U X x); auto with sets.
-intros Y0 H'7.
-elim (Strict_inclusion_is_transitive_with_inclusion U Y0 Y (Add U X x));
- auto with sets.
-intros H'2 H'4.
-elim (Included_Add U Y0 X x);
- [ intro H'14
- | intro H'14; elim H'14; intros A' E; elim E; intros H'15 H'16; clear E H'14
- | idtac ]; auto with sets.
-elim (Included_Strict_Included U Y0 X); auto with sets.
-intro H'9; apply H'5 with (Y := Y0); auto with sets.
-intro H'9; rewrite H'9.
-apply H'3; auto with sets.
-intros Y1 H'8; elim H'8.
-intros H'10 H'11; apply H'5 with (Y := Y1); auto with sets.
-elim (Included_Strict_Included U A' X); auto with sets.
-intro H'8; apply H'5 with (Y := A'); auto with sets.
-rewrite <- H'15; auto with sets.
-intro H'8.
-elim H'7.
-intros H'9 H'10; apply H'10 || elim H'10; try assumption.
-generalize H'6.
-rewrite <- H'8.
-rewrite <- H'15; auto with sets.
-Qed.
-
-End Finite_sets_facts. \ No newline at end of file
+End Finite_sets_facts.
diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v
index c97aa127..d3591acf 100644
--- a/theories/Sets/Image.v
+++ b/theories/Sets/Image.v
@@ -24,7 +24,7 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Image.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Image.v 9245 2006-10-17 12:53:34Z notin $ i*)
Require Export Finite_sets.
Require Export Constructive_sets.
@@ -39,167 +39,167 @@ Require Export Le.
Require Export Finite_sets_facts.
Section Image.
-Variables U V : Type.
-
-Inductive Im (X:Ensemble U) (f:U -> V) : Ensemble V :=
+ Variables U V : Type.
+
+ Inductive Im (X:Ensemble U) (f:U -> V) : Ensemble V :=
Im_intro : forall x:U, In _ X x -> forall y:V, y = f x -> In _ (Im X f) y.
+
+ Lemma Im_def :
+ forall (X:Ensemble U) (f:U -> V) (x:U), In _ X x -> In _ (Im X f) (f x).
+ Proof.
+ intros X f x H'; try assumption.
+ apply Im_intro with (x := x); auto with sets.
+ Qed.
+
+ Lemma Im_add :
+ forall (X:Ensemble U) (x:U) (f:U -> V),
+ Im (Add _ X x) f = Add _ (Im X f) (f x).
+ Proof.
+ intros X x f.
+ apply Extensionality_Ensembles.
+ split; red in |- *; intros x0 H'.
+ elim H'; intros.
+ rewrite H0.
+ elim Add_inv with U X x x1; auto using Im_def with sets.
+ destruct 1; auto using Im_def with sets.
+ elim Add_inv with V (Im X f) (f x) x0.
+ destruct 1 as [x0 H y H0].
+ rewrite H0; auto using Im_def with sets.
+ destruct 1; auto using Im_def with sets.
+ trivial.
+ Qed.
+
+ Lemma image_empty : forall f:U -> V, Im (Empty_set U) f = Empty_set V.
+ Proof.
+ intro f; try assumption.
+ apply Extensionality_Ensembles.
+ split; auto with sets.
+ red in |- *.
+ intros x H'; elim H'.
+ intros x0 H'0; elim H'0; auto with sets.
+ Qed.
+
+ Lemma finite_image :
+ forall (X:Ensemble U) (f:U -> V), Finite _ X -> Finite _ (Im X f).
+ Proof.
+ intros X f H'; elim H'.
+ rewrite (image_empty f); auto with sets.
+ intros A H'0 H'1 x H'2; clear H' X.
+ rewrite (Im_add A x f); auto with sets.
+ apply Add_preserves_Finite; auto with sets.
+ Qed.
+
+ Lemma Im_inv :
+ forall (X:Ensemble U) (f:U -> V) (y:V),
+ In _ (Im X f) y -> exists x : U, In _ X x /\ f x = y.
+ Proof.
+ intros X f y H'; elim H'.
+ intros x H'0 y0 H'1; rewrite H'1.
+ exists x; auto with sets.
+ Qed.
+
+ Definition injective (f:U -> V) := forall x y:U, f x = f y -> x = y.
+
+ Lemma not_injective_elim :
+ forall f:U -> V,
+ ~ injective f -> exists x : _, (exists y : _, f x = f y /\ x <> y).
+ Proof.
+ unfold injective in |- *; intros f H.
+ cut (exists x : _, ~ (forall y:U, f x = f y -> x = y)).
+ 2: apply not_all_ex_not with (P := fun x:U => forall y:U, f x = f y -> x = y);
+ trivial with sets.
+ destruct 1 as [x C]; exists x.
+ cut (exists y : _, ~ (f x = f y -> x = y)).
+ 2: apply not_all_ex_not with (P := fun y:U => f x = f y -> x = y);
+ trivial with sets.
+ destruct 1 as [y D]; exists y.
+ apply imply_to_and; trivial with sets.
+ Qed.
+
+ Lemma cardinal_Im_intro :
+ forall (A:Ensemble U) (f:U -> V) (n:nat),
+ cardinal _ A n -> exists p : nat, cardinal _ (Im A f) p.
+ Proof.
+ intros.
+ apply finite_cardinal; apply finite_image.
+ apply cardinal_finite with n; trivial with sets.
+ Qed.
+
+ Lemma In_Image_elim :
+ forall (A:Ensemble U) (f:U -> V),
+ injective f -> forall x:U, In _ (Im A f) (f x) -> In _ A x.
+ Proof.
+ intros.
+ elim Im_inv with A f (f x); trivial with sets.
+ intros z C; elim C; intros InAz E.
+ elim (H z x E); trivial with sets.
+ Qed.
+
+ Lemma injective_preserves_cardinal :
+ forall (A:Ensemble U) (f:U -> V) (n:nat),
+ injective f ->
+ cardinal _ A n -> forall n':nat, cardinal _ (Im A f) n' -> n' = n.
+ Proof.
+ induction 2 as [| A n H'0 H'1 x H'2]; auto with sets.
+ rewrite (image_empty f).
+ intros n' CE.
+ apply cardinal_unicity with V (Empty_set V); auto with sets.
+ intro n'.
+ rewrite (Im_add A x f).
+ intro H'3.
+ elim cardinal_Im_intro with A f n; trivial with sets.
+ intros i CI.
+ lapply (H'1 i); trivial with sets.
+ cut (~ In _ (Im A f) (f x)).
+ intros H0 H1.
+ apply cardinal_unicity with V (Add _ (Im A f) (f x)); trivial with sets.
+ apply card_add; auto with sets.
+ rewrite <- H1; trivial with sets.
+ red in |- *; intro; apply H'2.
+ apply In_Image_elim with f; trivial with sets.
+ Qed.
+
+ Lemma cardinal_decreases :
+ forall (A:Ensemble U) (f:U -> V) (n:nat),
+ cardinal U A n -> forall n':nat, cardinal V (Im A f) n' -> n' <= n.
+ Proof.
+ induction 1 as [| A n H'0 H'1 x H'2]; auto with sets.
+ rewrite (image_empty f); intros.
+ cut (n' = 0).
+ intro E; rewrite E; trivial with sets.
+ apply cardinal_unicity with V (Empty_set V); auto with sets.
+ intro n'.
+ rewrite (Im_add A x f).
+ elim cardinal_Im_intro with A f n; trivial with sets.
+ intros p C H'3.
+ apply le_trans with (S p).
+ apply card_Add_gen with V (Im A f) (f x); trivial with sets.
+ apply le_n_S; auto with sets.
+ Qed.
+
+ Theorem Pigeonhole :
+ forall (A:Ensemble U) (f:U -> V) (n:nat),
+ cardinal U A n ->
+ forall n':nat, cardinal V (Im A f) n' -> n' < n -> ~ injective f.
+ Proof.
+ unfold not in |- *; intros A f n CAn n' CIfn' ltn'n I.
+ cut (n' = n).
+ intro E; generalize ltn'n; rewrite E; exact (lt_irrefl n).
+ apply injective_preserves_cardinal with (A := A) (f := f) (n := n);
+ trivial with sets.
+ Qed.
+
+ Lemma Pigeonhole_principle :
+ forall (A:Ensemble U) (f:U -> V) (n:nat),
+ cardinal _ A n ->
+ forall n':nat,
+ cardinal _ (Im A f) n' ->
+ n' < n -> exists x : _, (exists y : _, f x = f y /\ x <> y).
+ Proof.
+ intros; apply not_injective_elim.
+ apply Pigeonhole with A n n'; trivial with sets.
+ Qed.
-Lemma Im_def :
- forall (X:Ensemble U) (f:U -> V) (x:U), In _ X x -> In _ (Im X f) (f x).
-Proof.
-intros X f x H'; try assumption.
-apply Im_intro with (x := x); auto with sets.
-Qed.
-Hint Resolve Im_def.
-
-Lemma Im_add :
- forall (X:Ensemble U) (x:U) (f:U -> V),
- Im (Add _ X x) f = Add _ (Im X f) (f x).
-Proof.
-intros X x f.
-apply Extensionality_Ensembles.
-split; red in |- *; intros x0 H'.
-elim H'; intros.
-rewrite H0.
-elim Add_inv with U X x x1; auto with sets.
-destruct 1; auto with sets.
-elim Add_inv with V (Im X f) (f x) x0; auto with sets.
-destruct 1 as [x0 H y H0].
-rewrite H0; auto with sets.
-destruct 1; auto with sets.
-Qed.
-
-Lemma image_empty : forall f:U -> V, Im (Empty_set U) f = Empty_set V.
-Proof.
-intro f; try assumption.
-apply Extensionality_Ensembles.
-split; auto with sets.
-red in |- *.
-intros x H'; elim H'.
-intros x0 H'0; elim H'0; auto with sets.
-Qed.
-Hint Resolve image_empty.
-
-Lemma finite_image :
- forall (X:Ensemble U) (f:U -> V), Finite _ X -> Finite _ (Im X f).
-Proof.
-intros X f H'; elim H'.
-rewrite (image_empty f); auto with sets.
-intros A H'0 H'1 x H'2; clear H' X.
-rewrite (Im_add A x f); auto with sets.
-apply Add_preserves_Finite; auto with sets.
-Qed.
-Hint Resolve finite_image.
-
-Lemma Im_inv :
- forall (X:Ensemble U) (f:U -> V) (y:V),
- In _ (Im X f) y -> exists x : U, In _ X x /\ f x = y.
-Proof.
-intros X f y H'; elim H'.
-intros x H'0 y0 H'1; rewrite H'1.
-exists x; auto with sets.
-Qed.
-
-Definition injective (f:U -> V) := forall x y:U, f x = f y -> x = y.
-
-Lemma not_injective_elim :
- forall f:U -> V,
- ~ injective f -> exists x : _, (exists y : _, f x = f y /\ x <> y).
-Proof.
-unfold injective in |- *; intros f H.
-cut (exists x : _, ~ (forall y:U, f x = f y -> x = y)).
-2: apply not_all_ex_not with (P := fun x:U => forall y:U, f x = f y -> x = y);
- trivial with sets.
-destruct 1 as [x C]; exists x.
-cut (exists y : _, ~ (f x = f y -> x = y)).
-2: apply not_all_ex_not with (P := fun y:U => f x = f y -> x = y);
- trivial with sets.
-destruct 1 as [y D]; exists y.
-apply imply_to_and; trivial with sets.
-Qed.
-
-Lemma cardinal_Im_intro :
- forall (A:Ensemble U) (f:U -> V) (n:nat),
- cardinal _ A n -> exists p : nat, cardinal _ (Im A f) p.
-Proof.
-intros.
-apply finite_cardinal; apply finite_image.
-apply cardinal_finite with n; trivial with sets.
-Qed.
-
-Lemma In_Image_elim :
- forall (A:Ensemble U) (f:U -> V),
- injective f -> forall x:U, In _ (Im A f) (f x) -> In _ A x.
-Proof.
-intros.
-elim Im_inv with A f (f x); trivial with sets.
-intros z C; elim C; intros InAz E.
-elim (H z x E); trivial with sets.
-Qed.
-
-Lemma injective_preserves_cardinal :
- forall (A:Ensemble U) (f:U -> V) (n:nat),
- injective f ->
- cardinal _ A n -> forall n':nat, cardinal _ (Im A f) n' -> n' = n.
-Proof.
-induction 2 as [| A n H'0 H'1 x H'2]; auto with sets.
-rewrite (image_empty f).
-intros n' CE.
-apply cardinal_unicity with V (Empty_set V); auto with sets.
-intro n'.
-rewrite (Im_add A x f).
-intro H'3.
-elim cardinal_Im_intro with A f n; trivial with sets.
-intros i CI.
-lapply (H'1 i); trivial with sets.
-cut (~ In _ (Im A f) (f x)).
-intros H0 H1.
-apply cardinal_unicity with V (Add _ (Im A f) (f x)); trivial with sets.
-apply card_add; auto with sets.
-rewrite <- H1; trivial with sets.
-red in |- *; intro; apply H'2.
-apply In_Image_elim with f; trivial with sets.
-Qed.
-
-Lemma cardinal_decreases :
- forall (A:Ensemble U) (f:U -> V) (n:nat),
- cardinal U A n -> forall n':nat, cardinal V (Im A f) n' -> n' <= n.
-Proof.
-induction 1 as [| A n H'0 H'1 x H'2]; auto with sets.
-rewrite (image_empty f); intros.
-cut (n' = 0).
-intro E; rewrite E; trivial with sets.
-apply cardinal_unicity with V (Empty_set V); auto with sets.
-intro n'.
-rewrite (Im_add A x f).
-elim cardinal_Im_intro with A f n; trivial with sets.
-intros p C H'3.
-apply le_trans with (S p).
-apply card_Add_gen with V (Im A f) (f x); trivial with sets.
-apply le_n_S; auto with sets.
-Qed.
-
-Theorem Pigeonhole :
- forall (A:Ensemble U) (f:U -> V) (n:nat),
- cardinal U A n ->
- forall n':nat, cardinal V (Im A f) n' -> n' < n -> ~ injective f.
-Proof.
-unfold not in |- *; intros A f n CAn n' CIfn' ltn'n I.
-cut (n' = n).
-intro E; generalize ltn'n; rewrite E; exact (lt_irrefl n).
-apply injective_preserves_cardinal with (A := A) (f := f) (n := n);
- trivial with sets.
-Qed.
-
-Lemma Pigeonhole_principle :
- forall (A:Ensemble U) (f:U -> V) (n:nat),
- cardinal _ A n ->
- forall n':nat,
- cardinal _ (Im A f) n' ->
- n' < n -> exists x : _, (exists y : _, f x = f y /\ x <> y).
-Proof.
-intros; apply not_injective_elim.
-apply Pigeonhole with A n n'; trivial with sets.
-Qed.
End Image.
+
Hint Resolve Im_def image_empty finite_image: sets v62. \ No newline at end of file
diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v
index 806e9dde..47554ac4 100644
--- a/theories/Sets/Infinite_sets.v
+++ b/theories/Sets/Infinite_sets.v
@@ -24,7 +24,7 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Infinite_sets.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Infinite_sets.v 9245 2006-10-17 12:53:34Z notin $ i*)
Require Export Finite_sets.
Require Export Constructive_sets.
@@ -40,205 +40,205 @@ Require Export Finite_sets_facts.
Require Export Image.
Section Approx.
-Variable U : Type.
+ Variable U : Type.
-Inductive Approximant (A X:Ensemble U) : Prop :=
+ Inductive Approximant (A X:Ensemble U) : Prop :=
Defn_of_Approximant : Finite U X -> Included U X A -> Approximant A X.
End Approx.
Hint Resolve Defn_of_Approximant.
Section Infinite_sets.
-Variable U : Type.
-
-Lemma make_new_approximant :
- forall A X:Ensemble U,
- ~ Finite U A -> Approximant U A X -> Inhabited U (Setminus U A X).
-Proof.
-intros A X H' H'0.
-elim H'0; intros H'1 H'2.
-apply Strict_super_set_contains_new_element; auto with sets.
-red in |- *; intro H'3; apply H'.
-rewrite <- H'3; auto with sets.
-Qed.
-
-Lemma approximants_grow :
- forall A X:Ensemble U,
- ~ Finite U A ->
- forall n:nat,
- cardinal U X n ->
- Included U X A -> exists Y : _, cardinal U Y (S n) /\ Included U Y A.
-Proof.
-intros A X H' n H'0; elim H'0; auto with sets.
-intro H'1.
-cut (Inhabited U (Setminus U A (Empty_set U))).
-intro H'2; elim H'2.
-intros x H'3.
-exists (Add U (Empty_set U) x); auto with sets.
-split.
-apply card_add; auto with sets.
-cut (In U A x).
-intro H'4; red in |- *; auto with sets.
-intros x0 H'5; elim H'5; auto with sets.
-intros x1 H'6; elim H'6; auto with sets.
-elim H'3; auto with sets.
-apply make_new_approximant; auto with sets.
-intros A0 n0 H'1 H'2 x H'3 H'5.
-lapply H'2; [ intro H'6; elim H'6; clear H'2 | clear H'2 ]; auto with sets.
-intros x0 H'2; try assumption.
-elim H'2; intros H'7 H'8; try exact H'8; clear H'2.
-elim (make_new_approximant A x0); auto with sets.
-intros x1 H'2; try assumption.
-exists (Add U x0 x1); auto with sets.
-split.
-apply card_add; auto with sets.
-elim H'2; auto with sets.
-red in |- *.
-intros x2 H'9; elim H'9; auto with sets.
-intros x3 H'10; elim H'10; auto with sets.
-elim H'2; auto with sets.
-auto with sets.
-apply Defn_of_Approximant; auto with sets.
-apply cardinal_finite with (n := S n0); auto with sets.
-Qed.
-
-Lemma approximants_grow' :
- forall A X:Ensemble U,
- ~ Finite U A ->
- forall n:nat,
- cardinal U X n ->
- Approximant U A X ->
- exists Y : _, cardinal U Y (S n) /\ Approximant U A Y.
-Proof.
-intros A X H' n H'0 H'1; try assumption.
-elim H'1.
-intros H'2 H'3.
-elimtype (exists Y : _, cardinal U Y (S n) /\ Included U Y A).
-intros x H'4; elim H'4; intros H'5 H'6; try exact H'5; clear H'4.
-exists x; auto with sets.
-split; [ auto with sets | idtac ].
-apply Defn_of_Approximant; auto with sets.
-apply cardinal_finite with (n := S n); auto with sets.
-apply approximants_grow with (X := X); auto with sets.
-Qed.
-
-Lemma approximant_can_be_any_size :
- forall A X:Ensemble U,
- ~ Finite U A ->
- forall n:nat, exists Y : _, cardinal U Y n /\ Approximant U A Y.
-Proof.
-intros A H' H'0 n; elim n.
-exists (Empty_set U); auto with sets.
-intros n0 H'1; elim H'1.
-intros x H'2.
-apply approximants_grow' with (X := x); tauto.
-Qed.
-
-Variable V : Type.
-
-Theorem Image_set_continuous :
- forall (A:Ensemble U) (f:U -> V) (X:Ensemble V),
- Finite V X ->
- Included V X (Im U V A f) ->
- exists n : _,
- (exists Y : _, (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X).
-Proof.
-intros A f X H'; elim H'.
-intro H'0; exists 0.
-exists (Empty_set U); auto with sets.
-intros A0 H'0 H'1 x H'2 H'3; try assumption.
-lapply H'1;
- [ intro H'4; elim H'4; intros n E; elim E; clear H'4 H'1 | clear H'1 ];
- auto with sets.
-intros x0 H'1; try assumption.
-exists (S n); try assumption.
-elim H'1; intros H'4 H'5; elim H'4; intros H'6 H'7; try exact H'6;
- clear H'4 H'1.
-clear E.
-generalize H'2.
-rewrite <- H'5.
-intro H'1; try assumption.
-red in H'3.
-generalize (H'3 x).
-intro H'4; lapply H'4; [ intro H'8; try exact H'8; clear H'4 | clear H'4 ];
- auto with sets.
-specialize 5Im_inv with (U := U) (V := V) (X := A) (f := f) (y := x);
- intro H'11; lapply H'11; [ intro H'13; elim H'11; clear H'11 | clear H'11 ];
- auto with sets.
-intros x1 H'4; try assumption.
-apply ex_intro with (x := Add U x0 x1).
-split; [ split; [ try assumption | idtac ] | idtac ].
-apply card_add; auto with sets.
-red in |- *; intro H'9; try exact H'9.
-apply H'1.
-elim H'4; intros H'10 H'11; rewrite <- H'11; clear H'4; auto with sets.
-elim H'4; intros H'9 H'10; try exact H'9; clear H'4; auto with sets.
-red in |- *; auto with sets.
-intros x2 H'4; elim H'4; auto with sets.
-intros x3 H'11; elim H'11; auto with sets.
-elim H'4; intros H'9 H'10; rewrite <- H'10; clear H'4; auto with sets.
-apply Im_add; auto with sets.
-Qed.
-
-Theorem Image_set_continuous' :
- forall (A:Ensemble U) (f:U -> V) (X:Ensemble V),
- Approximant V (Im U V A f) X ->
- exists Y : _, Approximant U A Y /\ Im U V Y f = X.
-Proof.
-intros A f X H'; try assumption.
-cut
- (exists n : _,
- (exists Y : _, (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X)).
-intro H'0; elim H'0; intros n E; elim E; clear H'0.
-intros x H'0; try assumption.
-elim H'0; intros H'1 H'2; elim H'1; intros H'3 H'4; try exact H'3;
- clear H'1 H'0; auto with sets.
-exists x.
-split; [ idtac | try assumption ].
-apply Defn_of_Approximant; auto with sets.
-apply cardinal_finite with (n := n); auto with sets.
-apply Image_set_continuous; auto with sets.
-elim H'; auto with sets.
-elim H'; auto with sets.
-Qed.
-
-Theorem Pigeonhole_bis :
- forall (A:Ensemble U) (f:U -> V),
- ~ Finite U A -> Finite V (Im U V A f) -> ~ injective U V f.
-Proof.
-intros A f H'0 H'1; try assumption.
-elim (Image_set_continuous' A f (Im U V A f)); auto with sets.
-intros x H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2.
-elim (make_new_approximant A x); auto with sets.
-intros x0 H'2; elim H'2.
-intros H'5 H'6.
-elim (finite_cardinal V (Im U V A f)); auto with sets.
-intros n E.
-elim (finite_cardinal U x); auto with sets.
-intros n0 E0.
-apply Pigeonhole with (A := Add U x x0) (n := S n0) (n' := n).
-apply card_add; auto with sets.
-rewrite (Im_add U V x x0 f); auto with sets.
-cut (In V (Im U V x f) (f x0)).
-intro H'8.
-rewrite (Non_disjoint_union V (Im U V x f) (f x0)); auto with sets.
-rewrite H'4; auto with sets.
-elim (Extension V (Im U V x f) (Im U V A f)); auto with sets.
-apply le_lt_n_Sm.
-apply cardinal_decreases with (U := U) (V := V) (A := x) (f := f);
- auto with sets.
-rewrite H'4; auto with sets.
-elim H'3; auto with sets.
-Qed.
-
-Theorem Pigeonhole_ter :
- forall (A:Ensemble U) (f:U -> V) (n:nat),
- injective U V f -> Finite V (Im U V A f) -> Finite U A.
-Proof.
-intros A f H' H'0 H'1.
-apply NNPP.
-red in |- *; intro H'2.
-elim (Pigeonhole_bis A f); auto with sets.
-Qed.
+ Variable U : Type.
+
+ Lemma make_new_approximant :
+ forall A X:Ensemble U,
+ ~ Finite U A -> Approximant U A X -> Inhabited U (Setminus U A X).
+ Proof.
+ intros A X H' H'0.
+ elim H'0; intros H'1 H'2.
+ apply Strict_super_set_contains_new_element; auto with sets.
+ red in |- *; intro H'3; apply H'.
+ rewrite <- H'3; auto with sets.
+ Qed.
+
+ Lemma approximants_grow :
+ forall A X:Ensemble U,
+ ~ Finite U A ->
+ forall n:nat,
+ cardinal U X n ->
+ Included U X A -> exists Y : _, cardinal U Y (S n) /\ Included U Y A.
+ Proof.
+ intros A X H' n H'0; elim H'0; auto with sets.
+ intro H'1.
+ cut (Inhabited U (Setminus U A (Empty_set U))).
+ intro H'2; elim H'2.
+ intros x H'3.
+ exists (Add U (Empty_set U) x); auto with sets.
+ split.
+ apply card_add; auto with sets.
+ cut (In U A x).
+ intro H'4; red in |- *; auto with sets.
+ intros x0 H'5; elim H'5; auto with sets.
+ intros x1 H'6; elim H'6; auto with sets.
+ elim H'3; auto with sets.
+ apply make_new_approximant; auto with sets.
+ intros A0 n0 H'1 H'2 x H'3 H'5.
+ lapply H'2; [ intro H'6; elim H'6; clear H'2 | clear H'2 ]; auto with sets.
+ intros x0 H'2; try assumption.
+ elim H'2; intros H'7 H'8; try exact H'8; clear H'2.
+ elim (make_new_approximant A x0); auto with sets.
+ intros x1 H'2; try assumption.
+ exists (Add U x0 x1); auto with sets.
+ split.
+ apply card_add; auto with sets.
+ elim H'2; auto with sets.
+ red in |- *.
+ intros x2 H'9; elim H'9; auto with sets.
+ intros x3 H'10; elim H'10; auto with sets.
+ elim H'2; auto with sets.
+ auto with sets.
+ apply Defn_of_Approximant; auto with sets.
+ apply cardinal_finite with (n := S n0); auto with sets.
+ Qed.
+
+ Lemma approximants_grow' :
+ forall A X:Ensemble U,
+ ~ Finite U A ->
+ forall n:nat,
+ cardinal U X n ->
+ Approximant U A X ->
+ exists Y : _, cardinal U Y (S n) /\ Approximant U A Y.
+ Proof.
+ intros A X H' n H'0 H'1; try assumption.
+ elim H'1.
+ intros H'2 H'3.
+ elimtype (exists Y : _, cardinal U Y (S n) /\ Included U Y A).
+ intros x H'4; elim H'4; intros H'5 H'6; try exact H'5; clear H'4.
+ exists x; auto with sets.
+ split; [ auto with sets | idtac ].
+ apply Defn_of_Approximant; auto with sets.
+ apply cardinal_finite with (n := S n); auto with sets.
+ apply approximants_grow with (X := X); auto with sets.
+ Qed.
+
+ Lemma approximant_can_be_any_size :
+ forall A X:Ensemble U,
+ ~ Finite U A ->
+ forall n:nat, exists Y : _, cardinal U Y n /\ Approximant U A Y.
+ Proof.
+ intros A H' H'0 n; elim n.
+ exists (Empty_set U); auto with sets.
+ intros n0 H'1; elim H'1.
+ intros x H'2.
+ apply approximants_grow' with (X := x); tauto.
+ Qed.
+
+ Variable V : Type.
+
+ Theorem Image_set_continuous :
+ forall (A:Ensemble U) (f:U -> V) (X:Ensemble V),
+ Finite V X ->
+ Included V X (Im U V A f) ->
+ exists n : _,
+ (exists Y : _, (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X).
+ Proof.
+ intros A f X H'; elim H'.
+ intro H'0; exists 0.
+ exists (Empty_set U); auto with sets.
+ intros A0 H'0 H'1 x H'2 H'3; try assumption.
+ lapply H'1;
+ [ intro H'4; elim H'4; intros n E; elim E; clear H'4 H'1 | clear H'1 ];
+ auto with sets.
+ intros x0 H'1; try assumption.
+ exists (S n); try assumption.
+ elim H'1; intros H'4 H'5; elim H'4; intros H'6 H'7; try exact H'6;
+ clear H'4 H'1.
+ clear E.
+ generalize H'2.
+ rewrite <- H'5.
+ intro H'1; try assumption.
+ red in H'3.
+ generalize (H'3 x).
+ intro H'4; lapply H'4; [ intro H'8; try exact H'8; clear H'4 | clear H'4 ];
+ auto with sets.
+ specialize 5Im_inv with (U := U) (V := V) (X := A) (f := f) (y := x);
+ intro H'11; lapply H'11; [ intro H'13; elim H'11; clear H'11 | clear H'11 ];
+ auto with sets.
+ intros x1 H'4; try assumption.
+ apply ex_intro with (x := Add U x0 x1).
+ split; [ split; [ try assumption | idtac ] | idtac ].
+ apply card_add; auto with sets.
+ red in |- *; intro H'9; try exact H'9.
+ apply H'1.
+ elim H'4; intros H'10 H'11; rewrite <- H'11; clear H'4; auto with sets.
+ elim H'4; intros H'9 H'10; try exact H'9; clear H'4; auto with sets.
+ red in |- *; auto with sets.
+ intros x2 H'4; elim H'4; auto with sets.
+ intros x3 H'11; elim H'11; auto with sets.
+ elim H'4; intros H'9 H'10; rewrite <- H'10; clear H'4; auto with sets.
+ apply Im_add; auto with sets.
+ Qed.
+
+ Theorem Image_set_continuous' :
+ forall (A:Ensemble U) (f:U -> V) (X:Ensemble V),
+ Approximant V (Im U V A f) X ->
+ exists Y : _, Approximant U A Y /\ Im U V Y f = X.
+ Proof.
+ intros A f X H'; try assumption.
+ cut
+ (exists n : _,
+ (exists Y : _, (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X)).
+ intro H'0; elim H'0; intros n E; elim E; clear H'0.
+ intros x H'0; try assumption.
+ elim H'0; intros H'1 H'2; elim H'1; intros H'3 H'4; try exact H'3;
+ clear H'1 H'0; auto with sets.
+ exists x.
+ split; [ idtac | try assumption ].
+ apply Defn_of_Approximant; auto with sets.
+ apply cardinal_finite with (n := n); auto with sets.
+ apply Image_set_continuous; auto with sets.
+ elim H'; auto with sets.
+ elim H'; auto with sets.
+ Qed.
+
+ Theorem Pigeonhole_bis :
+ forall (A:Ensemble U) (f:U -> V),
+ ~ Finite U A -> Finite V (Im U V A f) -> ~ injective U V f.
+ Proof.
+ intros A f H'0 H'1; try assumption.
+ elim (Image_set_continuous' A f (Im U V A f)); auto with sets.
+ intros x H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2.
+ elim (make_new_approximant A x); auto with sets.
+ intros x0 H'2; elim H'2.
+ intros H'5 H'6.
+ elim (finite_cardinal V (Im U V A f)); auto with sets.
+ intros n E.
+ elim (finite_cardinal U x); auto with sets.
+ intros n0 E0.
+ apply Pigeonhole with (A := Add U x x0) (n := S n0) (n' := n).
+ apply card_add; auto with sets.
+ rewrite (Im_add U V x x0 f); auto with sets.
+ cut (In V (Im U V x f) (f x0)).
+ intro H'8.
+ rewrite (Non_disjoint_union V (Im U V x f) (f x0)); auto with sets.
+ rewrite H'4; auto with sets.
+ elim (Extension V (Im U V x f) (Im U V A f)); auto with sets.
+ apply le_lt_n_Sm.
+ apply cardinal_decreases with (U := U) (V := V) (A := x) (f := f);
+ auto with sets.
+ rewrite H'4; auto with sets.
+ elim H'3; auto with sets.
+ Qed.
+
+ Theorem Pigeonhole_ter :
+ forall (A:Ensemble U) (f:U -> V) (n:nat),
+ injective U V f -> Finite V (Im U V A f) -> Finite U A.
+ Proof.
+ intros A f H' H'0 H'1.
+ apply NNPP.
+ red in |- *; intro H'2.
+ elim (Pigeonhole_bis A f); auto with sets.
+ Qed.
End Infinite_sets.
diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v
index cfadd81c..c969ad9c 100644
--- a/theories/Sets/Integers.v
+++ b/theories/Sets/Integers.v
@@ -24,7 +24,7 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Integers.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Integers.v 9245 2006-10-17 12:53:34Z notin $ i*)
Require Export Finite_sets.
Require Export Constructive_sets.
@@ -45,120 +45,117 @@ Require Export Partial_Order.
Require Export Cpo.
Section Integers_sect.
-
-Inductive Integers : Ensemble nat :=
+
+ Inductive Integers : Ensemble nat :=
Integers_defn : forall x:nat, In nat Integers x.
-Hint Resolve Integers_defn.
-
-Lemma le_reflexive : Reflexive nat le.
-Proof.
-red in |- *; auto with arith.
-Qed.
-
-Lemma le_antisym : Antisymmetric nat le.
-Proof.
-red in |- *; intros x y H H'; rewrite (le_antisym x y); auto.
-Qed.
-
-Lemma le_trans : Transitive nat le.
-Proof.
-red in |- *; intros; apply le_trans with y; auto.
-Qed.
-Hint Resolve le_reflexive le_antisym le_trans.
-
-Lemma le_Order : Order nat le.
-Proof.
-auto with sets arith.
-Qed.
-Hint Resolve le_Order.
-
-Lemma triv_nat : forall n:nat, In nat Integers n.
-Proof.
-auto with sets arith.
-Qed.
-Hint Resolve triv_nat.
-
-Definition nat_po : PO nat.
-apply Definition_of_PO with (Carrier_of := Integers) (Rel_of := le);
- auto with sets arith.
-apply Inhabited_intro with (x := 0); auto with sets arith.
-Defined.
-Hint Unfold nat_po.
-
-Lemma le_total_order : Totally_ordered nat nat_po Integers.
-Proof.
-apply Totally_ordered_definition.
-simpl in |- *.
-intros H' x y H'0.
-specialize 2le_or_lt with (n := x) (m := y); intro H'2; elim H'2.
-intro H'1; left; auto with sets arith.
-intro H'1; right.
-cut (y <= x); auto with sets arith.
-Qed.
-Hint Resolve le_total_order.
-
-Lemma Finite_subset_has_lub :
- forall X:Ensemble nat,
- Finite nat X -> exists m : nat, Upper_Bound nat nat_po X m.
-Proof.
-intros X H'; elim H'.
-exists 0.
-apply Upper_Bound_definition; auto with sets arith.
-intros y H'0; elim H'0; auto with sets arith.
-intros A H'0 H'1 x H'2; try assumption.
-elim H'1; intros x0 H'3; clear H'1.
-elim le_total_order.
-simpl in |- *.
-intro H'1; try assumption.
-lapply H'1; [ intro H'4; idtac | try assumption ]; auto with sets arith.
-generalize (H'4 x0 x).
-clear H'4.
-clear H'1.
-intro H'1; lapply H'1;
- [ intro H'4; elim H'4;
- [ intro H'5; try exact H'5; clear H'4 H'1 | intro H'5; clear H'4 H'1 ]
- | clear H'1 ].
-exists x.
-apply Upper_Bound_definition; auto with sets arith; simpl in |- *.
-intros y H'1; elim H'1.
-generalize le_trans.
-intro H'4; red in H'4.
-intros x1 H'6; try assumption.
-apply H'4 with (y := x0); auto with sets arith.
-elim H'3; simpl in |- *; auto with sets arith.
-intros x1 H'4; elim H'4; auto with sets arith.
-exists x0.
-apply Upper_Bound_definition; auto with sets arith; simpl in |- *.
-intros y H'1; elim H'1.
-intros x1 H'4; try assumption.
-elim H'3; simpl in |- *; auto with sets arith.
-intros x1 H'4; elim H'4; auto with sets arith.
-red in |- *.
-intros x1 H'1; elim H'1; auto with sets arith.
-Qed.
-
-Lemma Integers_has_no_ub :
- ~ (exists m : nat, Upper_Bound nat nat_po Integers m).
-Proof.
-red in |- *; intro H'; elim H'.
-intros x H'0.
-elim H'0; intros H'1 H'2.
-cut (In nat Integers (S x)).
-intro H'3.
-specialize 1H'2 with (y := S x); intro H'4; lapply H'4;
- [ intro H'5; clear H'4 | try assumption; clear H'4 ].
-simpl in H'5.
-absurd (S x <= x); auto with arith.
-auto with sets arith.
-Qed.
-Lemma Integers_infinite : ~ Finite nat Integers.
-Proof.
-generalize Integers_has_no_ub.
-intro H'; red in |- *; intro H'0; try exact H'0.
-apply H'.
-apply Finite_subset_has_lub; auto with sets arith.
-Qed.
+ Lemma le_reflexive : Reflexive nat le.
+ Proof.
+ red in |- *; auto with arith.
+ Qed.
+
+ Lemma le_antisym : Antisymmetric nat le.
+ Proof.
+ red in |- *; intros x y H H'; rewrite (le_antisym x y); auto.
+ Qed.
+
+ Lemma le_trans : Transitive nat le.
+ Proof.
+ red in |- *; intros; apply le_trans with y; auto.
+ Qed.
+
+ Lemma le_Order : Order nat le.
+ Proof.
+ split; [exact le_reflexive | exact le_trans | exact le_antisym].
+ Qed.
+
+ Lemma triv_nat : forall n:nat, In nat Integers n.
+ Proof.
+ exact Integers_defn.
+ Qed.
+
+ Definition nat_po : PO nat.
+ apply Definition_of_PO with (Carrier_of := Integers) (Rel_of := le);
+ auto with sets arith.
+ apply Inhabited_intro with (x := 0).
+ apply Integers_defn.
+ exact le_Order.
+ Defined.
+
+ Lemma le_total_order : Totally_ordered nat nat_po Integers.
+ Proof.
+ apply Totally_ordered_definition.
+ simpl in |- *.
+ intros H' x y H'0.
+ specialize 2le_or_lt with (n := x) (m := y); intro H'2; elim H'2.
+ intro H'1; left; auto with sets arith.
+ intro H'1; right.
+ cut (y <= x); auto with sets arith.
+ Qed.
+
+ Lemma Finite_subset_has_lub :
+ forall X:Ensemble nat,
+ Finite nat X -> exists m : nat, Upper_Bound nat nat_po X m.
+ Proof.
+ intros X H'; elim H'.
+ exists 0.
+ apply Upper_Bound_definition.
+ unfold nat_po. simpl. apply triv_nat.
+ intros y H'0; elim H'0; auto with sets arith.
+ intros A H'0 H'1 x H'2; try assumption.
+ elim H'1; intros x0 H'3; clear H'1.
+ elim le_total_order.
+ simpl in |- *.
+ intro H'1; try assumption.
+ lapply H'1; [ intro H'4; idtac | try assumption ]; auto with sets arith.
+ generalize (H'4 x0 x).
+ clear H'4.
+ clear H'1.
+ intro H'1; lapply H'1;
+ [ intro H'4; elim H'4;
+ [ intro H'5; try exact H'5; clear H'4 H'1 | intro H'5; clear H'4 H'1 ]
+ | clear H'1 ].
+ exists x.
+ apply Upper_Bound_definition. simpl in |- *. apply triv_nat.
+ intros y H'1; elim H'1.
+ generalize le_trans.
+ intro H'4; red in H'4.
+ intros x1 H'6; try assumption.
+ apply H'4 with (y := x0). elim H'3; simpl in |- *; auto with sets arith. trivial.
+ intros x1 H'4; elim H'4. unfold nat_po; simpl; trivial.
+ exists x0.
+ apply Upper_Bound_definition.
+ unfold nat_po. simpl. apply triv_nat.
+ intros y H'1; elim H'1.
+ intros x1 H'4; try assumption.
+ elim H'3; simpl in |- *; auto with sets arith.
+ intros x1 H'4; elim H'4; auto with sets arith.
+ red in |- *.
+ intros x1 H'1; elim H'1; apply triv_nat.
+ Qed.
+
+ Lemma Integers_has_no_ub :
+ ~ (exists m : nat, Upper_Bound nat nat_po Integers m).
+ Proof.
+ red in |- *; intro H'; elim H'.
+ intros x H'0.
+ elim H'0; intros H'1 H'2.
+ cut (In nat Integers (S x)).
+ intro H'3.
+ specialize 1H'2 with (y := S x); intro H'4; lapply H'4;
+ [ intro H'5; clear H'4 | try assumption; clear H'4 ].
+ simpl in H'5.
+ absurd (S x <= x); auto with arith.
+ apply triv_nat.
+ Qed.
+
+ Lemma Integers_infinite : ~ Finite nat Integers.
+ Proof.
+ generalize Integers_has_no_ub.
+ intro H'; red in |- *; intro H'0; try exact H'0.
+ apply H'.
+ apply Finite_subset_has_lub; auto with sets arith.
+ Qed.
End Integers_sect.
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index cdc8520c..7084a82d 100644
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Multiset.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Multiset.v 9245 2006-10-17 12:53:34Z notin $ i*)
(* G. Huet 1-9-95 *)
@@ -16,162 +16,156 @@ Set Implicit Arguments.
Section multiset_defs.
-Variable A : Set.
-Variable eqA : A -> A -> Prop.
-Hypothesis Aeq_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+ Variable A : Set.
+ Variable eqA : A -> A -> Prop.
+ Hypothesis Aeq_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
-Inductive multiset : Set :=
+ Inductive multiset : Set :=
Bag : (A -> nat) -> multiset.
-
-Definition EmptyBag := Bag (fun a:A => 0).
-Definition SingletonBag (a:A) :=
- Bag (fun a':A => match Aeq_dec a a' with
- | left _ => 1
- | right _ => 0
- end).
-
-Definition multiplicity (m:multiset) (a:A) : nat := let (f) := m in f a.
-
-(** multiset equality *)
-Definition meq (m1 m2:multiset) :=
- forall a:A, multiplicity m1 a = multiplicity m2 a.
-
-Hint Unfold meq multiplicity.
-
-Lemma meq_refl : forall x:multiset, meq x x.
-Proof.
-destruct x; auto.
-Qed.
-Hint Resolve meq_refl.
-
-Lemma meq_trans : forall x y z:multiset, meq x y -> meq y z -> meq x z.
-Proof.
-unfold meq in |- *.
-destruct x; destruct y; destruct z.
-intros; rewrite H; auto.
-Qed.
-
-Lemma meq_sym : forall x y:multiset, meq x y -> meq y x.
-Proof.
-unfold meq in |- *.
-destruct x; destruct y; auto.
-Qed.
-Hint Immediate meq_sym.
-
-(** multiset union *)
-Definition munion (m1 m2:multiset) :=
- Bag (fun a:A => multiplicity m1 a + multiplicity m2 a).
-
-Lemma munion_empty_left : forall x:multiset, meq x (munion EmptyBag x).
-Proof.
-unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto.
-Qed.
-Hint Resolve munion_empty_left.
-
-Lemma munion_empty_right : forall x:multiset, meq x (munion x EmptyBag).
-Proof.
-unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto.
-Qed.
-
-
-Require Import Plus. (* comm. and ass. of plus *)
-
-Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x).
-Proof.
-unfold meq in |- *; unfold multiplicity in |- *; unfold munion in |- *.
-destruct x; destruct y; auto with arith.
-Qed.
-Hint Resolve munion_comm.
-
-Lemma munion_ass :
- forall x y z:multiset, meq (munion (munion x y) z) (munion x (munion y z)).
-Proof.
-unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.
-destruct x; destruct y; destruct z; auto with arith.
-Qed.
-Hint Resolve munion_ass.
-
-Lemma meq_left :
- forall x y z:multiset, meq x y -> meq (munion x z) (munion y z).
-Proof.
-unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.
-destruct x; destruct y; destruct z.
-intros; elim H; auto with arith.
-Qed.
-Hint Resolve meq_left.
-
-Lemma meq_right :
- forall x y z:multiset, meq x y -> meq (munion z x) (munion z y).
-Proof.
-unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.
-destruct x; destruct y; destruct z.
-intros; elim H; auto.
-Qed.
-Hint Resolve meq_right.
-
-
-(** Here we should make multiset an abstract datatype, by hiding [Bag],
- [munion], [multiplicity]; all further properties are proved abstractly *)
-
-Lemma munion_rotate :
- forall x y z:multiset, meq (munion x (munion y z)) (munion z (munion x y)).
-Proof.
-intros; apply (op_rotate multiset munion meq); auto.
-exact meq_trans.
-Qed.
-
-Lemma meq_congr :
- forall x y z t:multiset, meq x y -> meq z t -> meq (munion x z) (munion y t).
-Proof.
-intros; apply (cong_congr multiset munion meq); auto.
-exact meq_trans.
-Qed.
-
-Lemma munion_perm_left :
- forall x y z:multiset, meq (munion x (munion y z)) (munion y (munion x z)).
-Proof.
-intros; apply (perm_left multiset munion meq); auto.
-exact meq_trans.
-Qed.
-
-Lemma multiset_twist1 :
- forall x y z t:multiset,
- meq (munion x (munion (munion y z) t)) (munion (munion y (munion x t)) z).
-Proof.
-intros; apply (twist multiset munion meq); auto.
-exact meq_trans.
-Qed.
-
-Lemma multiset_twist2 :
- forall x y z t:multiset,
- meq (munion x (munion (munion y z) t)) (munion (munion y (munion x z)) t).
-Proof.
-intros; apply meq_trans with (munion (munion x (munion y z)) t).
-apply meq_sym; apply munion_ass.
-apply meq_left; apply munion_perm_left.
-Qed.
-
-(** specific for treesort *)
-
-Lemma treesort_twist1 :
- forall x y z t u:multiset,
- meq u (munion y z) ->
- meq (munion x (munion u t)) (munion (munion y (munion x t)) z).
-Proof.
-intros; apply meq_trans with (munion x (munion (munion y z) t)).
-apply meq_right; apply meq_left; trivial.
-apply multiset_twist1.
-Qed.
-
-Lemma treesort_twist2 :
- forall x y z t u:multiset,
- meq u (munion y z) ->
- meq (munion x (munion u t)) (munion (munion y (munion x z)) t).
-Proof.
-intros; apply meq_trans with (munion x (munion (munion y z) t)).
-apply meq_right; apply meq_left; trivial.
-apply multiset_twist2.
-Qed.
+
+ Definition EmptyBag := Bag (fun a:A => 0).
+ Definition SingletonBag (a:A) :=
+ Bag (fun a':A => match Aeq_dec a a' with
+ | left _ => 1
+ | right _ => 0
+ end).
+
+ Definition multiplicity (m:multiset) (a:A) : nat := let (f) := m in f a.
+
+ (** multiset equality *)
+ Definition meq (m1 m2:multiset) :=
+ forall a:A, multiplicity m1 a = multiplicity m2 a.
+
+ Lemma meq_refl : forall x:multiset, meq x x.
+ Proof.
+ destruct x; unfold meq; reflexivity.
+ Qed.
+
+ Lemma meq_trans : forall x y z:multiset, meq x y -> meq y z -> meq x z.
+ Proof.
+ unfold meq in |- *.
+ destruct x; destruct y; destruct z.
+ intros; rewrite H; auto.
+ Qed.
+
+ Lemma meq_sym : forall x y:multiset, meq x y -> meq y x.
+ Proof.
+ unfold meq in |- *.
+ destruct x; destruct y; auto.
+ Qed.
+
+ (** multiset union *)
+ Definition munion (m1 m2:multiset) :=
+ Bag (fun a:A => multiplicity m1 a + multiplicity m2 a).
+
+ Lemma munion_empty_left : forall x:multiset, meq x (munion EmptyBag x).
+ Proof.
+ unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto.
+ Qed.
+
+ Lemma munion_empty_right : forall x:multiset, meq x (munion x EmptyBag).
+ Proof.
+ unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto.
+ Qed.
+
+
+ Require Plus. (* comm. and ass. of plus *)
+
+ Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x).
+ Proof.
+ unfold meq in |- *; unfold multiplicity in |- *; unfold munion in |- *.
+ destruct x; destruct y; auto with arith.
+ Qed.
+
+ Lemma munion_ass :
+ forall x y z:multiset, meq (munion (munion x y) z) (munion x (munion y z)).
+ Proof.
+ unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.
+ destruct x; destruct y; destruct z; auto with arith.
+ Qed.
+
+ Lemma meq_left :
+ forall x y z:multiset, meq x y -> meq (munion x z) (munion y z).
+ Proof.
+ unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.
+ destruct x; destruct y; destruct z.
+ intros; elim H; auto with arith.
+ Qed.
+
+ Lemma meq_right :
+ forall x y z:multiset, meq x y -> meq (munion z x) (munion z y).
+ Proof.
+ unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.
+ destruct x; destruct y; destruct z.
+ intros; elim H; auto.
+ Qed.
+
+ (** Here we should make multiset an abstract datatype, by hiding [Bag],
+ [munion], [multiplicity]; all further properties are proved abstractly *)
+
+ Lemma munion_rotate :
+ forall x y z:multiset, meq (munion x (munion y z)) (munion z (munion x y)).
+ Proof.
+ intros; apply (op_rotate multiset munion meq).
+ apply munion_comm.
+ apply munion_ass.
+ exact meq_trans.
+ exact meq_sym.
+ trivial.
+ Qed.
+
+ Lemma meq_congr :
+ forall x y z t:multiset, meq x y -> meq z t -> meq (munion x z) (munion y t).
+ Proof.
+ intros; apply (cong_congr multiset munion meq); auto using meq_left, meq_right.
+ exact meq_trans.
+ Qed.
+
+ Lemma munion_perm_left :
+ forall x y z:multiset, meq (munion x (munion y z)) (munion y (munion x z)).
+ Proof.
+ intros; apply (perm_left multiset munion meq); auto using munion_comm, munion_ass, meq_left, meq_right, meq_sym.
+ exact meq_trans.
+ Qed.
+
+ Lemma multiset_twist1 :
+ forall x y z t:multiset,
+ meq (munion x (munion (munion y z) t)) (munion (munion y (munion x t)) z).
+ Proof.
+ intros; apply (twist multiset munion meq); auto using munion_comm, munion_ass, meq_sym, meq_left, meq_right.
+ exact meq_trans.
+ Qed.
+
+ Lemma multiset_twist2 :
+ forall x y z t:multiset,
+ meq (munion x (munion (munion y z) t)) (munion (munion y (munion x z)) t).
+ Proof.
+ intros; apply meq_trans with (munion (munion x (munion y z)) t).
+ apply meq_sym; apply munion_ass.
+ apply meq_left; apply munion_perm_left.
+ Qed.
+
+ (** specific for treesort *)
+
+ Lemma treesort_twist1 :
+ forall x y z t u:multiset,
+ meq u (munion y z) ->
+ meq (munion x (munion u t)) (munion (munion y (munion x t)) z).
+ Proof.
+ intros; apply meq_trans with (munion x (munion (munion y z) t)).
+ apply meq_right; apply meq_left; trivial.
+ apply multiset_twist1.
+ Qed.
+
+ Lemma treesort_twist2 :
+ forall x y z t u:multiset,
+ meq u (munion y z) ->
+ meq (munion x (munion u t)) (munion (munion y (munion x z)) t).
+ Proof.
+ intros; apply meq_trans with (munion x (munion (munion y z) t)).
+ apply meq_right; apply meq_left; trivial.
+ apply multiset_twist2.
+ Qed.
(*i theory of minter to do similarly
@@ -188,4 +182,4 @@ Unset Implicit Arguments.
Hint Unfold meq multiplicity: v62 datatypes.
Hint Resolve munion_empty_right munion_comm munion_ass meq_left meq_right
munion_empty_left: v62 datatypes.
-Hint Immediate meq_sym: v62 datatypes. \ No newline at end of file
+Hint Immediate meq_sym: v62 datatypes.
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v
index 9924ba66..6210913c 100644
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.v
@@ -24,32 +24,32 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Partial_Order.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Partial_Order.v 9245 2006-10-17 12:53:34Z notin $ i*)
Require Export Ensembles.
Require Export Relations_1.
Section Partial_orders.
-Variable U : Type.
-
-Definition Carrier := Ensemble U.
-
-Definition Rel := Relation U.
-
-Record PO : Type := Definition_of_PO
- {Carrier_of : Ensemble U;
- Rel_of : Relation U;
- PO_cond1 : Inhabited U Carrier_of;
- PO_cond2 : Order U Rel_of}.
-Variable p : PO.
-
-Definition Strict_Rel_of : Rel := fun x y:U => Rel_of p x y /\ x <> y.
-
-Inductive covers (y x:U) : Prop :=
+ Variable U : Type.
+
+ Definition Carrier := Ensemble U.
+
+ Definition Rel := Relation U.
+
+ Record PO : Type := Definition_of_PO
+ { Carrier_of : Ensemble U;
+ Rel_of : Relation U;
+ PO_cond1 : Inhabited U Carrier_of;
+ PO_cond2 : Order U Rel_of }.
+ Variable p : PO.
+
+ Definition Strict_Rel_of : Rel := fun x y:U => Rel_of p x y /\ x <> y.
+
+ Inductive covers (y x:U) : Prop :=
Definition_of_covers :
- Strict_Rel_of x y ->
- ~ (exists z : _, Strict_Rel_of x z /\ Strict_Rel_of z y) ->
- covers y x.
+ Strict_Rel_of x y ->
+ ~ (exists z : _, Strict_Rel_of x z /\ Strict_Rel_of z y) ->
+ covers y x.
End Partial_orders.
@@ -58,43 +58,45 @@ Hint Resolve Definition_of_covers: sets v62.
Section Partial_order_facts.
-Variable U : Type.
-Variable D : PO U.
-
-Lemma Strict_Rel_Transitive_with_Rel :
- forall x y z:U,
- Strict_Rel_of U D x y -> Rel_of U D y z -> Strict_Rel_of U D x z.
-unfold Strict_Rel_of at 1 in |- *.
-red in |- *.
-elim D; simpl in |- *.
-intros C R H' H'0; elim H'0.
-intros H'1 H'2 H'3 x y z H'4 H'5; split.
-apply H'2 with (y := y); tauto.
-red in |- *; intro H'6.
-elim H'4; intros H'7 H'8; apply H'8; clear H'4.
-apply H'3; auto.
-rewrite H'6; tauto.
-Qed.
+ Variable U : Type.
+ Variable D : PO U.
+
+ Lemma Strict_Rel_Transitive_with_Rel :
+ forall x y z:U,
+ Strict_Rel_of U D x y -> Rel_of U D y z -> Strict_Rel_of U D x z.
+ Proof.
+ unfold Strict_Rel_of at 1 in |- *.
+ red in |- *.
+ elim D; simpl in |- *.
+ intros C R H' H'0; elim H'0.
+ intros H'1 H'2 H'3 x y z H'4 H'5; split.
+ apply H'2 with (y := y); tauto.
+ red in |- *; intro H'6.
+ elim H'4; intros H'7 H'8; apply H'8; clear H'4.
+ apply H'3; auto.
+ rewrite H'6; tauto.
+ Qed.
-Lemma Strict_Rel_Transitive_with_Rel_left :
- forall x y z:U,
- Rel_of U D x y -> Strict_Rel_of U D y z -> Strict_Rel_of U D x z.
-unfold Strict_Rel_of at 1 in |- *.
-red in |- *.
-elim D; simpl in |- *.
-intros C R H' H'0; elim H'0.
-intros H'1 H'2 H'3 x y z H'4 H'5; split.
-apply H'2 with (y := y); tauto.
-red in |- *; intro H'6.
-elim H'5; intros H'7 H'8; apply H'8; clear H'5.
-apply H'3; auto.
-rewrite <- H'6; auto.
-Qed.
+ Lemma Strict_Rel_Transitive_with_Rel_left :
+ forall x y z:U,
+ Rel_of U D x y -> Strict_Rel_of U D y z -> Strict_Rel_of U D x z.
+ Proof.
+ unfold Strict_Rel_of at 1 in |- *.
+ red in |- *.
+ elim D; simpl in |- *.
+ intros C R H' H'0; elim H'0.
+ intros H'1 H'2 H'3 x y z H'4 H'5; split.
+ apply H'2 with (y := y); tauto.
+ red in |- *; intro H'6.
+ elim H'5; intros H'7 H'8; apply H'8; clear H'5.
+ apply H'3; auto.
+ rewrite <- H'6; auto.
+ Qed.
-Lemma Strict_Rel_Transitive : Transitive U (Strict_Rel_of U D).
-red in |- *.
-intros x y z H' H'0.
-apply Strict_Rel_Transitive_with_Rel with (y := y);
- [ intuition | unfold Strict_Rel_of in H', H'0; intuition ].
-Qed.
+ Lemma Strict_Rel_Transitive : Transitive U (Strict_Rel_of U D).
+ red in |- *.
+ intros x y z H' H'0.
+ apply Strict_Rel_Transitive_with_Rel with (y := y);
+ [ intuition | unfold Strict_Rel_of in H', H'0; intuition ].
+ Qed.
End Partial_order_facts. \ No newline at end of file
diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v
index 2b6c899f..a7c3db3a 100644
--- a/theories/Sets/Permut.v
+++ b/theories/Sets/Permut.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Permut.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Permut.v 9245 2006-10-17 12:53:34Z notin $ i*)
(* G. Huet 1-9-95 *)
@@ -15,77 +15,75 @@
Section Axiomatisation.
-Variable U : Set.
-
-Variable op : U -> U -> U.
-
-Variable cong : U -> U -> Prop.
-
-Hypothesis op_comm : forall x y:U, cong (op x y) (op y x).
-Hypothesis op_ass : forall x y z:U, cong (op (op x y) z) (op x (op y z)).
-
-Hypothesis cong_left : forall x y z:U, cong x y -> cong (op x z) (op y z).
-Hypothesis cong_right : forall x y z:U, cong x y -> cong (op z x) (op z y).
-Hypothesis cong_trans : forall x y z:U, cong x y -> cong y z -> cong x z.
-Hypothesis cong_sym : forall x y:U, cong x y -> cong y x.
-
-(** Remark. we do not need: [Hypothesis cong_refl : (x:U)(cong x x)]. *)
-
-Lemma cong_congr :
- forall x y z t:U, cong x y -> cong z t -> cong (op x z) (op y t).
-Proof.
-intros; apply cong_trans with (op y z).
-apply cong_left; trivial.
-apply cong_right; trivial.
-Qed.
-
-Lemma comm_right : forall x y z:U, cong (op x (op y z)) (op x (op z y)).
-Proof.
-intros; apply cong_right; apply op_comm.
-Qed.
-
-Lemma comm_left : forall x y z:U, cong (op (op x y) z) (op (op y x) z).
-Proof.
-intros; apply cong_left; apply op_comm.
-Qed.
-
-Lemma perm_right : forall x y z:U, cong (op (op x y) z) (op (op x z) y).
-Proof.
-intros.
-apply cong_trans with (op x (op y z)).
-apply op_ass.
-apply cong_trans with (op x (op z y)).
-apply cong_right; apply op_comm.
-apply cong_sym; apply op_ass.
-Qed.
-
-Lemma perm_left : forall x y z:U, cong (op x (op y z)) (op y (op x z)).
-Proof.
-intros.
-apply cong_trans with (op (op x y) z).
-apply cong_sym; apply op_ass.
-apply cong_trans with (op (op y x) z).
-apply cong_left; apply op_comm.
-apply op_ass.
-Qed.
-
-Lemma op_rotate : forall x y z t:U, cong (op x (op y z)) (op z (op x y)).
-Proof.
-intros; apply cong_trans with (op (op x y) z).
-apply cong_sym; apply op_ass.
-apply op_comm.
-Qed.
-
-(* Needed for treesort ... *)
-Lemma twist :
- forall x y z t:U, cong (op x (op (op y z) t)) (op (op y (op x t)) z).
-Proof.
-intros.
-apply cong_trans with (op x (op (op y t) z)).
-apply cong_right; apply perm_right.
-apply cong_trans with (op (op x (op y t)) z).
-apply cong_sym; apply op_ass.
-apply cong_left; apply perm_left.
-Qed.
+ Variable U : Set.
+ Variable op : U -> U -> U.
+ Variable cong : U -> U -> Prop.
+
+ Hypothesis op_comm : forall x y:U, cong (op x y) (op y x).
+ Hypothesis op_ass : forall x y z:U, cong (op (op x y) z) (op x (op y z)).
+
+ Hypothesis cong_left : forall x y z:U, cong x y -> cong (op x z) (op y z).
+ Hypothesis cong_right : forall x y z:U, cong x y -> cong (op z x) (op z y).
+ Hypothesis cong_trans : forall x y z:U, cong x y -> cong y z -> cong x z.
+ Hypothesis cong_sym : forall x y:U, cong x y -> cong y x.
+
+ (** Remark. we do not need: [Hypothesis cong_refl : (x:U)(cong x x)]. *)
+
+ Lemma cong_congr :
+ forall x y z t:U, cong x y -> cong z t -> cong (op x z) (op y t).
+ Proof.
+ intros; apply cong_trans with (op y z).
+ apply cong_left; trivial.
+ apply cong_right; trivial.
+ Qed.
+
+ Lemma comm_right : forall x y z:U, cong (op x (op y z)) (op x (op z y)).
+ Proof.
+ intros; apply cong_right; apply op_comm.
+ Qed.
+
+ Lemma comm_left : forall x y z:U, cong (op (op x y) z) (op (op y x) z).
+ Proof.
+ intros; apply cong_left; apply op_comm.
+ Qed.
+
+ Lemma perm_right : forall x y z:U, cong (op (op x y) z) (op (op x z) y).
+ Proof.
+ intros.
+ apply cong_trans with (op x (op y z)).
+ apply op_ass.
+ apply cong_trans with (op x (op z y)).
+ apply cong_right; apply op_comm.
+ apply cong_sym; apply op_ass.
+ Qed.
+
+ Lemma perm_left : forall x y z:U, cong (op x (op y z)) (op y (op x z)).
+ Proof.
+ intros.
+ apply cong_trans with (op (op x y) z).
+ apply cong_sym; apply op_ass.
+ apply cong_trans with (op (op y x) z).
+ apply cong_left; apply op_comm.
+ apply op_ass.
+ Qed.
+
+ Lemma op_rotate : forall x y z t:U, cong (op x (op y z)) (op z (op x y)).
+ Proof.
+ intros; apply cong_trans with (op (op x y) z).
+ apply cong_sym; apply op_ass.
+ apply op_comm.
+ Qed.
+
+ (** Needed for treesort ... *)
+ Lemma twist :
+ forall x y z t:U, cong (op x (op (op y z) t)) (op (op y (op x t)) z).
+ Proof.
+ intros.
+ apply cong_trans with (op x (op (op y t) z)).
+ apply cong_right; apply perm_right.
+ apply cong_trans with (op (op x (op y t)) z).
+ apply cong_sym; apply op_ass.
+ apply cong_left; apply perm_left.
+ Qed.
End Axiomatisation. \ No newline at end of file
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v
index 210017d4..47857705 100644
--- a/theories/Sets/Powerset_Classical_facts.v
+++ b/theories/Sets/Powerset_Classical_facts.v
@@ -24,7 +24,7 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Powerset_Classical_facts.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Powerset_Classical_facts.v 9245 2006-10-17 12:53:34Z notin $ i*)
Require Export Ensembles.
Require Export Constructive_sets.
@@ -39,298 +39,294 @@ Require Export Classical_sets.
Section Sets_as_an_algebra.
-Variable U : Type.
+ Variable U : Type.
+
+ Lemma sincl_add_x :
+ forall (A B:Ensemble U) (x:U),
+ ~ In U A x ->
+ Strict_Included U (Add U A x) (Add U B x) -> Strict_Included U A B.
+ Proof.
+ intros A B x H' H'0; red in |- *.
+ lapply (Strict_Included_inv U (Add U A x) (Add U B x)); auto with sets.
+ clear H'0; intro H'0; split.
+ apply incl_add_x with (x := x); tauto.
+ elim H'0; intros H'1 H'2; elim H'2; clear H'0 H'2.
+ intros x0 H'0.
+ red in |- *; intro H'2.
+ elim H'0; clear H'0.
+ rewrite <- H'2; auto with sets.
+ Qed.
-Lemma sincl_add_x :
- forall (A B:Ensemble U) (x:U),
- ~ In U A x ->
- Strict_Included U (Add U A x) (Add U B x) -> Strict_Included U A B.
-Proof.
-intros A B x H' H'0; red in |- *.
-lapply (Strict_Included_inv U (Add U A x) (Add U B x)); auto with sets.
-clear H'0; intro H'0; split.
-apply incl_add_x with (x := x); tauto.
-elim H'0; intros H'1 H'2; elim H'2; clear H'0 H'2.
-intros x0 H'0.
-red in |- *; intro H'2.
-elim H'0; clear H'0.
-rewrite <- H'2; auto with sets.
-Qed.
+ Lemma incl_soustr_in :
+ forall (X:Ensemble U) (x:U), In U X x -> Included U (Subtract U X x) X.
+ Proof.
+ intros X x H'; red in |- *.
+ intros x0 H'0; elim H'0; auto with sets.
+ Qed.
+
+ Lemma incl_soustr :
+ forall (X Y:Ensemble U) (x:U),
+ Included U X Y -> Included U (Subtract U X x) (Subtract U Y x).
+ Proof.
+ intros X Y x H'; red in |- *.
+ intros x0 H'0; elim H'0.
+ intros H'1 H'2.
+ apply Subtract_intro; auto with sets.
+ Qed.
+
+ Lemma incl_soustr_add_l :
+ forall (X:Ensemble U) (x:U), Included U (Subtract U (Add U X x) x) X.
+ Proof.
+ intros X x; red in |- *.
+ intros x0 H'; elim H'; auto with sets.
+ intro H'0; elim H'0; auto with sets.
+ intros t H'1 H'2; elim H'2; auto with sets.
+ Qed.
-Lemma incl_soustr_in :
- forall (X:Ensemble U) (x:U), In U X x -> Included U (Subtract U X x) X.
-Proof.
-intros X x H'; red in |- *.
-intros x0 H'0; elim H'0; auto with sets.
-Qed.
-Hint Resolve incl_soustr_in: sets v62.
-
-Lemma incl_soustr :
- forall (X Y:Ensemble U) (x:U),
- Included U X Y -> Included U (Subtract U X x) (Subtract U Y x).
-Proof.
-intros X Y x H'; red in |- *.
-intros x0 H'0; elim H'0.
-intros H'1 H'2.
-apply Subtract_intro; auto with sets.
-Qed.
-Hint Resolve incl_soustr: sets v62.
-
-
-Lemma incl_soustr_add_l :
- forall (X:Ensemble U) (x:U), Included U (Subtract U (Add U X x) x) X.
-Proof.
-intros X x; red in |- *.
-intros x0 H'; elim H'; auto with sets.
-intro H'0; elim H'0; auto with sets.
-intros t H'1 H'2; elim H'2; auto with sets.
-Qed.
-Hint Resolve incl_soustr_add_l: sets v62.
+ Lemma incl_soustr_add_r :
+ forall (X:Ensemble U) (x:U),
+ ~ In U X x -> Included U X (Subtract U (Add U X x) x).
+ Proof.
+ intros X x H'; red in |- *.
+ intros x0 H'0; try assumption.
+ apply Subtract_intro; auto with sets.
+ red in |- *; intro H'1; apply H'; rewrite H'1; auto with sets.
+ Qed.
+ Hint Resolve incl_soustr_add_r: sets v62.
+
+ Lemma add_soustr_2 :
+ forall (X:Ensemble U) (x:U),
+ In U X x -> Included U X (Add U (Subtract U X x) x).
+ Proof.
+ intros X x H'; red in |- *.
+ intros x0 H'0; try assumption.
+ elim (classic (x = x0)); intro K; auto with sets.
+ elim K; auto with sets.
+ Qed.
+
+ Lemma add_soustr_1 :
+ forall (X:Ensemble U) (x:U),
+ In U X x -> Included U (Add U (Subtract U X x) x) X.
+ Proof.
+ intros X x H'; red in |- *.
+ intros x0 H'0; elim H'0; auto with sets.
+ intros y H'1; elim H'1; auto with sets.
+ intros t H'1; try assumption.
+ rewrite <- (Singleton_inv U x t); auto with sets.
+ Qed.
+
+ Lemma add_soustr_xy :
+ forall (X:Ensemble U) (x y:U),
+ x <> y -> Subtract U (Add U X x) y = Add U (Subtract U X y) x.
+ Proof.
+ intros X x y H'; apply Extensionality_Ensembles.
+ split; red in |- *.
+ intros x0 H'0; elim H'0; auto with sets.
+ intro H'1; elim H'1.
+ intros u H'2 H'3; try assumption.
+ apply Add_intro1.
+ apply Subtract_intro; auto with sets.
+ intros t H'2 H'3; try assumption.
+ elim (Singleton_inv U x t); auto with sets.
+ intros u H'2; try assumption.
+ elim (Add_inv U (Subtract U X y) x u); auto with sets.
+ intro H'0; elim H'0; auto with sets.
+ intro H'0; rewrite <- H'0; auto with sets.
+ Qed.
+
+ Lemma incl_st_add_soustr :
+ forall (X Y:Ensemble U) (x:U),
+ ~ In U X x ->
+ Strict_Included U (Add U X x) Y -> Strict_Included U X (Subtract U Y x).
+ Proof.
+ intros X Y x H' H'0; apply sincl_add_x with (x := x); auto using add_soustr_1 with sets.
+ split.
+ elim H'0.
+ intros H'1 H'2.
+ generalize (Inclusion_is_transitive U).
+ intro H'4; red in H'4.
+ apply H'4 with (y := Y); auto using add_soustr_2 with sets.
+ red in H'0.
+ elim H'0; intros H'1 H'2; try exact H'1; clear H'0. (* PB *)
+ red in |- *; intro H'0; apply H'2.
+ rewrite H'0; auto 8 using add_soustr_xy, add_soustr_1, add_soustr_2 with sets.
+ Qed.
+
+ Lemma Sub_Add_new :
+ forall (X:Ensemble U) (x:U), ~ In U X x -> X = Subtract U (Add U X x) x.
+ Proof.
+ auto using incl_soustr_add_l with sets.
+ Qed.
+
+ Lemma Simplify_add :
+ forall (X X0:Ensemble U) (x:U),
+ ~ In U X x -> ~ In U X0 x -> Add U X x = Add U X0 x -> X = X0.
+ Proof.
+ intros X X0 x H' H'0 H'1; try assumption.
+ rewrite (Sub_Add_new X x); auto with sets.
+ rewrite (Sub_Add_new X0 x); auto with sets.
+ rewrite H'1; auto with sets.
+ Qed.
+
+ Lemma Included_Add :
+ forall (X A:Ensemble U) (x:U),
+ Included U X (Add U A x) ->
+ Included U X A \/ (exists A' : _, X = Add U A' x /\ Included U A' A).
+ Proof.
+ intros X A x H'0; try assumption.
+ elim (classic (In U X x)).
+ intro H'1; right; try assumption.
+ exists (Subtract U X x).
+ split; auto using incl_soustr_in, add_soustr_xy, add_soustr_1, add_soustr_2 with sets.
+ red in H'0.
+ red in |- *.
+ intros x0 H'2; try assumption.
+ lapply (Subtract_inv U X x x0); auto with sets.
+ intro H'3; elim H'3; intros K K'; clear H'3.
+ lapply (H'0 x0); auto with sets.
+ intro H'3; try assumption.
+ lapply (Add_inv U A x x0); auto with sets.
+ intro H'4; elim H'4;
+ [ intro H'5; try exact H'5; clear H'4 | intro H'5; clear H'4 ].
+ elim K'; auto with sets.
+ intro H'1; left; try assumption.
+ red in H'0.
+ red in |- *.
+ intros x0 H'2; try assumption.
+ lapply (H'0 x0); auto with sets.
+ intro H'3; try assumption.
+ lapply (Add_inv U A x x0); auto with sets.
+ intro H'4; elim H'4;
+ [ intro H'5; try exact H'5; clear H'4 | intro H'5; clear H'4 ].
+ absurd (In U X x0); auto with sets.
+ rewrite <- H'5; auto with sets.
+ Qed.
+
+ Lemma setcover_inv :
+ forall A x y:Ensemble U,
+ covers (Ensemble U) (Power_set_PO U A) y x ->
+ Strict_Included U x y /\
+ (forall z:Ensemble U, Included U x z -> Included U z y -> x = z \/ z = y).
+ Proof.
+ intros A x y H'; elim H'.
+ unfold Strict_Rel_of in |- *; simpl in |- *.
+ intros H'0 H'1; split; [ auto with sets | idtac ].
+ intros z H'2 H'3; try assumption.
+ elim (classic (x = z)); auto with sets.
+ intro H'4; right; try assumption.
+ elim (classic (z = y)); auto with sets.
+ intro H'5; try assumption.
+ elim H'1.
+ exists z; auto with sets.
+ Qed.
+
+ Theorem Add_covers :
+ forall A a:Ensemble U,
+ Included U a A ->
+ forall x:U,
+ In U A x ->
+ ~ In U a x -> covers (Ensemble U) (Power_set_PO U A) (Add U a x) a.
+ Proof.
+ intros A a H' x H'0 H'1; try assumption.
+ apply setcover_intro; auto with sets.
+ red in |- *.
+ split; [ idtac | red in |- *; intro H'2; try exact H'2 ]; auto with sets.
+ apply H'1.
+ rewrite H'2; auto with sets.
+ red in |- *; intro H'2; elim H'2; clear H'2.
+ intros z H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2.
+ lapply (Strict_Included_inv U a z); auto with sets; clear H'3.
+ intro H'2; elim H'2; intros H'3 H'5; elim H'5; clear H'2 H'5.
+ intros x0 H'2; elim H'2.
+ intros H'5 H'6; try assumption.
+ generalize H'4; intro K.
+ red in H'4.
+ elim H'4; intros H'8 H'9; red in H'8; clear H'4.
+ lapply (H'8 x0); auto with sets.
+ intro H'7; try assumption.
+ elim (Add_inv U a x x0); auto with sets.
+ intro H'15.
+ cut (Included U (Add U a x) z).
+ intro H'10; try assumption.
+ red in K.
+ elim K; intros H'11 H'12; apply H'12; clear K; auto with sets.
+ rewrite H'15.
+ red in |- *.
+ intros x1 H'10; elim H'10; auto with sets.
+ intros x2 H'11; elim H'11; auto with sets.
+ Qed.
+
+ Theorem covers_Add :
+ forall A a a':Ensemble U,
+ Included U a A ->
+ Included U a' A ->
+ covers (Ensemble U) (Power_set_PO U A) a' a ->
+ exists x : _, a' = Add U a x /\ In U A x /\ ~ In U a x.
+ Proof.
+ intros A a a' H' H'0 H'1; try assumption.
+ elim (setcover_inv A a a'); auto with sets.
+ intros H'6 H'7.
+ clear H'1.
+ elim (Strict_Included_inv U a a'); auto with sets.
+ intros H'5 H'8; elim H'8.
+ intros x H'1; elim H'1.
+ intros H'2 H'3; try assumption.
+ exists x.
+ split; [ try assumption | idtac ].
+ clear H'8 H'1.
+ elim (H'7 (Add U a x)); auto with sets.
+ intro H'1.
+ absurd (a = Add U a x); auto with sets.
+ red in |- *; intro H'8; try exact H'8.
+ apply H'3.
+ rewrite H'8; auto with sets.
+ auto with sets.
+ red in |- *.
+ intros x0 H'1; elim H'1; auto with sets.
+ intros x1 H'8; elim H'8; auto with sets.
+ split; [ idtac | try assumption ].
+ red in H'0; auto with sets.
+ Qed.
-Lemma incl_soustr_add_r :
- forall (X:Ensemble U) (x:U),
- ~ In U X x -> Included U X (Subtract U (Add U X x) x).
-Proof.
-intros X x H'; red in |- *.
-intros x0 H'0; try assumption.
-apply Subtract_intro; auto with sets.
-red in |- *; intro H'1; apply H'; rewrite H'1; auto with sets.
-Qed.
-Hint Resolve incl_soustr_add_r: sets v62.
-
-Lemma add_soustr_2 :
- forall (X:Ensemble U) (x:U),
- In U X x -> Included U X (Add U (Subtract U X x) x).
-Proof.
-intros X x H'; red in |- *.
-intros x0 H'0; try assumption.
-elim (classic (x = x0)); intro K; auto with sets.
-elim K; auto with sets.
-Qed.
-
-Lemma add_soustr_1 :
- forall (X:Ensemble U) (x:U),
- In U X x -> Included U (Add U (Subtract U X x) x) X.
-Proof.
-intros X x H'; red in |- *.
-intros x0 H'0; elim H'0; auto with sets.
-intros y H'1; elim H'1; auto with sets.
-intros t H'1; try assumption.
-rewrite <- (Singleton_inv U x t); auto with sets.
-Qed.
-Hint Resolve add_soustr_1 add_soustr_2: sets v62.
-
-Lemma add_soustr_xy :
- forall (X:Ensemble U) (x y:U),
- x <> y -> Subtract U (Add U X x) y = Add U (Subtract U X y) x.
-Proof.
-intros X x y H'; apply Extensionality_Ensembles.
-split; red in |- *.
-intros x0 H'0; elim H'0; auto with sets.
-intro H'1; elim H'1.
-intros u H'2 H'3; try assumption.
-apply Add_intro1.
-apply Subtract_intro; auto with sets.
-intros t H'2 H'3; try assumption.
-elim (Singleton_inv U x t); auto with sets.
-intros u H'2; try assumption.
-elim (Add_inv U (Subtract U X y) x u); auto with sets.
-intro H'0; elim H'0; auto with sets.
-intro H'0; rewrite <- H'0; auto with sets.
-Qed.
-Hint Resolve add_soustr_xy: sets v62.
-
-Lemma incl_st_add_soustr :
- forall (X Y:Ensemble U) (x:U),
- ~ In U X x ->
- Strict_Included U (Add U X x) Y -> Strict_Included U X (Subtract U Y x).
-Proof.
-intros X Y x H' H'0; apply sincl_add_x with (x := x); auto with sets.
-split.
-elim H'0.
-intros H'1 H'2.
-generalize (Inclusion_is_transitive U).
-intro H'4; red in H'4.
-apply H'4 with (y := Y); auto with sets.
-red in H'0.
-elim H'0; intros H'1 H'2; try exact H'1; clear H'0. (* PB *)
-red in |- *; intro H'0; apply H'2.
-rewrite H'0; auto 8 with sets.
-Qed.
-
-Lemma Sub_Add_new :
- forall (X:Ensemble U) (x:U), ~ In U X x -> X = Subtract U (Add U X x) x.
-Proof.
-auto with sets.
-Qed.
-
-Lemma Simplify_add :
- forall (X X0:Ensemble U) (x:U),
- ~ In U X x -> ~ In U X0 x -> Add U X x = Add U X0 x -> X = X0.
-Proof.
-intros X X0 x H' H'0 H'1; try assumption.
-rewrite (Sub_Add_new X x); auto with sets.
-rewrite (Sub_Add_new X0 x); auto with sets.
-rewrite H'1; auto with sets.
-Qed.
-
-Lemma Included_Add :
- forall (X A:Ensemble U) (x:U),
- Included U X (Add U A x) ->
- Included U X A \/ (exists A' : _, X = Add U A' x /\ Included U A' A).
-Proof.
-intros X A x H'0; try assumption.
-elim (classic (In U X x)).
-intro H'1; right; try assumption.
-exists (Subtract U X x).
-split; auto with sets.
-red in H'0.
-red in |- *.
-intros x0 H'2; try assumption.
-lapply (Subtract_inv U X x x0); auto with sets.
-intro H'3; elim H'3; intros K K'; clear H'3.
-lapply (H'0 x0); auto with sets.
-intro H'3; try assumption.
-lapply (Add_inv U A x x0); auto with sets.
-intro H'4; elim H'4;
- [ intro H'5; try exact H'5; clear H'4 | intro H'5; clear H'4 ].
-elim K'; auto with sets.
-intro H'1; left; try assumption.
-red in H'0.
-red in |- *.
-intros x0 H'2; try assumption.
-lapply (H'0 x0); auto with sets.
-intro H'3; try assumption.
-lapply (Add_inv U A x x0); auto with sets.
-intro H'4; elim H'4;
- [ intro H'5; try exact H'5; clear H'4 | intro H'5; clear H'4 ].
-absurd (In U X x0); auto with sets.
-rewrite <- H'5; auto with sets.
-Qed.
-
-Lemma setcover_inv :
- forall A x y:Ensemble U,
- covers (Ensemble U) (Power_set_PO U A) y x ->
- Strict_Included U x y /\
- (forall z:Ensemble U, Included U x z -> Included U z y -> x = z \/ z = y).
-Proof.
-intros A x y H'; elim H'.
-unfold Strict_Rel_of in |- *; simpl in |- *.
-intros H'0 H'1; split; [ auto with sets | idtac ].
-intros z H'2 H'3; try assumption.
-elim (classic (x = z)); auto with sets.
-intro H'4; right; try assumption.
-elim (classic (z = y)); auto with sets.
-intro H'5; try assumption.
-elim H'1.
-exists z; auto with sets.
-Qed.
-
-Theorem Add_covers :
- forall A a:Ensemble U,
- Included U a A ->
- forall x:U,
- In U A x ->
- ~ In U a x -> covers (Ensemble U) (Power_set_PO U A) (Add U a x) a.
-Proof.
-intros A a H' x H'0 H'1; try assumption.
-apply setcover_intro; auto with sets.
-red in |- *.
-split; [ idtac | red in |- *; intro H'2; try exact H'2 ]; auto with sets.
-apply H'1.
-rewrite H'2; auto with sets.
-red in |- *; intro H'2; elim H'2; clear H'2.
-intros z H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2.
-lapply (Strict_Included_inv U a z); auto with sets; clear H'3.
-intro H'2; elim H'2; intros H'3 H'5; elim H'5; clear H'2 H'5.
-intros x0 H'2; elim H'2.
-intros H'5 H'6; try assumption.
-generalize H'4; intro K.
-red in H'4.
-elim H'4; intros H'8 H'9; red in H'8; clear H'4.
-lapply (H'8 x0); auto with sets.
-intro H'7; try assumption.
-elim (Add_inv U a x x0); auto with sets.
-intro H'15.
-cut (Included U (Add U a x) z).
-intro H'10; try assumption.
-red in K.
-elim K; intros H'11 H'12; apply H'12; clear K; auto with sets.
-rewrite H'15.
-red in |- *.
-intros x1 H'10; elim H'10; auto with sets.
-intros x2 H'11; elim H'11; auto with sets.
-Qed.
-
-Theorem covers_Add :
- forall A a a':Ensemble U,
- Included U a A ->
- Included U a' A ->
- covers (Ensemble U) (Power_set_PO U A) a' a ->
- exists x : _, a' = Add U a x /\ In U A x /\ ~ In U a x.
-Proof.
-intros A a a' H' H'0 H'1; try assumption.
-elim (setcover_inv A a a'); auto with sets.
-intros H'6 H'7.
-clear H'1.
-elim (Strict_Included_inv U a a'); auto with sets.
-intros H'5 H'8; elim H'8.
-intros x H'1; elim H'1.
-intros H'2 H'3; try assumption.
-exists x.
-split; [ try assumption | idtac ].
-clear H'8 H'1.
-elim (H'7 (Add U a x)); auto with sets.
-intro H'1.
-absurd (a = Add U a x); auto with sets.
-red in |- *; intro H'8; try exact H'8.
-apply H'3.
-rewrite H'8; auto with sets.
-auto with sets.
-red in |- *.
-intros x0 H'1; elim H'1; auto with sets.
-intros x1 H'8; elim H'8; auto with sets.
-split; [ idtac | try assumption ].
-red in H'0; auto with sets.
-Qed.
-
-Theorem covers_is_Add :
- forall A a a':Ensemble U,
- Included U a A ->
- Included U a' A ->
- (covers (Ensemble U) (Power_set_PO U A) a' a <->
- (exists x : _, a' = Add U a x /\ In U A x /\ ~ In U a x)).
-Proof.
-intros A a a' H' H'0; split; intro K.
-apply covers_Add with (A := A); auto with sets.
-elim K.
-intros x H'1; elim H'1; intros H'2 H'3; rewrite H'2; clear H'1.
-apply Add_covers; intuition.
-Qed.
-
-Theorem Singleton_atomic :
- forall (x:U) (A:Ensemble U),
- In U A x ->
- covers (Ensemble U) (Power_set_PO U A) (Singleton U x) (Empty_set U).
-intros x A H'.
-rewrite <- (Empty_set_zero' U x).
-apply Add_covers; auto with sets.
-Qed.
-
-Lemma less_than_singleton :
- forall (X:Ensemble U) (x:U),
- Strict_Included U X (Singleton U x) -> X = Empty_set U.
-intros X x H'; try assumption.
-red in H'.
-lapply (Singleton_atomic x (Full_set U));
- [ intro H'2; try exact H'2 | apply Full_intro ].
-elim H'; intros H'0 H'1; try exact H'1; clear H'.
-elim (setcover_inv (Full_set U) (Empty_set U) (Singleton U x));
- [ intros H'6 H'7; try exact H'7 | idtac ]; auto with sets.
-elim (H'7 X); [ intro H'5; try exact H'5 | intro H'5 | idtac | idtac ];
- auto with sets.
-elim H'1; auto with sets.
-Qed.
+ Theorem covers_is_Add :
+ forall A a a':Ensemble U,
+ Included U a A ->
+ Included U a' A ->
+ (covers (Ensemble U) (Power_set_PO U A) a' a <->
+ (exists x : _, a' = Add U a x /\ In U A x /\ ~ In U a x)).
+ Proof.
+ intros A a a' H' H'0; split; intro K.
+ apply covers_Add with (A := A); auto with sets.
+ elim K.
+ intros x H'1; elim H'1; intros H'2 H'3; rewrite H'2; clear H'1.
+ apply Add_covers; intuition.
+ Qed.
+
+ Theorem Singleton_atomic :
+ forall (x:U) (A:Ensemble U),
+ In U A x ->
+ covers (Ensemble U) (Power_set_PO U A) (Singleton U x) (Empty_set U).
+ Proof.
+ intros x A H'.
+ rewrite <- (Empty_set_zero' U x).
+ apply Add_covers; auto with sets.
+ Qed.
+
+ Lemma less_than_singleton :
+ forall (X:Ensemble U) (x:U),
+ Strict_Included U X (Singleton U x) -> X = Empty_set U.
+ Proof.
+ intros X x H'; try assumption.
+ red in H'.
+ lapply (Singleton_atomic x (Full_set U));
+ [ intro H'2; try exact H'2 | apply Full_intro ].
+ elim H'; intros H'0 H'1; try exact H'1; clear H'.
+ elim (setcover_inv (Full_set U) (Empty_set U) (Singleton U x));
+ [ intros H'6 H'7; try exact H'7 | idtac ]; auto with sets.
+ elim (H'7 X); [ intro H'5; try exact H'5 | intro H'5 | idtac | idtac ];
+ auto with sets.
+ elim H'1; auto with sets.
+ Qed.
End Sets_as_an_algebra.
@@ -339,4 +335,4 @@ Hint Resolve incl_soustr: sets v62.
Hint Resolve incl_soustr_add_l: sets v62.
Hint Resolve incl_soustr_add_r: sets v62.
Hint Resolve add_soustr_1 add_soustr_2: sets v62.
-Hint Resolve add_soustr_xy: sets v62. \ No newline at end of file
+Hint Resolve add_soustr_xy: sets v62.
diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v
index 47ef2ea7..edb6a215 100644
--- a/theories/Sets/Powerset_facts.v
+++ b/theories/Sets/Powerset_facts.v
@@ -24,7 +24,7 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Powerset_facts.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Powerset_facts.v 9245 2006-10-17 12:53:34Z notin $ i*)
Require Export Ensembles.
Require Export Constructive_sets.
@@ -35,231 +35,223 @@ Require Export Cpo.
Require Export Powerset.
Section Sets_as_an_algebra.
-Variable U : Type.
-Hint Unfold not.
+ Variable U : Type.
-Theorem Empty_set_zero : forall X:Ensemble U, Union U (Empty_set U) X = X.
-Proof.
-auto 6 with sets.
-Qed.
-Hint Resolve Empty_set_zero.
+ Theorem Empty_set_zero : forall X:Ensemble U, Union U (Empty_set U) X = X.
+ Proof.
+ auto 6 with sets.
+ Qed.
+
+ Theorem Empty_set_zero' : forall x:U, Add U (Empty_set U) x = Singleton U x.
+ Proof.
+ unfold Add at 1 in |- *; auto using Empty_set_zero with sets.
+ Qed.
+
+ Lemma less_than_empty :
+ forall X:Ensemble U, Included U X (Empty_set U) -> X = Empty_set U.
+ Proof.
+ auto with sets.
+ Qed.
+
+ Theorem Union_commutative : forall A B:Ensemble U, Union U A B = Union U B A.
+ Proof.
+ auto with sets.
+ Qed.
+
+ Theorem Union_associative :
+ forall A B C:Ensemble U, Union U (Union U A B) C = Union U A (Union U B C).
+ Proof.
+ auto 9 with sets.
+ Qed.
+
+ Theorem Union_idempotent : forall A:Ensemble U, Union U A A = A.
+ Proof.
+ auto 7 with sets.
+ Qed.
+
+ Lemma Union_absorbs :
+ forall A B:Ensemble U, Included U B A -> Union U A B = A.
+ Proof.
+ auto 7 with sets.
+ Qed.
-Theorem Empty_set_zero' : forall x:U, Add U (Empty_set U) x = Singleton U x.
-Proof.
-unfold Add at 1 in |- *; auto with sets.
-Qed.
-Hint Resolve Empty_set_zero'.
+ Theorem Couple_as_union :
+ forall x y:U, Union U (Singleton U x) (Singleton U y) = Couple U x y.
+ Proof.
+ intros x y; apply Extensionality_Ensembles; split; red in |- *.
+ intros x0 H'; elim H'; (intros x1 H'0; elim H'0; auto with sets).
+ intros x0 H'; elim H'; auto with sets.
+ Qed.
+
+ Theorem Triple_as_union :
+ forall x y z:U,
+ Union U (Union U (Singleton U x) (Singleton U y)) (Singleton U z) =
+ Triple U x y z.
+ Proof.
+ intros x y z; apply Extensionality_Ensembles; split; red in |- *.
+ intros x0 H'; elim H'.
+ intros x1 H'0; elim H'0; (intros x2 H'1; elim H'1; auto with sets).
+ intros x1 H'0; elim H'0; auto with sets.
+ intros x0 H'; elim H'; auto with sets.
+ Qed.
+
+ Theorem Triple_as_Couple : forall x y:U, Couple U x y = Triple U x x y.
+ Proof.
+ intros x y.
+ rewrite <- (Couple_as_union x y).
+ rewrite <- (Union_idempotent (Singleton U x)).
+ apply Triple_as_union.
+ Qed.
+
+ Theorem Triple_as_Couple_Singleton :
+ forall x y z:U, Triple U x y z = Union U (Couple U x y) (Singleton U z).
+ Proof.
+ intros x y z.
+ rewrite <- (Triple_as_union x y z).
+ rewrite <- (Couple_as_union x y); auto with sets.
+ Qed.
+
+ Theorem Intersection_commutative :
+ forall A B:Ensemble U, Intersection U A B = Intersection U B A.
+ Proof.
+ intros A B.
+ apply Extensionality_Ensembles.
+ split; red in |- *; intros x H'; elim H'; auto with sets.
+ Qed.
+
+ Theorem Distributivity :
+ forall A B C:Ensemble U,
+ Intersection U A (Union U B C) =
+ Union U (Intersection U A B) (Intersection U A C).
+ Proof.
+ intros A B C.
+ apply Extensionality_Ensembles.
+ split; red in |- *; intros x H'.
+ elim H'.
+ intros x0 H'0 H'1; generalize H'0.
+ elim H'1; auto with sets.
+ elim H'; intros x0 H'0; elim H'0; auto with sets.
+ Qed.
+
+ Theorem Distributivity' :
+ forall A B C:Ensemble U,
+ Union U A (Intersection U B C) =
+ Intersection U (Union U A B) (Union U A C).
+ Proof.
+ intros A B C.
+ apply Extensionality_Ensembles.
+ split; red in |- *; intros x H'.
+ elim H'; auto with sets.
+ intros x0 H'0; elim H'0; auto with sets.
+ elim H'.
+ intros x0 H'0; elim H'0; auto with sets.
+ intros x1 H'1 H'2; try exact H'2.
+ generalize H'1.
+ elim H'2; auto with sets.
+ Qed.
+
+ Theorem Union_add :
+ forall (A B:Ensemble U) (x:U), Add U (Union U A B) x = Union U A (Add U B x).
+ Proof.
+ unfold Add in |- *; auto using Union_associative with sets.
+ Qed.
+
+ Theorem Non_disjoint_union :
+ forall (X:Ensemble U) (x:U), In U X x -> Add U X x = X.
+ Proof.
+ intros X x H'; unfold Add in |- *.
+ apply Extensionality_Ensembles; red in |- *.
+ split; red in |- *; auto with sets.
+ intros x0 H'0; elim H'0; auto with sets.
+ intros t H'1; elim H'1; auto with sets.
+ Qed.
+
+ Theorem Non_disjoint_union' :
+ forall (X:Ensemble U) (x:U), ~ In U X x -> Subtract U X x = X.
+ Proof.
+ intros X x H'; unfold Subtract in |- *.
+ apply Extensionality_Ensembles.
+ split; red in |- *; auto with sets.
+ intros x0 H'0; elim H'0; auto with sets.
+ intros x0 H'0; apply Setminus_intro; auto with sets.
+ red in |- *; intro H'1; elim H'1.
+ lapply (Singleton_inv U x x0); auto with sets.
+ intro H'4; apply H'; rewrite H'4; auto with sets.
+ Qed.
+
+ Lemma singlx : forall x y:U, In U (Add U (Empty_set U) x) y -> x = y.
+ Proof.
+ intro x; rewrite (Empty_set_zero' x); auto with sets.
+ Qed.
+
+ Lemma incl_add :
+ forall (A B:Ensemble U) (x:U),
+ Included U A B -> Included U (Add U A x) (Add U B x).
+ Proof.
+ intros A B x H'; red in |- *; auto with sets.
+ intros x0 H'0.
+ lapply (Add_inv U A x x0); auto with sets.
+ intro H'1; elim H'1;
+ [ intro H'2; clear H'1 | intro H'2; rewrite <- H'2; clear H'1 ];
+ auto with sets.
+ Qed.
-Lemma less_than_empty :
- forall X:Ensemble U, Included U X (Empty_set U) -> X = Empty_set U.
-Proof.
-auto with sets.
-Qed.
-Hint Resolve less_than_empty.
+ Lemma incl_add_x :
+ forall (A B:Ensemble U) (x:U),
+ ~ In U A x -> Included U (Add U A x) (Add U B x) -> Included U A B.
+ Proof.
+ unfold Included in |- *.
+ intros A B x H' H'0 x0 H'1.
+ lapply (H'0 x0); auto with sets.
+ intro H'2; lapply (Add_inv U B x x0); auto with sets.
+ intro H'3; elim H'3;
+ [ intro H'4; try exact H'4; clear H'3 | intro H'4; clear H'3 ].
+ absurd (In U A x0); auto with sets.
+ rewrite <- H'4; auto with sets.
+ Qed.
+
+ Lemma Add_commutative :
+ forall (A:Ensemble U) (x y:U), Add U (Add U A x) y = Add U (Add U A y) x.
+ Proof.
+ intros A x y.
+ unfold Add in |- *.
+ rewrite (Union_associative A (Singleton U x) (Singleton U y)).
+ rewrite (Union_commutative (Singleton U x) (Singleton U y)).
+ rewrite <- (Union_associative A (Singleton U y) (Singleton U x));
+ auto with sets.
+ Qed.
+
+ Lemma Add_commutative' :
+ forall (A:Ensemble U) (x y z:U),
+ Add U (Add U (Add U A x) y) z = Add U (Add U (Add U A z) x) y.
+ Proof.
+ intros A x y z.
+ rewrite (Add_commutative (Add U A x) y z).
+ rewrite (Add_commutative A x z); auto with sets.
+ Qed.
+
+ Lemma Add_distributes :
+ forall (A B:Ensemble U) (x y:U),
+ Included U B A -> Add U (Add U A x) y = Union U (Add U A x) (Add U B y).
+ Proof.
+ intros A B x y H'; try assumption.
+ rewrite <- (Union_add (Add U A x) B y).
+ unfold Add at 4 in |- *.
+ rewrite (Union_commutative A (Singleton U x)).
+ rewrite Union_associative.
+ rewrite (Union_absorbs A B H').
+ rewrite (Union_commutative (Singleton U x) A).
+ auto with sets.
+ Qed.
-Theorem Union_commutative : forall A B:Ensemble U, Union U A B = Union U B A.
-Proof.
-auto with sets.
-Qed.
-
-Theorem Union_associative :
- forall A B C:Ensemble U, Union U (Union U A B) C = Union U A (Union U B C).
-Proof.
-auto 9 with sets.
-Qed.
-Hint Resolve Union_associative.
-
-Theorem Union_idempotent : forall A:Ensemble U, Union U A A = A.
-Proof.
-auto 7 with sets.
-Qed.
-
-Lemma Union_absorbs :
- forall A B:Ensemble U, Included U B A -> Union U A B = A.
-Proof.
-auto 7 with sets.
-Qed.
-
-Theorem Couple_as_union :
- forall x y:U, Union U (Singleton U x) (Singleton U y) = Couple U x y.
-Proof.
-intros x y; apply Extensionality_Ensembles; split; red in |- *.
-intros x0 H'; elim H'; (intros x1 H'0; elim H'0; auto with sets).
-intros x0 H'; elim H'; auto with sets.
-Qed.
-
-Theorem Triple_as_union :
- forall x y z:U,
- Union U (Union U (Singleton U x) (Singleton U y)) (Singleton U z) =
- Triple U x y z.
-Proof.
-intros x y z; apply Extensionality_Ensembles; split; red in |- *.
-intros x0 H'; elim H'.
-intros x1 H'0; elim H'0; (intros x2 H'1; elim H'1; auto with sets).
-intros x1 H'0; elim H'0; auto with sets.
-intros x0 H'; elim H'; auto with sets.
-Qed.
-
-Theorem Triple_as_Couple : forall x y:U, Couple U x y = Triple U x x y.
-Proof.
-intros x y.
-rewrite <- (Couple_as_union x y).
-rewrite <- (Union_idempotent (Singleton U x)).
-apply Triple_as_union.
-Qed.
-
-Theorem Triple_as_Couple_Singleton :
- forall x y z:U, Triple U x y z = Union U (Couple U x y) (Singleton U z).
-Proof.
-intros x y z.
-rewrite <- (Triple_as_union x y z).
-rewrite <- (Couple_as_union x y); auto with sets.
-Qed.
-
-Theorem Intersection_commutative :
- forall A B:Ensemble U, Intersection U A B = Intersection U B A.
-Proof.
-intros A B.
-apply Extensionality_Ensembles.
-split; red in |- *; intros x H'; elim H'; auto with sets.
-Qed.
-
-Theorem Distributivity :
- forall A B C:Ensemble U,
- Intersection U A (Union U B C) =
- Union U (Intersection U A B) (Intersection U A C).
-Proof.
-intros A B C.
-apply Extensionality_Ensembles.
-split; red in |- *; intros x H'.
-elim H'.
-intros x0 H'0 H'1; generalize H'0.
-elim H'1; auto with sets.
-elim H'; intros x0 H'0; elim H'0; auto with sets.
-Qed.
-
-Theorem Distributivity' :
- forall A B C:Ensemble U,
- Union U A (Intersection U B C) =
- Intersection U (Union U A B) (Union U A C).
-Proof.
-intros A B C.
-apply Extensionality_Ensembles.
-split; red in |- *; intros x H'.
-elim H'; auto with sets.
-intros x0 H'0; elim H'0; auto with sets.
-elim H'.
-intros x0 H'0; elim H'0; auto with sets.
-intros x1 H'1 H'2; try exact H'2.
-generalize H'1.
-elim H'2; auto with sets.
-Qed.
-
-Theorem Union_add :
- forall (A B:Ensemble U) (x:U), Add U (Union U A B) x = Union U A (Add U B x).
-Proof.
-unfold Add in |- *; auto with sets.
-Qed.
-Hint Resolve Union_add.
-
-Theorem Non_disjoint_union :
- forall (X:Ensemble U) (x:U), In U X x -> Add U X x = X.
-intros X x H'; unfold Add in |- *.
-apply Extensionality_Ensembles; red in |- *.
-split; red in |- *; auto with sets.
-intros x0 H'0; elim H'0; auto with sets.
-intros t H'1; elim H'1; auto with sets.
-Qed.
-
-Theorem Non_disjoint_union' :
- forall (X:Ensemble U) (x:U), ~ In U X x -> Subtract U X x = X.
-Proof.
-intros X x H'; unfold Subtract in |- *.
-apply Extensionality_Ensembles.
-split; red in |- *; auto with sets.
-intros x0 H'0; elim H'0; auto with sets.
-intros x0 H'0; apply Setminus_intro; auto with sets.
-red in |- *; intro H'1; elim H'1.
-lapply (Singleton_inv U x x0); auto with sets.
-intro H'4; apply H'; rewrite H'4; auto with sets.
-Qed.
-
-Lemma singlx : forall x y:U, In U (Add U (Empty_set U) x) y -> x = y.
-Proof.
-intro x; rewrite (Empty_set_zero' x); auto with sets.
-Qed.
-Hint Resolve singlx.
-
-Lemma incl_add :
- forall (A B:Ensemble U) (x:U),
- Included U A B -> Included U (Add U A x) (Add U B x).
-Proof.
-intros A B x H'; red in |- *; auto with sets.
-intros x0 H'0.
-lapply (Add_inv U A x x0); auto with sets.
-intro H'1; elim H'1;
- [ intro H'2; clear H'1 | intro H'2; rewrite <- H'2; clear H'1 ];
- auto with sets.
-Qed.
-Hint Resolve incl_add.
-
-Lemma incl_add_x :
- forall (A B:Ensemble U) (x:U),
- ~ In U A x -> Included U (Add U A x) (Add U B x) -> Included U A B.
-Proof.
-unfold Included in |- *.
-intros A B x H' H'0 x0 H'1.
-lapply (H'0 x0); auto with sets.
-intro H'2; lapply (Add_inv U B x x0); auto with sets.
-intro H'3; elim H'3;
- [ intro H'4; try exact H'4; clear H'3 | intro H'4; clear H'3 ].
-absurd (In U A x0); auto with sets.
-rewrite <- H'4; auto with sets.
-Qed.
-
-Lemma Add_commutative :
- forall (A:Ensemble U) (x y:U), Add U (Add U A x) y = Add U (Add U A y) x.
-Proof.
-intros A x y.
-unfold Add in |- *.
-rewrite (Union_associative A (Singleton U x) (Singleton U y)).
-rewrite (Union_commutative (Singleton U x) (Singleton U y)).
-rewrite <- (Union_associative A (Singleton U y) (Singleton U x));
- auto with sets.
-Qed.
-
-Lemma Add_commutative' :
- forall (A:Ensemble U) (x y z:U),
- Add U (Add U (Add U A x) y) z = Add U (Add U (Add U A z) x) y.
-Proof.
-intros A x y z.
-rewrite (Add_commutative (Add U A x) y z).
-rewrite (Add_commutative A x z); auto with sets.
-Qed.
-
-Lemma Add_distributes :
- forall (A B:Ensemble U) (x y:U),
- Included U B A -> Add U (Add U A x) y = Union U (Add U A x) (Add U B y).
-Proof.
-intros A B x y H'; try assumption.
-rewrite <- (Union_add (Add U A x) B y).
-unfold Add at 4 in |- *.
-rewrite (Union_commutative A (Singleton U x)).
-rewrite Union_associative.
-rewrite (Union_absorbs A B H').
-rewrite (Union_commutative (Singleton U x) A).
-auto with sets.
-Qed.
-
-Lemma setcover_intro :
- forall (U:Type) (A x y:Ensemble U),
- Strict_Included U x y ->
- ~ (exists z : _, Strict_Included U x z /\ Strict_Included U z y) ->
- covers (Ensemble U) (Power_set_PO U A) y x.
-Proof.
-intros; apply Definition_of_covers; auto with sets.
-Qed.
-Hint Resolve setcover_intro.
+ Lemma setcover_intro :
+ forall (U:Type) (A x y:Ensemble U),
+ Strict_Included U x y ->
+ ~ (exists z : _, Strict_Included U x z /\ Strict_Included U z y) ->
+ covers (Ensemble U) (Power_set_PO U A) y x.
+ Proof.
+ intros; apply Definition_of_covers; auto with sets.
+ Qed.
End Sets_as_an_algebra.