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 set "baseuri" "cic:/matita/ordered_sets/".
17 include "higher_order_defs/relations.ma".
18 include "nat/plus.ma".
19 include "constructive_connectives.ma".
21 definition cotransitive ≝
22 λC:Type.λle:C→C→Prop.∀x,y,z:C. le x y → le x z ∨ le z y.
24 definition antisimmetric ≝
25 λC:Type.λle:C→C→Prop.∀x,y:C. le x y → le y x → x=y.
27 record is_order_relation (C:Type) (le:C→C→Prop) : Type ≝
28 { or_reflexive: reflexive ? le;
29 or_transitive: transitive ? le;
30 or_antisimmetric: antisimmetric ? le
33 record ordered_set: Type ≝
35 os_le: os_carrier → os_carrier → Prop;
36 os_order_relation_properties:> is_order_relation ? os_le
39 interpretation "Ordered Sets le" 'leq a b =
40 (cic:/matita/ordered_sets/os_le.con _ a b).
42 theorem antisimmetric_to_cotransitive_to_transitive:
43 ∀C.∀le:relation C. antisimmetric ? le → cotransitive ? le →
50 | rewrite < (H ? ? H2 t);
55 definition is_increasing ≝ λO:ordered_set.λa:nat→O.∀n:nat.a n ≤ a (S n).
56 definition is_decreasing ≝ λO:ordered_set.λa:nat→O.∀n:nat.a (S n) ≤ a n.
58 definition is_upper_bound ≝ λO:ordered_set.λa:nat→O.λu:O.∀n:nat.a n ≤ u.
59 definition is_lower_bound ≝ λO:ordered_set.λa:nat→O.λu:O.∀n:nat.u ≤ a n.
61 record is_sup (O:ordered_set) (a:nat→O) (u:O) : Prop ≝
62 { sup_upper_bound: is_upper_bound O a u;
63 sup_least_upper_bound: ∀v:O. is_upper_bound O a v → u≤v
66 record is_inf (O:ordered_set) (a:nat→O) (u:O) : Prop ≝
67 { inf_lower_bound: is_lower_bound O a u;
68 inf_greatest_lower_bound: ∀v:O. is_lower_bound O a v → v≤u
71 record is_bounded_below (O:ordered_set) (a:nat→O) : Type ≝
73 ib_lower_bound_is_lower_bound: is_lower_bound ? a ib_lower_bound
76 record is_bounded_above (O:ordered_set) (a:nat→O) : Type ≝
78 ib_upper_bound_is_upper_bound: is_upper_bound ? a ib_upper_bound
81 record is_bounded (O:ordered_set) (a:nat→O) : Type ≝
82 { ib_bounded_below:> is_bounded_below ? a;
83 ib_bounded_above:> is_bounded_above ? a
86 record bounded_below_sequence (O:ordered_set) : Type ≝
88 bbs_is_bounded_below:> is_bounded_below ? bbs_seq
91 record bounded_above_sequence (O:ordered_set) : Type ≝
93 bas_is_bounded_above:> is_bounded_above ? bas_seq
96 record bounded_sequence (O:ordered_set) : Type ≝
98 bs_is_bounded_below: is_bounded_below ? bs_seq;
99 bs_is_bounded_above: is_bounded_above ? bs_seq
102 definition bounded_below_sequence_of_bounded_sequence ≝
103 λO:ordered_set.λb:bounded_sequence O.
104 mk_bounded_below_sequence ? b (bs_is_bounded_below ? b).
106 coercion cic:/matita/ordered_sets/bounded_below_sequence_of_bounded_sequence.con.
108 definition bounded_above_sequence_of_bounded_sequence ≝
109 λO:ordered_set.λb:bounded_sequence O.
110 mk_bounded_above_sequence ? b (bs_is_bounded_above ? b).
112 coercion cic:/matita/ordered_sets/bounded_above_sequence_of_bounded_sequence.con.
114 definition lower_bound ≝
115 λO:ordered_set.λb:bounded_below_sequence O.
116 ib_lower_bound ? b (bbs_is_bounded_below ? b).
118 lemma lower_bound_is_lower_bound:
119 ∀O:ordered_set.∀b:bounded_below_sequence O.
120 is_lower_bound ? b (lower_bound ? b).
123 apply ib_lower_bound_is_lower_bound.
126 definition upper_bound ≝
127 λO:ordered_set.λb:bounded_above_sequence O.
128 ib_upper_bound ? b (bas_is_bounded_above ? b).
130 lemma upper_bound_is_upper_bound:
131 ∀O:ordered_set.∀b:bounded_above_sequence O.
132 is_upper_bound ? b (upper_bound ? b).
135 apply ib_upper_bound_is_upper_bound.
138 definition lt ≝ λO:ordered_set.λa,b:O.a ≤ b ∧ a ≠ b.
140 interpretation "Ordered set lt" 'lt a b =
141 (cic:/matita/ordered_sets/lt.con _ a b).
143 definition reverse_ordered_set: ordered_set → ordered_set.
145 apply mk_ordered_set;
146 [2:apply (λx,y:o.y ≤ x)
148 | apply mk_is_order_relation;
151 apply (or_reflexive ? ? o)
154 apply (or_transitive ? ? o);
161 apply (or_antisimmetric ? ? o);
167 interpretation "Ordered set ge" 'geq a b =
168 (cic:/matita/ordered_sets/os_le.con _
169 (cic:/matita/ordered_sets/os_pre_ordered_set.con _
170 (cic:/matita/ordered_sets/reverse_ordered_set.con _ _)) a b).
172 lemma is_lower_bound_reverse_is_upper_bound:
173 ∀O:ordered_set.∀a:nat→O.∀l:O.
174 is_lower_bound O a l → is_upper_bound (reverse_ordered_set O) a l.
179 unfold reverse_ordered_set;
184 lemma is_upper_bound_reverse_is_lower_bound:
185 ∀O:ordered_set.∀a:nat→O.∀l:O.
186 is_upper_bound O a l → is_lower_bound (reverse_ordered_set O) a l.
191 unfold reverse_ordered_set;
196 lemma reverse_is_lower_bound_is_upper_bound:
197 ∀O:ordered_set.∀a:nat→O.∀l:O.
198 is_lower_bound (reverse_ordered_set O) a l → is_upper_bound O a l.
201 unfold reverse_ordered_set in H;
205 lemma reverse_is_upper_bound_is_lower_bound:
206 ∀O:ordered_set.∀a:nat→O.∀l:O.
207 is_upper_bound (reverse_ordered_set O) a l → is_lower_bound O a l.
210 unfold reverse_ordered_set in H;
215 lemma is_inf_to_reverse_is_sup:
216 ∀O:ordered_set.∀a:bounded_below_sequence O.∀l:O.
217 is_inf O a l → is_sup (reverse_ordered_set O) a l.
219 apply (mk_is_sup (reverse_ordered_set O));
220 [ apply is_lower_bound_reverse_is_upper_bound;
221 apply inf_lower_bound;
224 change in v with (os_carrier O);
226 apply (inf_greatest_lower_bound ? ? ? H);
227 apply reverse_is_upper_bound_is_lower_bound;
232 lemma is_sup_to_reverse_is_inf:
233 ∀O:ordered_set.∀a:bounded_above_sequence O.∀l:O.
234 is_sup O a l → is_inf (reverse_ordered_set O) a l.
236 apply (mk_is_inf (reverse_ordered_set O));
237 [ apply is_upper_bound_reverse_is_lower_bound;
238 apply sup_upper_bound;
241 change in v with (os_carrier O);
243 apply (sup_least_upper_bound ? ? ? H);
244 apply reverse_is_lower_bound_is_upper_bound;
249 lemma reverse_is_sup_to_is_inf:
250 ∀O:ordered_set.∀a:bounded_above_sequence O.∀l:O.
251 is_sup (reverse_ordered_set O) a l → is_inf O a l.
254 [ apply reverse_is_upper_bound_is_lower_bound;
255 change in l with (os_carrier (reverse_ordered_set O));
256 apply sup_upper_bound;
259 change in l with (os_carrier (reverse_ordered_set O));
260 change in v with (os_carrier (reverse_ordered_set O));
261 change with (os_le (reverse_ordered_set O) l v);
262 apply (sup_least_upper_bound ? ? ? H);
263 change in v with (os_carrier O);
264 apply is_lower_bound_reverse_is_upper_bound;
269 lemma reverse_is_inf_to_is_sup:
270 ∀O:ordered_set.∀a:bounded_above_sequence O.∀l:O.
271 is_inf (reverse_ordered_set O) a l → is_sup O a l.
274 [ apply reverse_is_lower_bound_is_upper_bound;
275 change in l with (os_carrier (reverse_ordered_set O));
276 apply (inf_lower_bound ? ? ? H)
278 change in l with (os_carrier (reverse_ordered_set O));
279 change in v with (os_carrier (reverse_ordered_set O));
280 change with (os_le (reverse_ordered_set O) v l);
281 apply (inf_greatest_lower_bound ? ? ? H);
282 change in v with (os_carrier O);
283 apply is_upper_bound_reverse_is_lower_bound;
288 record cotransitively_ordered_set: Type :=
289 { cos_ordered_set :> ordered_set;
290 cos_cotransitive: cotransitive ? (os_le cos_ordered_set)