1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "nat_ordered_set.ma".
16 include "bishop_set_rewrite.ma".
19 definition discrete_uniform_space_of_bishop_set:bishop_set → uniform_space.
20 intro C; apply (mk_uniform_space C);
21 [1: intro; apply (∃_:unit.∀n:C square.(fst n ≈ snd n → P n) ∧ (P n → fst n ≈ snd n));
22 |2: intros 4 (U H x Hx); unfold in Hx;
23 cases H (_ H1); cases (H1 x); apply H2; apply Hx;
24 |3: intros; cases H (_ PU); cases H1 (_ PV);
25 exists[apply (λx.U x ∧ V x)] split;
26 [1: exists[apply something] intro; cases (PU n); cases (PV n);
27 split; intros; try split;[apply H2;|apply H4] try assumption;
28 apply H3; cases H6; assumption;
29 |2: simplify; unfold mk_set; intros; assumption;]
30 |4: intros; cases H (_ PU); exists [apply U] split;
31 [1: exists [apply something] intro n; cases (PU n);
32 split; intros; try split;[apply H1;|apply H2] assumption;
33 |2: intros 2 (x Hx); cases Hx; cases H1; clear H1;
34 cases (PU 〈(fst x),x1〉); lapply (H4 H2) as H5; simplify in H5;
35 cases (PU 〈x1,(snd x)〉); lapply (H7 H3) as H8; simplify in H8;
36 generalize in match H5; generalize in match H8;
37 generalize in match (PU x); clear H6 H7 H1 H4 H2 H3 H5 H8;
38 cases x; simplify; intros; cases H1; clear H1; apply H4;
39 apply (eq_trans ???? H3 H2);]
40 |5: intros; cases H (_ H1); split; cases x;
41 [2: cases (H1 〈b,b1〉); intro; apply H2; cases (H1 〈b1,b〉);
42 lapply (H6 H4) as H7; apply eq_sym; apply H7;
43 |1: cases (H1 〈b1,b〉); intro; apply H2; cases (H1 〈b,b1〉);
44 lapply (H6 H4) as H7; apply eq_sym; apply H7;]]
48 notation "\naturals" non associative with precedence 99 for @{'nat}.
50 interpretation "naturals" 'nat = nat.
51 interpretation "Ordered set N" 'nat = nat_ordered_set.
53 include "russell_support.ma".
55 inductive cmp_cases (n,m:nat) : CProp ≝
56 | cmp_lt : n < m → cmp_cases n m
57 | cmp_eq : n = m → cmp_cases n m
58 | cmp_gt : m < n → cmp_cases n m.
60 lemma cmp_nat: ∀n,m.cmp_cases n m.
62 simplify; intros; generalize in match (nat_compare_to_Prop n m);
63 cases (nat_compare n m); intros;
64 [constructor 1|constructor 2|constructor 3]
69 ∀n,m,o:nat.n≤m→m<o→n<o.
70 intros; apply (trans_le ? (S m)); [apply le_S_S;apply H;|apply H1]
73 alias symbol "lt" (instance 2) = "ordered sets less than".
75 ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing → ∀n,m. a n < a m → n < m.
76 intros; cases (cmp_nat n m);
78 |generalize in match H1; rewrite < H2; intros;
79 cases (not_lt_n_n (fst (a n))); apply os_lt_to_nat_lt; apply H3;
80 |cases (not_lt_n_n (fst (a m)));
81 apply (trans_le_lt_lt ? (fst (a n)));
82 [2: apply os_lt_to_nat_lt; apply H1;
83 |1: apply os_le_to_nat_le; apply (trans_increasing ?? H m n);
84 apply nat_le_to_os_le; apply le_S_S_to_le; apply le_S; apply H2]]
87 lemma le_lt_transitive:
88 ∀O:ordered_set.∀a,b,c:O.a≤b→b<c→a<c.
91 [1: apply (le_transitive ???? H); cases H1; assumption;
92 |2: cases H1; cases (bs_cotransitive ??? a H3); [2:assumption]
93 cut (a<b);[2: split; [assumption] apply bs_symmetric; assumption]
94 cut (a<c);[2: apply (lt_transitive ???? Hcut H1);]
95 cases Hcut1; assumption]
98 alias symbol "pi1" = "sigma pi1".
99 lemma nat_dedekind_sigma_complete:
100 ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing →
101 ∀x.x is_supremum a → ∃i.∀j.i ≤ j → fst x = fst (a j).
102 intros 5; cases x (s Hs); clear x; letin X ≝ (sig_in ℕ (λx:ℕ.x∈[l,u]) s Hs);
103 fold normalize X; intros; cases H1;
104 alias symbol "pi1" = "sigma pi1".
105 letin spec ≝ (λi,j.fst (a j) = s ∨ (i ≤ j ∧ match i with [ O ⇒ fst (a j) = fst (a O) | S m ⇒ fst(a m) < fst (a j)]));
112 let apred ≝ a pred in
113 match cmp_nat (fst apred) s with
115 | cmp_gt nP ⇒ match ? in False return λ_.nat with []
116 | cmp_lt nP ⇒ fst (H3 apred nP)]]
119 ∀i:nat.∃j:nat.spec i j);unfold spec in aux ⊢ %;
120 [1: apply (H2 pred nP);
121 |4: right; split; whd; constructor 1;
122 |2,3: whd in ⊢ (? ? %);
124 |2: elim (H3 (a (aux n1)) H5) (res_n);
125 change with (fst (a res_n) = s ∨ (n1 < res_n ∧ fst (a n1) < fst (a res_n)));
126 change in H7 with (fst (a (aux n1)) < fst (a res_n));
127 elim (aux n1) in H7 ⊢ % (pred);
128 change in H8 with (fst (a pred) < fst (a res_n));
130 [ left; apply le_to_le_to_eq;
131 [ apply os_le_to_nat_le; apply (H2 res_n);
132 | rewrite < H9; apply le_S_S_to_le; apply le_S; apply H8;]
133 | cases H9; clear H9; right; split;
134 [ lapply (trans_increasing ?? H n1 pred (nat_le_to_os_le ?? H7)) as H11;
135 clear H6; apply (key ??? H);
136 apply (le_lt_transitive ?? (a pred)); [assumption]
137 generalize in match H8; cases (a pred); cases (a res_n);
138 simplify; intro D; lapply (nat_lt_to_os_lt ?? D) as Q;
139 cases Q; clear D Q; split; assumption;
140 | generalize in match H10; generalize in match H7; clear H7 H10;
142 [ rewrite < H9; assumption
143 | clear H9; apply (trans_le_lt_lt ??? ? H8);
144 apply os_le_to_nat_le; lapply (nat_le_to_os_le ?? H7) as H77;
145 apply(trans_increasing ?? H (S n2) (pred) H77);]]]]]
146 clearbody m; unfold spec in m; clear spec;
147 cut (∀i.fst a (m i) = s ∨ i ≤ fst (a (m i))) as key2;[
149 let rec find i u on u : nat ≝
152 | S w ⇒ match eqb (fst (a (m i))) s with
154 | false ⇒ find (S i) w]]
157 ∀i,bound.∃j.i + bound = u → s = fst (a j));
158 [1: cases (find (S n) n2); intro; change with (s = fst (a w));
159 apply H6; rewrite < H7; simplify; apply plus_n_Sm;
160 |2: intros; rewrite > (eqb_true_to_eq ?? H5); reflexivity
161 |3: intros; rewrite > sym_plus in H5; rewrite > H5; clear H5 H4 n n1;
162 cases (key2 u); [symmetry;assumption]
163 cases Hs; apply le_to_le_to_eq;[2:change with (fst (a (m u)) ≤ fst X); apply os_le_to_nat_le; apply (H2 (m u));]
164 apply (trans_le ??? (os_le_to_nat_le ?? H5) H4);
165 |4: clearbody find; cases (find O u);
166 exists [apply w]; intros; change with (s = fst (a j));
167 rewrite > (H4 ?); [2: reflexivity]
168 apply le_to_le_to_eq; [apply os_le_to_nat_le;
169 apply (trans_increasing ?? H ? ? (nat_le_to_os_le ?? H5));]
170 apply (trans_le ? s ?);[apply os_le_to_nat_le; apply (H2 j);]
171 rewrite < (H4 ?); [2: reflexivity] apply le_n;]]
172 alias symbol "pi1" (instance 15) = "exT fst".
173 alias symbol "pi1" (instance 10) = "exT fst".
174 alias symbol "pi1" (instance 7) = "exT fst".
175 alias symbol "pi1" (instance 4) = "exT fst".
176 alias symbol "nat" = "naturals".
177 cut (∀i.fst (a (fst (m i))) = s
181 match i in nat return λn:ℕ.Prop with
182 [O⇒ fst (a (fst(m i))) = fst (a O)
183 |S (w:ℕ)⇒fst (a w) < fst (a (fst(m i)))]) as mitico;[2:
184 intro; cases (m i); apply H4;]
185 cut (∀i.fst (a (m i)) = s ∨ fst (a (m i)) < fst (a (m (S i))));[2:
187 cases (mitico (S i));
188 [2: cases (mitico i);
189 [2: cases H5 (H6 _); cases H4 (_ H7); clear H4 H5;
190 change in H7 with (fst (a i) < fst (a (fst (m (S i)))));
194 generalize in match (mitico i); clear mitico;
197 cases (m i); intros; cases H5; clear H5;
199 cases H6; clear H6; simplify in H7;
201 change with (fst (a w)=s ∨ a w<a (m (S i)));
202 cases H4; [left; assumption]
203 cases H5; clear H4 H5;
204 cases (m (S i)); change with (fst (a w)=s ∨ a w<a w1);
211 [1: cases (m (S O)); change with (fst (a (m O))=s∨a (m O)<a w);
212 |2: cases (m (S (S n))); change with (fst (a (m (S n)))=s∨a (m (S n))<a w);
216 [change with (le nat_ordered_set (fst (a (m O))) (fst (a w)));
217 rewrite > H5; apply (H2 (m O));
219 |2: cases H5; clear H5; change in H6 with (fst (a O) < fst (a w));
220 right; split; [change with (le nat_ordered_set (fst (a (m O))) (fst (a w)));
221 apply nat_le_to_os_le; apply le_S_S_to_le; apply le_S;
227 cases (m O); change with (fst (a w) = s ∨ a w < a (m (S O)));
228 cases H4[left; assumption] cases H5; clear H4 H5;
229 change in H7 with (fst (a w) = fst (a O));
232 intro; elim i; [1: right; apply le_O_n;]
233 generalize in match (refl_eq ? (S n):S n = S n);
234 generalize in match (S n) in ⊢ (? ? ? % → %); intro R;
235 cases (m R); intros; change with (fst (a w) = s ∨ R ≤ fst (a w));
236 rewrite < H6 in H5 ⊢ %; clear H6 R; cases H5; [left; assumption]
237 cases H6; clear H6 H5; change in H8 with (fst (a n) < fst (a w));
238 lapply (key l u a H n w);
252 match cmp_nat (fst a0) s with
254 | cmp_gt nP ⇒ match ? in False return λ_.nat with []
255 | cmp_lt nP ⇒ fst (H3 a0 nP)]
258 let apred ≝ a pred in
259 match cmp_nat (fst apred) s with
261 | cmp_gt nP ⇒ match ? in False return λ_.nat with []
267 ∀i:nat.∃j:nat.spec i j);unfold spec in aux ⊢ %;
269 |2: apply (H2 pred nP);
270 |5: left; assumption;
271 |6: right; cases (H3 (a O) H5); change with (fst (a O) < fst (a w));
273 |4: right; elim (H3 (a (aux n1)) H5); change with (fst (a (S n1)) < fst (a a1));
274 rewrite < H4; elim (aux n1) in H7 ⊢ %; elim H7 in H8; clear H7;
277 |3: clear H6; generalize in match H5; cases (aux n1); intros; clear H5;
284 definition nat_uniform_space: uniform_space.
285 apply (discrete_uniform_space_of_bishop_set ℕ);
288 interpretation "Uniform space N" 'nat = nat_uniform_space.
290 include "ordered_uniform.ma".
292 definition nat_ordered_uniform_space:ordered_uniform_space.
293 apply (mk_ordered_uniform_space (mk_ordered_uniform_space_ ℕ ℕ (refl_eq ? ℕ)));
294 simplify; intros 7; cases H3; cases H4; cases H5; clear H5 H4;
295 cases H (_); cases (H4 y); apply H5; clear H5 H10; cases (H4 p);
296 lapply (H10 H1) as H11; clear H10 H5; apply (le_le_eq);
297 [1: apply (le_transitive ???? H6); apply (Le≪ ? H11); assumption;
298 |2: apply (le_transitive ????? H7); apply (Le≫ (snd p) H11); assumption;]
301 interpretation "Uniform space N" 'nat = nat_ordered_uniform_space.
303 lemma nat_us_is_oc: ∀l,u:ℕ.order_continuity {[l,u]}.
304 intros 4; split; intros 3; cases H; cases H3; clear H3 H;
306 cases (H10 (sig_in ?? x1 H2));
308 exists [1,3:apply x1]