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 "bishop_set.ma".
  48
  49 lemma uniq_supremum:
  50   ∀O:ordered_set.∀s:sequence O.∀t1,t2:O.
  51     t1 is_supremum s → t2 is_supremum s → t1 ≈ t2.
  52 intros (O s t1 t2 Ht1 Ht2); cases Ht1 (U1 H1); cases Ht2 (U2 H2);
  53 apply le_le_eq; intro X;
  54 [1: cases (H1 ? X); apply (U2 w); assumption
  55 |2: cases (H2 ? X); apply (U1 w); assumption]
  56 qed.
  57
  58 (* Fact 2.5 *)
  59 lemma supremum_is_upper_bound:
  60   ∀C:ordered_set.∀a:sequence C.∀u:C.
  61    u is_supremum a → ∀v.v is_upper_bound a → u ≤ v.
  62 intros 7 (C s u Hu v Hv H); cases Hu (_ H1); clear Hu;
  63 cases (H1 ? H) (w Hw); apply Hv; assumption;
  64 qed.
  65
  66 (* Lemma 2.6 *)
  67 definition strictly_increasing ≝
  68   λC:ordered_set.λa:sequence C.∀n:nat.a (S n) ≰ a n.
  69
  70 notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 50
  71   for @{'strictly_increasing $s}.
  72 notation > "s 'is_strictly_increasing'" non associative with precedence 50
  73   for @{'strictly_increasing $s}.
  74 interpretation "Ordered set increasing"  'strictly_increasing s    =
  75   (cic:/matita/dama/supremum/strictly_increasing.con _ s).
  76
  77 notation "a \uparrow u" non associative with precedence 50 for @{'sup_inc $a $u}.
  78 interpretation "Ordered set supremum of increasing" 'sup_inc s u =
  79  (cic:/matita/dama/cprop_connectives/And.ind#xpointer(1/1)
  80   (cic:/matita/dama/supremum/increasing.con _ s)
  81   (cic:/matita/dama/supremum/supremum.con _ s u)).
  82
  83 include "nat_ordered_set.ma".
  84
  85 alias symbol "nleq" = "Ordered set excess".
  86 alias symbol "leq" = "Ordered set less or equal than".
  87 lemma trans_increasing:
  88   ∀C:ordered_set.∀a:sequence C.a is_increasing → ∀n,m:nat_ordered_set. m ≰ n → a n ≤ a m.
  89 intros 5 (C a Hs n m); elim m; [cases (not_le_Sn_O n H);]
  90 intro; apply H;
  91 [1: change in n1 with (os_carr nat_ordered_set); (* canonical structures *)
  92     change with (n<n1); (* is sort elimination not allowed preserved by delta? *)
  93     cases (le_to_or_lt_eq ?? H1); [apply le_S_S_to_le;assumption]
  94     cases (Hs n); rewrite < H3 in H2; assumption (* ogni goal di tipo Prop non è anche di tipo CProp *)
  95 |2: cases (os_cotransitive ??? (a n1) H2); [assumption]
  96     cases (Hs n1); assumption;]
  97 qed.
  98
  99 lemma strictly_increasing_reaches:
 100   ∀C:ordered_set.∀m:sequence nat_ordered_set.
 101    m is_strictly_increasing → ∀w.∃t.m t ≰ w.
 102 intros; elim w;
 103 [1: cases (nat_discriminable O (m O)); [2: cases (not_le_Sn_n O (ltn_to_ltO ?? H1))]
 104     cases H1; [exists [apply O] apply H2;]
 105     exists [apply (S O)] lapply (H O) as H3; rewrite < H2 in H3; assumption
 106 |2: cases H1 (p Hp); cases (nat_discriminable (S n) (m p));
 107     [1: cases H2; clear H2;
 108         [1: exists [apply p]; assumption;
 109         |2: exists [apply (S p)]; rewrite > H3; apply H;]
 110     |2: cases (?:False); change in Hp with (n<m p);
 111         apply (not_le_Sn_n (m p));
 112         apply (transitive_le ??? H2 Hp);]]
 113 qed.
 114
 115 lemma selection:
 116   ∀C:ordered_set.∀m:sequence nat_ordered_set.m is_strictly_increasing →
 117     ∀a:sequence C.∀u.a ↑ u → (λx.a (m x)) ↑ u.
 118 intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split;
 119 [1: intro n; simplify; apply trans_increasing; [assumption] apply (Hm n);
 120 |2: intro n; simplify; apply Uu;
 121 |3: intros (y Hy); simplify; cases (Hu ? Hy);
 122     cases (strictly_increasing_reaches C ? Hm w);
 123     exists [apply w1]; cases (os_cotransitive ??? (a (m w1)) H); [2:assumption]
 124     cases (trans_increasing C ? Ia ?? H1); assumption;]
 125 qed.
 126