matita/dama/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 set "baseuri" "cic:/matita/ordered_sets/".
  16
  17 include "ordered_sets.ma".
  18
  19 record is_porder_relation (C:Type) (le:C→C→Prop) (eq:C→C→Prop) : Type ≝ {
  20   por_reflexive: reflexive ? le;
  21   por_transitive: transitive ? le;
  22   por_antisimmetric: antisymmetric ? le eq
  23 }.
  24
  25 record pordered_set: Type ≝ {
  26   pos_carr:> excedence;
  27   pos_order_relation_properties:> is_porder_relation ? (le pos_carr) (eq pos_carr)
  28 }.
  29
  30 lemma pordered_set_of_excedence: excedence → pordered_set.
  31 intros (E); apply (mk_pordered_set E); apply (mk_is_porder_relation);
  32 [apply le_reflexive|apply le_transitive|apply le_antisymmetric]
  33 qed.
  34
  35 definition total_order : ∀E:excedence. Type ≝
  36   λE:excedence. ∀a,b:E. a ≰ b → a < b.
  37
  38 alias id "transitive" = "cic:/matita/higher_order_defs/relations/transitive.con".
  39 alias id "cotransitive" = "cic:/matita/higher_order_defs/relations/cotransitive.con".
  40 alias id "antisymmetric" = "cic:/matita/higher_order_defs/relations/antisymmetric.con".
  41 theorem antisimmetric_to_cotransitive_to_transitive:
  42  ∀C:Type.∀le:C→C→Prop. antisymmetric ? le → cotransitive ? le → transitive ? le.
  43 intros (T f Af cT); unfold transitive; intros (x y z fxy fyz);
  44 lapply (cT ? ? fxy z) as H; cases H; [assumption] cases (Af ? ? fyz H1);
  45 qed.
  46
  47 definition is_increasing ≝ λO:pordered_set.λa:nat→O.∀n:nat.a n ≤ a (S n).
  48 definition is_decreasing ≝ λO:pordered_set.λa:nat→O.∀n:nat.a (S n) ≤ a n.
  49
  50 definition is_upper_bound ≝ λO:pordered_set.λa:nat→O.λu:O.∀n:nat.a n ≤ u.
  51 definition is_lower_bound ≝ λO:pordered_set.λa:nat→O.λu:O.∀n:nat.u ≤ a n.
  52
  53 record is_sup (O:pordered_set) (a:nat→O) (u:O) : Prop ≝
  54  { sup_upper_bound: is_upper_bound O a u;
  55    sup_least_upper_bound: ∀v:O. is_upper_bound O a v → u≤v
  56  }.
  57
  58 record is_inf (O:pordered_set) (a:nat→O) (u:O) : Prop ≝
  59  { inf_lower_bound: is_lower_bound O a u;
  60    inf_greatest_lower_bound: ∀v:O. is_lower_bound O a v → v≤u
  61  }.
  62
  63 record is_bounded_below (O:pordered_set) (a:nat→O) : Type ≝
  64  { ib_lower_bound: O;
  65    ib_lower_bound_is_lower_bound: is_lower_bound ? a ib_lower_bound
  66  }.
  67
  68 record is_bounded_above (O:pordered_set) (a:nat→O) : Type ≝
  69  { ib_upper_bound: O;
  70    ib_upper_bound_is_upper_bound: is_upper_bound ? a ib_upper_bound
  71  }.
  72
  73 record is_bounded (O:pordered_set) (a:nat→O) : Type ≝
  74  { ib_bounded_below:> is_bounded_below ? a;
  75    ib_bounded_above:> is_bounded_above ? a
  76  }.
  77
  78 record bounded_below_sequence (O:pordered_set) : Type ≝
  79  { bbs_seq:1> nat→O;
  80    bbs_is_bounded_below:> is_bounded_below ? bbs_seq
  81  }.
  82
  83 record bounded_above_sequence (O:pordered_set) : Type ≝
  84  { bas_seq:1> nat→O;
  85    bas_is_bounded_above:> is_bounded_above ? bas_seq
  86  }.
  87
  88 record bounded_sequence (O:pordered_set) : Type ≝
  89  { bs_seq:1> nat → O;
  90    bs_is_bounded_below: is_bounded_below ? bs_seq;
  91    bs_is_bounded_above: is_bounded_above ? bs_seq
  92  }.
  93
  94 definition bounded_below_sequence_of_bounded_sequence ≝
  95  λO:pordered_set.λb:bounded_sequence O.
  96   mk_bounded_below_sequence ? b (bs_is_bounded_below ? b).
  97
  98 coercion cic:/matita/ordered_sets/bounded_below_sequence_of_bounded_sequence.con.
  99
 100 definition bounded_above_sequence_of_bounded_sequence ≝
 101  λO:pordered_set.λb:bounded_sequence O.
 102   mk_bounded_above_sequence ? b (bs_is_bounded_above ? b).
 103
 104 coercion cic:/matita/ordered_sets/bounded_above_sequence_of_bounded_sequence.con.
 105
 106 definition lower_bound ≝
 107  λO:ordered_set.λb:bounded_below_sequence O.
 108   ib_lower_bound ? b (bbs_is_bounded_below ? b).
 109
 110 lemma lower_bound_is_lower_bound:
 111  ∀O:ordered_set.∀b:bounded_below_sequence O.
 112   is_lower_bound ? b (lower_bound ? b).
 113  intros;
 114  unfold lower_bound;
 115  apply ib_lower_bound_is_lower_bound.
 116 qed.
 117
 118 definition upper_bound ≝
 119  λO:ordered_set.λb:bounded_above_sequence O.
 120   ib_upper_bound ? b (bas_is_bounded_above ? b).
 121
 122 lemma upper_bound_is_upper_bound:
 123  ∀O:ordered_set.∀b:bounded_above_sequence O.
 124   is_upper_bound ? b (upper_bound ? b).
 125  intros;
 126  unfold upper_bound;
 127  apply ib_upper_bound_is_upper_bound.
 128 qed.
 129
 130 definition lt ≝ λO:ordered_set.λa,b:O.a ≤ b ∧ a ≠ b.
 131
 132 interpretation "Ordered set lt" 'lt a b =
 133  (cic:/matita/ordered_sets/lt.con _ a b).
 134
 135 definition reverse_ordered_set: ordered_set → ordered_set.
 136  intros;
 137  apply mk_ordered_set;
 138   [2:apply (λx,y:o.y ≤ x)
 139   | skip
 140   | apply mk_is_order_relation;
 141      [ simplify;
 142        intros;
 143        apply (or_reflexive ? ? o)
 144      | simplify;
 145        intros;
 146        apply (or_transitive ? ? o);
 147         [2: apply H1
 148         | skip
 149         | assumption
 150         ]
 151      | simplify;
 152        intros;
 153        apply (or_antisimmetric ? ? o);
 154        assumption
 155      ]
 156   ].
 157 qed.
 158
 159 interpretation "Ordered set ge" 'geq a b =
 160  (cic:/matita/ordered_sets/os_le.con _
 161   (cic:/matita/ordered_sets/os_pre_ordered_set.con _
 162    (cic:/matita/ordered_sets/reverse_ordered_set.con _ _)) a b).
 163
 164 lemma is_lower_bound_reverse_is_upper_bound:
 165  ∀O:ordered_set.∀a:nat→O.∀l:O.
 166   is_lower_bound O a l → is_upper_bound (reverse_ordered_set O) a l.
 167  intros;
 168  unfold;
 169  intro;
 170  unfold;
 171  unfold reverse_ordered_set;
 172  simplify;
 173  apply H.
 174 qed.
 175
 176 lemma is_upper_bound_reverse_is_lower_bound:
 177  ∀O:ordered_set.∀a:nat→O.∀l:O.
 178   is_upper_bound O a l → is_lower_bound (reverse_ordered_set O) a l.
 179  intros;
 180  unfold;
 181  intro;
 182  unfold;
 183  unfold reverse_ordered_set;
 184  simplify;
 185  apply H.
 186 qed.
 187
 188 lemma reverse_is_lower_bound_is_upper_bound:
 189  ∀O:ordered_set.∀a:nat→O.∀l:O.
 190   is_lower_bound (reverse_ordered_set O) a l → is_upper_bound O a l.
 191  intros;
 192  unfold in H;
 193  unfold reverse_ordered_set in H;
 194  apply H.
 195 qed.
 196
 197 lemma reverse_is_upper_bound_is_lower_bound:
 198  ∀O:ordered_set.∀a:nat→O.∀l:O.
 199   is_upper_bound (reverse_ordered_set O) a l → is_lower_bound O a l.
 200  intros;
 201  unfold in H;
 202  unfold reverse_ordered_set in H;
 203  apply H.
 204 qed.
 205
 206
 207 lemma is_inf_to_reverse_is_sup:
 208  ∀O:ordered_set.∀a:bounded_below_sequence O.∀l:O.
 209   is_inf O a l → is_sup (reverse_ordered_set O) a l.
 210  intros;
 211  apply (mk_is_sup (reverse_ordered_set O));
 212   [ apply is_lower_bound_reverse_is_upper_bound;
 213     apply inf_lower_bound;
 214     assumption
 215   | intros;
 216     change in v with (os_carrier O);
 217     change with (v ≤ l);
 218     apply (inf_greatest_lower_bound ? ? ? H);
 219     apply reverse_is_upper_bound_is_lower_bound;
 220     assumption
 221   ].
 222 qed.
 223
 224 lemma is_sup_to_reverse_is_inf:
 225  ∀O:ordered_set.∀a:bounded_above_sequence O.∀l:O.
 226   is_sup O a l → is_inf (reverse_ordered_set O) a l.
 227  intros;
 228  apply (mk_is_inf (reverse_ordered_set O));
 229   [ apply is_upper_bound_reverse_is_lower_bound;
 230     apply sup_upper_bound;
 231     assumption
 232   | intros;
 233     change in v with (os_carrier O);
 234     change with (l ≤ v);
 235     apply (sup_least_upper_bound ? ? ? H);
 236     apply reverse_is_lower_bound_is_upper_bound;
 237     assumption
 238   ].
 239 qed.
 240
 241 lemma reverse_is_sup_to_is_inf:
 242  ∀O:ordered_set.∀a:bounded_above_sequence O.∀l:O.
 243   is_sup (reverse_ordered_set O) a l → is_inf O a l.
 244  intros;
 245  apply mk_is_inf;
 246   [ apply reverse_is_upper_bound_is_lower_bound;
 247     change in l with (os_carrier (reverse_ordered_set O));
 248     apply sup_upper_bound;
 249     assumption
 250   | intros;
 251     change in l with (os_carrier (reverse_ordered_set O));
 252     change in v with (os_carrier (reverse_ordered_set O));
 253     change with (os_le (reverse_ordered_set O) l v);
 254     apply (sup_least_upper_bound ? ? ? H);
 255     change in v with (os_carrier O);
 256     apply is_lower_bound_reverse_is_upper_bound;
 257     assumption
 258   ].
 259 qed.
 260
 261 lemma reverse_is_inf_to_is_sup:
 262  ∀O:ordered_set.∀a:bounded_above_sequence O.∀l:O.
 263   is_inf (reverse_ordered_set O) a l → is_sup O a l.
 264  intros;
 265  apply mk_is_sup;
 266   [ apply reverse_is_lower_bound_is_upper_bound;
 267     change in l with (os_carrier (reverse_ordered_set O));
 268     apply (inf_lower_bound ? ? ? H)
 269   | intros;
 270     change in l with (os_carrier (reverse_ordered_set O));
 271     change in v with (os_carrier (reverse_ordered_set O));
 272     change with (os_le (reverse_ordered_set O) v l);
 273     apply (inf_greatest_lower_bound ? ? ? H);
 274     change in v with (os_carrier O);
 275     apply is_upper_bound_reverse_is_lower_bound;
 276     assumption
 277   ].
 278 qed.
 279
 280 record cotransitively_ordered_set: Type :=
 281  { cos_ordered_set :> ordered_set;
 282    cos_cotransitive: cotransitive ? (os_le cos_ordered_set)
 283  }.