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 "cprop_connectives.ma".
  16
  17 (* Definition 2.1 *)
  18 record ordered_set: Type ≝ {
  19   os_carr:> Type;
  20   os_excess: os_carr → os_carr → CProp;
  21   os_coreflexive: coreflexive ? os_excess;
  22   os_cotransitive: cotransitive ? os_excess
  23 }.
  24
  25 interpretation "Ordered set excess" 'nleq a b = (os_excess _ a b).
  26
  27 (* Definition 2.2 (3) *)
  28 definition le ≝ λE:ordered_set.λa,b:E. ¬ (a ≰ b).
  29
  30 interpretation "Ordered set greater or equal than" 'geq a b = (le _ b a).
  31
  32 interpretation "Ordered set less or equal than" 'leq a b = (le _ a b).
  33
  34 lemma le_reflexive: ∀E.reflexive ? (le E).
  35 unfold reflexive; intros 3 (E x H); apply (os_coreflexive ?? H);
  36 qed.
  37
  38 lemma le_transitive: ∀E.transitive ? (le E).
  39 unfold transitive; intros 7 (E x y z H1 H2 H3); cases (os_cotransitive ??? y H3) (H4 H4);
  40 [cases (H1 H4)|cases (H2 H4)]
  41 qed.
  42
  43 (* Lemma 2.3 *)
  44 lemma exc_le_variance:
  45   ∀O:ordered_set.∀a,b,a',b':O.a ≰ b → a ≤ a' → b' ≤ b → a' ≰ b'.
  46 intros (O a b a1 b1 Eab Laa1 Lb1b);
  47 cases (os_cotransitive ??? a1 Eab) (H H); [cases (Laa1 H)]
  48 cases (os_cotransitive ??? b1 H) (H1 H1); [assumption]
  49 cases (Lb1b H1);
  50 qed.
  51
  52 lemma square_ordered_set: ordered_set → ordered_set.
  53 intro O;
  54 apply (mk_ordered_set (O × O));
  55 [1: intros (x y); apply (\fst x ≰ \fst y ∨ \snd x ≰ \snd y);
  56 |2: intro x0; cases x0 (x y); clear x0; simplify; intro H;
  57     cases H (X X); apply (os_coreflexive ?? X);
  58 |3: intros 3 (x0 y0 z0); cases x0 (x1 x2); cases y0 (y1 y2) ; cases z0 (z1 z2);
  59     clear x0 y0 z0; simplify; intro H; cases H (H1 H1); clear H;
  60     [1: cases (os_cotransitive ??? z1 H1); [left; left|right;left]assumption;
  61     |2: cases (os_cotransitive ??? z2 H1); [left;right|right;right]assumption]]
  62 qed.
  63
  64 notation "s 2 \atop \nleq" non associative with precedence 90
  65   for @{ 'square_os $s }.
  66 notation > "s 'square'" non associative with precedence 90
  67   for @{ 'square $s }.
  68 interpretation "ordered set square" 'square s = (square_ordered_set s).
  69 interpretation "ordered set square" 'square_os s = (square_ordered_set s).
  70
  71 definition os_subset ≝ λO:ordered_set.λP,Q:O→Prop.∀x:O.P x → Q x.
  72
  73 notation "a \subseteq u" left associative with precedence 70
  74   for @{ 'subset $a $u }.
  75 interpretation "ordered set subset" 'subset a b = (os_subset _ a b).
  76