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 "dama/models/nat_uniform.ma".
16 include "dama/supremum.ma".
17 include "nat/le_arith.ma".
18 include "dama/russell_support.ma".
21 ∀s.sequence (Type_of_ordered_set (segment_ordered_set nat_ordered_set s))
22 → sequence (hos_carr (os_l (segment_ordered_set nat_ordered_set s))).
26 coercion hint1 nocomposites.
28 alias symbol "pi1" = "exT \fst".
29 alias symbol "N" = "ordered set N".
30 lemma increasing_supremum_stabilizes:
31 ∀sg:‡ℕ.∀a:sequence {[sg]}.
33 ∀X.X is_supremum a → ∃i.∀j.i ≤ j → \fst X = \fst (a j).
34 intros 4; cases X (x Hx); clear X; letin X ≝ ≪x,Hx≫;
35 fold normalize X; intros; cases H1;
36 alias symbol "N" = "Natural numbers".
37 letin spec ≝ (λi,j:ℕ.(𝕦_sg ≤ i ∧ x = \fst (a j)) ∨ (i < 𝕦_sg ∧ x + i ≤ 𝕦_sg + \fst (a j)));
38 (* x - aj <= max 0 (u - i) *)
46 match cmp_nat x (\fst apred) with
48 | cmp_gt nP ⇒ \fst (H3 apred ?)]]
51 ∀i:nat.∃j:nat.spec i j));[whd; apply nP;] unfold spec in aux ⊢ %;
52 [3: unfold X in H2; clear H4 n aux spec H3 H1 H X;
53 cases (cases_in_segment ??? Hx);
54 elim 𝕦_sg in H1 ⊢ %; intros (a Hs H);
55 [1: left; split; [apply le_n]
56 generalize in match H;
57 generalize in match Hx;
59 [2: cases Hx; lapply (os_le_to_nat_le ?? H1);
60 apply (symmetric_eq nat O x ?).apply (le_n_O_to_eq x ?).apply (Hletin).
61 |1: intros; unfold Type_of_ordered_set in sg;
62 lapply (H2 O) as K; lapply (sl2l_ ?? (a O) ≪x,Hx≫ K) as P;
63 simplify in P:(???%); lapply (le_transitive ??? P H1) as W;
64 lapply (os_le_to_nat_le ?? W) as R; apply (le_n_O_to_eq (\fst (a O)) R);]
65 |2: right; cases Hx; rewrite > (sym_plus x O); split; [apply le_S_S; apply le_O_n];
66 apply (trans_le ??? (os_le_to_nat_le ?? H3));
68 |2: clear H6; cut (x = \fst (a (aux n1))); [2:
69 cases (le_to_or_lt_eq ?? H5); [2: assumption]
70 cases (?:False); apply (H2 (aux n1) H6);] clear H5;
71 generalize in match Hcut; clear Hcut; intro H5;
74 cases (aux n1) in H5 ⊢ %; intros;
75 change in match (a ≪w,H5≫) in H6 ⊢ % with (a w);
76 cases H5; clear H5; cases H7; clear H7;
77 [1: left; split; [ apply (le_S ?? H5); | assumption]
78 |3: cases (?:False); rewrite < H8 in H6; apply (not_le_Sn_n ? H6);
79 |*: cases (cmp_nat 𝕦_sg (S n1));
80 [1,3: left; split; [1,3: assumption |2: assumption]
81 cut (𝕦_sg = S n1); [2: apply le_to_le_to_eq; assumption ]
82 clear H7 H5 H4;rewrite > Hcut in H8:(? ? (? % ?)); clear Hcut;
83 cut (x = S (\fst (a w)));
84 [2: apply le_to_le_to_eq; [2: assumption]
85 change in H8 with (x + n1 ≤ S (n1 + \fst (a w)));
86 rewrite > plus_n_Sm in H8; rewrite > sym_plus in H8;
87 apply (le_plus_to_le ??? H8);]
89 change with (x = \fst (a w1));
90 change in H4 with (\fst (a w) < \fst (a w1));
91 apply le_to_le_to_eq; [ rewrite > Hcut; assumption ]
92 apply (os_le_to_nat_le (\fst (a w1)) x (H2 w1));
93 |*: right; split; try assumption;
94 [1: rewrite > sym_plus in ⊢ (? ? %);
95 rewrite < H6; apply le_plus_r; assumption;
96 |2: cases (H3 (a w) H6);
97 change with (x + S n1 ≤ 𝕦_sg + \fst (a w1));rewrite < plus_n_Sm;
98 apply (trans_le ??? (le_S_S ?? H8)); rewrite > plus_n_Sm;
99 apply (le_plus ???? (le_n ?) H9);]]]]
100 clearbody m; unfold spec in m; clear spec;
102 let rec find i u on u : nat ≝
105 | S w ⇒ match eqb (\fst (a (m i))) x with
107 | false ⇒ find (S i) w]]
110 ∀i,bound.∃j.i + bound = 𝕦_sg → x = \fst (a j));
111 [1: cases (find (S n) n2); intro; change with (x = \fst (a w));
112 apply H6; rewrite < H7; simplify; apply plus_n_Sm;
113 |2: intros; rewrite > (eqb_true_to_eq ?? H5); reflexivity
114 |3: intros; rewrite > sym_plus in H5; rewrite > H5; clear H5 H4 n n1;
115 cases (m 𝕦_sg); cases H4; clear H4; cases H5; clear H5; [assumption]
116 cases (not_le_Sn_n ? H4)]
117 clearbody find; cases (find O 𝕦_sg);
118 exists [apply w]; intros; change with (x = \fst (a j));
119 rewrite > (H4 ?); [2: reflexivity]
120 apply le_to_le_to_eq;
121 [1: apply os_le_to_nat_le;
122 apply (trans_increasing ? H ? ? (nat_le_to_os_le ?? H5));
123 |2: apply (trans_le ? x ?);[apply os_le_to_nat_le; apply (H2 j);]
124 rewrite < (H4 ?); [2: reflexivity] apply le_n;]
128 ∀s.sequence (Type_of_ordered_set (segment_ordered_set nat_ordered_set s))
129 → sequence (hos_carr (os_r (segment_ordered_set nat_ordered_set s))).
133 coercion hint2 nocomposites.
135 alias symbol "N" = "ordered set N".
136 axiom increasing_supremum_stabilizes_r:
137 ∀s:‡ℕ.∀a:sequence {[s]}.a is_decreasing →
138 ∀x.x is_infimum a → ∃i.∀j.i ≤ j → \fst x = \fst (a j).