blob: 2cd2df78ab5e5ae98f8351cf0d39c64d9b12836d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
(****************************************************************************)
(* *)
(* Naive Set Theory in Coq *)
(* *)
(* INRIA INRIA *)
(* Rocquencourt Sophia-Antipolis *)
(* *)
(* Coq V6.1 *)
(* *)
(* Gilles Kahn *)
(* Gerard Huet *)
(* *)
(* *)
(* *)
(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *)
(* to the Newton Institute for providing an exceptional work environment *)
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
(* $Id$ *)
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:
(A: (Ensemble U)) ~ (Included U A (Empty_set U)) -> (Inhabited U A).
Proof.
Intros A NI.
Elim (not_all_ex_not U [x:U]~(In U A x)).
Intros x H; Apply Inhabited_intro with x.
Apply NNPP; Auto with sets.
Red; Intro.
Apply NI; Red.
Intros x H'; Elim (H x); Trivial with sets.
Qed.
Hints Resolve not_included_empty_Inhabited.
Lemma not_empty_Inhabited:
(A: (Ensemble U)) ~ A == (Empty_set U) -> (Inhabited U A).
Proof.
Intros; Apply not_included_empty_Inhabited.
Red; Auto with sets.
Qed.
Lemma Inhabited_Setminus :
(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 [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.
Hints Resolve Inhabited_Setminus.
Lemma Strict_super_set_contains_new_element:
(X, Y: (Ensemble U)) (Included U X Y) -> ~ X == Y ->
(Inhabited U (Setminus U Y X)).
Proof.
Auto 7 with sets.
Qed.
Hints Resolve Strict_super_set_contains_new_element.
Lemma Subtract_intro:
(A: (Ensemble U)) (x, y: U) (In U A y) -> ~ x == y ->
(In U (Subtract U A x) y).
Proof.
Unfold 1 Subtract; Auto with sets.
Qed.
Hints Resolve Subtract_intro.
Lemma Subtract_inv:
(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:
(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:
(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:
(X: (Ensemble U)) ~ (Strict_Included U X (Empty_set U)).
Proof.
Intro X; Red; 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 :
(A: (Ensemble U)) (Complement U (Complement U A)) == A.
Proof.
Unfold Complement; Intros; Apply Extensionality_Ensembles; Auto with sets.
Red; Split; Auto with sets.
Red; Intros; Apply NNPP; Auto with sets.
Qed.
End Ensembles_classical.
Hints Resolve Strict_super_set_contains_new_element Subtract_intro
not_SIncl_empty : sets v62.
|
