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 (**************************************************************************)
19 record is_dedekind_sigma_complete (O:excess) : Type ≝
20 { dsc_inf: ∀a:nat→O.∀m:O. is_lower_bound ? a m → ex ? (λs:O.is_inf O a s);
21 dsc_inf_proof_irrelevant:
22 ∀a:nat→O.∀m,m':O.∀p:is_lower_bound ? a m.∀p':is_lower_bound ? a m'.
23 (match dsc_inf a m p with [ ex_intro s _ ⇒ s ]) =
24 (match dsc_inf a m' p' with [ ex_intro s' _ ⇒ s' ]);
25 dsc_sup: ∀a:nat→O.∀m:O. is_upper_bound ? a m → ex ? (λs:O.is_sup O a s);
26 dsc_sup_proof_irrelevant:
27 ∀a:nat→O.∀m,m':O.∀p:is_upper_bound ? a m.∀p':is_upper_bound ? a m'.
28 (match dsc_sup a m p with [ ex_intro s _ ⇒ s ]) =
29 (match dsc_sup a m' p' with [ ex_intro s' _ ⇒ s' ])
32 record dedekind_sigma_complete_ordered_set : Type ≝
33 { dscos_ordered_set:> excess;
34 dscos_dedekind_sigma_complete_properties:>
35 is_dedekind_sigma_complete dscos_ordered_set
39 ∀O:dedekind_sigma_complete_ordered_set.
40 bounded_below_sequence O → O.
43 (dsc_inf O (dscos_dedekind_sigma_complete_properties O) b);
45 | apply (lower_bound ? b)
46 | apply lower_bound_is_lower_bound
51 ∀O:dedekind_sigma_complete_ordered_set.
52 ∀a:bounded_below_sequence O.
57 elim (dsc_inf O (dscos_dedekind_sigma_complete_properties O) a
58 (lower_bound O a) (lower_bound_is_lower_bound O a));
63 lemma inf_proof_irrelevant:
64 ∀O:dedekind_sigma_complete_ordered_set.
65 ∀a,a':bounded_below_sequence O.
66 bbs_seq ? a = bbs_seq ? a' →
72 generalize in match i1;
77 rewrite < (dsc_inf_proof_irrelevant O O f (ib_lower_bound ? f i)
78 (ib_lower_bound ? f i2) (ib_lower_bound_is_lower_bound ? f i)
79 (ib_lower_bound_is_lower_bound ? f i2));
84 ∀O:dedekind_sigma_complete_ordered_set.
85 bounded_above_sequence O → O.
88 (dsc_sup O (dscos_dedekind_sigma_complete_properties O) b);
90 | apply (upper_bound ? b)
91 | apply upper_bound_is_upper_bound
96 ∀O:dedekind_sigma_complete_ordered_set.
97 ∀a:bounded_above_sequence O.
102 elim (dsc_sup O (dscos_dedekind_sigma_complete_properties O) a
103 (upper_bound O a) (upper_bound_is_upper_bound O a));
108 lemma sup_proof_irrelevant:
109 ∀O:dedekind_sigma_complete_ordered_set.
110 ∀a,a':bounded_above_sequence O.
111 bas_seq ? a = bas_seq ? a' →
117 generalize in match i1;
122 rewrite < (dsc_sup_proof_irrelevant O O f (ib_upper_bound ? f i2)
123 (ib_upper_bound ? f i) (ib_upper_bound_is_upper_bound ? f i2)
124 (ib_upper_bound_is_upper_bound ? f i));
131 ∀O:dedekind_sigma_complete_ordered_set.
132 ∀a:bounded_sequence O. inf ? a ≤ sup ? a.
134 apply (or_transitive ? ? O' ? (a O));
135 [ elim daemon (*apply (inf_lower_bound ? ? ? ? (inf_is_inf ? ? a))*)
136 | elim daemon (*apply (sup_upper_bound ? ? ? ? (sup_is_sup ? ? a))*)
140 lemma inf_respects_le:
141 ∀O:dedekind_sigma_complete_ordered_set.
142 ∀a:bounded_below_sequence O.∀m:O.
143 is_upper_bound ? a m → inf ? a ≤ m.
145 apply (or_transitive ? ? O' ? (sup ? (mk_bounded_sequence ? a ? ?)));
146 [ apply (bbs_is_bounded_below ? a)
147 | apply (mk_is_bounded_above ? ? m H)
150 (sup_least_upper_bound ? ? ?
151 (sup_is_sup ? (mk_bounded_sequence O' a a
152 (mk_is_bounded_above O' a m H))));
157 definition is_sequentially_monotone ≝
159 ∀a:nat→O.∀p:is_increasing ? a.
160 is_increasing ? (λi.f (a i)).
162 record is_order_continuous
163 (O:dedekind_sigma_complete_ordered_set) (f:O→O) : Prop
165 { ioc_is_sequentially_monotone: is_sequentially_monotone ? f;
166 ioc_is_upper_bound_f_sup:
167 ∀a:bounded_above_sequence O.
168 is_upper_bound ? (λi.f (a i)) (f (sup ? a));
170 ∀a:bounded_above_sequence O.
173 sup ? (mk_bounded_above_sequence ? (λi.f (a i))
174 (mk_is_bounded_above ? ? (f (sup ? a))
175 (ioc_is_upper_bound_f_sup a)));
176 ioc_is_lower_bound_f_inf:
177 ∀a:bounded_below_sequence O.
178 is_lower_bound ? (λi.f (a i)) (f (inf ? a));
180 ∀a:bounded_below_sequence O.
183 inf ? (mk_bounded_below_sequence ? (λi.f (a i))
184 (mk_is_bounded_below ? ? (f (inf ? a))
185 (ioc_is_lower_bound_f_inf a)))
188 theorem tail_inf_increasing:
189 ∀O:dedekind_sigma_complete_ordered_set.
190 ∀a:bounded_below_sequence O.
191 let y ≝ λi.mk_bounded_below_sequence ? (λj.a (i+j)) ? in
192 let x ≝ λi.inf ? (y i) in
194 [ apply (mk_is_bounded_below ? ? (ib_lower_bound ? a a));
197 apply (ib_lower_bound_is_lower_bound ? a a)
199 unfold is_increasing;
201 unfold x in ⊢ (? ? ? %);
202 apply (inf_greatest_lower_bound ? ? ? (inf_is_inf ? (y (S n))));
203 change with (is_lower_bound ? (y (S n)) (inf ? (y n)));
204 unfold is_lower_bound;
206 generalize in match (inf_lower_bound ? ? ? (inf_is_inf ? (y n)) (S n1));
207 (*CSC: coercion per FunClass inserita a mano*)
208 suppose (inf ? (y n) ≤ bbs_seq ? (y n) (S n1)) (H);
209 cut (bbs_seq ? (y n) (S n1) = bbs_seq ? (y (S n)) n1);
214 autobatch paramodulation library
219 definition is_liminf:
220 ∀O:dedekind_sigma_complete_ordered_set.
221 bounded_below_sequence O → O → Prop.
224 (is_sup ? (λi.inf ? (mk_bounded_below_sequence ? (λj.b (i+j)) ?)) t);
225 apply (mk_is_bounded_below ? ? (ib_lower_bound ? b b));
228 apply (ib_lower_bound_is_lower_bound ? b b).
232 ∀O:dedekind_sigma_complete_ordered_set.
233 bounded_sequence O → O.
237 (mk_bounded_above_sequence ?
239 (mk_bounded_below_sequence ?
240 (λj.b (i+j)) ?)) ?));
241 [ apply (mk_is_bounded_below ? ? (ib_lower_bound ? b b));
244 apply (ib_lower_bound_is_lower_bound ? b b)
245 | apply (mk_is_bounded_above ? ? (ib_upper_bound ? b b));
246 unfold is_upper_bound;
250 (mk_bounded_below_sequence O (\lambda j:nat.b (n+j))
251 (mk_is_bounded_below O (\lambda j:nat.b (n+j)) (ib_lower_bound O b b)
252 (\lambda j:nat.ib_lower_bound_is_lower_bound O b b (n+j))))
253 \leq ib_upper_bound O b b);
254 apply (inf_respects_le O);
257 apply (ib_upper_bound_is_upper_bound ? b b)
262 definition reverse_dedekind_sigma_complete_ordered_set:
263 dedekind_sigma_complete_ordered_set → dedekind_sigma_complete_ordered_set.
265 apply mk_dedekind_sigma_complete_ordered_set;
266 [ apply (reverse_ordered_set d)
268 (*apply mk_is_dedekind_sigma_complete;
270 elim (dsc_sup ? ? d a m) 0;
271 [ generalize in match H; clear H;
272 generalize in match m; clear m;
276 change in a1 with (Type_OF_ordered_set ? (reverse_ordered_set ? o));
277 apply (ex_intro ? ? a1);
279 change in m with (Type_OF_ordered_set ? o);
280 apply (is_sup_to_reverse_is_inf ? ? ? ? H1)
281 | generalize in match H; clear H;
282 generalize in match m; clear m;
285 change in t with (Type_OF_ordered_set ? o);
287 apply reverse_is_lower_bound_is_upper_bound;
290 | apply is_sup_reverse_is_inf;
297 definition reverse_bounded_sequence:
298 ∀O:dedekind_sigma_complete_ordered_set.
300 bounded_sequence (reverse_dedekind_sigma_complete_ordered_set O).
302 apply mk_bounded_sequence;
304 unfold reverse_dedekind_sigma_complete_ordered_set;
313 λO:dedekind_sigma_complete_ordered_set.
314 λa:bounded_sequence O.
315 liminf (reverse_dedekind_sigma_complete_ordered_set O)
316 (reverse_bounded_sequence O a).
318 notation "hvbox(〈a〉)"
319 non associative with precedence 45
320 for @{ 'hide_everything_but $a }.
322 interpretation "mk_bounded_above_sequence" 'hide_everything_but a
323 = (cic:/matita/classical_pointfree/ordered_sets/bounded_above_sequence.ind#xpointer(1/1/1) _ _ a _).
325 interpretation "mk_bounded_below_sequence" 'hide_everything_but a
326 = (cic:/matita/classical_pointfree/ordered_sets/bounded_below_sequence.ind#xpointer(1/1/1) _ _ a _).
328 theorem eq_f_sup_sup_f:
329 ∀O':dedekind_sigma_complete_ordered_set.
330 ∀f:O'→O'. ∀H:is_order_continuous ? f.
331 ∀a:bounded_above_sequence O'.
332 ∀p:is_increasing ? a.
333 f (sup ? a) = sup ? (mk_bounded_above_sequence ? (λi.f (a i)) ?).
334 [ apply (mk_is_bounded_above ? ? (f (sup ? a)));
335 apply ioc_is_upper_bound_f_sup;
338 apply ioc_respects_sup;
343 theorem eq_f_sup_sup_f':
344 ∀O':dedekind_sigma_complete_ordered_set.
345 ∀f:O'→O'. ∀H:is_order_continuous ? f.
346 ∀a:bounded_above_sequence O'.
347 ∀p:is_increasing ? a.
348 ∀p':is_bounded_above ? (λi.f (a i)).
349 f (sup ? a) = sup ? (mk_bounded_above_sequence ? (λi.f (a i)) p').
351 rewrite > (eq_f_sup_sup_f ? f H a H1);
352 apply sup_proof_irrelevant;
356 theorem eq_f_liminf_sup_f_inf:
357 ∀O':dedekind_sigma_complete_ordered_set.
358 ∀f:O'→O'. ∀H:is_order_continuous ? f.
359 ∀a:bounded_sequence O'.
363 (mk_bounded_above_sequence ?
365 (mk_bounded_below_sequence ?
369 [ apply (mk_is_bounded_below ? ? (ib_lower_bound ? a a));
372 apply (ib_lower_bound_is_lower_bound ? a a)
373 | apply (mk_is_bounded_above ? ? (f (sup ? a)));
374 unfold is_upper_bound;
376 apply (or_transitive ? ? O' ? (f (a n)));
377 [ generalize in match (ioc_is_lower_bound_f_inf ? ? H);
380 rewrite > (plus_n_O n) in ⊢ (? ? ? (? (? ? ? %)));
381 apply (H1 (mk_bounded_below_sequence O' (\lambda j:nat.a (n+j))
382 (mk_is_bounded_below O' (\lambda j:nat.a (n+j)) (ib_lower_bound O' a a)
383 (\lambda j:nat.ib_lower_bound_is_lower_bound O' a a (n+j)))) O);
384 | elim daemon (*apply (ioc_is_upper_bound_f_sup ? ? ? H)*)
389 generalize in match (\lambda n:nat
391 (mk_bounded_below_sequence O' (\lambda j:nat.a (plus n j))
392 (mk_is_bounded_below O' (\lambda j:nat.a (plus n j))
393 (ib_lower_bound O' a a)
394 (\lambda j:nat.ib_lower_bound_is_lower_bound O' a a (plus n j))))
395 (ib_upper_bound O' a a)
396 (\lambda n1:nat.ib_upper_bound_is_upper_bound O' a a (plus n n1)));
398 apply (eq_f_sup_sup_f' ? f H (mk_bounded_above_sequence O'
401 (mk_bounded_below_sequence O' (\lambda j:nat.a (plus i j))
402 (mk_is_bounded_below O' (\lambda j:nat.a (plus i j))
403 (ib_lower_bound O' a a)
404 (\lambda n:nat.ib_lower_bound_is_lower_bound O' a a (plus i n)))))
405 (mk_is_bounded_above O'
408 (mk_bounded_below_sequence O' (\lambda j:nat.a (plus i j))
409 (mk_is_bounded_below O' (\lambda j:nat.a (plus i j))
410 (ib_lower_bound O' a a)
411 (\lambda n:nat.ib_lower_bound_is_lower_bound O' a a (plus i n)))))
412 (ib_upper_bound O' a a) p2)));
415 (is_increasing ? (\lambda i:nat
417 (mk_bounded_below_sequence O' (\lambda j:nat.a (plus i j))
418 (mk_is_bounded_below O' (\lambda j:nat.a (plus i j))
419 (ib_lower_bound O' a a)
420 (\lambda n:nat.ib_lower_bound_is_lower_bound O' a a (plus i n))))));
421 apply tail_inf_increasing