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
  21 definition supremum ≝
  22   λO:ordered_set.λs:sequence O.λx.upper_bound ? s x ∧ (∀y:O.x ≰ y → ∃n.s n ≰ y).
  23
  24 definition increasing ≝ λO:ordered_set.λa:sequence O.∀n:nat.a n ≤ a (S n).
  25
  26 notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 50
  27   for @{'upper_bound $s $x}.
  28 notation < "s \nbsp 'is_increasing'"          non associative with precedence 50
  29   for @{'increasing $s}.
  30 notation < "x \nbsp 'is_supremum' \nbsp s"  non associative with precedence 50
  31   for @{'supremum $s $x}.
  32
  33 notation > "x 'is_upper_bound' s" non associative with precedence 50
  34   for @{'upper_bound $s $x}.
  35 notation > "s 'is_increasing'"    non associative with precedence 50
  36   for @{'increasing $s}.
  37 notation > "x 'is_supremum' s"  non associative with precedence 50
  38   for @{'supremum $s $x}.
  39
  40 interpretation "Ordered set upper bound" 'upper_bound s x =
  41   (cic:/matita/dama/supremum/upper_bound.con _ s x).
  42 interpretation "Ordered set increasing"  'increasing s    =
  43   (cic:/matita/dama/supremum/increasing.con _ s).
  44 interpretation "Ordered set strong sup"  'supremum s x  =
  45   (cic:/matita/dama/supremum/supremum.con _ s x).
  46
  47 include "nat/compare.ma".
  48 include "nat/plus.ma".
  49 include "bishop_set.ma".
  50
  51 lemma uniq_supremum:
  52   ∀O:ordered_set.∀s:sequence O.∀t1,t2:O.
  53     t1 is_supremum s → t2 is_supremum s → t1 ≈ t2.
  54 intros (O s t1 t2 Ht1 Ht2); cases Ht1 (U1 H1); cases Ht2 (U2 H2);
  55 apply le_le_eq; intro X;
  56 [1: cases (H1 ? X); apply (U2 w); assumption
  57 |2: cases (H2 ? X); apply (U1 w); assumption]
  58 qed.
  59
  60 (* Fact 2.5 *)
  61 lemma supremum_is_upper_bound:
  62   ∀C:ordered_set.∀a:sequence C.∀u:C.
  63    u is_supremum a → ∀v.v is_upper_bound a → u ≤ v.
  64 intros 7 (C s u Hu v Hv H); cases Hu (_ H1); clear Hu;
  65 cases (H1 ? H) (w Hw); apply Hv; assumption;
  66 qed.
  67
  68 (* Lemma 2.6 *)
  69 definition strictly_increasing ≝ λC:ordered_set.λa:sequence C.∀n:nat.a (S n) ≰ a n.
  70
  71 definition nat_excess : nat → nat → CProp ≝ λn,m. leb (m+S O) n = true.
  72
  73 axiom nat_excess_cotransitive: cotransitive ? nat_excess.
  74 (*intros 3 (x y z); elim x 0; elim y 0; elim z 0;
  75     [1: intros; left; assumption
  76     |2,5,6,7: intros; first [right; constructor 1|left; constructor 1]
  77     |3: intros (n H abs); simplify in abs; destruct abs;
  78     |4: intros (n H m W abs); simplify in abs; destruct abs;
  79     |8: clear x y z; intros (x H1 y H2 z H3 H4);
  80 *)
  81
  82 lemma nat_ordered_set : ordered_set.
  83 apply (mk_ordered_set ? nat_excess);
  84 [1: intro x; elim x (w H); simplify; intro X; [destruct X] apply H; assumption;
  85 |2: apply nat_excess_cotransitive]
  86 qed.
  87
  88 notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 50
  89   for @{'strictly_increasing $s}.
  90 notation > "s 'is_strictly_increasing'" non associative with precedence 50
  91   for @{'strictly_increasing $s}.
  92 interpretation "Ordered set increasing"  'strictly_increasing s    =
  93   (cic:/matita/dama/supremum/strictly_increasing.con _ s).
  94
  95 notation "a \uparrow u"  non associative with precedence 50 for  @{'sup_inc $a $u}.
  96 interpretation "Ordered set supremum of increasing" 'sup_inc s u =
  97  (cic:/matita/dama/cprop_connectives/And.ind#xpointer(1/1)
  98   (cic:/matita/dama/supremum/increasing.con _ s)
  99   (cic:/matita/dama/supremum/supremum.con _ s u)).
 100
 101 lemma trans_increasing:
 102   ∀C:ordered_set.∀s:sequence C.s is_increasing → ∀n,m. m ≰ n → s n ≤ s m.
 103 intros 5 (C s Hs n m); elim m; [1: cases (?:False); autobatch]
 104 cases (le_to_or_lt_eq ?? H1);
 105  [2: destruct H2; apply Hs;
 106  |1: apply (le_transitive ???? (H (lt_S_S_to_lt ?? H2))); apply Hs;]
 107 qed.
 108
 109 lemma selection:
 110   ∀C:ordered_set.∀m:sequence nat_ordered_set.m is_strictly_increasing →
 111     ∀a:sequence C.∀u.a ↑ u → (λx.a (m x)) ↑ u.
 112 intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split;
 113 [1: intro n; simplify; apply trans_increasing; [assumption]
 114     lapply (Hm n) as W; unfold nat_ordered_set in W; simplify in W;
 115     cases W;
 116 |2: intro n;
 117 |3:
 118