diff options
Diffstat (limited to 'theories/Sets/Classical_sets.v')
| -rw-r--r-- | theories/Sets/Classical_sets.v | 189 |
1 files changed, 92 insertions, 97 deletions
diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v index 382b5d72..e6755898 100644 --- a/theories/Sets/Classical_sets.v +++ b/theories/Sets/Classical_sets.v @@ -24,109 +24,104 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id: Classical_sets.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Classical_sets.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Export Ensembles. Require Export Constructive_sets. Require Export Classical_Type. -(* Hints Unfold not . *) - Section Ensembles_classical. -Variable U : Type. - -Lemma not_included_empty_Inhabited : - forall A:Ensemble U, ~ Included U A (Empty_set U) -> Inhabited U A. -Proof. -intros A NI. -elim (not_all_ex_not U (fun x:U => ~ In U A x)). -intros x H; apply Inhabited_intro with x. -apply NNPP; auto with sets. -red in |- *; intro. -apply NI; red in |- *. -intros x H'; elim (H x); trivial with sets. -Qed. -Hint Resolve not_included_empty_Inhabited. - -Lemma not_empty_Inhabited : - forall A:Ensemble U, A <> Empty_set U -> Inhabited U A. -Proof. -intros; apply not_included_empty_Inhabited. -red in |- *; auto with sets. -Qed. - -Lemma Inhabited_Setminus : - forall X Y:Ensemble U, - Included U X Y -> ~ Included U Y X -> Inhabited U (Setminus U Y X). -Proof. -intros X Y I NI. -elim (not_all_ex_not U (fun x:U => In U Y x -> In U X x) NI). -intros x YX. -apply Inhabited_intro with x. -apply Setminus_intro. -apply not_imply_elim with (In U X x); trivial with sets. -auto with sets. -Qed. -Hint Resolve Inhabited_Setminus. - -Lemma Strict_super_set_contains_new_element : - forall X Y:Ensemble U, - Included U X Y -> X <> Y -> Inhabited U (Setminus U Y X). -Proof. -auto 7 with sets. -Qed. -Hint Resolve Strict_super_set_contains_new_element. - -Lemma Subtract_intro : - forall (A:Ensemble U) (x y:U), In U A y -> x <> y -> In U (Subtract U A x) y. -Proof. -unfold Subtract at 1 in |- *; auto with sets. -Qed. -Hint Resolve Subtract_intro. - -Lemma Subtract_inv : - forall (A:Ensemble U) (x y:U), In U (Subtract U A x) y -> In U A y /\ x <> y. -Proof. -intros A x y H'; elim H'; auto with sets. -Qed. - -Lemma Included_Strict_Included : - forall X Y:Ensemble U, Included U X Y -> Strict_Included U X Y \/ X = Y. -Proof. -intros X Y H'; try assumption. -elim (classic (X = Y)); auto with sets. -Qed. - -Lemma Strict_Included_inv : - forall X Y:Ensemble U, - Strict_Included U X Y -> Included U X Y /\ Inhabited U (Setminus U Y X). -Proof. -intros X Y H'; red in H'. -split; [ tauto | idtac ]. -elim H'; intros H'0 H'1; try exact H'1; clear H'. -apply Strict_super_set_contains_new_element; auto with sets. -Qed. - -Lemma not_SIncl_empty : - forall X:Ensemble U, ~ Strict_Included U X (Empty_set U). -Proof. -intro X; red in |- *; intro H'; try exact H'. -lapply (Strict_Included_inv X (Empty_set U)); auto with sets. -intro H'0; elim H'0; intros H'1 H'2; elim H'2; clear H'0. -intros x H'0; elim H'0. -intro H'3; elim H'3. -Qed. - -Lemma Complement_Complement : - forall A:Ensemble U, Complement U (Complement U A) = A. -Proof. -unfold Complement in |- *; intros; apply Extensionality_Ensembles; - auto with sets. -red in |- *; split; auto with sets. -red in |- *; intros; apply NNPP; auto with sets. -Qed. + Variable U : Type. + + Lemma not_included_empty_Inhabited : + forall A:Ensemble U, ~ Included U A (Empty_set U) -> Inhabited U A. + Proof. + intros A NI. + elim (not_all_ex_not U (fun x:U => ~ In U A x)). + intros x H; apply Inhabited_intro with x. + apply NNPP; auto with sets. + red in |- *; intro. + apply NI; red in |- *. + intros x H'; elim (H x); trivial with sets. + Qed. + + Lemma not_empty_Inhabited : + forall A:Ensemble U, A <> Empty_set U -> Inhabited U A. + Proof. + intros; apply not_included_empty_Inhabited. + red in |- *; auto with sets. + Qed. + + Lemma Inhabited_Setminus : + forall X Y:Ensemble U, + Included U X Y -> ~ Included U Y X -> Inhabited U (Setminus U Y X). + Proof. + intros X Y I NI. + elim (not_all_ex_not U (fun x:U => In U Y x -> In U X x) NI). + intros x YX. + apply Inhabited_intro with x. + apply Setminus_intro. + apply not_imply_elim with (In U X x); trivial with sets. + auto with sets. + Qed. + + Lemma Strict_super_set_contains_new_element : + forall X Y:Ensemble U, + Included U X Y -> X <> Y -> Inhabited U (Setminus U Y X). + Proof. + auto 7 using Inhabited_Setminus with sets. + Qed. + + Lemma Subtract_intro : + forall (A:Ensemble U) (x y:U), In U A y -> x <> y -> In U (Subtract U A x) y. + Proof. + unfold Subtract at 1 in |- *; auto with sets. + Qed. + Hint Resolve Subtract_intro : sets. + + Lemma Subtract_inv : + forall (A:Ensemble U) (x y:U), In U (Subtract U A x) y -> In U A y /\ x <> y. + Proof. + intros A x y H'; elim H'; auto with sets. + Qed. + + Lemma Included_Strict_Included : + forall X Y:Ensemble U, Included U X Y -> Strict_Included U X Y \/ X = Y. + Proof. + intros X Y H'; try assumption. + elim (classic (X = Y)); auto with sets. + Qed. + + Lemma Strict_Included_inv : + forall X Y:Ensemble U, + Strict_Included U X Y -> Included U X Y /\ Inhabited U (Setminus U Y X). + Proof. + intros X Y H'; red in H'. + split; [ tauto | idtac ]. + elim H'; intros H'0 H'1; try exact H'1; clear H'. + apply Strict_super_set_contains_new_element; auto with sets. + Qed. + + Lemma not_SIncl_empty : + forall X:Ensemble U, ~ Strict_Included U X (Empty_set U). + Proof. + intro X; red in |- *; intro H'; try exact H'. + lapply (Strict_Included_inv X (Empty_set U)); auto with sets. + intro H'0; elim H'0; intros H'1 H'2; elim H'2; clear H'0. + intros x H'0; elim H'0. + intro H'3; elim H'3. + Qed. + + Lemma Complement_Complement : + forall A:Ensemble U, Complement U (Complement U A) = A. + Proof. + unfold Complement in |- *; intros; apply Extensionality_Ensembles; + auto with sets. + red in |- *; split; auto with sets. + red in |- *; intros; apply NNPP; auto with sets. + Qed. End Ensembles_classical. -Hint Resolve Strict_super_set_contains_new_element Subtract_intro - not_SIncl_empty: sets v62.
\ No newline at end of file + Hint Resolve Strict_super_set_contains_new_element Subtract_intro + not_SIncl_empty: sets v62. |