helm/software/matita/contribs/dama/dama/bishop_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 "ordered_set.ma".
  16
  17 (* Definition 2.2, setoid *)
  18 record bishop_set: Type ≝ {
  19   bs_carr:> Type;
  20   bs_apart: bs_carr → bs_carr → CProp;
  21   bs_coreflexive: coreflexive ? bs_apart;
  22   bs_symmetric: symmetric ? bs_apart;
  23   bs_cotransitive: cotransitive ? bs_apart
  24 }.
  25
  26 notation "hvbox(a break # b)" non associative with precedence 45
  27   for @{ 'apart $a $b}.
  28
  29 interpretation "bishop set apartness" 'apart x y = (bs_apart _ x y).
  30
  31 definition bishop_set_of_ordered_set: ordered_set → bishop_set.
  32 intros (E); apply (mk_bishop_set E (λa,b:E. a ≰ b ∨ b ≰ a));
  33 [1: unfold; cases E; simplify; clear E; intros (x); unfold;
  34     intros (H1); apply (H x); cases H1; assumption;
  35 |2: unfold; intros(x y H); cases H; clear H; [right|left] assumption;
  36 |3: intros (E); unfold; cases E (T f _ cTf); simplify; intros (x y z Axy);
  37     cases Axy (H H); lapply (cTf ? ? z H) as H1; cases H1; clear Axy H1;
  38     [left; left|right; left|right; right|left; right] assumption]
  39 qed.
  40
  41 (* Definition 2.2 (2) *)
  42 definition eq ≝ λA:bishop_set.λa,b:A. ¬ (a # b).
  43
  44 notation "hvbox(a break \approx b)" non associative with precedence 45
  45   for @{ 'napart $a $b}.
  46
  47 interpretation "Bishop set alikeness" 'napart a b = (eq _ a b).
  48
  49 lemma eq_reflexive:∀E:bishop_set. reflexive ? (eq E).
  50 intros (E); unfold; intros (x); apply bs_coreflexive;
  51 qed.
  52
  53 lemma eq_sym_:∀E:bishop_set.symmetric ? (eq E).
  54 intros 4 (E x y H); intro T; cases (H (bs_symmetric ??? T));
  55 qed.
  56
  57 lemma eq_sym:∀E:bishop_set.∀x,y:E.x ≈ y → y ≈ x ≝ eq_sym_.
  58
  59 lemma eq_trans_: ∀E:bishop_set.transitive ? (eq E).
  60 intros 6 (E x y z Exy Eyz); intro Axy; cases (bs_cotransitive ???y Axy);
  61 [apply Exy|apply Eyz] assumption.
  62 qed.
  63
  64 coercion cic:/matita/dama/bishop_set/bishop_set_of_ordered_set.con.
  65
  66 lemma le_antisymmetric:
  67   ∀E:ordered_set.antisymmetric E (le E) (eq E).
  68 intros 5 (E x y Lxy Lyx); intro H;
  69 cases H; [apply Lxy;|apply Lyx] assumption;
  70 qed.
  71
  72 lemma le_le_eq: ∀E:ordered_set.∀a,b:E. a ≤ b → b ≤ a → a ≈ b.
  73 intros (E x y L1 L2); intro H; cases H; [apply L1|apply L2] assumption;
  74 qed.
  75
  76 definition lt ≝ λE:ordered_set.λa,b:E. a ≤ b ∧ a # b.
  77
  78 interpretation "ordered sets less than" 'lt a b = (lt _ a b).
  79
  80 lemma lt_coreflexive: ∀E.coreflexive ? (lt E).
  81 intros 2 (E x); intro H; cases H (_ ABS);
  82 apply (bs_coreflexive ? x ABS);
  83 qed.
  84
  85 lemma lt_transitive: ∀E.transitive ? (lt E).
  86 intros (E); unfold; intros (x y z H1 H2); cases H1 (Lxy Axy); cases H2 (Lyz Ayz);
  87 split; [apply (le_transitive ???? Lxy Lyz)] clear H1 H2;
  88 cases Axy (H1 H1); cases Ayz (H2 H2); [1:cases (Lxy H1)|3:cases (Lyz H2)]clear Axy Ayz;
  89 [1: cases (os_cotransitive ??? y H1) (X X); [cases (Lxy X)|cases (os_coreflexive ?? X)]
  90 |2: cases (os_cotransitive ??? x H2) (X X); [right;assumption|cases (Lxy X)]]
  91 qed.
  92
  93 theorem lt_to_excess: ∀E:ordered_set.∀a,b:E. (a < b) → (b ≰ a).
  94 intros (E a b Lab); cases Lab (LEab Aab); cases Aab (H H);[cases (LEab H)]
  95 assumption;
  96 qed.
  97
  98 definition bs_subset ≝ λO:bishop_set.λP,Q:O→Prop.∀x:O.P x → Q x.
  99
 100 interpretation "bishop set subset" 'subset a b = (bs_subset _ a b).
 101
 102 definition square_bishop_set : bishop_set → bishop_set.
 103 intro S; apply (mk_bishop_set (S × S));
 104 [1: intros (x y); apply ((fst x # fst y) ∨ (snd x # snd y));
 105 |2: intro x; simplify; intro; cases H (X X); clear H; apply (bs_coreflexive ?? X);
 106 |3: intros 2 (x y); simplify; intro H; cases H (X X); clear H; [left|right] apply (bs_symmetric ??? X);
 107 |4: intros 3 (x y z); simplify; intro H; cases H (X X); clear H;
 108     [1: cases (bs_cotransitive ??? (fst z) X); [left;left|right;left]assumption;
 109     |2: cases (bs_cotransitive ??? (snd z) X); [left;right|right;right]assumption;]]
 110 qed.
 111
 112 notation "s 2 \atop \neq" non associative with precedence 90
 113   for @{ 'square_bs $s }.
 114 interpretation "bishop set square" 'square x = (square_bishop_set x).
 115 interpretation "bishop set square" 'square_bs x = (square_bishop_set x).