helm/software/matita/contribs/dama/dama/ordered_set.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 include "datatypes/constructors.ma".
  16 include "logic/cprop_connectives.ma".
  17
  18
  19 (* TEMPLATES
  20 notation "''" non associative with precedence 90 for @{'}.
  21 notation "''" non associative with precedence 90 for @{'}.
  22
  23 interpretation "" ' = ( (os_l _)).
  24 interpretation "" ' = ( (os_r _)).
  25 *)
  26
  27 (* Definition 2.1 *)
  28 record half_ordered_set: Type ≝ {
  29   hos_carr:> Type;
  30   hos_excess: hos_carr → hos_carr → CProp;
  31   hos_coreflexive: coreflexive ? hos_excess;
  32   hos_cotransitive: cotransitive ? hos_excess
  33 }.
  34
  35 definition dual_hos : half_ordered_set → half_ordered_set.
  36 intro; constructor 1;
  37 [ apply (hos_carr h);
  38 | apply (λx,y.hos_excess h y x);
  39 | apply (hos_coreflexive h);
  40 | intros 4 (x y z H); simplify in H ⊢ %; cases (hos_cotransitive h ?? z H);
  41   [right|left] assumption;]
  42 qed.
  43
  44 record ordered_set : Type ≝ {
  45   os_l_ : half_ordered_set;
  46   os_r_ : half_ordered_set;
  47   os_with : os_r_ = dual_hos os_l_
  48 }.
  49
  50 definition os_l : ordered_set → half_ordered_set.
  51 intro h; constructor 1;
  52 [ apply (hos_carr (os_l_ h));
  53 | apply (λx,y.hos_excess (os_l_ h) x y);
  54 | apply (hos_coreflexive (os_l_ h));
  55 | apply (hos_cotransitive (os_l_ h));
  56 ]
  57 qed.
  58
  59 definition os_r : ordered_set → half_ordered_set.
  60 intro o; apply (dual_hos (os_l_ o)); qed.
  61
  62 lemma half2full : half_ordered_set → ordered_set.
  63 intro hos;
  64 constructor 1; [apply hos; | apply (dual_hos hos); | reflexivity]
  65 qed.
  66
  67 (* coercion half2full. *)
  68
  69 definition Type_of_ordered_set : ordered_set → Type.
  70 intro o; apply (hos_carr (os_l o)); qed.
  71
  72 definition Type_of_ordered_set_dual : ordered_set → Type.
  73 intro o; apply (hos_carr (os_r o)); qed.
  74
  75 coercion Type_of_ordered_set_dual.
  76 coercion Type_of_ordered_set.
  77
  78 notation "a ≰≰ b" non associative with precedence 45 for @{'nleq_low $a $b}.
  79 interpretation "Ordered half set excess" 'nleq_low a b = (hos_excess _ a b).
  80
  81 interpretation "Ordered set excess (dual)" 'ngeq a b = (hos_excess (os_r _) a b).
  82 interpretation "Ordered set excess" 'nleq a b = (hos_excess (os_l _) a b).
  83
  84 notation "'exc_coreflexive'" non associative with precedence 90 for @{'exc_coreflexive}.
  85 notation "'cxe_coreflexive'" non associative with precedence 90 for @{'cxe_coreflexive}.
  86
  87 interpretation "exc_coreflexive" 'exc_coreflexive = (hos_coreflexive (os_l _)).
  88 interpretation "cxe_coreflexive" 'cxe_coreflexive = (hos_coreflexive (os_r _)).
  89
  90 notation "'exc_cotransitive'" non associative with precedence 90 for @{'exc_cotransitive}.
  91 notation "'cxe_cotransitive'" non associative with precedence 90 for @{'cxe_cotransitive}.
  92
  93 interpretation "exc_cotransitive" 'exc_cotransitive = (hos_cotransitive (os_l _)).
  94 interpretation "cxe_cotransitive" 'cxe_cotransitive = (hos_cotransitive (os_r _)).
  95
  96 (* Definition 2.2 (3) *)
  97 definition le ≝ λE:half_ordered_set.λa,b:E. ¬ (a ≰≰ b).
  98
  99 notation "hvbox(a break ≤≤ b)" non associative with precedence 45 for @{ 'leq_low $a $b }.
 100 interpretation "Ordered half set less or equal than" 'leq_low a b = (le _ a b).
 101
 102 interpretation "Ordered set greater or equal than" 'geq a b = (le (os_r _) a b).
 103 interpretation "Ordered set less or equal than" 'leq a b = (le (os_l _) a b).
 104
 105 lemma hle_reflexive: ∀E.reflexive ? (le E).
 106 unfold reflexive; intros 3 (E x H); apply (hos_coreflexive ?? H);
 107 qed.
 108
 109 notation "'le_reflexive'" non associative with precedence 90 for @{'le_reflexive}.
 110 notation "'ge_reflexive'" non associative with precedence 90 for @{'ge_reflexive}.
 111
 112 interpretation "le reflexive" 'le_reflexive = (hle_reflexive (os_l _)).
 113 interpretation "ge reflexive" 'ge_reflexive = (hle_reflexive (os_r _)).
 114
 115 (* DUALITY TESTS
 116 lemma test_le_ge_convertible :∀o:ordered_set.∀x,y:o. x ≤ y → y ≥ x.
 117 intros; assumption; qed.
 118
 119 lemma test_ge_reflexive :∀o:ordered_set.∀x:o. x ≥ x.
 120 intros; apply ge_reflexive. qed.
 121
 122 lemma test_le_reflexive :∀o:ordered_set.∀x:o. x ≤ x.
 123 intros; apply le_reflexive. qed.
 124 *)
 125
 126 lemma hle_transitive: ∀E.transitive ? (le E).
 127 unfold transitive; intros 7 (E x y z H1 H2 H3); cases (hos_cotransitive ??? y H3) (H4 H4);
 128 [cases (H1 H4)|cases (H2 H4)]
 129 qed.
 130
 131 notation "'le_transitive'" non associative with precedence 90 for @{'le_transitive}.
 132 notation "'ge_transitive'" non associative with precedence 90 for @{'ge_transitive}.
 133
 134 interpretation "le transitive" 'le_transitive = (hle_transitive (os_l _)).
 135 interpretation "ge transitive" 'ge_transitive = (hle_transitive (os_r _)).
 136
 137 (* Lemma 2.3 *)
 138 lemma exc_hle_variance:
 139   ∀O:half_ordered_set.∀a,b,a',b':O.a ≰≰ b → a ≤≤ a' → b' ≤≤ b → a' ≰≰ b'.
 140 intros (O a b a1 b1 Eab Laa1 Lb1b);
 141 cases (hos_cotransitive ??? a1 Eab) (H H); [cases (Laa1 H)]
 142 cases (hos_cotransitive ??? b1 H) (H1 H1); [assumption]
 143 cases (Lb1b H1);
 144 qed.
 145
 146 notation "'exc_le_variance'" non associative with precedence 90 for @{'exc_le_variance}.
 147 notation "'exc_ge_variance'" non associative with precedence 90 for @{'exc_ge_variance}.
 148
 149 interpretation "exc_le_variance" 'exc_le_variance = (exc_hle_variance (os_l _)).
 150 interpretation "exc_ge_variance" 'exc_ge_variance = (exc_hle_variance (os_r _)).
 151
 152 lemma square_half_ordered_set: half_ordered_set → half_ordered_set.
 153 intro O;
 154 apply (mk_half_ordered_set (O × O));
 155 [1: intros (x y); apply (\fst x ≰≰ \fst y ∨ \snd x ≰≰ \snd y);
 156 |2: intro x0; cases x0 (x y); clear x0; simplify; intro H;
 157     cases H (X X); apply (hos_coreflexive ?? X);
 158 |3: intros 3 (x0 y0 z0); cases x0 (x1 x2); cases y0 (y1 y2) ; cases z0 (z1 z2);
 159     clear x0 y0 z0; simplify; intro H; cases H (H1 H1); clear H;
 160     [1: cases (hos_cotransitive ??? z1 H1); [left; left|right;left]assumption;
 161     |2: cases (hos_cotransitive ??? z2 H1); [left;right|right;right]assumption]]
 162 qed.
 163
 164 lemma square_ordered_set: ordered_set → ordered_set.
 165 intro O; constructor 1;
 166 [ apply (square_half_ordered_set (os_l O));
 167 | apply (dual_hos (square_half_ordered_set (os_l O)));
 168 | reflexivity]
 169 qed.
 170
 171 notation "s 2 \atop \nleq" non associative with precedence 90
 172   for @{ 'square_os $s }.
 173 notation > "s 'squareO'" non associative with precedence 90
 174   for @{ 'squareO $s }.
 175 interpretation "ordered set square" 'squareO s = (square_ordered_set s).
 176 interpretation "ordered set square" 'square_os s = (square_ordered_set s).
 177
 178 definition os_subset ≝ λO:ordered_set.λP,Q:O→Prop.∀x:O.P x → Q x.
 179
 180 interpretation "ordered set subset" 'subseteq a b = (os_subset _ a b).
 181