matita/contribs/dama/dama/classical_pointfree/ordered_sets.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
  17 include "excess.ma".
  18
  19 record is_dedekind_sigma_complete (O:excess) : Type ≝
  20  { dsc_inf: ∀a:nat→O.∀m:O. is_lower_bound ? a m → ex ? (λs:O.is_inf O a s);
  21    dsc_inf_proof_irrelevant:
  22     ∀a:nat→O.∀m,m':O.∀p:is_lower_bound ? a m.∀p':is_lower_bound ? a m'.
  23      (match dsc_inf a m p with [ ex_intro s _ ⇒ s ]) =
  24      (match dsc_inf a m' p' with [ ex_intro s' _ ⇒ s' ]);
  25    dsc_sup: ∀a:nat→O.∀m:O. is_upper_bound ? a m → ex ? (λs:O.is_sup O a s);
  26    dsc_sup_proof_irrelevant:
  27     ∀a:nat→O.∀m,m':O.∀p:is_upper_bound ? a m.∀p':is_upper_bound ? a m'.
  28      (match dsc_sup a m p with [ ex_intro s _ ⇒ s ]) =
  29      (match dsc_sup a m' p' with [ ex_intro s' _ ⇒ s' ])
  30  }.
  31
  32 record dedekind_sigma_complete_ordered_set : Type ≝
  33  { dscos_ordered_set:> excess;
  34    dscos_dedekind_sigma_complete_properties:>
  35     is_dedekind_sigma_complete dscos_ordered_set
  36  }.
  37
  38 definition inf:
  39  ∀O:dedekind_sigma_complete_ordered_set.
  40   bounded_below_sequence O → O.
  41  intros;
  42  elim
  43   (dsc_inf O (dscos_dedekind_sigma_complete_properties O) b);
  44   [ apply a
  45   | apply (lower_bound ? b)
  46   | apply lower_bound_is_lower_bound
  47   ]
  48 qed.
  49
  50 lemma inf_is_inf:
  51  ∀O:dedekind_sigma_complete_ordered_set.
  52   ∀a:bounded_below_sequence O.
  53    is_inf ? a (inf ? a).
  54  intros;
  55  unfold inf;
  56  simplify;
  57  elim (dsc_inf O (dscos_dedekind_sigma_complete_properties O) a
  58 (lower_bound O a) (lower_bound_is_lower_bound O a));
  59  simplify;
  60  assumption.
  61 qed.
  62
  63 lemma inf_proof_irrelevant:
  64  ∀O:dedekind_sigma_complete_ordered_set.
  65   ∀a,a':bounded_below_sequence O.
  66    bbs_seq ? a = bbs_seq ? a' →
  67     inf ? a = inf ? a'.
  68  intros 3;
  69  elim a 0;
  70  elim a';
  71  simplify in H;
  72  generalize in match i1;
  73  clear i1;
  74  rewrite > H;
  75  intro;
  76  simplify;
  77  rewrite < (dsc_inf_proof_irrelevant O O f (ib_lower_bound ? f i)
  78   (ib_lower_bound ? f i2) (ib_lower_bound_is_lower_bound ? f i)
  79   (ib_lower_bound_is_lower_bound ? f i2));
  80  reflexivity.
  81 qed.
  82
  83 definition sup:
  84  ∀O:dedekind_sigma_complete_ordered_set.
  85   bounded_above_sequence O → O.
  86  intros;
  87  elim
  88   (dsc_sup O (dscos_dedekind_sigma_complete_properties O) b);
  89   [ apply a
  90   | apply (upper_bound ? b)
  91   | apply upper_bound_is_upper_bound
  92   ].
  93 qed.
  94
  95 lemma sup_is_sup:
  96  ∀O:dedekind_sigma_complete_ordered_set.
  97   ∀a:bounded_above_sequence O.
  98    is_sup ? a (sup ? a).
  99  intros;
 100  unfold sup;
 101  simplify;
 102  elim (dsc_sup O (dscos_dedekind_sigma_complete_properties O) a
 103 (upper_bound O a) (upper_bound_is_upper_bound O a));
 104  simplify;
 105  assumption.
 106 qed.
 107
 108 lemma sup_proof_irrelevant:
 109  ∀O:dedekind_sigma_complete_ordered_set.
 110   ∀a,a':bounded_above_sequence O.
 111    bas_seq ? a = bas_seq ? a' →
 112     sup ? a = sup ? a'.
 113  intros 3;
 114  elim a 0;
 115  elim a';
 116  simplify in H;
 117  generalize in match i1;
 118  clear i1;
 119  rewrite > H;
 120  intro;
 121  simplify;
 122  rewrite < (dsc_sup_proof_irrelevant O O f (ib_upper_bound ? f i2)
 123   (ib_upper_bound ? f i) (ib_upper_bound_is_upper_bound ? f i2)
 124   (ib_upper_bound_is_upper_bound ? f i));
 125  reflexivity.
 126 qed.
 127
 128 axiom daemon: False.
 129
 130 theorem inf_le_sup:
 131  ∀O:dedekind_sigma_complete_ordered_set.
 132   ∀a:bounded_sequence O. inf ? a ≤ sup ? a.
 133  intros (O');
 134  apply (or_transitive ? ? O' ? (a O));
 135   [ elim daemon (*apply (inf_lower_bound ? ? ? ? (inf_is_inf ? ? a))*)
 136   | elim daemon (*apply (sup_upper_bound ? ? ? ? (sup_is_sup ? ? a))*)
 137   ].
 138 qed.
 139
 140 lemma inf_respects_le:
 141  ∀O:dedekind_sigma_complete_ordered_set.
 142   ∀a:bounded_below_sequence O.∀m:O.
 143    is_upper_bound ? a m → inf ? a ≤ m.
 144  intros (O');
 145  apply (or_transitive ? ? O' ? (sup ? (mk_bounded_sequence ? a ? ?)));
 146   [ apply (bbs_is_bounded_below ? a)
 147   | apply (mk_is_bounded_above ? ? m H)
 148   | apply inf_le_sup
 149   | apply
 150      (sup_least_upper_bound ? ? ?
 151       (sup_is_sup ? (mk_bounded_sequence O' a a
 152         (mk_is_bounded_above O' a m H))));
 153     assumption
 154   ].
 155 qed.
 156
 157 definition is_sequentially_monotone ≝
 158  λO:excess.λf:O→O.
 159   ∀a:nat→O.∀p:is_increasing ? a.
 160    is_increasing ? (λi.f (a i)).
 161
 162 record is_order_continuous
 163  (O:dedekind_sigma_complete_ordered_set) (f:O→O) : Prop
 164 ≝
 165  { ioc_is_sequentially_monotone: is_sequentially_monotone ? f;
 166    ioc_is_upper_bound_f_sup:
 167     ∀a:bounded_above_sequence O.
 168      is_upper_bound ? (λi.f (a i)) (f (sup ? a));
 169    ioc_respects_sup:
 170     ∀a:bounded_above_sequence O.
 171      is_increasing ? a →
 172       f (sup ? a) =
 173        sup ? (mk_bounded_above_sequence ? (λi.f (a i))
 174         (mk_is_bounded_above ? ? (f (sup ? a))
 175          (ioc_is_upper_bound_f_sup a)));
 176    ioc_is_lower_bound_f_inf:
 177     ∀a:bounded_below_sequence O.
 178      is_lower_bound ? (λi.f (a i)) (f (inf ? a));
 179    ioc_respects_inf:
 180     ∀a:bounded_below_sequence O.
 181      is_decreasing ? a →
 182       f (inf ? a) =
 183        inf ? (mk_bounded_below_sequence ? (λi.f (a i))
 184         (mk_is_bounded_below ? ? (f (inf ? a))
 185          (ioc_is_lower_bound_f_inf a)))
 186  }.
 187
 188 theorem tail_inf_increasing:
 189  ∀O:dedekind_sigma_complete_ordered_set.
 190   ∀a:bounded_below_sequence O.
 191    let y ≝ λi.mk_bounded_below_sequence ? (λj.a (i+j)) ? in
 192    let x ≝ λi.inf ? (y i) in
 193     is_increasing ? x.
 194  [ apply (mk_is_bounded_below ? ? (ib_lower_bound ? a a));
 195    simplify;
 196    intro;
 197    apply (ib_lower_bound_is_lower_bound ? a a)
 198  | intros;
 199    unfold is_increasing;
 200    intro;
 201    unfold x in ⊢ (? ? ? %);
 202    apply (inf_greatest_lower_bound ? ? ? (inf_is_inf ? (y (S n))));
 203    change with (is_lower_bound ? (y (S n)) (inf ? (y n)));
 204    unfold is_lower_bound;
 205    intro;
 206    generalize in match (inf_lower_bound ? ? ? (inf_is_inf ? (y n)) (S n1));
 207    (*CSC: coercion per FunClass inserita a mano*)
 208    suppose (inf ? (y n) ≤ bbs_seq ? (y n) (S n1)) (H);
 209    cut (bbs_seq ? (y n) (S n1) = bbs_seq ? (y (S n)) n1);
 210     [ rewrite < Hcut;
 211       assumption
 212     | unfold y;
 213       simplify;
 214       autobatch paramodulation library
 215     ]
 216  ].
 217 qed.
 218
 219 definition is_liminf:
 220  ∀O:dedekind_sigma_complete_ordered_set.
 221   bounded_below_sequence O → O → Prop.
 222  intros;
 223  apply
 224   (is_sup ? (λi.inf ? (mk_bounded_below_sequence ? (λj.b (i+j)) ?)) t);
 225  apply (mk_is_bounded_below ? ? (ib_lower_bound ? b b));
 226  simplify;
 227  intros;
 228  apply (ib_lower_bound_is_lower_bound ? b b).
 229 qed.
 230
 231 definition liminf:
 232  ∀O:dedekind_sigma_complete_ordered_set.
 233   bounded_sequence O → O.
 234  intros;
 235  apply
 236   (sup ?
 237    (mk_bounded_above_sequence ?
 238      (λi.inf ?
 239        (mk_bounded_below_sequence ?
 240          (λj.b (i+j)) ?)) ?));
 241   [ apply (mk_is_bounded_below ? ? (ib_lower_bound ? b b));
 242     simplify;
 243     intros;
 244     apply (ib_lower_bound_is_lower_bound ? b b)
 245   | apply (mk_is_bounded_above ? ? (ib_upper_bound ? b b));
 246     unfold is_upper_bound;
 247     intro;
 248     change with
 249      (inf O
 250   (mk_bounded_below_sequence O (\lambda j:nat.b (n+j))
 251    (mk_is_bounded_below O (\lambda j:nat.b (n+j)) (ib_lower_bound O b b)
 252     (\lambda j:nat.ib_lower_bound_is_lower_bound O b b (n+j))))
 253 \leq ib_upper_bound O b b);
 254     apply (inf_respects_le O);
 255     simplify;
 256     intro;
 257     apply (ib_upper_bound_is_upper_bound ? b b)
 258   ].
 259 qed.
 260
 261
 262 definition reverse_dedekind_sigma_complete_ordered_set:
 263  dedekind_sigma_complete_ordered_set → dedekind_sigma_complete_ordered_set.
 264  intros;
 265  apply mk_dedekind_sigma_complete_ordered_set;
 266   [ apply (reverse_ordered_set d)
 267   | elim daemon
 268     (*apply mk_is_dedekind_sigma_complete;
 269      [ intros;
 270        elim (dsc_sup ? ? d a m) 0;
 271         [ generalize in match H; clear H;
 272           generalize in match m; clear m;
 273           elim d;
 274           simplify in a1;
 275           simplify;
 276           change in a1 with (Type_OF_ordered_set ? (reverse_ordered_set ? o));
 277           apply (ex_intro ? ? a1);
 278           simplify in H1;
 279           change in m with (Type_OF_ordered_set ? o);
 280           apply (is_sup_to_reverse_is_inf ? ? ? ? H1)
 281         | generalize in match H; clear H;
 282           generalize in match m; clear m;
 283           elim d;
 284           simplify;
 285           change in t with (Type_OF_ordered_set ? o);
 286           simplify in t;
 287           apply reverse_is_lower_bound_is_upper_bound;
 288           assumption
 289         ]
 290      | apply is_sup_reverse_is_inf;
 291      | apply m
 292      |
 293      ]*)
 294   ].
 295 qed.
 296
 297 definition reverse_bounded_sequence:
 298  ∀O:dedekind_sigma_complete_ordered_set.
 299   bounded_sequence O →
 300    bounded_sequence (reverse_dedekind_sigma_complete_ordered_set O).
 301  intros;
 302  apply mk_bounded_sequence;
 303   [ apply bs_seq;
 304     unfold reverse_dedekind_sigma_complete_ordered_set;
 305     simplify;
 306     elim daemon
 307   | elim daemon
 308   | elim daemon
 309   ].
 310 qed.
 311
 312 definition limsup ≝
 313  λO:dedekind_sigma_complete_ordered_set.
 314   λa:bounded_sequence O.
 315    liminf (reverse_dedekind_sigma_complete_ordered_set O)
 316     (reverse_bounded_sequence O a).
 317
 318 notation "hvbox(〈a〉)"
 319  non associative with precedence 45
 320 for @{ 'hide_everything_but $a }.
 321
 322 interpretation "mk_bounded_above_sequence" 'hide_everything_but a
 323 = (cic:/matita/classical_pointfree/ordered_sets/bounded_above_sequence.ind#xpointer(1/1/1) _ _ a _).
 324
 325 interpretation "mk_bounded_below_sequence" 'hide_everything_but a
 326 = (cic:/matita/classical_pointfree/ordered_sets/bounded_below_sequence.ind#xpointer(1/1/1) _ _ a _).
 327
 328 theorem eq_f_sup_sup_f:
 329  ∀O':dedekind_sigma_complete_ordered_set.
 330   ∀f:O'→O'. ∀H:is_order_continuous ? f.
 331    ∀a:bounded_above_sequence O'.
 332     ∀p:is_increasing ? a.
 333      f (sup ? a) = sup ? (mk_bounded_above_sequence ? (λi.f (a i)) ?).
 334  [ apply (mk_is_bounded_above ? ? (f (sup ? a)));
 335    apply ioc_is_upper_bound_f_sup;
 336    assumption
 337  | intros;
 338    apply ioc_respects_sup;
 339    assumption
 340  ].
 341 qed.
 342
 343 theorem eq_f_sup_sup_f':
 344  ∀O':dedekind_sigma_complete_ordered_set.
 345   ∀f:O'→O'. ∀H:is_order_continuous ? f.
 346    ∀a:bounded_above_sequence O'.
 347     ∀p:is_increasing ? a.
 348      ∀p':is_bounded_above ? (λi.f (a i)).
 349       f (sup ? a) = sup ? (mk_bounded_above_sequence ? (λi.f (a i)) p').
 350  intros;
 351  rewrite > (eq_f_sup_sup_f ? f H a H1);
 352  apply sup_proof_irrelevant;
 353  reflexivity.
 354 qed.
 355
 356 theorem eq_f_liminf_sup_f_inf:
 357  ∀O':dedekind_sigma_complete_ordered_set.
 358   ∀f:O'→O'. ∀H:is_order_continuous ? f.
 359    ∀a:bounded_sequence O'.
 360    let p1 := ? in
 361     f (liminf ? a) =
 362      sup ?
 363       (mk_bounded_above_sequence ?
 364         (λi.f (inf ?
 365           (mk_bounded_below_sequence ?
 366             (λj.a (i+j))
 367             ?)))
 368         p1).
 369  [ apply (mk_is_bounded_below ? ? (ib_lower_bound ? a a));
 370    simplify;
 371    intro;
 372    apply (ib_lower_bound_is_lower_bound ? a a)
 373  | apply (mk_is_bounded_above ? ? (f (sup ? a)));
 374    unfold is_upper_bound;
 375    intro;
 376    apply (or_transitive ? ? O' ? (f (a n)));
 377     [ generalize in match (ioc_is_lower_bound_f_inf ? ? H);
 378       intro H1;
 379       simplify in H1;
 380       rewrite > (plus_n_O n) in ⊢ (? ? ? (? (? ? ? %)));
 381       apply (H1 (mk_bounded_below_sequence O' (\lambda j:nat.a (n+j))
 382 (mk_is_bounded_below O' (\lambda j:nat.a (n+j)) (ib_lower_bound O' a a)
 383  (\lambda j:nat.ib_lower_bound_is_lower_bound O' a a (n+j)))) O);
 384     | elim daemon (*apply (ioc_is_upper_bound_f_sup ? ? ? H)*)
 385     ]
 386  | intros;
 387    unfold liminf;
 388    clearbody p1;
 389    generalize in match (\lambda n:nat
 390 .inf_respects_le O'
 391  (mk_bounded_below_sequence O' (\lambda j:nat.a (plus n j))
 392   (mk_is_bounded_below O' (\lambda j:nat.a (plus n j))
 393    (ib_lower_bound O' a a)
 394    (\lambda j:nat.ib_lower_bound_is_lower_bound O' a a (plus n j))))
 395  (ib_upper_bound O' a a)
 396  (\lambda n1:nat.ib_upper_bound_is_upper_bound O' a a (plus n n1)));
 397    intro p2;
 398    apply (eq_f_sup_sup_f' ? f H (mk_bounded_above_sequence O'
 399 (\lambda i:nat
 400  .inf O'
 401   (mk_bounded_below_sequence O' (\lambda j:nat.a (plus i j))
 402    (mk_is_bounded_below O' (\lambda j:nat.a (plus i j))
 403     (ib_lower_bound O' a a)
 404     (\lambda n:nat.ib_lower_bound_is_lower_bound O' a a (plus i n)))))
 405 (mk_is_bounded_above O'
 406  (\lambda i:nat
 407   .inf O'
 408    (mk_bounded_below_sequence O' (\lambda j:nat.a (plus i j))
 409     (mk_is_bounded_below O' (\lambda j:nat.a (plus i j))
 410      (ib_lower_bound O' a a)
 411      (\lambda n:nat.ib_lower_bound_is_lower_bound O' a a (plus i n)))))
 412  (ib_upper_bound O' a a) p2)));
 413    unfold bas_seq;
 414    change with
 415     (is_increasing ? (\lambda i:nat
 416 .inf O'
 417  (mk_bounded_below_sequence O' (\lambda j:nat.a (plus i j))
 418   (mk_is_bounded_below O' (\lambda j:nat.a (plus i j))
 419    (ib_lower_bound O' a a)
 420    (\lambda n:nat.ib_lower_bound_is_lower_bound O' a a (plus i n))))));
 421    apply tail_inf_increasing
 422  ].
 423 qed.
 424