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
  16 include "datatypes/constructors.ma".
  17 include "nat/plus.ma".
  18 include "nat_ordered_set.ma".
  19 include "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 (* se non faccio il bs_of_hos perdo dualità qui *)
  67 lemma uniq_supremum:
  68   ∀O:ordered_set.∀s:sequence O.∀t1,t2:O.
  69     t1 is_supremum s → t2 is_supremum s → t1 ≈ t2.
  70 intros (O s t1 t2 Ht1 Ht2); cases Ht1 (U1 H1); cases Ht2 (U2 H2);
  71 apply le_le_eq; intro X;
  72 [1: cases (H1 ? X); apply (U2 w); assumption
  73 |2: cases (H2 ? X); apply (U1 w); assumption]
  74 qed.
  75
  76 (* Fact 2.5 *)
  77 lemma h_supremum_is_upper_bound:
  78   ∀C:half_ordered_set.∀a:sequence C.∀u:C.
  79    supremum ? a u → ∀v.upper_bound ? a v → u ≤≤ v.
  80 intros 7 (C s u Hu v Hv H); cases Hu (_ H1); clear Hu;
  81 cases (H1 ? H) (w Hw); apply Hv; [apply w] assumption;
  82 qed.
  83
  84 notation "'supremum_is_upper_bound'" non associative with precedence 90 for @{'supremum_is_upper_bound}.
  85 notation "'infimum_is_lower_bound'" non associative with precedence 90 for @{'infimum_is_lower_bound}.
  86
  87 interpretation "supremum_is_upper_bound" 'supremum_is_upper_bound = (h_supremum_is_upper_bound (os_l _)).
  88 interpretation "infimum_is_lower_bound" 'infimum_is_lower_bound = (h_supremum_is_upper_bound (os_r _)).
  89
  90 (* TEST DUALITY
  91 lemma test_infimum_is_lower_bound_duality:
  92   ∀C:ordered_set.∀a:sequence C.∀u:C.
  93    u is_infimum a → ∀v.v is_lower_bound a → u ≥ v.
  94 intros; lapply (infimum_is_lower_bound a u H v H1); assumption;
  95 qed.
  96 *)
  97
  98 (* Lemma 2.6 *)
  99 definition strictly_increasing ≝
 100   λC:half_ordered_set.λa:sequence C.∀n:nat.a (S n) ≰≰ a n.
 101
 102 notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 45
 103   for @{'strictly_increasing $s}.
 104 notation > "s 'is_strictly_increasing'" non associative with precedence 45
 105   for @{'strictly_increasing $s}.
 106 interpretation "Ordered set strict increasing"  'strictly_increasing s    =
 107   (strictly_increasing (os_l _) s).
 108
 109 notation < "s \nbsp 'is_strictly_decreasing'" non associative with precedence 45
 110   for @{'strictly_decreasing $s}.
 111 notation > "s 'is_strictly_decreasing'" non associative with precedence 45
 112   for @{'strictly_decreasing $s}.
 113 interpretation "Ordered set strict decreasing"  'strictly_decreasing s    =
 114   (strictly_increasing (os_r _) s).
 115
 116 definition uparrow ≝
 117   λC:half_ordered_set.λs:sequence C.λu:C.
 118    increasing ? s ∧ supremum ? s u.
 119 (*
 120 notation < "a \uparrow \nbsp u" non associative with precedence 45 for @{'sup_inc $a $u}.
 121 notation > "a \uparrow u" non associative with precedence 45 for @{'sup_inc $a $u}.
 122 *)
 123 interpretation "Ordered set uparrow" 'funion s u = (uparrow (os_l _) s u).
 124
 125 (*
 126 notation < "a \downarrow \nbsp u" non associative with precedence 45 for @{'inf_dec $a $u}.
 127 notation > "a \downarrow u" non associative with precedence 45 for @{'inf_dec $a $u}.
 128 *)
 129 interpretation "Ordered set downarrow" 'fintersects s u = (uparrow (os_r _) s u).
 130
 131 lemma h_trans_increasing:
 132   ∀C:half_ordered_set.∀a:sequence C.increasing ? a →
 133    ∀n,m:nat_ordered_set. n ≤ m → a n ≤≤ a m.
 134 intros 5 (C a Hs n m); elim m; [
 135   rewrite > (le_n_O_to_eq n (not_lt_to_le O n H));
 136   intro X; cases (hos_coreflexive ?? X);]
 137 cases (le_to_or_lt_eq ?? (not_lt_to_le (S n1) n H1)); clear H1;
 138 [2: rewrite > H2; intro; cases (hos_coreflexive ?? H1);
 139 |1: apply (hle_transitive ???? (H ?) (Hs ?));
 140     intro; whd in H1; apply (not_le_Sn_n n); apply (transitive_le ??? H2 H1);]
 141 qed.
 142
 143 notation "'trans_increasing'" non associative with precedence 90 for @{'trans_increasing}.
 144 notation "'trans_decreasing'" non associative with precedence 90 for @{'trans_decreasing}.
 145
 146 interpretation "trans_increasing" 'trans_increasing = (h_trans_increasing (os_l _)).
 147 interpretation "trans_decreasing" 'trans_decreasing = (h_trans_increasing (os_r _)).
 148
 149 (* TEST DUALITY
 150 lemma test_trans_decreasing_duality:
 151   ∀C:ordered_set.∀a:sequence C.a is_decreasing →
 152    ∀n,m:nat_ordered_set. n ≤ m → a m ≤ a n.
 153 intros; apply (trans_decreasing ? H ?? H1); qed.
 154 *)
 155
 156 lemma h_trans_increasing_exc:
 157   ∀C:half_ordered_set.∀a:sequence C.increasing ? a →
 158    ∀n,m:nat_ordered_set. m ≰ n → a n ≤≤ a m.
 159 intros 5 (C a Hs n m); elim m; [cases (not_le_Sn_O n H);]
 160 intro; apply H;
 161 [1: change in n1 with (hos_carr (os_l nat_ordered_set));
 162     change with (n<n1);
 163     cases (le_to_or_lt_eq ?? H1); [apply le_S_S_to_le;assumption]
 164     cases (Hs n); rewrite < H3 in H2; assumption;
 165 |2: cases (hos_cotransitive ??? (a n1) H2); [assumption]
 166     cases (Hs n1); assumption;]
 167 qed.
 168
 169 notation "'trans_increasing_exc'" non associative with precedence 90 for @{'trans_increasing_exc}.
 170 notation "'trans_decreasing_exc'" non associative with precedence 90 for @{'trans_decreasing_exc}.
 171
 172 interpretation "trans_increasing_exc" 'trans_increasing_exc = (h_trans_increasing_exc (os_l _)).
 173 interpretation "trans_decreasing_exc" 'trans_decreasing_exc = (h_trans_increasing_exc (os_r _)).
 174
 175 alias symbol "exists" = "CProp exists".
 176 lemma nat_strictly_increasing_reaches:
 177   ∀m:sequence nat_ordered_set.
 178    m is_strictly_increasing → ∀w.∃t.m t ≰ w.
 179 intros; elim w;
 180 [1: cases (nat_discriminable O (m O)); [2: cases (not_le_Sn_n O (ltn_to_ltO ?? H1))]
 181     cases H1; [exists [apply O] apply H2;]
 182     exists [apply (S O)] lapply (H O) as H3; rewrite < H2 in H3; assumption
 183 |2: cases H1 (p Hp); cases (nat_discriminable (S n) (m p));
 184     [1: cases H2; clear H2;
 185         [1: exists [apply p]; assumption;
 186         |2: exists [apply (S p)]; rewrite > H3; apply H;]
 187     |2: cases (?:False); change in Hp with (n<m p);
 188         apply (not_le_Sn_n (m p));
 189         apply (transitive_le ??? H2 Hp);]]
 190 qed.
 191
 192 lemma h_selection_uparrow:
 193   ∀C:half_ordered_set.∀m:sequence nat_ordered_set.
 194    m is_strictly_increasing →
 195     ∀a:sequence C.∀u.uparrow ? a u → uparrow ? ⌊x,a (m x)⌋ u.
 196 intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split;
 197 [1: intro n; simplify; apply (h_trans_increasing_exc ? a Ia); apply (Hm n);
 198 |2: intro n; simplify; apply Uu;
 199 |3: intros (y Hy); simplify; cases (Hu ? Hy);
 200     cases (nat_strictly_increasing_reaches ? Hm w);
 201     exists [apply w1]; cases (hos_cotransitive ??? (a (m w1)) H); [2:assumption]
 202     cases (h_trans_increasing_exc ?? Ia ?? H1); assumption;]
 203 qed.
 204
 205 notation "'selection_uparrow'" non associative with precedence 90 for @{'selection_uparrow}.
 206 notation "'selection_downarrow'" non associative with precedence 90 for @{'selection_downarrow}.
 207
 208 interpretation "selection_uparrow" 'selection_uparrow = (h_selection_uparrow (os_l _)).
 209 interpretation "selection_downarrow" 'selection_downarrow = (h_selection_uparrow (os_r _)).
 210
 211 (* Definition 2.7 *)
 212 definition order_converge ≝
 213   λO:ordered_set.λa:sequence O.λx:O.
 214    exT23 (sequence O) (λl.l ↑ x) (λu.u ↓ x)
 215      (λl,u:sequence O.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧
 216                    (u i) is_supremum ⌊w,a (w+i)⌋).
 217
 218 notation < "a \nbsp (\cir \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 45
 219   for @{'order_converge $a $x}.
 220 notation > "a 'order_converges' x" non associative with precedence 45
 221   for @{'order_converge $a $x}.
 222 interpretation "Order convergence" 'order_converge s u = (order_converge _ s u).
 223
 224 (* Definition 2.8 *)
 225 definition segment ≝ λO:half_ordered_set.λa,b:O.λx:O.(x ≤≤ b) ∧ (a ≤≤ x).
 226
 227 notation "[term 19 a,term 19 b]" non associative with precedence 90 for @{'segment $a $b}.
 228 interpretation "Ordered set sergment" 'segment a b = (segment (os_l _) a b).
 229
 230 notation "hvbox(x \in break [term 19 a, term 19 b])" non associative with precedence 45
 231   for @{'segment_in $a $b $x}.
 232 interpretation "Ordered set sergment in" 'segment_in a b x= (segment (os_l _) a b x).
 233
 234 definition segment_ordered_set_carr ≝
 235   λO:half_ordered_set.λu,v:O.∃x.segment ? u v x.
 236 definition segment_ordered_set_exc ≝
 237   λO:half_ordered_set.λu,v:O.
 238    λx,y:segment_ordered_set_carr ? u v.\fst x ≰≰ \fst y.
 239 lemma segment_ordered_set_corefl:
 240  ∀O,u,v. coreflexive ? (segment_ordered_set_exc O u v).
 241 intros 4; cases x; simplify; apply hos_coreflexive; qed.
 242 lemma segment_ordered_set_cotrans :
 243   ∀O,u,v. cotransitive ? (segment_ordered_set_exc O u v).
 244 intros 6 (O u v x y z); cases x; cases y ; cases z; simplify; apply hos_cotransitive;
 245 qed.
 246
 247 lemma half_segment_ordered_set:
 248   ∀O:half_ordered_set.∀u,v:O.half_ordered_set.
 249 intros (O u v); apply (mk_half_ordered_set ?? (segment_ordered_set_corefl O u v) (segment_ordered_set_cotrans ???));
 250 qed.
 251
 252 lemma segment_ordered_set:
 253   ∀O:ordered_set.∀u,v:O.ordered_set.
 254 intros (O u v);
 255 apply half2full; apply (half_segment_ordered_set (os_l O) u v);
 256 qed.
 257
 258 (*
 259 notation < "hvbox({[a, break b]/})" non associative with precedence 90
 260   for @{'h_segment_set $a $b}.
 261 notation > "hvbox({[a, break b]/})" non associative with precedence 90
 262   for @{'h_segment_set $a $b}.
 263 interpretation "Half ordered set segment" 'h_segment_set a b =
 264   (half_segment_ordered_set _ a b).
 265 *)
 266
 267 notation < "hvbox({[a, break b]})" non associative with precedence 90
 268   for @{'segment_set $a $b}.
 269 notation > "hvbox({[a, break b]})" non associative with precedence 90
 270   for @{'segment_set $a $b}.
 271 interpretation "Ordered set segment" 'segment_set a b =
 272   (segment_ordered_set _ a b).
 273
 274 definition hint_sequence:
 275   ∀C:ordered_set.
 276     sequence (hos_carr (os_l C)) → sequence (Type_of_ordered_set C).
 277 intros;assumption;
 278 qed.
 279
 280 definition hint_sequence1:
 281   ∀C:ordered_set.
 282     sequence (hos_carr (os_r C)) → sequence (Type_of_ordered_set_dual C).
 283 intros;assumption;
 284 qed.
 285
 286 definition hint_sequence2:
 287   ∀C:ordered_set.
 288     sequence (Type_of_ordered_set C) → sequence (hos_carr (os_l C)).
 289 intros;assumption;
 290 qed.
 291
 292 definition hint_sequence3:
 293   ∀C:ordered_set.
 294     sequence (Type_of_ordered_set_dual C) → sequence (hos_carr (os_r C)).
 295 intros;assumption;
 296 qed.
 297
 298 coercion hint_sequence nocomposites.
 299 coercion hint_sequence1 nocomposites.
 300 coercion hint_sequence2 nocomposites.
 301 coercion hint_sequence3 nocomposites.
 302
 303 (* Lemma 2.9 - non easily dualizable *)
 304 lemma segment_preserves_supremum:
 305   ∀O:ordered_set.∀l,u:O.∀a:sequence {[l,u]}.∀x:{[l,u]}.
 306     ⌊n,\fst (a n)⌋ is_increasing ∧
 307     (\fst x) is_supremum ⌊n,\fst (a n)⌋ → a ↑ x.
 308 intros; split; cases H; clear H;
 309 [1: apply H1;
 310 |2: cases H2; split; clear H2;
 311     [1: apply H;
 312     |2: clear H; intro y0; apply (H3 (\fst y0));]]
 313 qed.
 314
 315 lemma segment_preserves_infimum:
 316   ∀O:ordered_set.∀l,u:O.∀a:sequence {[l,u]}.∀x:{[l,u]}.
 317     ⌊n,\fst (a n)⌋ is_decreasing ∧
 318     (\fst x) is_infimum ⌊n,\fst (a n)⌋ → a ↓ x.
 319 intros; split; cases H; clear H;
 320 [1: apply H1;
 321 |2: cases H2; split; clear H2;
 322     [1: apply H;
 323     |2: clear H; intro y0; apply (H3 (\fst y0));]]
 324 qed.
 325
 326 (* Definition 2.10 *)
 327 alias symbol "pi2" = "pair pi2".
 328 alias symbol "pi1" = "pair pi1".
 329 definition square_segment ≝
 330   λO:ordered_set.λa,b:O.λx: O squareO.
 331     And4 (\fst x ≤ b) (a ≤ \fst x) (\snd x ≤ b) (a ≤ \snd x).
 332
 333 definition convex ≝
 334   λO:ordered_set.λU:O squareO → Prop.
 335     ∀p.U p → \fst p ≤ \snd p → ∀y.
 336       square_segment O (\fst p) (\snd p) y → U y.
 337
 338 (* Definition 2.11 *)
 339 definition upper_located ≝
 340   λO:half_ordered_set.λa:sequence O.∀x,y:O. y ≰≰ x →
 341     (∃i:nat.a i ≰≰ x) ∨ (∃b:O.y ≰≰ b ∧ ∀i:nat.a i ≤≤ b).
 342
 343 notation < "s \nbsp 'is_upper_located'" non associative with precedence 45
 344   for @{'upper_located $s}.
 345 notation > "s 'is_upper_located'" non associative with precedence 45
 346   for @{'upper_located $s}.
 347 interpretation "Ordered set upper locatedness" 'upper_located s =
 348   (upper_located (os_l _) s).
 349
 350 notation < "s \nbsp 'is_lower_located'" non associative with precedence 45
 351   for @{'lower_located $s}.
 352 notation > "s 'is_lower_located'" non associative with precedence 45
 353   for @{'lower_located $s}.
 354 interpretation "Ordered set lower locatedness" 'lower_located s =
 355   (upper_located (os_r _) s).
 356
 357 (* Lemma 2.12 *)
 358 lemma h_uparrow_upperlocated:
 359   ∀C:half_ordered_set.∀a:sequence C.∀u:C.uparrow ? a u → upper_located ? a.
 360 intros (C a u H); cases H (H2 H3); clear H; intros 3 (x y Hxy);
 361 cases H3 (H4 H5); clear H3; cases (hos_cotransitive ??? u Hxy) (W W);
 362 [2: cases (H5 ? W) (w Hw); left; exists [apply w] assumption;
 363 |1: right; exists [apply u]; split; [apply W|apply H4]]
 364 qed.
 365
 366 notation "'uparrow_upperlocated'" non associative with precedence 90 for @{'uparrow_upperlocated}.
 367 notation "'downarrow_lowerlocated'" non associative with precedence 90 for @{'downarrow_lowerlocated}.
 368
 369 interpretation "uparrow_upperlocated" 'uparrow_upperlocated = (h_uparrow_upperlocated (os_l _)).
 370 interpretation "downarrow_lowerlocated" 'downarrow_lowerlocated = (h_uparrow_upperlocated (os_r _)).