helm/software/matita/library/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
  16 include "datatypes/constructors.ma".
  17 include "nat/plus.ma".
  18 include "dama/nat_ordered_set.ma".
  19 include "dama/sequence.ma".
  20
  21 (* Definition 2.4 *)
  22 definition upper_bound ≝
  23   λO:half_ordered_set.λa:sequence O.λu:O.∀n:nat.a n ≤≤ u.
  24
  25 definition supremum ≝
  26   λO:half_ordered_set.λs:sequence O.λx.
  27     upper_bound ? s x ∧ (∀y:O.x ≰≰ y → ∃n.s n ≰≰ y).
  28
  29 definition increasing ≝
  30   λO:half_ordered_set.λa:sequence O.∀n:nat.a n ≤≤ a (S n).
  31
  32 notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 45
  33   for @{'upper_bound $s $x}.
  34 notation < "x \nbsp 'is_lower_bound' \nbsp s" non associative with precedence 45
  35   for @{'lower_bound $s $x}.
  36 notation < "s \nbsp 'is_increasing'" non associative with precedence 45
  37   for @{'increasing $s}.
  38 notation < "s \nbsp 'is_decreasing'" non associative with precedence 45
  39   for @{'decreasing $s}.
  40 notation < "x \nbsp 'is_supremum' \nbsp s" non associative with precedence 45
  41   for @{'supremum $s $x}.
  42 notation < "x \nbsp 'is_infimum' \nbsp s" non associative with precedence 45
  43   for @{'infimum $s $x}.
  44 notation > "x 'is_upper_bound' s" non associative with precedence 45
  45   for @{'upper_bound $s $x}.
  46 notation > "x 'is_lower_bound' s" non associative with precedence 45
  47   for @{'lower_bound $s $x}.
  48 notation > "s 'is_increasing'"    non associative with precedence 45
  49   for @{'increasing $s}.
  50 notation > "s 'is_decreasing'"    non associative with precedence 45
  51   for @{'decreasing $s}.
  52 notation > "x 'is_supremum' s"  non associative with precedence 45
  53   for @{'supremum $s $x}.
  54 notation > "x 'is_infimum' s"  non associative with precedence 45
  55   for @{'infimum $s $x}.
  56
  57 interpretation "Ordered set upper bound" 'upper_bound s x = (upper_bound (os_l _) s x).
  58 interpretation "Ordered set lower bound" 'lower_bound s x = (upper_bound (os_r _) s x).
  59
  60 interpretation "Ordered set increasing"  'increasing s = (increasing (os_l _) s).
  61 interpretation "Ordered set decreasing"  'decreasing s = (increasing (os_r _) s).
  62
  63 interpretation "Ordered set strong sup"  'supremum s x = (supremum (os_l _) s x).
  64 interpretation "Ordered set strong inf"  'infimum s x = (supremum (os_r _) s x).
  65
  66 (* Fact 2.5 *)
  67 lemma h_supremum_is_upper_bound:
  68   ∀C:half_ordered_set.∀a:sequence C.∀u:C.
  69    supremum ? a u → ∀v.upper_bound ? a v → u ≤≤ v.
  70 intros 7 (C s u Hu v Hv H); cases Hu (_ H1); clear Hu;
  71 cases (H1 ? H) (w Hw); apply Hv; [apply w] assumption;
  72 qed.
  73
  74 notation "'supremum_is_upper_bound'" non associative with precedence 90 for @{'supremum_is_upper_bound}.
  75 notation "'infimum_is_lower_bound'" non associative with precedence 90 for @{'infimum_is_lower_bound}.
  76
  77 interpretation "supremum_is_upper_bound" 'supremum_is_upper_bound = (h_supremum_is_upper_bound (os_l _)).
  78 interpretation "infimum_is_lower_bound" 'infimum_is_lower_bound = (h_supremum_is_upper_bound (os_r _)).
  79
  80 (* Lemma 2.6 *)
  81 definition strictly_increasing ≝
  82   λC:half_ordered_set.λa:sequence C.∀n:nat.a (S n) ≰≰ a n.
  83
  84 notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 45
  85   for @{'strictly_increasing $s}.
  86 notation > "s 'is_strictly_increasing'" non associative with precedence 45
  87   for @{'strictly_increasing $s}.
  88 interpretation "Ordered set strict increasing"  'strictly_increasing s    =
  89   (strictly_increasing (os_l _) s).
  90
  91 notation < "s \nbsp 'is_strictly_decreasing'" non associative with precedence 45
  92   for @{'strictly_decreasing $s}.
  93 notation > "s 'is_strictly_decreasing'" non associative with precedence 45
  94   for @{'strictly_decreasing $s}.
  95 interpretation "Ordered set strict decreasing"  'strictly_decreasing s    =
  96   (strictly_increasing (os_r _) s).
  97
  98 definition uparrow ≝
  99   λC:half_ordered_set.λs:sequence C.λu:C.
 100    increasing ? s ∧ supremum ? s u.
 101
 102 interpretation "Ordered set uparrow" 'funion s u = (uparrow (os_l _) s u).
 103 interpretation "Ordered set downarrow" 'fintersects s u = (uparrow (os_r _) s u).
 104
 105 lemma h_trans_increasing:
 106   ∀C:half_ordered_set.∀a:sequence C.increasing ? a →
 107    ∀n,m:nat_ordered_set. n ≤ m → a n ≤≤ a m.
 108 intros 5 (C a Hs n m); elim m; [
 109   rewrite > (le_n_O_to_eq n (not_lt_to_le O n H));
 110   intro X; cases (hos_coreflexive ? (a n) X);]
 111 cases (le_to_or_lt_eq ?? (not_lt_to_le (S n1) n H1)); clear H1;
 112 [2: rewrite > H2; intro; cases (hos_coreflexive ? (a (S n1)) H1);
 113 |1: apply (hle_transitive ???? (H ?) (Hs ?));
 114     intro; whd in H1; apply (not_le_Sn_n n); apply (transitive_le ??? H2 H1);]
 115 qed.
 116
 117 notation "'trans_increasing'" non associative with precedence 90 for @{'trans_increasing}.
 118 notation "'trans_decreasing'" non associative with precedence 90 for @{'trans_decreasing}.
 119
 120 interpretation "trans_increasing" 'trans_increasing = (h_trans_increasing (os_l _)).
 121 interpretation "trans_decreasing" 'trans_decreasing = (h_trans_increasing (os_r _)).
 122
 123 lemma hint_nat :
 124  Type_OF_ordered_set nat_ordered_set →
 125    hos_carr (os_l (nat_ordered_set)).
 126 intros; assumption;
 127 qed.
 128
 129 coercion hint_nat nocomposites.
 130
 131 lemma h_trans_increasing_exc:
 132   ∀C:half_ordered_set.∀a:sequence C.increasing ? a →
 133    ∀n,m:nat_ordered_set. m ≰≰ n → a n ≤≤ a m.
 134 intros 5 (C a Hs n m); elim m; [cases (not_le_Sn_O n H);]
 135 intro; apply H;
 136 [1: change in n1 with (hos_carr (os_l nat_ordered_set));
 137     change with (n<n1);
 138     cases (le_to_or_lt_eq ?? H1); [apply le_S_S_to_le;assumption]
 139     cases (Hs n); rewrite < H3 in H2; assumption;
 140 |2: cases (hos_cotransitive ? (a n) (a (S n1)) (a n1) H2); [assumption]
 141     cases (Hs n1); assumption;]
 142 qed.
 143
 144 notation "'trans_increasing_exc'" non associative with precedence 90 for @{'trans_increasing_exc}.
 145 notation "'trans_decreasing_exc'" non associative with precedence 90 for @{'trans_decreasing_exc}.
 146
 147 interpretation "trans_increasing_exc" 'trans_increasing_exc = (h_trans_increasing_exc (os_l _)).
 148 interpretation "trans_decreasing_exc" 'trans_decreasing_exc = (h_trans_increasing_exc (os_r _)).
 149
 150 alias symbol "exists" = "CProp exists".
 151 lemma nat_strictly_increasing_reaches:
 152   ∀m:sequence nat_ordered_set.
 153    m is_strictly_increasing → ∀w.∃t.m t ≰ w.
 154 intros; elim w;
 155 [1: cases (nat_discriminable O (m O)); [2: cases (not_le_Sn_n O (ltn_to_ltO ?? H1))]
 156     cases H1; [exists [apply O] apply H2;]
 157     exists [apply (S O)] lapply (H O) as H3; rewrite < H2 in H3; assumption
 158 |2: cases H1 (p Hp); cases (nat_discriminable (S n) (m p));
 159     [1: cases H2; clear H2;
 160         [1: exists [apply p]; assumption;
 161         |2: exists [apply (S p)]; rewrite > H3; apply H;]
 162     |2: cases (?:False); change in Hp with (n<m p);
 163         apply (not_le_Sn_n (m p));
 164         apply (transitive_le ??? H2 Hp);]]
 165 qed.
 166
 167 lemma h_selection_uparrow:
 168   ∀C:half_ordered_set.∀m:sequence nat_ordered_set.
 169    m is_strictly_increasing →
 170     ∀a:sequence C.∀u.uparrow ? a u → uparrow ? ⌊x,a (m x)⌋ u.
 171 intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split;
 172 [1: intro n; simplify; apply (h_trans_increasing_exc ? a Ia); apply (Hm n);
 173 |2: intro n; simplify; apply Uu;
 174 |3: intros (y Hy); simplify; cases (Hu ? Hy);
 175     cases (nat_strictly_increasing_reaches ? Hm w);
 176     exists [apply w1]; cases (hos_cotransitive ? (a w) y (a (m w1)) H); [2:assumption]
 177     cases (h_trans_increasing_exc ?? Ia w (m w1) H1); assumption;]
 178 qed.
 179
 180 notation "'selection_uparrow'" non associative with precedence 90 for @{'selection_uparrow}.
 181 notation "'selection_downarrow'" non associative with precedence 90 for @{'selection_downarrow}.
 182
 183 interpretation "selection_uparrow" 'selection_uparrow = (h_selection_uparrow (os_l _)).
 184 interpretation "selection_downarrow" 'selection_downarrow = (h_selection_uparrow (os_r _)).
 185
 186 (* Definition 2.7 *)
 187 definition order_converge ≝
 188   λO:ordered_set.λa:sequence O.λx:O.
 189    exT23 (sequence O) (λl.l ↑ x) (λu.u ↓ x)
 190      (λl,u:sequence O.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧
 191                    (u i) is_supremum ⌊w,a (w+i)⌋).
 192
 193 notation < "a \nbsp (\cir \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 45
 194   for @{'order_converge $a $x}.
 195 notation > "a 'order_converges' x" non associative with precedence 45
 196   for @{'order_converge $a $x}.
 197 interpretation "Order convergence" 'order_converge s u = (order_converge _ s u).
 198
 199 (* Definition 2.8 *)
 200 record segment (O : Type) : Type ≝ {
 201    seg_l_ : O;
 202    seg_u_ : O
 203 }.
 204
 205 notation > "𝕦_term 90 s" non associative with precedence 90 for @{'upp $s}.
 206 notation "𝕦 \sub term 90 s" non associative with precedence 90 for @{'upp $s}.
 207 notation > "𝕝_term 90 s" non associative with precedence 90 for @{'low $s}.
 208 notation "𝕝 \sub term 90 s" non associative with precedence 90 for @{'low $s}.
 209
 210 definition seg_u ≝
 211  λO:half_ordered_set.λs:segment O.
 212    wloss O ?? (λl,u.l) (seg_u_ ? s) (seg_l_ ? s).
 213 definition seg_l ≝
 214  λO:half_ordered_set.λs:segment O.
 215    wloss O ?? (λl,u.l) (seg_l_ ? s) (seg_u_ ? s).
 216
 217 interpretation "uppper" 'upp s = (seg_u (os_l _) s).
 218 interpretation "lower" 'low s = (seg_l (os_l _) s).
 219 interpretation "uppper dual" 'upp s = (seg_l (os_r _) s).
 220 interpretation "lower dual" 'low s = (seg_u (os_r _) s).
 221
 222 definition in_segment ≝
 223   λO:half_ordered_set.λs:segment O.λx:O.
 224     wloss O ?? (λp1,p2.p1 ∧ p2) (seg_l ? s ≤≤ x) (x ≤≤ seg_u ? s).
 225
 226 notation "‡O" non associative with precedence 90 for @{'segment $O}.
 227 interpretation "Ordered set sergment" 'segment x = (segment x).
 228
 229 interpretation "Ordered set sergment in" 'mem x s = (in_segment _ s x).
 230
 231 definition segment_ordered_set_carr ≝
 232   λO:half_ordered_set.λs:‡O.∃x.x ∈ s.
 233 definition segment_ordered_set_exc ≝
 234   λO:half_ordered_set.λs:‡O.
 235    λx,y:segment_ordered_set_carr O s.hos_excess_ O (\fst x) (\fst y).
 236 lemma segment_ordered_set_corefl:
 237  ∀O,s. coreflexive ? (wloss O ?? (segment_ordered_set_exc O s)).
 238 intros 3; cases x; cases (wloss_prop O);
 239 generalize in match (hos_coreflexive O w);
 240 rewrite < (H1 ?? (segment_ordered_set_exc O s));
 241 rewrite < (H1 ?? (hos_excess_ O)); intros; assumption;
 242 qed.
 243 lemma segment_ordered_set_cotrans :
 244   ∀O,s. cotransitive ? (wloss O ?? (segment_ordered_set_exc O s)).
 245 intros 5 (O s x y z); cases x; cases y ; cases z; clear x y z;
 246 generalize in match (hos_cotransitive O w w1 w2);
 247 cases (wloss_prop O);
 248 do 3 rewrite < (H3 ?? (segment_ordered_set_exc O s));
 249 do 3 rewrite < (H3 ?? (hos_excess_ O)); intros; apply H4; assumption;
 250 qed.
 251
 252 lemma half_segment_ordered_set:
 253   ∀O:half_ordered_set.∀s:segment O.half_ordered_set.
 254 intros (O a); constructor 1;
 255 [ apply (segment_ordered_set_carr O a);
 256 | apply (wloss O);
 257 | apply (wloss_prop O);
 258 | apply (segment_ordered_set_exc O a);
 259 | apply (segment_ordered_set_corefl O a);
 260 | apply (segment_ordered_set_cotrans ??);
 261 ]
 262 qed.
 263
 264 lemma segment_ordered_set:
 265   ∀O:ordered_set.∀s:‡O.ordered_set.
 266 intros (O s);
 267 apply half2full; apply (half_segment_ordered_set (os_l O) s);
 268 qed.
 269
 270 notation "{[ term 19 s ]}" non associative with precedence 90 for @{'segset $s}.
 271 interpretation "Ordered set segment" 'segset s = (segment_ordered_set _ s).
 272
 273 (* test :
 274  ∀O:ordered_set.∀s: segment (os_l O).∀x:O.
 275    in_segment (os_l O) s x
 276    =
 277    in_segment (os_r O) s x.
 278 intros; try reflexivity;
 279 *)
 280
 281 lemma prove_in_segment:
 282  ∀O:half_ordered_set.∀s:segment O.∀x:O.
 283    (seg_l O s) ≤≤ x → x ≤≤ (seg_u O s) → x ∈ s.
 284 intros; unfold; cases (wloss_prop O); rewrite < H2;
 285 split; assumption;
 286 qed.
 287
 288 lemma cases_in_segment:
 289   ∀C:half_ordered_set.∀s:segment C.∀x. x ∈ s → (seg_l C s) ≤≤ x ∧ x ≤≤ (seg_u C s).
 290 intros; unfold in H; cases (wloss_prop C) (W W); rewrite<W in H; [cases H; split;assumption]
 291 cases H; split; assumption;
 292 qed.
 293
 294 definition hint_sequence:
 295   ∀C:ordered_set.
 296     sequence (hos_carr (os_l C)) → sequence (Type_of_ordered_set C).
 297 intros;assumption;
 298 qed.
 299
 300 definition hint_sequence1:
 301   ∀C:ordered_set.
 302     sequence (hos_carr (os_r C)) → sequence (Type_of_ordered_set_dual C).
 303 intros;assumption;
 304 qed.
 305
 306 definition hint_sequence2:
 307   ∀C:ordered_set.
 308     sequence (Type_of_ordered_set C) → sequence (hos_carr (os_l C)).
 309 intros;assumption;
 310 qed.
 311
 312 definition hint_sequence3:
 313   ∀C:ordered_set.
 314     sequence (Type_of_ordered_set_dual C) → sequence (hos_carr (os_r C)).
 315 intros;assumption;
 316 qed.
 317
 318 coercion hint_sequence nocomposites.
 319 coercion hint_sequence1 nocomposites.
 320 coercion hint_sequence2 nocomposites.
 321 coercion hint_sequence3 nocomposites.
 322
 323 (* Lemma 2.9 - non easily dualizable *)
 324
 325 lemma x2sx_:
 326   ∀O:half_ordered_set.
 327    ∀s:segment O.∀x,y:half_segment_ordered_set ? s.
 328     \fst x ≰≰ \fst y → x ≰≰ y.
 329 intros 4; cases x; cases y; clear x y; simplify; unfold hos_excess;
 330 whd in ⊢ (?→? (% ? ?)? ? ? ? ?); simplify in ⊢ (?→%);
 331 cases (wloss_prop O) (E E); do 2 rewrite < E; intros; assumption;
 332 qed.
 333
 334 lemma sx2x_:
 335   ∀O:half_ordered_set.
 336    ∀s:segment O.∀x,y:half_segment_ordered_set ? s.
 337     x ≰≰ y → \fst x ≰≰ \fst y.
 338 intros 4; cases x; cases y; clear x y; simplify; unfold hos_excess;
 339 whd in ⊢ (? (% ? ?) ?? ? ? ? → ?); simplify in ⊢ (% → ?);
 340 cases (wloss_prop O) (E E); do 2 rewrite < E; intros; assumption;
 341 qed.
 342
 343 lemma l2sl_:
 344   ∀C,s.∀x,y:half_segment_ordered_set C s. \fst x ≤≤ \fst y → x ≤≤ y.
 345 intros; intro; apply H; apply sx2x_; apply H1;
 346 qed.
 347
 348
 349 lemma sl2l_:
 350   ∀C,s.∀x,y:half_segment_ordered_set C s. x ≤≤ y → \fst x ≤≤ \fst y.
 351 intros; intro; apply H; apply x2sx_; apply H1;
 352 qed.
 353
 354 coercion x2sx_ nocomposites.
 355 coercion sx2x_ nocomposites.
 356 coercion l2sl_ nocomposites.
 357 coercion sl2l_ nocomposites.
 358
 359 lemma h_segment_preserves_supremum:
 360   ∀O:half_ordered_set.∀s:segment O.
 361    ∀a:sequence (half_segment_ordered_set ? s).
 362     ∀x:half_segment_ordered_set ? s.
 363       increasing ? ⌊n,\fst (a n)⌋ ∧
 364       supremum ? ⌊n,\fst (a n)⌋ (\fst x) → uparrow ? a x.
 365 intros; split; cases H; clear H;
 366 [1: intro n; lapply (H1 n) as K; clear H1 H2;
 367     intro; apply K; clear K; apply rule H;
 368 |2: cases H2; split; clear H2;
 369     [1: intro n; lapply (H n) as K; intro W; apply K;
 370         apply rule W;
 371     |2: clear H1 H; intros (y0 Hy0); cases (H3 (\fst y0));[exists[apply w]]
 372         [1: change in H with (\fst (a w) ≰≰ \fst y0); apply rule H;
 373         |2: apply rule Hy0;]]]
 374 qed.
 375
 376 notation "'segment_preserves_supremum'" non associative with precedence 90 for @{'segment_preserves_supremum}.
 377 notation "'segment_preserves_infimum'" non associative with precedence 90 for @{'segment_preserves_infimum}.
 378
 379 interpretation "segment_preserves_supremum" 'segment_preserves_supremum = (h_segment_preserves_supremum (os_l _)).
 380 interpretation "segment_preserves_infimum" 'segment_preserves_infimum = (h_segment_preserves_supremum (os_r _)).
 381
 382 (*
 383 test segment_preserves_infimum2:
 384   ∀O:ordered_set.∀s:‡O.∀a:sequence {[s]}.∀x:{[s]}.
 385     ⌊n,\fst (a n)⌋ is_decreasing ∧
 386     (\fst x) is_infimum ⌊n,\fst (a n)⌋ → a ↓ x.
 387 intros; apply (segment_preserves_infimum s a x H);
 388 qed.
 389 *)
 390
 391 (* Definition 2.10 *)
 392
 393 alias symbol "pi2" = "pair pi2".
 394 alias symbol "pi1" = "pair pi1".
 395 (*
 396 definition square_segment ≝
 397   λO:half_ordered_set.λs:segment O.λx: square_half_ordered_set O.
 398     in_segment ? s (\fst x) ∧ in_segment ? s (\snd x).
 399 *)
 400 definition convex ≝
 401   λO:half_ordered_set.λU:square_half_ordered_set O → Prop.
 402     ∀s.U s → le O (\fst s) (\snd s) →
 403      ∀y.
 404        le O (\fst y) (\snd s) →
 405        le O (\fst s) (\fst y) →
 406        le O (\snd y) (\snd s) →
 407        le O (\fst y) (\snd y) →
 408        U y.
 409
 410 (* Definition 2.11 *)
 411 definition upper_located ≝
 412   λO:half_ordered_set.λa:sequence O.∀x,y:O. y ≰≰ x →
 413     (∃i:nat.a i ≰≰ x) ∨ (∃b:O.y ≰≰ b ∧ ∀i:nat.a i ≤≤ b).
 414
 415 notation < "s \nbsp 'is_upper_located'" non associative with precedence 45
 416   for @{'upper_located $s}.
 417 notation > "s 'is_upper_located'" non associative with precedence 45
 418   for @{'upper_located $s}.
 419 interpretation "Ordered set upper locatedness" 'upper_located s =
 420   (upper_located (os_l _) s).
 421
 422 notation < "s \nbsp 'is_lower_located'" non associative with precedence 45
 423   for @{'lower_located $s}.
 424 notation > "s 'is_lower_located'" non associative with precedence 45
 425   for @{'lower_located $s}.
 426 interpretation "Ordered set lower locatedness" 'lower_located s =
 427   (upper_located (os_r _) s).
 428
 429 (* Lemma 2.12 *)
 430 lemma h_uparrow_upperlocated:
 431   ∀C:half_ordered_set.∀a:sequence C.∀u:C.uparrow ? a u → upper_located ? a.
 432 intros (C a u H); cases H (H2 H3); clear H; intros 3 (x y Hxy);
 433 cases H3 (H4 H5); clear H3; cases (hos_cotransitive C y x u Hxy) (W W);
 434 [2: cases (H5 x W) (w Hw); left; exists [apply w] assumption;
 435 |1: right; exists [apply u]; split; [apply W|apply H4]]
 436 qed.
 437
 438 notation "'uparrow_upperlocated'" non associative with precedence 90 for @{'uparrow_upperlocated}.
 439 notation "'downarrow_lowerlocated'" non associative with precedence 90 for @{'downarrow_lowerlocated}.
 440
 441 interpretation "uparrow_upperlocated" 'uparrow_upperlocated = (h_uparrow_upperlocated (os_l _)).
 442 interpretation "downarrow_lowerlocated" 'downarrow_lowerlocated = (h_uparrow_upperlocated (os_r _)).