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 (**************************************************************************)
16 include "datatypes/constructors.ma".
17 include "nat/plus.ma".
18 include "nat_ordered_set.ma".
19 include "sequence.ma".
22 definition upper_bound ≝
23 λO:half_ordered_set.λa:sequence O.λu:O.∀n:nat.a n ≤≤ u.
26 λO:half_ordered_set.λs:sequence O.λx.
27 upper_bound ? s x ∧ (∀y:O.x ≰≰ y → ∃n.s n ≰≰ y).
29 definition increasing ≝
30 λO:half_ordered_set.λa:sequence O.∀n:nat.a n ≤≤ a (S n).
32 notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 45
33 for @{'upper_bound $s $x}.
34 notation < "x \nbsp 'is_lower_bound' \nbsp s" non associative with precedence 45
35 for @{'lower_bound $s $x}.
36 notation < "s \nbsp 'is_increasing'" non associative with precedence 45
37 for @{'increasing $s}.
38 notation < "s \nbsp 'is_decreasing'" non associative with precedence 45
39 for @{'decreasing $s}.
40 notation < "x \nbsp 'is_supremum' \nbsp s" non associative with precedence 45
41 for @{'supremum $s $x}.
42 notation < "x \nbsp 'is_infimum' \nbsp s" non associative with precedence 45
43 for @{'infimum $s $x}.
44 notation > "x 'is_upper_bound' s" non associative with precedence 45
45 for @{'upper_bound $s $x}.
46 notation > "x 'is_lower_bound' s" non associative with precedence 45
47 for @{'lower_bound $s $x}.
48 notation > "s 'is_increasing'" non associative with precedence 45
49 for @{'increasing $s}.
50 notation > "s 'is_decreasing'" non associative with precedence 45
51 for @{'decreasing $s}.
52 notation > "x 'is_supremum' s" non associative with precedence 45
53 for @{'supremum $s $x}.
54 notation > "x 'is_infimum' s" non associative with precedence 45
55 for @{'infimum $s $x}.
57 interpretation "Ordered set upper bound" 'upper_bound s x = (upper_bound (os_l _) s x).
58 interpretation "Ordered set lower bound" 'lower_bound s x = (upper_bound (os_r _) s x).
60 interpretation "Ordered set increasing" 'increasing s = (increasing (os_l _) s).
61 interpretation "Ordered set decreasing" 'decreasing s = (increasing (os_r _) s).
63 interpretation "Ordered set strong sup" 'supremum s x = (supremum (os_l _) s x).
64 interpretation "Ordered set strong inf" 'infimum s x = (supremum (os_r _) s x).
66 (* se non faccio il bs_of_hos perdo dualità qui *)
68 ∀O:ordered_set.∀s:sequence O.∀t1,t2:O.
69 t1 is_supremum s → t2 is_supremum s → t1 ≈ t2.
70 intros (O s t1 t2 Ht1 Ht2); cases Ht1 (U1 H1); cases Ht2 (U2 H2);
71 apply le_le_eq; intro X;
72 [1: cases (H1 ? X); apply (U2 w); assumption
73 |2: cases (H2 ? X); apply (U1 w); assumption]
77 lemma h_supremum_is_upper_bound:
78 ∀C:half_ordered_set.∀a:sequence C.∀u:C.
79 supremum ? a u → ∀v.upper_bound ? a v → u ≤≤ v.
80 intros 7 (C s u Hu v Hv H); cases Hu (_ H1); clear Hu;
81 cases (H1 ? H) (w Hw); apply Hv; [apply w] assumption;
84 notation "'supremum_is_upper_bound'" non associative with precedence 90 for @{'supremum_is_upper_bound}.
85 notation "'infimum_is_lower_bound'" non associative with precedence 90 for @{'infimum_is_lower_bound}.
87 interpretation "supremum_is_upper_bound" 'supremum_is_upper_bound = (h_supremum_is_upper_bound (os_l _)).
88 interpretation "infimum_is_lower_bound" 'infimum_is_lower_bound = (h_supremum_is_upper_bound (os_r _)).
91 lemma test_infimum_is_lower_bound_duality:
92 ∀C:ordered_set.∀a:sequence C.∀u:C.
93 u is_infimum a → ∀v.v is_lower_bound a → u ≥ v.
94 intros; lapply (infimum_is_lower_bound a u H v H1); assumption;
99 definition strictly_increasing ≝
100 λC:half_ordered_set.λa:sequence C.∀n:nat.a (S n) ≰≰ a n.
102 notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 45
103 for @{'strictly_increasing $s}.
104 notation > "s 'is_strictly_increasing'" non associative with precedence 45
105 for @{'strictly_increasing $s}.
106 interpretation "Ordered set strict increasing" 'strictly_increasing s =
107 (strictly_increasing (os_l _) s).
109 notation < "s \nbsp 'is_strictly_decreasing'" non associative with precedence 45
110 for @{'strictly_decreasing $s}.
111 notation > "s 'is_strictly_decreasing'" non associative with precedence 45
112 for @{'strictly_decreasing $s}.
113 interpretation "Ordered set strict decreasing" 'strictly_decreasing s =
114 (strictly_increasing (os_r _) s).
117 λC:half_ordered_set.λs:sequence C.λu:C.
118 increasing ? s ∧ supremum ? s u.
120 notation < "a \uparrow \nbsp u" non associative with precedence 45 for @{'sup_inc $a $u}.
121 notation > "a \uparrow u" non associative with precedence 45 for @{'sup_inc $a $u}.
123 interpretation "Ordered set uparrow" 'funion s u = (uparrow (os_l _) s u).
126 notation < "a \downarrow \nbsp u" non associative with precedence 45 for @{'inf_dec $a $u}.
127 notation > "a \downarrow u" non associative with precedence 45 for @{'inf_dec $a $u}.
129 interpretation "Ordered set downarrow" 'fintersects s u = (uparrow (os_r _) s u).
131 lemma h_trans_increasing:
132 ∀C:half_ordered_set.∀a:sequence C.increasing ? a →
133 ∀n,m:nat_ordered_set. n ≤ m → a n ≤≤ a m.
134 intros 5 (C a Hs n m); elim m; [
135 rewrite > (le_n_O_to_eq n (not_lt_to_le O n H));
136 intro X; cases (hos_coreflexive ?? X);]
137 cases (le_to_or_lt_eq ?? (not_lt_to_le (S n1) n H1)); clear H1;
138 [2: rewrite > H2; intro; cases (hos_coreflexive ?? H1);
139 |1: apply (hle_transitive ???? (H ?) (Hs ?));
140 intro; whd in H1; apply (not_le_Sn_n n); apply (transitive_le ??? H2 H1);]
143 notation "'trans_increasing'" non associative with precedence 90 for @{'trans_increasing}.
144 notation "'trans_decreasing'" non associative with precedence 90 for @{'trans_decreasing}.
146 interpretation "trans_increasing" 'trans_increasing = (h_trans_increasing (os_l _)).
147 interpretation "trans_decreasing" 'trans_decreasing = (h_trans_increasing (os_r _)).
150 lemma test_trans_decreasing_duality:
151 ∀C:ordered_set.∀a:sequence C.a is_decreasing →
152 ∀n,m:nat_ordered_set. n ≤ m → a m ≤ a n.
153 intros; apply (trans_decreasing ? H ?? H1); qed.
156 lemma h_trans_increasing_exc:
157 ∀C:half_ordered_set.∀a:sequence C.increasing ? a →
158 ∀n,m:nat_ordered_set. m ≰ n → a n ≤≤ a m.
159 intros 5 (C a Hs n m); elim m; [cases (not_le_Sn_O n H);]
161 [1: change in n1 with (hos_carr (os_l nat_ordered_set));
163 cases (le_to_or_lt_eq ?? H1); [apply le_S_S_to_le;assumption]
164 cases (Hs n); rewrite < H3 in H2; assumption;
165 |2: cases (hos_cotransitive ??? (a n1) H2); [assumption]
166 cases (Hs n1); assumption;]
169 notation "'trans_increasing_exc'" non associative with precedence 90 for @{'trans_increasing_exc}.
170 notation "'trans_decreasing_exc'" non associative with precedence 90 for @{'trans_decreasing_exc}.
172 interpretation "trans_increasing_exc" 'trans_increasing_exc = (h_trans_increasing_exc (os_l _)).
173 interpretation "trans_decreasing_exc" 'trans_decreasing_exc = (h_trans_increasing_exc (os_r _)).
175 alias symbol "exists" = "CProp exists".
176 lemma nat_strictly_increasing_reaches:
177 ∀m:sequence nat_ordered_set.
178 m is_strictly_increasing → ∀w.∃t.m t ≰ w.
180 [1: cases (nat_discriminable O (m O)); [2: cases (not_le_Sn_n O (ltn_to_ltO ?? H1))]
181 cases H1; [exists [apply O] apply H2;]
182 exists [apply (S O)] lapply (H O) as H3; rewrite < H2 in H3; assumption
183 |2: cases H1 (p Hp); cases (nat_discriminable (S n) (m p));
184 [1: cases H2; clear H2;
185 [1: exists [apply p]; assumption;
186 |2: exists [apply (S p)]; rewrite > H3; apply H;]
187 |2: cases (?:False); change in Hp with (n<m p);
188 apply (not_le_Sn_n (m p));
189 apply (transitive_le ??? H2 Hp);]]
192 lemma h_selection_uparrow:
193 ∀C:half_ordered_set.∀m:sequence nat_ordered_set.
194 m is_strictly_increasing →
195 ∀a:sequence C.∀u.uparrow ? a u → uparrow ? ⌊x,a (m x)⌋ u.
196 intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split;
197 [1: intro n; simplify; apply (h_trans_increasing_exc ? a Ia); apply (Hm n);
198 |2: intro n; simplify; apply Uu;
199 |3: intros (y Hy); simplify; cases (Hu ? Hy);
200 cases (nat_strictly_increasing_reaches ? Hm w);
201 exists [apply w1]; cases (hos_cotransitive ??? (a (m w1)) H); [2:assumption]
202 cases (h_trans_increasing_exc ?? Ia ?? H1); assumption;]
205 notation "'selection_uparrow'" non associative with precedence 90 for @{'selection_uparrow}.
206 notation "'selection_downarrow'" non associative with precedence 90 for @{'selection_downarrow}.
208 interpretation "selection_uparrow" 'selection_uparrow = (h_selection_uparrow (os_l _)).
209 interpretation "selection_downarrow" 'selection_downarrow = (h_selection_uparrow (os_r _)).
212 definition order_converge ≝
213 λO:ordered_set.λa:sequence O.λx:O.
214 exT23 (sequence O) (λl.l ↑ x) (λu.u ↓ x)
215 (λl,u:sequence O.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧
216 (u i) is_supremum ⌊w,a (w+i)⌋).
218 notation < "a \nbsp (\cir \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 45
219 for @{'order_converge $a $x}.
220 notation > "a 'order_converges' x" non associative with precedence 45
221 for @{'order_converge $a $x}.
222 interpretation "Order convergence" 'order_converge s u = (order_converge _ s u).
225 definition segment ≝ λO:half_ordered_set.λa,b:O.λx:O.(x ≤≤ b) ∧ (a ≤≤ x).
227 notation "[term 19 a,term 19 b]" non associative with precedence 90 for @{'segment $a $b}.
228 interpretation "Ordered set sergment" 'segment a b = (segment (os_l _) a b).
230 notation "hvbox(x \in break [term 19 a, term 19 b])" non associative with precedence 45
231 for @{'segment_in $a $b $x}.
232 interpretation "Ordered set sergment in" 'segment_in a b x= (segment (os_l _) a b x).
234 definition segment_ordered_set_carr ≝
235 λO:half_ordered_set.λu,v:O.∃x.segment ? u v x.
236 definition segment_ordered_set_exc ≝
237 λO:half_ordered_set.λu,v:O.
238 λx,y:segment_ordered_set_carr ? u v.\fst x ≰≰ \fst y.
239 lemma segment_ordered_set_corefl:
240 ∀O,u,v. coreflexive ? (segment_ordered_set_exc O u v).
241 intros 4; cases x; simplify; apply hos_coreflexive; qed.
242 lemma segment_ordered_set_cotrans :
243 ∀O,u,v. cotransitive ? (segment_ordered_set_exc O u v).
244 intros 6 (O u v x y z); cases x; cases y ; cases z; simplify; apply hos_cotransitive;
247 lemma half_segment_ordered_set:
248 ∀O:half_ordered_set.∀u,v:O.half_ordered_set.
249 intros (O u v); apply (mk_half_ordered_set ?? (segment_ordered_set_corefl O u v) (segment_ordered_set_cotrans ???));
252 lemma segment_ordered_set:
253 ∀O:ordered_set.∀u,v:O.ordered_set.
254 intros (O u v); letin hos ≝ (half_segment_ordered_set (os_l O) u v);
255 constructor 1; [apply hos; | apply (dual_hos hos); | reflexivity]
258 notation "hvbox({[a, break b]})" non associative with precedence 90
259 for @{'segment_set $a $b}.
260 interpretation "Ordered set segment" 'segment_set a b =
261 (half_segment_ordered_set _ a b).
262 interpretation "Ordered set segment" 'segment_set a b =
263 (segment_ordered_set _ a b).
267 lemma h_segment_preserves_supremum:
268 ∀O:half_ordered_set.∀l,u:O.∀a:sequence {[l,u]}.∀x:{[l,u]}.
269 increasing ? ⌊n,\fst (a n)⌋ ∧
270 supremum ? ⌊n,\fst (a n)⌋ (\fst x) → uparrow ? a x.
271 intros; split; cases H; clear H;
273 |2: cases H2; split; clear H2;
275 |2: clear H; intro y0; apply (H3 (\fst y0));]]
278 notation "'segment_preserves_supremum'" non associative with precedence 90 for @{'segment_preserves_supremum}.
279 notation "'segment_preserves_infimum'" non associative with precedence 90 for @{'segment_preserves_infimum}.
281 interpretation "segment_preserves_supremum" 'segment_preserves_supremum = (h_segment_preserves_supremum (os_l _)).
282 interpretation "segment_preserves_infimum" 'segment_preserves_infimum = (h_segment_preserves_supremum (os_r _)).
284 (* Definition 2.10 *)
285 alias symbol "square" = "ordered set square".
286 alias symbol "pi2" = "pair pi2".
287 alias symbol "pi1" = "pair pi1".
288 definition square_segment ≝
289 λO:ordered_set.λa,b:O.λx: O square.
290 And4 (\fst x ≤ b) (a ≤ \fst x) (\snd x ≤ b) (a ≤ \snd x).
293 λO:ordered_set.λU:O square → Prop.
294 ∀p.U p → \fst p ≤ \snd p → ∀y. square_segment ? (\fst p) (\snd p) y → U y.
296 (* Definition 2.11 *)
297 definition upper_located ≝
298 λO:half_ordered_set.λa:sequence O.∀x,y:O. y ≰≰ x →
299 (∃i:nat.a i ≰≰ x) ∨ (∃b:O.y ≰≰ b ∧ ∀i:nat.a i ≤≤ b).
301 notation < "s \nbsp 'is_upper_located'" non associative with precedence 45
302 for @{'upper_located $s}.
303 notation > "s 'is_upper_located'" non associative with precedence 45
304 for @{'upper_located $s}.
305 interpretation "Ordered set upper locatedness" 'upper_located s =
306 (upper_located (os_l _) s).
308 notation < "s \nbsp 'is_lower_located'" non associative with precedence 45
309 for @{'lower_located $s}.
310 notation > "s 'is_lower_located'" non associative with precedence 45
311 for @{'lower_located $s}.
312 interpretation "Ordered set lower locatedness" 'lower_located s =
313 (upper_located (os_r _) s).
316 lemma h_uparrow_upperlocated:
317 ∀C:half_ordered_set.∀a:sequence C.∀u:C.uparrow ? a u → upper_located ? a.
318 intros (C a u H); cases H (H2 H3); clear H; intros 3 (x y Hxy);
319 cases H3 (H4 H5); clear H3; cases (hos_cotransitive ??? u Hxy) (W W);
320 [2: cases (H5 ? W) (w Hw); left; exists [apply w] assumption;
321 |1: right; exists [apply u]; split; [apply W|apply H4]]
324 notation "'uparrow_upperlocated'" non associative with precedence 90 for @{'uparrow_upperlocated}.
325 notation "'downarrow_lowerlocated'" non associative with precedence 90 for @{'downarrow_lowerlocated}.
327 interpretation "uparrow_upperlocated" 'uparrow_upperlocated = (h_uparrow_upperlocated (os_l _)).
328 interpretation "downarrow_lowerlocated" 'downarrow_lowerlocated = (h_uparrow_upperlocated (os_r _)).