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 "sequence.ma".
16 include "ordered_set.ma".
19 definition upper_bound ≝ λO:ordered_set.λa:sequence O.λu:O.∀n:nat.a n ≤ u.
22 λO:ordered_set.λs:sequence O.λx.upper_bound ? s x ∧ (∀y:O.x ≰ y → ∃n.s n ≰ y).
24 definition increasing ≝ λO:ordered_set.λa:sequence O.∀n:nat.a n ≤ a (S n).
26 notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 50
27 for @{'upper_bound $s $x}.
28 notation < "s \nbsp 'is_increasing'" non associative with precedence 50
29 for @{'increasing $s}.
30 notation < "x \nbsp 'is_supremum' \nbsp s" non associative with precedence 50
31 for @{'supremum $s $x}.
33 notation > "x 'is_upper_bound' s" non associative with precedence 50
34 for @{'upper_bound $s $x}.
35 notation > "s 'is_increasing'" non associative with precedence 50
36 for @{'increasing $s}.
37 notation > "x 'is_supremum' s" non associative with precedence 50
38 for @{'supremum $s $x}.
40 interpretation "Ordered set upper bound" 'upper_bound s x =
41 (cic:/matita/dama/supremum/upper_bound.con _ s x).
42 interpretation "Ordered set increasing" 'increasing s =
43 (cic:/matita/dama/supremum/increasing.con _ s).
44 interpretation "Ordered set strong sup" 'supremum s x =
45 (cic:/matita/dama/supremum/supremum.con _ s x).
47 include "nat/compare.ma".
48 include "nat/plus.ma".
49 include "bishop_set.ma".
52 ∀O:ordered_set.∀s:sequence O.∀t1,t2:O.
53 t1 is_supremum s → t2 is_supremum s → t1 ≈ t2.
54 intros (O s t1 t2 Ht1 Ht2); cases Ht1 (U1 H1); cases Ht2 (U2 H2);
55 apply le_le_eq; intro X;
56 [1: cases (H1 ? X); apply (U2 w); assumption
57 |2: cases (H2 ? X); apply (U1 w); assumption]
61 lemma supremum_is_upper_bound:
62 ∀C:ordered_set.∀a:sequence C.∀u:C.
63 u is_supremum a → ∀v.v is_upper_bound a → u ≤ v.
64 intros 7 (C s u Hu v Hv H); cases Hu (_ H1); clear Hu;
65 cases (H1 ? H) (w Hw); apply Hv; assumption;
69 definition strictly_increasing ≝ λC:ordered_set.λa:sequence C.∀n:nat.a (S n) ≰ a n.
71 definition nat_excess : nat → nat → CProp ≝ λn,m. leb (m+S O) n = true.
73 axiom nat_excess_cotransitive: cotransitive ? nat_excess.
74 (*intros 3 (x y z); elim x 0; elim y 0; elim z 0;
75 [1: intros; left; assumption
76 |2,5,6,7: intros; first [right; constructor 1|left; constructor 1]
77 |3: intros (n H abs); simplify in abs; destruct abs;
78 |4: intros (n H m W abs); simplify in abs; destruct abs;
79 |8: clear x y z; intros (x H1 y H2 z H3 H4);
82 lemma nat_ordered_set : ordered_set.
83 apply (mk_ordered_set ? nat_excess);
84 [1: intro x; elim x (w H); simplify; intro X; [destruct X] apply H; assumption;
85 |2: apply nat_excess_cotransitive]
88 notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 50
89 for @{'strictly_increasing $s}.
90 notation > "s 'is_strictly_increasing'" non associative with precedence 50
91 for @{'strictly_increasing $s}.
92 interpretation "Ordered set increasing" 'strictly_increasing s =
93 (cic:/matita/dama/supremum/strictly_increasing.con _ s).
95 notation "a \uparrow u" non associative with precedence 50 for @{'sup_inc $a $u}.
96 interpretation "Ordered set supremum of increasing" 'sup_inc s u =
97 (cic:/matita/dama/cprop_connectives/And.ind#xpointer(1/1)
98 (cic:/matita/dama/supremum/increasing.con _ s)
99 (cic:/matita/dama/supremum/supremum.con _ s u)).
101 lemma trans_increasing:
102 ∀C:ordered_set.∀s:sequence C.s is_increasing → ∀n,m. m ≰ n → s n ≤ s m.
103 intros 5 (C s Hs n m); elim m; [1: cases (?:False); autobatch]
104 cases (le_to_or_lt_eq ?? H1);
105 [2: destruct H2; apply Hs;
106 |1: apply (le_transitive ???? (H (lt_S_S_to_lt ?? H2))); apply Hs;]
110 ∀C:ordered_set.∀m:sequence nat_ordered_set.m is_strictly_increasing →
111 ∀a:sequence C.∀u.a ↑ u → (λx.a (m x)) ↑ u.
112 intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split;
113 [1: intro n; simplify; apply trans_increasing; [assumption]
114 lapply (Hm n) as W; unfold nat_ordered_set in W; simplify in W;