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 "excedence.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 alias id "transitive" = "cic:/matita/higher_order_defs/relations/transitive.con".
  36 alias id "cotransitive" = "cic:/matita/higher_order_defs/relations/cotransitive.con".
  37 alias id "antisymmetric" = "cic:/matita/higher_order_defs/relations/antisymmetric.con".
  38
  39 theorem antisimmetric_to_cotransitive_to_transitive:
  40  ∀C:Type.∀le:C→C→Prop. antisymmetric ? le → cotransitive ? le → transitive ? le.
  41 intros (T f Af cT); unfold transitive; intros (x y z fxy fyz);
  42 lapply (cT ? ? fxy z) as H; cases H; [assumption] cases (Af ? ? fyz H1);
  43 qed.
  44
  45 definition is_increasing ≝ λO:pordered_set.λa:nat→O.∀n:nat.a n ≤ a (S n).
  46 definition is_decreasing ≝ λO:pordered_set.λa:nat→O.∀n:nat.a (S n) ≤ a n.
  47
  48 definition is_upper_bound ≝ λO:pordered_set.λa:nat→O.λu:O.∀n:nat.a n ≤ u.
  49 definition is_lower_bound ≝ λO:pordered_set.λa:nat→O.λu:O.∀n:nat.u ≤ a n.
  50
  51 record is_sup (O:pordered_set) (a:nat→O) (u:O) : Prop ≝
  52  { sup_upper_bound: is_upper_bound O a u;
  53    sup_least_upper_bound: ∀v:O. is_upper_bound O a v → u≤v
  54  }.
  55
  56 record is_inf (O:pordered_set) (a:nat→O) (u:O) : Prop ≝
  57  { inf_lower_bound: is_lower_bound O a u;
  58    inf_greatest_lower_bound: ∀v:O. is_lower_bound O a v → v≤u
  59  }.
  60
  61 record is_bounded_below (O:pordered_set) (a:nat→O) : Type ≝
  62  { ib_lower_bound: O;
  63    ib_lower_bound_is_lower_bound: is_lower_bound ? a ib_lower_bound
  64  }.
  65
  66 record is_bounded_above (O:pordered_set) (a:nat→O) : Type ≝
  67  { ib_upper_bound: O;
  68    ib_upper_bound_is_upper_bound: is_upper_bound ? a ib_upper_bound
  69  }.
  70
  71 record is_bounded (O:pordered_set) (a:nat→O) : Type ≝
  72  { ib_bounded_below:> is_bounded_below ? a;
  73    ib_bounded_above:> is_bounded_above ? a
  74  }.
  75
  76 record bounded_below_sequence (O:pordered_set) : Type ≝
  77  { bbs_seq:1> nat→O;
  78    bbs_is_bounded_below:> is_bounded_below ? bbs_seq
  79  }.
  80
  81 record bounded_above_sequence (O:pordered_set) : Type ≝
  82  { bas_seq:1> nat→O;
  83    bas_is_bounded_above:> is_bounded_above ? bas_seq
  84  }.
  85
  86 record bounded_sequence (O:pordered_set) : Type ≝
  87  { bs_seq:1> nat → O;
  88    bs_is_bounded_below: is_bounded_below ? bs_seq;
  89    bs_is_bounded_above: is_bounded_above ? bs_seq
  90  }.
  91
  92 definition bounded_below_sequence_of_bounded_sequence ≝
  93  λO:pordered_set.λb:bounded_sequence O.
  94   mk_bounded_below_sequence ? b (bs_is_bounded_below ? b).
  95
  96 coercion cic:/matita/ordered_sets/bounded_below_sequence_of_bounded_sequence.con.
  97
  98 definition bounded_above_sequence_of_bounded_sequence ≝
  99  λO:pordered_set.λb:bounded_sequence O.
 100   mk_bounded_above_sequence ? b (bs_is_bounded_above ? b).
 101
 102 coercion cic:/matita/ordered_sets/bounded_above_sequence_of_bounded_sequence.con.
 103
 104 definition lower_bound ≝
 105  λO:pordered_set.λb:bounded_below_sequence O.
 106   ib_lower_bound ? b (bbs_is_bounded_below ? b).
 107
 108 lemma lower_bound_is_lower_bound:
 109  ∀O:pordered_set.∀b:bounded_below_sequence O.
 110   is_lower_bound ? b (lower_bound ? b).
 111 intros; unfold lower_bound; apply ib_lower_bound_is_lower_bound.
 112 qed.
 113
 114 definition upper_bound ≝
 115  λO:pordered_set.λb:bounded_above_sequence O.
 116   ib_upper_bound ? b (bas_is_bounded_above ? b).
 117
 118 lemma upper_bound_is_upper_bound:
 119  ∀O:pordered_set.∀b:bounded_above_sequence O.
 120   is_upper_bound ? b (upper_bound ? b).
 121 intros; unfold upper_bound; apply ib_upper_bound_is_upper_bound.
 122 qed.
 123
 124 lemma Or_symmetric: symmetric ? Or.
 125 unfold; intros (x y H); cases H; [right|left] assumption;
 126 qed.
 127
 128 definition reverse_excedence: excedence → excedence.
 129 intros (E); apply (mk_excedence E); [apply (λx,y.exc_relation E y x)]
 130 cases E (T f cRf cTf); simplify;
 131 [1: unfold Not; intros (x H); apply (cRf x); assumption
 132 |2: intros (x y z); apply Or_symmetric; apply cTf; assumption;]
 133 qed.
 134
 135 (*
 136
 137 definition reverse_pordered_set: pordered_set → pordered_set.
 138 intros (p); apply (mk_pordered_set (reverse_excedence p));
 139 generalize in match (reverse_excedence p); intros (E); cases E (T f cRf cTf);
 140 simplify; apply mk_is_porder_relation; unfold; intros;
 141 [apply le_reflexive|apply (le_transitive ???? H H1);|apply (le_antisymmetric ??? H H1)]
 142 qed.
 143
 144 lemma is_lower_bound_reverse_is_upper_bound:
 145  ∀O:pordered_set.∀a:nat→O.∀l:O.
 146   is_lower_bound O a l → is_upper_bound (reverse_pordered_set O) a l.
 147 intros (O a l H); unfold; intros (n); unfold reverse_pordered_set;
 148 unfold reverse_excedence; simplify; fold unfold le (le ? l (a n)); apply H;
 149 qed.
 150
 151 lemma is_upper_bound_reverse_is_lower_bound:
 152  ∀O:pordered_set.∀a:nat→O.∀l:O.
 153   is_upper_bound O a l → is_lower_bound (reverse_pordered_set O) a l.
 154 intros (O a l H); unfold; intros (n); unfold reverse_pordered_set;
 155 unfold reverse_excedence; simplify; fold unfold le (le ? (a n) l); apply H;
 156 qed.
 157
 158 lemma reverse_is_lower_bound_is_upper_bound:
 159  ∀O:pordered_set.∀a:nat→O.∀l:O.
 160   is_lower_bound (reverse_pordered_set O) a l → is_upper_bound O a l.
 161 intros (O a l H); unfold; intros (n); unfold reverse_pordered_set in H;
 162 unfold reverse_excedence in H; simplify in H; apply H;
 163 qed.
 164
 165 lemma reverse_is_upper_bound_is_lower_bound:
 166  ∀O:pordered_set.∀a:nat→O.∀l:O.
 167   is_upper_bound (reverse_pordered_set O) a l → is_lower_bound O a l.
 168 intros (O a l H); unfold; intros (n); unfold reverse_pordered_set in H;
 169 unfold reverse_excedence in H; simplify in H; apply H;
 170 qed.
 171
 172 lemma is_inf_to_reverse_is_sup:
 173  ∀O:pordered_set.∀a:bounded_below_sequence O.∀l:O.
 174   is_inf O a l → is_sup (reverse_pordered_set O) a l.
 175 intros (O a l H); apply (mk_is_sup (reverse_pordered_set O));
 176 [1: apply is_lower_bound_reverse_is_upper_bound; apply inf_lower_bound; assumption
 177 |2: unfold reverse_pordered_set; simplify; unfold reverse_excedence; simplify;
 178     intros (m H1); apply (inf_greatest_lower_bound ? ? ? H); apply H1;]
 179 qed.
 180
 181 lemma is_sup_to_reverse_is_inf:
 182  ∀O:pordered_set.∀a:bounded_above_sequence O.∀l:O.
 183   is_sup O a l → is_inf (reverse_pordered_set O) a l.
 184 intros (O a l H); apply (mk_is_inf (reverse_pordered_set O));
 185 [1: apply is_upper_bound_reverse_is_lower_bound; apply sup_upper_bound; assumption
 186 |2: unfold reverse_pordered_set; simplify; unfold reverse_excedence; simplify;
 187     intros (m H1); apply (sup_least_upper_bound ? ? ? H); apply H1;]
 188 qed.
 189
 190 lemma reverse_is_sup_to_is_inf:
 191  ∀O:pordered_set.∀a:bounded_above_sequence O.∀l:O.
 192   is_sup (reverse_pordered_set O) a l → is_inf O a l.
 193 intros (O a l H); apply mk_is_inf;
 194 [1: apply reverse_is_upper_bound_is_lower_bound;
 195     apply (sup_upper_bound (reverse_pordered_set O)); assumption
 196 |2: intros (v H1); apply (sup_least_upper_bound (reverse_pordered_set O) a l H v);
 197     apply is_lower_bound_reverse_is_upper_bound; assumption;]
 198 qed.
 199
 200 lemma reverse_is_inf_to_is_sup:
 201  ∀O:pordered_set.∀a:bounded_above_sequence O.∀l:O.
 202   is_inf (reverse_pordered_set O) a l → is_sup O a l.
 203 intros (O a l H); apply mk_is_sup;
 204 [1: apply reverse_is_lower_bound_is_upper_bound;
 205     apply (inf_lower_bound (reverse_pordered_set O)); assumption
 206 |2: intros (v H1); apply (inf_greatest_lower_bound (reverse_pordered_set O) a l H v);
 207     apply is_upper_bound_reverse_is_lower_bound; assumption;]
 208 qed.
 209
 210 (*
 211 record cotransitively_ordered_set: Type :=
 212  { cos_ordered_set :> ordered_set;
 213    cos_cotransitive: cotransitive ? (os_le cos_ordered_set)
 214  }.
 215 *)
 216
 217 *)
 218
 219 definition total_order_property : ∀E:excedence. Type ≝
 220   λE:excedence. ∀a,b:E. a ≰ b → a < b.
 221
 222 record tordered_set : Type ≝ {
 223  tos_poset:> pordered_set;
 224  tos_totality: total_order_property tos_poset
 225 }.