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 "bishop_set.ma".
50 ∀O:ordered_set.∀s:sequence O.∀t1,t2:O.
51 t1 is_supremum s → t2 is_supremum s → t1 ≈ t2.
52 intros (O s t1 t2 Ht1 Ht2); cases Ht1 (U1 H1); cases Ht2 (U2 H2);
53 apply le_le_eq; intro X;
54 [1: cases (H1 ? X); apply (U2 w); assumption
55 |2: cases (H2 ? X); apply (U1 w); assumption]
59 lemma supremum_is_upper_bound:
60 ∀C:ordered_set.∀a:sequence C.∀u:C.
61 u is_supremum a → ∀v.v is_upper_bound a → u ≤ v.
62 intros 7 (C s u Hu v Hv H); cases Hu (_ H1); clear Hu;
63 cases (H1 ? H) (w Hw); apply Hv; assumption;
67 definition strictly_increasing ≝
68 λC:ordered_set.λa:sequence C.∀n:nat.a (S n) ≰ a n.
70 notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 50
71 for @{'strictly_increasing $s}.
72 notation > "s 'is_strictly_increasing'" non associative with precedence 50
73 for @{'strictly_increasing $s}.
74 interpretation "Ordered set increasing" 'strictly_increasing s =
75 (cic:/matita/dama/supremum/strictly_increasing.con _ s).
77 notation "a \uparrow u" non associative with precedence 50 for @{'sup_inc $a $u}.
78 interpretation "Ordered set supremum of increasing" 'sup_inc s u =
79 (cic:/matita/dama/cprop_connectives/And.ind#xpointer(1/1)
80 (cic:/matita/dama/supremum/increasing.con _ s)
81 (cic:/matita/dama/supremum/supremum.con _ s u)).
83 include "nat_ordered_set.ma".
85 alias symbol "nleq" = "Ordered set excess".
86 alias symbol "leq" = "Ordered set less or equal than".
87 lemma trans_increasing:
88 ∀C:ordered_set.∀a:sequence C.a is_increasing → ∀n,m:nat_ordered_set. m ≰ n → a n ≤ a m.
89 intros 5 (C a Hs n m); elim m; [cases (not_le_Sn_O n H);]
91 [1: change in n1 with (os_carr nat_ordered_set); (* canonical structures *)
92 change with (n<n1); (* is sort elimination not allowed preserved by delta? *)
93 cases (le_to_or_lt_eq ?? H1); [apply le_S_S_to_le;assumption]
94 cases (Hs n); rewrite < H3 in H2; assumption (* ogni goal di tipo Prop non è anche di tipo CProp *)
95 |2: cases (os_cotransitive ??? (a n1) H2); [assumption]
96 cases (Hs n1); assumption;]
99 lemma strictly_increasing_reaches:
100 ∀C:ordered_set.∀m:sequence nat_ordered_set.
101 m is_strictly_increasing → ∀w.∃t.m t ≰ w.
103 [1: cases (nat_discriminable O (m O)); [2: cases (not_le_Sn_n O (ltn_to_ltO ?? H1))]
104 cases H1; [exists [apply O] apply H2;]
105 exists [apply (S O)] lapply (H O) as H3; rewrite < H2 in H3; assumption
106 |2: cases H1 (p Hp); cases (nat_discriminable (S n) (m p));
107 [1: cases H2; clear H2;
108 [1: exists [apply p]; assumption;
109 |2: exists [apply (S p)]; rewrite > H3; apply H;]
110 |2: cases (?:False); change in Hp with (n<m p);
111 apply (not_le_Sn_n (m p));
112 apply (transitive_le ??? H2 Hp);]]
116 ∀C:ordered_set.∀m:sequence nat_ordered_set.m is_strictly_increasing →
117 ∀a:sequence C.∀u.a ↑ u → (λx.a (m x)) ↑ u.
118 intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split;
119 [1: intro n; simplify; apply trans_increasing; [assumption] apply (Hm n);
120 |2: intro n; simplify; apply Uu;
121 |3: intros (y Hy); simplify; cases (Hu ? Hy);
122 cases (strictly_increasing_reaches C ? Hm w);
123 exists [apply w1]; cases (os_cotransitive ??? (a (m w1)) H); [2:assumption]
124 cases (trans_increasing C ? Ia ?? H1); assumption;]