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 is_increasing ≝ λO:pordered_set.λa:sequence O.∀n:nat.a n ≤ a (S n).
  28 definition is_decreasing ≝ λO:pordered_set.λa:sequence O.∀n:nat.a (S n) ≤ a n.
  29
  30 definition is_upper_bound ≝ λO:pordered_set.λa:sequence O.λu:O.∀n:nat.a n ≤ u.
  31 definition is_lower_bound ≝ λO:pordered_set.λa:sequence O.λu:O.∀n:nat.u ≤ a n.
  32
  33 record is_sup (O:pordered_set) (a:sequence O) (u:O) : Prop ≝
  34  { sup_upper_bound: is_upper_bound O a u;
  35    sup_least_upper_bound: ∀v:O. is_upper_bound O a v → u≤v
  36  }.
  37
  38 record is_inf (O:pordered_set) (a:sequence O) (u:O) : Prop ≝
  39  { inf_lower_bound: is_lower_bound O a u;
  40    inf_greatest_lower_bound: ∀v:O. is_lower_bound O a v → v≤u
  41  }.
  42
  43 record is_bounded_below (O:pordered_set) (a:sequence O) : Type ≝
  44  { ib_lower_bound: O;
  45    ib_lower_bound_is_lower_bound: is_lower_bound ? a ib_lower_bound
  46  }.
  47
  48 record is_bounded_above (O:pordered_set) (a:sequence O) : Type ≝
  49  { ib_upper_bound: O;
  50    ib_upper_bound_is_upper_bound: is_upper_bound ? a ib_upper_bound
  51  }.
  52
  53 record is_bounded (O:pordered_set) (a:sequence O) : Type ≝
  54  { ib_bounded_below:> is_bounded_below ? a;
  55    ib_bounded_above:> is_bounded_above ? a
  56  }.
  57
  58 record bounded_below_sequence (O:pordered_set) : Type ≝
  59  { bbs_seq:> sequence O;
  60    bbs_is_bounded_below:> is_bounded_below ? bbs_seq
  61  }.
  62
  63 record bounded_above_sequence (O:pordered_set) : Type ≝
  64  { bas_seq:> sequence O;
  65    bas_is_bounded_above:> is_bounded_above ? bas_seq
  66  }.
  67
  68 record bounded_sequence (O:pordered_set) : Type ≝
  69  { bs_seq:> sequence O;
  70    bs_is_bounded_below: is_bounded_below ? bs_seq;
  71    bs_is_bounded_above: is_bounded_above ? bs_seq
  72  }.
  73
  74 definition bounded_below_sequence_of_bounded_sequence ≝
  75  λO:pordered_set.λb:bounded_sequence O.
  76   mk_bounded_below_sequence ? b (bs_is_bounded_below ? b).
  77
  78 coercion cic:/matita/sequence/bounded_below_sequence_of_bounded_sequence.con.
  79
  80 definition bounded_above_sequence_of_bounded_sequence ≝
  81  λO:pordered_set.λb:bounded_sequence O.
  82   mk_bounded_above_sequence ? b (bs_is_bounded_above ? b).
  83
  84 coercion cic:/matita/sequence/bounded_above_sequence_of_bounded_sequence.con.
  85
  86 definition lower_bound ≝
  87  λO:pordered_set.λb:bounded_below_sequence O.
  88   ib_lower_bound ? b (bbs_is_bounded_below ? b).
  89
  90 lemma lower_bound_is_lower_bound:
  91  ∀O:pordered_set.∀b:bounded_below_sequence O.
  92   is_lower_bound ? b (lower_bound ? b).
  93 intros; unfold lower_bound; apply ib_lower_bound_is_lower_bound.
  94 qed.
  95
  96 definition upper_bound ≝
  97  λO:pordered_set.λb:bounded_above_sequence O.
  98   ib_upper_bound ? b (bas_is_bounded_above ? b).
  99
 100 lemma upper_bound_is_upper_bound:
 101  ∀O:pordered_set.∀b:bounded_above_sequence O.
 102   is_upper_bound ? b (upper_bound ? b).
 103 intros; unfold upper_bound; apply ib_upper_bound_is_upper_bound.
 104 qed.
 105
 106 definition reverse_excedence: excedence → excedence.
 107 intros (E); apply (mk_excedence E); [apply (λx,y.exc_relation E y x)]
 108 cases E (T f cRf cTf); simplify;
 109 [1: unfold Not; intros (x H); apply (cRf x); assumption
 110 |2: intros (x y z); apply Or_symmetric; apply cTf; assumption;]
 111 qed.
 112
 113 definition reverse_pordered_set: pordered_set → pordered_set.
 114 intros (p); apply (mk_pordered_set (reverse_excedence p));
 115 generalize in match (reverse_excedence p); intros (E);
 116 apply mk_is_porder_relation;
 117 [apply le_reflexive|apply le_transitive|apply le_antisymmetric]
 118 qed.
 119
 120 lemma is_lower_bound_reverse_is_upper_bound:
 121  ∀O:pordered_set.∀a:sequence O.∀l:O.
 122   is_lower_bound O a l → is_upper_bound (reverse_pordered_set O) a l.
 123 intros (O a l H); unfold; intros (n); unfold reverse_pordered_set;
 124 unfold reverse_excedence; simplify; fold unfold le (le ? l (a n)); apply H;
 125 qed.
 126
 127 lemma is_upper_bound_reverse_is_lower_bound:
 128  ∀O:pordered_set.∀a:sequence O.∀l:O.
 129   is_upper_bound O a l → is_lower_bound (reverse_pordered_set O) a l.
 130 intros (O a l H); unfold; intros (n); unfold reverse_pordered_set;
 131 unfold reverse_excedence; simplify; fold unfold le (le ? (a n) l); apply H;
 132 qed.
 133
 134 lemma reverse_is_lower_bound_is_upper_bound:
 135  ∀O:pordered_set.∀a:sequence O.∀l:O.
 136   is_lower_bound (reverse_pordered_set O) a l → is_upper_bound O a l.
 137 intros (O a l H); unfold; intros (n); unfold reverse_pordered_set in H;
 138 unfold reverse_excedence in H; simplify in H; apply H;
 139 qed.
 140
 141 lemma reverse_is_upper_bound_is_lower_bound:
 142  ∀O:pordered_set.∀a:sequence O.∀l:O.
 143   is_upper_bound (reverse_pordered_set O) a l → is_lower_bound O a l.
 144 intros (O a l H); unfold; intros (n); unfold reverse_pordered_set in H;
 145 unfold reverse_excedence in H; simplify in H; apply H;
 146 qed.
 147
 148 lemma is_inf_to_reverse_is_sup:
 149  ∀O:pordered_set.∀a:bounded_below_sequence O.∀l:O.
 150   is_inf O a l → is_sup (reverse_pordered_set O) a l.
 151 intros (O a l H); apply (mk_is_sup (reverse_pordered_set O));
 152 [1: apply is_lower_bound_reverse_is_upper_bound; apply inf_lower_bound; assumption
 153 |2: unfold reverse_pordered_set; simplify; unfold reverse_excedence; simplify;
 154     intros (m H1); apply (inf_greatest_lower_bound ? ? ? H); apply H1;]
 155 qed.
 156
 157 lemma is_sup_to_reverse_is_inf:
 158  ∀O:pordered_set.∀a:bounded_above_sequence O.∀l:O.
 159   is_sup O a l → is_inf (reverse_pordered_set O) a l.
 160 intros (O a l H); apply (mk_is_inf (reverse_pordered_set O));
 161 [1: apply is_upper_bound_reverse_is_lower_bound; apply sup_upper_bound; assumption
 162 |2: unfold reverse_pordered_set; simplify; unfold reverse_excedence; simplify;
 163     intros (m H1); apply (sup_least_upper_bound ? ? ? H); apply H1;]
 164 qed.
 165
 166 lemma reverse_is_sup_to_is_inf:
 167  ∀O:pordered_set.∀a:bounded_above_sequence O.∀l:O.
 168   is_sup (reverse_pordered_set O) a l → is_inf O a l.
 169 intros (O a l H); apply mk_is_inf;
 170 [1: apply reverse_is_upper_bound_is_lower_bound;
 171     apply (sup_upper_bound (reverse_pordered_set O)); assumption
 172 |2: intros (v H1); apply (sup_least_upper_bound (reverse_pordered_set O) a l H v);
 173     apply is_lower_bound_reverse_is_upper_bound; assumption;]
 174 qed.
 175
 176 lemma reverse_is_inf_to_is_sup:
 177  ∀O:pordered_set.∀a:bounded_above_sequence O.∀l:O.
 178   is_inf (reverse_pordered_set O) a l → is_sup O a l.
 179 intros (O a l H); apply mk_is_sup;
 180 [1: apply reverse_is_lower_bound_is_upper_bound;
 181     apply (inf_lower_bound (reverse_pordered_set O)); assumption
 182 |2: intros (v H1); apply (inf_greatest_lower_bound (reverse_pordered_set O) a l H v);
 183     apply is_upper_bound_reverse_is_lower_bound; assumption;]
 184 qed.