helm/software/matita/contribs/dama/dama/supremum.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "sequence.ma".
  16 include "ordered_set.ma".
  17
  18 (* Definition 2.4 *)
  19 definition upper_bound ≝ λO:ordered_set.λa:sequence O.λu:O.∀n:nat.a n ≤ u.
  20 definition lower_bound ≝ λO:ordered_set.λa:sequence O.λu:O.∀n:nat.u ≤ a n.
  21
  22 definition supremum ≝
  23   λO:ordered_set.λs:sequence O.λx.upper_bound ? s x ∧ (∀y:O.x ≰ y → ∃n.s n ≰ y).
  24 definition infimum ≝
  25   λO:ordered_set.λs:sequence O.λx.lower_bound ? s x ∧ (∀y:O.y ≰ x → ∃n.y ≰ s n).
  26
  27 definition increasing ≝ λO:ordered_set.λa:sequence O.∀n:nat.a n ≤ a (S n).
  28 definition decreasing ≝ λO:ordered_set.λa:sequence O.∀n:nat.a (S n) ≤ a n.
  29
  30 notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 50
  31   for @{'upper_bound $s $x}.
  32 notation < "x \nbsp 'is_lower_bound' \nbsp s" non associative with precedence 50
  33   for @{'lower_bound $s $x}.
  34 notation < "s \nbsp 'is_increasing'" non associative with precedence 50
  35   for @{'increasing $s}.
  36 notation < "s \nbsp 'is_decreasing'" non associative with precedence 50
  37   for @{'decreasing $s}.
  38 notation < "x \nbsp 'is_supremum' \nbsp s" non associative with precedence 50
  39   for @{'supremum $s $x}.
  40 notation < "x \nbsp 'is_infimum' \nbsp s" non associative with precedence 50
  41   for @{'infimum $s $x}.
  42
  43 notation > "x 'is_upper_bound' s" non associative with precedence 50
  44   for @{'upper_bound $s $x}.
  45 notation > "x 'is_lower_bound' s" non associative with precedence 50
  46   for @{'lower_bound $s $x}.
  47 notation > "s 'is_increasing'"    non associative with precedence 50
  48   for @{'increasing $s}.
  49 notation > "s 'is_decreasing'"    non associative with precedence 50
  50   for @{'decreasing $s}.
  51 notation > "x 'is_supremum' s"  non associative with precedence 50
  52   for @{'supremum $s $x}.
  53 notation > "x 'is_infimum' s"  non associative with precedence 50
  54   for @{'infimum $s $x}.
  55
  56 interpretation "Ordered set upper bound" 'upper_bound s x =
  57   (cic:/matita/dama/supremum/upper_bound.con _ s x).
  58 interpretation "Ordered set lower bound" 'lower_bound s x =
  59   (cic:/matita/dama/supremum/lower_bound.con _ s x).
  60 interpretation "Ordered set increasing"  'increasing s    =
  61   (cic:/matita/dama/supremum/increasing.con _ s).
  62 interpretation "Ordered set decreasing"  'decreasing s    =
  63   (cic:/matita/dama/supremum/decreasing.con _ s).
  64 interpretation "Ordered set strong sup"  'supremum s x  =
  65   (cic:/matita/dama/supremum/supremum.con _ s x).
  66 interpretation "Ordered set strong inf"  'infimum s x  =
  67   (cic:/matita/dama/supremum/infimum.con _ s x).
  68
  69 include "bishop_set.ma".
  70
  71 lemma uniq_supremum:
  72   ∀O:ordered_set.∀s:sequence O.∀t1,t2:O.
  73     t1 is_supremum s → t2 is_supremum s → t1 ≈ t2.
  74 intros (O s t1 t2 Ht1 Ht2); cases Ht1 (U1 H1); cases Ht2 (U2 H2);
  75 apply le_le_eq; intro X;
  76 [1: cases (H1 ? X); apply (U2 w); assumption
  77 |2: cases (H2 ? X); apply (U1 w); assumption]
  78 qed.
  79
  80 (* Fact 2.5 *)
  81 lemma supremum_is_upper_bound:
  82   ∀C:ordered_set.∀a:sequence C.∀u:C.
  83    u is_supremum a → ∀v.v is_upper_bound a → u ≤ v.
  84 intros 7 (C s u Hu v Hv H); cases Hu (_ H1); clear Hu;
  85 cases (H1 ? H) (w Hw); apply Hv; assumption;
  86 qed.
  87
  88 (* Lemma 2.6 *)
  89 definition strictly_increasing ≝
  90   λC:ordered_set.λa:sequence C.∀n:nat.a (S n) ≰ a n.
  91 definition strictly_decreasing ≝
  92   λC:ordered_set.λa:sequence C.∀n:nat.a n ≰ a (S n).
  93
  94
  95 notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 50
  96   for @{'strictly_increasing $s}.
  97 notation > "s 'is_strictly_increasing'" non associative with precedence 50
  98   for @{'strictly_increasing $s}.
  99 interpretation "Ordered set strict increasing"  'strictly_increasing s    =
 100   (cic:/matita/dama/supremum/strictly_increasing.con _ s).
 101 notation < "s \nbsp 'is_strictly_decreasing'" non associative with precedence 50
 102   for @{'strictly_decreasing $s}.
 103 notation > "s 'is_strictly_decreasing'" non associative with precedence 50
 104   for @{'strictly_decreasing $s}.
 105 interpretation "Ordered set strict decreasing"  'strictly_decreasing s    =
 106   (cic:/matita/dama/supremum/strictly_decreasing.con _ s).
 107
 108 notation "a \uparrow u" non associative with precedence 50 for @{'sup_inc $a $u}.
 109 interpretation "Ordered set supremum of increasing" 'sup_inc s u =
 110  (cic:/matita/dama/cprop_connectives/And.ind#xpointer(1/1)
 111   (cic:/matita/dama/supremum/increasing.con _ s)
 112   (cic:/matita/dama/supremum/supremum.con _ s u)).
 113 notation "a \downarrow u" non associative with precedence 50 for @{'inf_dec $a $u}.
 114 interpretation "Ordered set supremum of increasing" 'inf_dec s u =
 115  (cic:/matita/dama/cprop_connectives/And.ind#xpointer(1/1)
 116   (cic:/matita/dama/supremum/decreasing.con _ s)
 117   (cic:/matita/dama/supremum/infimum.con _ s u)).
 118
 119 include "nat/plus.ma".
 120 include "nat_ordered_set.ma".
 121
 122 alias symbol "nleq" = "Ordered set excess".
 123 alias symbol "leq" = "Ordered set less or equal than".
 124 lemma trans_increasing:
 125   ∀C:ordered_set.∀a:sequence C.a is_increasing → ∀n,m:nat_ordered_set. m ≰ n → a n ≤ a m.
 126 intros 5 (C a Hs n m); elim m; [cases (not_le_Sn_O n H);]
 127 intro; apply H;
 128 [1: change in n1 with (os_carr nat_ordered_set); (* canonical structures *)
 129     change with (n<n1); (* is sort elimination not allowed preserved by delta? *)
 130     cases (le_to_or_lt_eq ?? H1); [apply le_S_S_to_le;assumption]
 131     cases (Hs n); rewrite < H3 in H2; assumption (* ogni goal di tipo Prop non è anche di tipo CProp *)
 132 |2: cases (os_cotransitive ??? (a n1) H2); [assumption]
 133     cases (Hs n1); assumption;]
 134 qed.
 135
 136 lemma strictly_increasing_reaches:
 137   ∀C:ordered_set.∀m:sequence nat_ordered_set.
 138    m is_strictly_increasing → ∀w.∃t.m t ≰ w.
 139 intros; elim w;
 140 [1: cases (nat_discriminable O (m O)); [2: cases (not_le_Sn_n O (ltn_to_ltO ?? H1))]
 141     cases H1; [exists [apply O] apply H2;]
 142     exists [apply (S O)] lapply (H O) as H3; rewrite < H2 in H3; assumption
 143 |2: cases H1 (p Hp); cases (nat_discriminable (S n) (m p));
 144     [1: cases H2; clear H2;
 145         [1: exists [apply p]; assumption;
 146         |2: exists [apply (S p)]; rewrite > H3; apply H;]
 147     |2: cases (?:False); change in Hp with (n<m p);
 148         apply (not_le_Sn_n (m p));
 149         apply (transitive_le ??? H2 Hp);]]
 150 qed.
 151
 152 lemma selection:
 153   ∀C:ordered_set.∀m:sequence nat_ordered_set.m is_strictly_increasing →
 154     ∀a:sequence C.∀u.a ↑ u → (λx.a (m x)) ↑ u.
 155 intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split;
 156 [1: intro n; simplify; apply trans_increasing; [assumption] apply (Hm n);
 157 |2: intro n; simplify; apply Uu;
 158 |3: intros (y Hy); simplify; cases (Hu ? Hy);
 159     cases (strictly_increasing_reaches C ? Hm w);
 160     exists [apply w1]; cases (os_cotransitive ??? (a (m w1)) H); [2:assumption]
 161     cases (trans_increasing C ? Ia ?? H1); assumption;]
 162 qed.
 163
 164 (* Definition 2.7 *)
 165 alias symbol "exists" = "CProp exists".
 166 alias symbol "and" = "constructive and".
 167 definition order_converge ≝
 168   λO:ordered_set.λa:sequence O.λx:O.
 169    ∃l:sequence O.∃u:sequence O.
 170     l is_increasing ∧ u is_decreasing ∧ l ↑ x ∧ u ↓ x ∧
 171     ∀i:nat. (l i) is_infimum (λw.a (w+i)) ∧ (u i) is_supremum (λw.a (w+i)).
 172
 173 notation < "a \nbsp (\circ \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 50
 174   for @{'order_converge $a $x}.
 175 notation > "a 'order_converges' x" non associative with precedence 50
 176   for @{'order_converge $a $x}.
 177 interpretation "Order convergence" 'order_converge s u =
 178  (cic:/matita/dama/supremum/order_converge.con _ s u).
 179
 180 (* Definition 2.8 *)
 181
 182 definition segment ≝ λO:ordered_set.λa,b:O.λx:O.
 183   (cic:/matita/logic/connectives/And.ind#xpointer(1/1) (x ≤ b) (a ≤ x)).
 184
 185 notation "[a,b]" non associative with precedence 50
 186   for @{'segment $a $b}.
 187 interpretation "Ordered set sergment" 'segment a b =
 188   (cic:/matita/dama/supremum/segment.con _ a b).
 189
 190 notation "x \in [a,b]" non associative with precedence 50
 191   for @{'segment2 $a $b $x}.
 192 interpretation "Ordered set sergment in" 'segment2 a b x=
 193   (cic:/matita/dama/supremum/segment.con _ a b x).
 194
 195 coinductive sigma (A:Type) (P:A→Prop) : Type ≝ sig_in : ∀x.P x → sigma A P.
 196
 197 definition pi1 : ∀A.∀P.sigma A P → A ≝ λA,P,s.match s with [sig_in x _ ⇒ x].
 198
 199 notation < "\pi \sub 1 x" non associative with precedence 50 for @{'pi1 $x}.
 200 notation < "\pi \sub 2 x" non associative with precedence 50 for @{'pi2 $x}.
 201 notation > "'fst' x" non associative with precedence 50 for @{'pi1 $x}.
 202 notation > "'snd' x" non associative with precedence 50 for @{'pi2 $x}.
 203 interpretation "sigma pi1" 'pi1 x =
 204  (cic:/matita/dama/supremum/pi1.con _ _ x).
 205
 206 interpretation "Type exists" 'exists \eta.x =
 207   (cic:/matita/dama/supremum/sigma.ind#xpointer(1/1) _ x).
 208
 209 lemma segment_ordered_set:
 210   ∀O:ordered_set.∀u,v:O.ordered_set.
 211 intros (O u v); apply (mk_ordered_set (∃x.x ∈ [u,v]));
 212 [1: intros (x y); apply (fst x ≰ fst y);
 213 |2: intro x; cases x; simplify; apply os_coreflexive;
 214 |3: intros 3 (x y z); cases x; cases y ; cases z; simplify; apply os_cotransitive]
 215 qed.
 216
 217 notation < "{\x|\x \in [a,b]}" non associative with precedence 90
 218   for @{'segment_set $a $b}.
 219 interpretation "Ordered set segment" 'segment_set a b =
 220  (cic:/matita/dama/supremum/segment_ordered_set.con _ a b).
 221
 222 (* Lemma 2.9 *)
 223 lemma segment_preserves_supremum:
 224   ∀O:ordered_set.∀l,u:O.∀a:sequence (segment_ordered_set ? l u).
 225     ∀x:(segment_ordered_set ? l u).
 226     (λn.fst (a n)) is_increasing ∧
 227     (fst x) is_supremum (λn.fst (a n)) → a ↑ x.
 228 intros; split; cases H; clear H;
 229 [1: apply H1;
 230 |2: cases H2; split; clear H2;
 231     [1: apply H;
 232     |2: clear H; intro y0; apply (H3 (fst y0));]]
 233 qed.
 234
 235 (* Definition 2.10 *)
 236 coinductive pair (A,B:Type) : Type ≝ prod : ∀a:A.∀b:B.pair A B.
 237 definition first : ∀A.∀P.pair A P → A ≝ λA,P,s.match s with [prod x _ ⇒ x].
 238 definition second : ∀A.∀P.pair A P → P ≝ λA,P,s.match s with [prod _ y ⇒ y].
 239
 240 interpretation "pair pi1" 'pi1 x =
 241  (cic:/matita/dama/supremum/first.con _ _ x).
 242 interpretation "pair pi2" 'pi2 x =
 243  (cic:/matita/dama/supremum/second.con _ _ x).
 244
 245 lemma square_ordered_set: ordered_set → ordered_set.
 246 intro O; apply (mk_ordered_set (pair O O));
 247 [1: intros (x y); apply (fst x ≰ fst y ∨ snd x ≰ snd y);
 248 |2: intro x0; cases x0 (x y); clear x0; simplify; intro H;
 249     cases H (X X); apply (os_coreflexive ?? X);
 250 |3: intros 3 (x0 y0 z0); cases x0 (x1 x2); cases y0 (y1 y2) ; cases z0 (z1 z2);
 251     clear x0 y0 z0; simplify; intro H; cases H (H1 H1); clear H;
 252     [1: cases (os_cotransitive ??? z1 H1); [left; left|right;left]assumption;
 253     |2: cases (os_cotransitive ??? z2 H1); [left;right|right;right]assumption]]
 254 qed.
 255
 256 definition square_segment ≝
 257   λO:ordered_set.λa,b:O.λx:square_ordered_set O.
 258   (cic:/matita/logic/connectives/And.ind#xpointer(1/1)
 259    (cic:/matita/logic/connectives/And.ind#xpointer(1/1) (fst x ≤ b) (a ≤ fst x))
 260    (cic:/matita/logic/connectives/And.ind#xpointer(1/1) (snd x ≤ b) (a ≤ snd x))).
 261
 262 definition convex ≝
 263   λO:ordered_set.λU:square_ordered_set O → Prop.
 264   ∀p.U p → fst p ≤ snd p → ∀y. square_segment ? (fst p) (snd p) y → U y.
 265
 266 (* Definition 2.11 *)
 267 definition upper_located ≝
 268   λO:ordered_set.λa:sequence O.∀x,y:O. y ≰ x →
 269     (∃i:nat.a i ≰ x) ∨ (∃b:O.y≰b ∧ ∀i:nat.a i ≤ b).
 270
 271 (* Lemma 2.12 *)
 272 lemma uparrow_located:
 273   ∀C:ordered_set.∀a:sequence C.∀u:C.a ↑ u → upper_located ? a.
 274 intros (C a u H); cases H (H2 H3); clear H; intros 3 (x y Hxy);
 275 cases H3 (H4 H5); clear H3; cases (os_cotransitive ??? u Hxy) (W W);
 276 [2: cases (H5 ? W) (w Hw); left; exists [apply w] assumption;
 277 |1: right; exists [apply u]; split; [apply W|apply H4]]
 278 qed.
 279
 280
 281