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/Classical_sets.v | |
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/Classical_sets.v')
-rw-r--r-- | theories/Sets/Classical_sets.v | 187 |
1 files changed, 91 insertions, 96 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. |