diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-17 12:53:34 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-17 12:53:34 +0000 |
| commit | 28dc7a05cc1d3e03ed1435b3db4340db954a59e2 (patch) | |
| tree | 63cdf18cd47260eb90550f62f7b22e2e2e208f6c /theories/Sets | |
| parent | 744e7f6a319f4d459a3cc2309f575d43041d75aa (diff) | |
Mise en forme des theories
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Sets')
| -rw-r--r-- | theories/Sets/Classical_sets.v | 187 | ||||
| -rw-r--r-- | theories/Sets/Constructive_sets.v | 229 | ||||
| -rw-r--r-- | theories/Sets/Cpo.v | 103 | ||||
| -rw-r--r-- | theories/Sets/Ensembles.v | 101 | ||||
| -rw-r--r-- | theories/Sets/Finite_sets.v | 64 | ||||
| -rw-r--r-- | theories/Sets/Finite_sets_facts.v | 581 | ||||
| -rw-r--r-- | theories/Sets/Image.v | 320 | ||||
| -rw-r--r-- | theories/Sets/Infinite_sets.v | 386 | ||||
| -rw-r--r-- | theories/Sets/Integers.v | 221 | ||||
| -rw-r--r-- | theories/Sets/Multiset.v | 304 | ||||
| -rw-r--r-- | theories/Sets/Partial_Order.v | 114 | ||||
| -rw-r--r-- | theories/Sets/Permut.v | 142 | ||||
| -rw-r--r-- | theories/Sets/Powerset_Classical_facts.v | 576 | ||||
| -rw-r--r-- | theories/Sets/Powerset_facts.v | 434 |
14 files changed, 1860 insertions, 1902 deletions
diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v index a21534bd5..62fd4df1a 100644 --- a/theories/Sets/Classical_sets.v +++ b/theories/Sets/Classical_sets.v @@ -30,103 +30,98 @@ 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 09a941bcd..65ce03e28 100644 --- a/theories/Sets/Constructive_sets.v +++ b/theories/Sets/Constructive_sets.v @@ -29,131 +29,118 @@ 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 efd83c106..c1e64babc 100644 --- a/theories/Sets/Cpo.v +++ b/theories/Sets/Cpo.v @@ -31,79 +31,80 @@ 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 9c85d67d0..339298572 100644 --- a/theories/Sets/Ensembles.v +++ b/theories/Sets/Ensembles.v @@ -27,69 +27,68 @@ (*i $Id$ 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 53981ea8d..a75c3b767 100644 --- a/theories/Sets/Finite_sets.v +++ b/theories/Sets/Finite_sets.v @@ -29,17 +29,17 @@ 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 94ea964c2..0615c9c9d 100644 --- a/theories/Sets/Finite_sets_facts.v +++ b/theories/Sets/Finite_sets_facts.v @@ -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 469b41783..da3aec320 100644 --- a/theories/Sets/Image.v +++ b/theories/Sets/Image.v @@ -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 c3492ba78..f30c5b763 100644 --- a/theories/Sets/Infinite_sets.v +++ b/theories/Sets/Infinite_sets.v @@ -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 970d6dab1..88cdabe3f 100644 --- a/theories/Sets/Integers.v +++ b/theories/Sets/Integers.v @@ -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 aad294e93..80491c0aa 100644 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -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 07244e66f..8589f387e 100644 --- a/theories/Sets/Partial_Order.v +++ b/theories/Sets/Partial_Order.v @@ -30,26 +30,26 @@ 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 006831909..7c6b551c6 100644 --- a/theories/Sets/Permut.v +++ b/theories/Sets/Permut.v @@ -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 1ac59056b..8116045b6 100644 --- a/theories/Sets/Powerset_Classical_facts.v +++ b/theories/Sets/Powerset_Classical_facts.v @@ -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 cae796861..dee4af65a 100644 --- a/theories/Sets/Powerset_facts.v +++ b/theories/Sets/Powerset_facts.v @@ -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. |