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   wloss: ∀A,B:Type. (A → A → B) → A → A → B;
  31   wloss_prop: (∀T,R,P,x,y.P x y = wloss T R P x y) ∨ (∀T,R,P,x,y.P y x = wloss T R P x y);
  32   hos_excess_: hos_carr → hos_carr → CProp;
  33   hos_coreflexive: coreflexive ? (wloss ?? hos_excess_);
  34   hos_cotransitive: cotransitive ? (wloss ?? hos_excess_)
  35 }.
  36
  37 definition hos_excess ≝ λO:half_ordered_set.wloss O ?? (hos_excess_ O).
  38
  39 (*
  40 lemma find_leq : half_ordered_set → half_ordered_set.
  41 intro O; constructor 1;
  42 [1: apply (hos_carr O);
  43 |2: apply (λT:Type.λf:T→T→CProp.f);
  44 |3: intros; left; intros; reflexivity;
  45 |4: apply (hos_excess_ O);
  46 |5: intro x; lapply (hos_coreflexive O x) as H; cases (wloss_prop O);
  47     rewrite < H1 in H; apply H;
  48 |6: intros 4 (x y z H); cases (wloss_prop O);
  49     rewrite > (H1 ? (hos_excess_ O)) in H ⊢ %;
  50     rewrite > (H1 ? (hos_excess_ O)); lapply (hos_cotransitive O ?? z H);
  51     [assumption] cases Hletin;[right|left]assumption;]
  52 qed.
  53 *)
  54
  55 definition dual_hos : half_ordered_set → half_ordered_set.
  56 intro; constructor 1;
  57 [ apply (hos_carr h);
  58 | apply (λT,R,f,x,y.wloss h T R f y x);
  59 | intros; cases (wloss_prop h);[right|left]intros;apply H;
  60 | apply (hos_excess_ h);
  61 | apply (hos_coreflexive h);
  62 | intros 4 (x y z H); simplify in H ⊢ %; cases (hos_cotransitive h y x z H);
  63   [right|left] assumption;]
  64 qed.
  65
  66 record ordered_set : Type ≝ {
  67   os_l : half_ordered_set;
  68   os_r_ : half_ordered_set;
  69   os_with : os_r_ = dual_hos os_l
  70 }.
  71
  72 definition os_r : ordered_set → half_ordered_set.
  73 intro o; apply (dual_hos (os_l o)); qed.
  74
  75 lemma half2full : half_ordered_set → ordered_set.
  76 intro hos;
  77 constructor 1; [apply hos; | apply (dual_hos hos); | reflexivity]
  78 qed.
  79
  80 definition Type_of_ordered_set : ordered_set → Type.
  81 intro o; apply (hos_carr (os_l o)); qed.
  82
  83 definition Type_of_ordered_set_dual : ordered_set → Type.
  84 intro o; apply (hos_carr (os_r o)); qed.
  85
  86 coercion Type_of_ordered_set_dual.
  87 coercion Type_of_ordered_set.
  88
  89 notation "a ≰≰ b" non associative with precedence 45 for @{'nleq_low $a $b}.
  90 interpretation "Ordered half set excess" 'nleq_low a b = (hos_excess _ a b).
  91
  92 interpretation "Ordered set excess (dual)" 'ngeq a b = (hos_excess (os_r _) a b).
  93 interpretation "Ordered set excess" 'nleq a b = (hos_excess (os_l _) a b).
  94
  95 notation "'exc_coreflexive'" non associative with precedence 90 for @{'exc_coreflexive}.
  96 notation "'cxe_coreflexive'" non associative with precedence 90 for @{'cxe_coreflexive}.
  97
  98 interpretation "exc_coreflexive" 'exc_coreflexive = ((hos_coreflexive (os_l _))).
  99 interpretation "cxe_coreflexive" 'cxe_coreflexive = ((hos_coreflexive (os_r _))).
 100
 101 notation "'exc_cotransitive'" non associative with precedence 90 for @{'exc_cotransitive}.
 102 notation "'cxe_cotransitive'" non associative with precedence 90 for @{'cxe_cotransitive}.
 103
 104 interpretation "exc_cotransitive" 'exc_cotransitive = ((hos_cotransitive (os_l _))).
 105 interpretation "cxe_cotransitive" 'cxe_cotransitive = ((hos_cotransitive (os_r _))).
 106
 107 (* Definition 2.2 (3) *)
 108 definition le ≝ λE:half_ordered_set.λa,b:E. ¬ (a ≰≰ b).
 109
 110 notation "hvbox(a break ≤≤ b)" non associative with precedence 45 for @{ 'leq_low $a $b }.
 111 interpretation "Half ordered set greater or equal than" 'leq_low a b = ((le _ a b)).
 112
 113 interpretation "Ordered set greater or equal than" 'geq a b = ((le (os_r _) a b)).
 114 interpretation "Ordered set less or equal than" 'leq a b = ((le (os_l _) a b)).
 115
 116 lemma hle_reflexive: ∀E.reflexive ? (le E).
 117 unfold reflexive; intros 3; apply (hos_coreflexive ? x H);
 118 qed.
 119
 120 notation "'le_reflexive'" non associative with precedence 90 for @{'le_reflexive}.
 121 notation "'ge_reflexive'" non associative with precedence 90 for @{'ge_reflexive}.
 122
 123 interpretation "le reflexive" 'le_reflexive = (hle_reflexive (os_l _)).
 124 interpretation "ge reflexive" 'ge_reflexive = (hle_reflexive (os_r _)).
 125
 126 (* DUALITY TESTS
 127 lemma test_le_ge_convertible :∀o:ordered_set.∀x,y:o. x ≤ y → y ≥ x.
 128 intros; assumption; qed.
 129
 130 lemma test_ge_reflexive :∀o:ordered_set.∀x:o. x ≥ x.
 131 intros; apply ge_reflexive. qed.
 132
 133 lemma test_le_reflexive :∀o:ordered_set.∀x:o. x ≤ x.
 134 intros; apply le_reflexive. qed.
 135 *)
 136
 137 lemma hle_transitive: ∀E.transitive ? (le E).
 138 unfold transitive; intros 7 (E x y z H1 H2 H3); cases (hos_cotransitive E x z y H3) (H4 H4);
 139 [cases (H1 H4)|cases (H2 H4)]
 140 qed.
 141
 142 notation "'le_transitive'" non associative with precedence 90 for @{'le_transitive}.
 143 notation "'ge_transitive'" non associative with precedence 90 for @{'ge_transitive}.
 144
 145 interpretation "le transitive" 'le_transitive = (hle_transitive (os_l _)).
 146 interpretation "ge transitive" 'ge_transitive = (hle_transitive (os_r _)).
 147
 148 (* Lemma 2.3 *)
 149 lemma exc_hle_variance:
 150   ∀O:half_ordered_set.∀a,b,a',b':O.a ≰≰ b → a ≤≤ a' → b' ≤≤ b → a' ≰≰ b'.
 151 intros (O a b a1 b1 Eab Laa1 Lb1b);
 152 cases (hos_cotransitive ? a b a1 Eab) (H H); [cases (Laa1 H)]
 153 cases (hos_cotransitive ? ?? b1 H) (H1 H1); [assumption]
 154 cases (Lb1b H1);
 155 qed.
 156
 157 notation "'exc_le_variance'" non associative with precedence 90 for @{'exc_le_variance}.
 158 notation "'exc_ge_variance'" non associative with precedence 90 for @{'exc_ge_variance}.
 159
 160 interpretation "exc_le_variance" 'exc_le_variance = (exc_hle_variance (os_l _)).
 161 interpretation "exc_ge_variance" 'exc_ge_variance = (exc_hle_variance (os_r _)).
 162
 163 definition square_exc ≝
 164  λO:half_ordered_set.λx,y:O×O.\fst x ≰≰ \fst y ∨ \snd x ≰≰ \snd y.
 165
 166 lemma square_half_ordered_set: half_ordered_set → half_ordered_set.
 167 intro O;
 168 apply (mk_half_ordered_set (O × O));
 169 [1: apply (wloss O);
 170 |2: intros; cases (wloss_prop O); [left|right] intros; apply H;
 171 |3: apply (square_exc O);
 172 |4: intro x; cases (wloss_prop O); rewrite < (H  ?? (square_exc O) x x); clear H;
 173     cases x; clear x; unfold square_exc; intro H; cases H; clear H; simplify in H1;
 174     [1,3: apply (hos_coreflexive O h H1);
 175     |*: apply (hos_coreflexive O h1 H1);]
 176 |5: intros 3 (x0 y0 z0); cases (wloss_prop O);
 177     do 3 rewrite < (H  ?? (square_exc O)); clear H; cases x0; cases y0; cases z0; clear x0 y0 z0;
 178     simplify; intro H; cases H; clear H;
 179     [1: cases (hos_cotransitive ? h h2 h4 H1); [left;left|right;left] assumption;
 180     |2: cases (hos_cotransitive ? h1 h3 h5 H1); [left;right|right;right] assumption;
 181     |3: cases (hos_cotransitive ? h2 h h4 H1); [right;left|left;left] assumption;
 182     |4: cases (hos_cotransitive ? h3 h1 h5 H1); [right;right|left;right] assumption;]]
 183 qed.
 184
 185 lemma square_ordered_set: ordered_set → ordered_set.
 186 intro O; constructor 1;
 187 [ apply (square_half_ordered_set (os_l O));
 188 | apply (dual_hos (square_half_ordered_set (os_l O)));
 189 | reflexivity]
 190 qed.
 191
 192 notation "s 2 \atop \nleq" non associative with precedence 90
 193   for @{ 'square_os $s }.
 194 notation > "s 'squareO'" non associative with precedence 90
 195   for @{ 'squareO $s }.
 196 interpretation "ordered set square" 'squareO s = (square_ordered_set s).
 197 interpretation "ordered set square" 'square_os s = (square_ordered_set s).
 198
 199 definition os_subset ≝ λO:ordered_set.λP,Q:O→Prop.∀x:O.P x → Q x.
 200
 201 interpretation "ordered set subset" 'subseteq a b = (os_subset _ a b).
 202