helm/software/matita/dama/sequence.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 set "baseuri" "cic:/matita/sequence/".
  16
  17 include "ordered_set.ma".
  18
  19 definition sequence := λO:pordered_set.nat → O.
  20
  21 definition fun_of_sequence: ∀O:pordered_set.sequence O → nat → O.
  22 intros; apply s; assumption;
  23 qed.
  24
  25 coercion cic:/matita/sequence/fun_of_sequence.con 1.
  26
  27 definition upper_bound ≝
  28   λO:pordered_set.λa:sequence O.λu:O.∀n:nat.a n ≤ u.
  29
  30 definition lower_bound ≝
  31   λO:pordered_set.λa:sequence O.λu:O.∀n:nat.u ≤ a n.
  32
  33 definition strong_sup ≝
  34   λO:pordered_set.λs:sequence O.λx.
  35     upper_bound ? s x ∧ (∀y:O.x ≰ y → ∃n.s n ≰ y).
  36
  37 definition strong_inf ≝
  38   λO:pordered_set.λs:sequence O.λx.
  39     lower_bound ? s x ∧ (∀y:O.y ≰ x → ∃n.y ≰ s n).
  40
  41 definition weak_sup ≝
  42   λO:pordered_set.λs:sequence O.λx.
  43     upper_bound ? s x ∧ (∀y:O.upper_bound ? s y → x ≤ y).
  44
  45 definition weak_inf ≝
  46   λO:pordered_set.λs:sequence O.λx.
  47     lower_bound ? s x ∧ (∀y:O.lower_bound ? s y → y ≤ x).
  48
  49 lemma strong_sup_is_weak:
  50   ∀O:pordered_set.∀s:sequence O.∀x:O.strong_sup ? s x → weak_sup ? s x.
  51 intros (O s x Ssup); elim Ssup (Ubx M); clear Ssup; split; [assumption]
  52 intros 3 (y Uby E); cases (M ? E) (n En); unfold in Uby; cases (Uby ? En);
  53 qed.
  54
  55 lemma strong_inf_is_weak:
  56   ∀O:pordered_set.∀s:sequence O.∀x:O.strong_inf ? s x → weak_inf ? s x.
  57 intros (O s x Ssup); elim Ssup (Ubx M); clear Ssup; split; [assumption]
  58 intros 3 (y Uby E); cases (M ? E) (n En); unfold in Uby; cases (Uby ? En);
  59 qed.
  60
  61 include "ordered_group.ma".
  62 include "nat/orders.ma".
  63
  64 definition tends ≝
  65   λO:ogroup.λs:sequence O.
  66     ∀e:O.0 < e → ∃N.∀n.N < n → -e < s n ∧ s n < e.
  67
  68 definition increasing ≝
  69   λO:pordered_set.λa:sequence O.∀n:nat.a n ≤ a (S n).
  70
  71 definition decreasing ≝
  72   λO:pordered_set.λa:sequence O.∀n:nat.a (S n) ≤ a n.
  73
  74
  75 (*
  76
  77 definition is_upper_bound ≝ λO:pordered_set.λa:sequence O.λu:O.∀n:nat.a n ≤ u.
  78 definition is_lower_bound ≝ λO:pordered_set.λa:sequence O.λu:O.∀n:nat.u ≤ a n.
  79
  80 record is_sup (O:pordered_set) (a:sequence O) (u:O) : Prop ≝
  81  { sup_upper_bound: is_upper_bound O a u;
  82    sup_least_upper_bound: ∀v:O. is_upper_bound O a v → u≤v
  83  }.
  84
  85 record is_inf (O:pordered_set) (a:sequence O) (u:O) : Prop ≝
  86  { inf_lower_bound: is_lower_bound O a u;
  87    inf_greatest_lower_bound: ∀v:O. is_lower_bound O a v → v≤u
  88  }.
  89
  90 record is_bounded_below (O:pordered_set) (a:sequence O) : Type ≝
  91  { ib_lower_bound: O;
  92    ib_lower_bound_is_lower_bound: is_lower_bound ? a ib_lower_bound
  93  }.
  94
  95 record is_bounded_above (O:pordered_set) (a:sequence O) : Type ≝
  96  { ib_upper_bound: O;
  97    ib_upper_bound_is_upper_bound: is_upper_bound ? a ib_upper_bound
  98  }.
  99
 100 record is_bounded (O:pordered_set) (a:sequence O) : Type ≝
 101  { ib_bounded_below:> is_bounded_below ? a;
 102    ib_bounded_above:> is_bounded_above ? a
 103  }.
 104
 105 record bounded_below_sequence (O:pordered_set) : Type ≝
 106  { bbs_seq:> sequence O;
 107    bbs_is_bounded_below:> is_bounded_below ? bbs_seq
 108  }.
 109
 110 record bounded_above_sequence (O:pordered_set) : Type ≝
 111  { bas_seq:> sequence O;
 112    bas_is_bounded_above:> is_bounded_above ? bas_seq
 113  }.
 114
 115 record bounded_sequence (O:pordered_set) : Type ≝
 116  { bs_seq:> sequence O;
 117    bs_is_bounded_below: is_bounded_below ? bs_seq;
 118    bs_is_bounded_above: is_bounded_above ? bs_seq
 119  }.
 120
 121 definition bounded_below_sequence_of_bounded_sequence ≝
 122  λO:pordered_set.λb:bounded_sequence O.
 123   mk_bounded_below_sequence ? b (bs_is_bounded_below ? b).
 124
 125 coercion cic:/matita/sequence/bounded_below_sequence_of_bounded_sequence.con.
 126
 127 definition bounded_above_sequence_of_bounded_sequence ≝
 128  λO:pordered_set.λb:bounded_sequence O.
 129   mk_bounded_above_sequence ? b (bs_is_bounded_above ? b).
 130
 131 coercion cic:/matita/sequence/bounded_above_sequence_of_bounded_sequence.con.
 132
 133 definition lower_bound ≝
 134  λO:pordered_set.λb:bounded_below_sequence O.
 135   ib_lower_bound ? b (bbs_is_bounded_below ? b).
 136
 137 lemma lower_bound_is_lower_bound:
 138  ∀O:pordered_set.∀b:bounded_below_sequence O.
 139   is_lower_bound ? b (lower_bound ? b).
 140 intros; unfold lower_bound; apply ib_lower_bound_is_lower_bound.
 141 qed.
 142
 143 definition upper_bound ≝
 144  λO:pordered_set.λb:bounded_above_sequence O.
 145   ib_upper_bound ? b (bas_is_bounded_above ? b).
 146
 147 lemma upper_bound_is_upper_bound:
 148  ∀O:pordered_set.∀b:bounded_above_sequence O.
 149   is_upper_bound ? b (upper_bound ? b).
 150 intros; unfold upper_bound; apply ib_upper_bound_is_upper_bound.
 151 qed.
 152
 153 definition reverse_excedence: excedence → excedence.
 154 intros (E); apply (mk_excedence E); [apply (λx,y.exc_relation E y x)]
 155 cases E (T f cRf cTf); simplify;
 156 [1: unfold Not; intros (x H); apply (cRf x); assumption
 157 |2: intros (x y z); apply Or_symmetric; apply cTf; assumption;]
 158 qed.
 159
 160 definition reverse_pordered_set: pordered_set → pordered_set.
 161 intros (p); apply (mk_pordered_set (reverse_excedence p));
 162 generalize in match (reverse_excedence p); intros (E);
 163 apply mk_is_porder_relation;
 164 [apply le_reflexive|apply le_transitive|apply le_antisymmetric]
 165 qed.
 166
 167 lemma is_lower_bound_reverse_is_upper_bound:
 168  ∀O:pordered_set.∀a:sequence O.∀l:O.
 169   is_lower_bound O a l → is_upper_bound (reverse_pordered_set O) a l.
 170 intros (O a l H); unfold; intros (n); unfold reverse_pordered_set;
 171 unfold reverse_excedence; simplify; fold unfold le (le ? l (a n)); apply H;
 172 qed.
 173
 174 lemma is_upper_bound_reverse_is_lower_bound:
 175  ∀O:pordered_set.∀a:sequence O.∀l:O.
 176   is_upper_bound O a l → is_lower_bound (reverse_pordered_set O) a l.
 177 intros (O a l H); unfold; intros (n); unfold reverse_pordered_set;
 178 unfold reverse_excedence; simplify; fold unfold le (le ? (a n) l); apply H;
 179 qed.
 180
 181 lemma reverse_is_lower_bound_is_upper_bound:
 182  ∀O:pordered_set.∀a:sequence O.∀l:O.
 183   is_lower_bound (reverse_pordered_set O) a l → is_upper_bound O a l.
 184 intros (O a l H); unfold; intros (n); unfold reverse_pordered_set in H;
 185 unfold reverse_excedence in H; simplify in H; apply H;
 186 qed.
 187
 188 lemma reverse_is_upper_bound_is_lower_bound:
 189  ∀O:pordered_set.∀a:sequence O.∀l:O.
 190   is_upper_bound (reverse_pordered_set O) a l → is_lower_bound O a l.
 191 intros (O a l H); unfold; intros (n); unfold reverse_pordered_set in H;
 192 unfold reverse_excedence in H; simplify in H; apply H;
 193 qed.
 194
 195 lemma is_inf_to_reverse_is_sup:
 196  ∀O:pordered_set.∀a:bounded_below_sequence O.∀l:O.
 197   is_inf O a l → is_sup (reverse_pordered_set O) a l.
 198 intros (O a l H); apply (mk_is_sup (reverse_pordered_set O));
 199 [1: apply is_lower_bound_reverse_is_upper_bound; apply inf_lower_bound; assumption
 200 |2: unfold reverse_pordered_set; simplify; unfold reverse_excedence; simplify;
 201     intros (m H1); apply (inf_greatest_lower_bound ? ? ? H); apply H1;]
 202 qed.
 203
 204 lemma is_sup_to_reverse_is_inf:
 205  ∀O:pordered_set.∀a:bounded_above_sequence O.∀l:O.
 206   is_sup O a l → is_inf (reverse_pordered_set O) a l.
 207 intros (O a l H); apply (mk_is_inf (reverse_pordered_set O));
 208 [1: apply is_upper_bound_reverse_is_lower_bound; apply sup_upper_bound; assumption
 209 |2: unfold reverse_pordered_set; simplify; unfold reverse_excedence; simplify;
 210     intros (m H1); apply (sup_least_upper_bound ? ? ? H); apply H1;]
 211 qed.
 212
 213 lemma reverse_is_sup_to_is_inf:
 214  ∀O:pordered_set.∀a:bounded_above_sequence O.∀l:O.
 215   is_sup (reverse_pordered_set O) a l → is_inf O a l.
 216 intros (O a l H); apply mk_is_inf;
 217 [1: apply reverse_is_upper_bound_is_lower_bound;
 218     apply (sup_upper_bound (reverse_pordered_set O)); assumption
 219 |2: intros (v H1); apply (sup_least_upper_bound (reverse_pordered_set O) a l H v);
 220     apply is_lower_bound_reverse_is_upper_bound; assumption;]
 221 qed.
 222
 223 lemma reverse_is_inf_to_is_sup:
 224  ∀O:pordered_set.∀a:bounded_above_sequence O.∀l:O.
 225   is_inf (reverse_pordered_set O) a l → is_sup O a l.
 226 intros (O a l H); apply mk_is_sup;
 227 [1: apply reverse_is_lower_bound_is_upper_bound;
 228     apply (inf_lower_bound (reverse_pordered_set O)); assumption
 229 |2: intros (v H1); apply (inf_greatest_lower_bound (reverse_pordered_set O) a l H v);
 230     apply is_upper_bound_reverse_is_lower_bound; assumption;]
 231 qed.
 232
 233 *)