blob: 371730944254237d61752f93de4290f435ffedbd (
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \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. *)
(****************************************************************************)
(*i $Id: Integers.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
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 Integers : Ensemble nat :=
Integers_defn : forall x:nat, In nat Integers x.
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.
elim le_or_lt with (n := x) (m := y).
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 H'2 with (y := S x); lapply H'2;
[ intro H'5; clear H'2 | try assumption; clear H'2 ].
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.
|
