blob: 03572d760612a7d1882675c375b4cc4e1691e66b (
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
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(****************************************************************************)
(* *)
(* 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 Finite_sets.
Require Export Constructive_sets.
Require Export Classical_Type.
Require Export Classical_sets.
Require Export Powerset.
Require Export Powerset_facts.
Require Export Powerset_Classical_facts.
Require Export Gt.
Require Export Lt.
Require Export Le.
Require Export Finite_sets_facts.
Require Export Image.
Require Export Infinite_sets.
Require Export Compare_dec.
Require Export Relations_1.
Require Export Partial_Order.
Require Export Cpo.
Section Integers_sect.
Inductive Nat : Type :=
mkNat: nat -> Nat.
Parameter nat_of_Nat: Nat -> nat.
Axiom nat_of_nat_returns: (n: nat) (nat_of_Nat (mkNat n)) = n.
Lemma mkNat_injective: (n1, n2: nat) (mkNat n1) == (mkNat n2) -> n1 = n2.
Proof.
Intros n1 n2 H'; Try Assumption.
Rewrite <- (nat_of_nat_returns n1).
Rewrite <- (nat_of_nat_returns n2).
Rewrite H'; Auto with sets arith.
Qed.
Inductive Integers : (Ensemble Nat) :=
Integers_defn: (x: Nat) (In Nat Integers x).
Hints Resolve Integers_defn.
Inductive Le_Nat [x, y:Nat]: Prop :=
Definition_of_Le_nat:
(n1, n2: nat) x == (mkNat n1) -> y == (mkNat n2) -> (le n1 n2) ->
(Le_Nat x y).
Lemma Le_Nat_direct: (n1, n2: nat) (le n1 n2) -> (Le_Nat (mkNat n1) (mkNat n2)).
Proof.
Intros n1 n2 H'.
Apply Definition_of_Le_nat with n1 := n1 n2 := n2; Auto with sets arith.
Qed.
Hints Resolve Le_Nat_direct.
Lemma Le_Nat_Reflexive: (Reflexive Nat Le_Nat).
Proof.
Red.
Intro x; Elim x; Auto with sets arith.
Qed.
Hints Resolve Le_Nat_Reflexive.
Lemma Le_Nat_antisym: (Antisymmetric Nat Le_Nat).
Proof.
Red.
Intros x y H'; Elim H'.
Intros n1 n2 H'0 H'1 H'2 H'3; Elim H'3.
Intros n3 n4 H'4 H'5 H'6.
Cut n1 = n4 /\ n2 = n3.
Intro H'7.
Generalize H'6.
Elim H'7; Intros H'8 H'9; Rewrite <- H'8; Clear H'7.
Rewrite <- H'9.
Intro H'7.
Cut n1 = n2.
Rewrite H'0; Rewrite H'1.
Intro H'10; Rewrite <- H'10; Auto with sets arith.
Apply le_antisym; Auto with sets arith.
Split; Apply mkNat_injective.
Rewrite <- H'5; Rewrite H'0; Auto with sets arith.
Rewrite <- H'4; Rewrite H'1; Auto with sets arith.
Qed.
Hints Resolve Le_Nat_antisym.
Lemma Le_Nat_trans: (Transitive Nat Le_Nat).
Proof.
Red.
Intros x y z H'; Elim H'.
Intros n1 n2 H'0 H'1 H'2 H'3; Elim H'3.
Intros n3 n4 H'4 H'5 H'6.
Rewrite H'0; Rewrite H'5.
Apply Le_Nat_direct.
Apply le_trans with m := n3; Auto with sets arith.
Cut n2 = n3.
Intro H'7; Rewrite <- H'7; Auto with sets arith.
Apply mkNat_injective.
Rewrite <- H'4; Rewrite <- H'1; Auto with sets arith.
Qed.
Hints Resolve Le_Nat_trans.
Lemma Le_Nat_Order: (Order Nat Le_Nat).
Proof.
Auto with sets arith.
Qed.
Hints Resolve Le_Nat_Order.
Definition Nat_O := (mkNat O).
Lemma triv_Nat: (n: nat) (In Nat Integers (mkNat n)).
Proof.
Auto with sets arith.
Qed.
Hints Resolve triv_Nat.
Definition Nat_po: (PO Nat).
Apply Definition_of_PO with Carrier_of := Integers Rel_of := Le_Nat; Auto with sets arith.
Apply Inhabited_intro with x := Nat_O; Auto with sets arith.
Defined.
Hints Unfold Nat_po.
Lemma Le_Nat_total_order: (Totally_ordered Nat Nat_po Integers).
Proof.
Apply Totally_ordered_definition.
Simpl.
Intros H' x; Elim x.
Intros n y; Elim y.
Intros n0 H'0.
Specialize 2 le_or_lt with n := n m := n0; Intro H'2; Elim H'2.
Intro H'1; Left; Auto with sets arith.
Intro H'1; Right.
Cut (le n0 n); Auto with sets arith.
Qed.
Hints Resolve Le_Nat_total_order.
Lemma Finite_subset_has_lub:
(X: (Ensemble Nat)) (Finite Nat X) ->
(EXT m: Nat | (Upper_Bound Nat Nat_po X m)).
Proof.
Intros X H'; Elim H'.
Exists Nat_O.
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_Nat_total_order.
Simpl.
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.
Intros y H'1; Elim H'1.
Generalize Le_Nat_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; 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.
Intros y H'1; Elim H'1.
Intros x1 H'4; Try Assumption.
Elim H'3; Simpl; Auto with sets arith.
Intros x1 H'4; Elim H'4; Auto with sets arith.
Red.
Intros x1 H'1; Elim H'1; Auto with sets arith.
Qed.
Lemma Integers_has_no_ub: ~ (EXT m:Nat | (Upper_Bound Nat Nat_po Integers m)).
Proof.
Red; Intro H'; Elim H'.
Intro x; Elim x.
Intros n H'0; Elim H'0.
Intros H'1 H'2; Try Assumption.
Cut (In Nat Integers (mkNat (S n))).
Intro H'3; Try Assumption.
Specialize 1 H'2 with y := (mkNat (S n)); Intro H'4; LApply H'4;
[Intro H'5; Clear H'4 | Try Assumption; Clear H'4].
Simpl in H'5.
Elim H'5.
Intros n1 n2 H'4 H'6; Try Assumption.
Specialize 2 mkNat_injective with n1 := (S n) n2 := n1; Intro H'8; LApply H'8;
[Intro H'9; Rewrite <- H'9; Clear H'8 | Clear H'8]; Auto with sets arith.
Specialize 2 mkNat_injective with n1 := n n2 := n2; Intro H'8; LApply H'8;
[Intro H'10; Rewrite <- H'10; Clear H'8 | Clear H'8]; Auto with sets arith.
Intro H'7; Try Assumption.
Specialize 1 le_Sn_n with n := n; Intro H'8; Elim H'8.
Auto with sets arith.
Auto with sets arith.
Qed.
Lemma Integers_infinite: ~ (Finite Nat Integers).
Proof.
Generalize Integers_has_no_ub.
Intro H'; Red; Intro H'0; Try Exact H'0.
Apply H'.
Apply Finite_subset_has_lub; Auto with sets arith.
Qed.
End Integers_sect.
|
