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