1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ordered_set.ma".
17 (* Definition 2.2, setoid *)
18 record bishop_set: 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
26 notation "hvbox(a break # b)" non associative with precedence 50
29 interpretation "bishop_setapartness" 'apart x y =
30 (cic:/matita/dama/bishop_set/bs_apart.con _ x y).
32 definition bishop_set_of_ordered_set: ordered_set → bishop_set.
33 intros (E); apply (mk_bishop_set E (λa,b:E. a ≰ b ∨ b ≰ a));
34 [1: unfold; cases E; simplify; clear E; intros (x); unfold;
35 intros (H1); apply (H x); cases H1; assumption;
36 |2: unfold; intros(x y H); cases H; clear H; [right|left] assumption;
37 |3: intros (E); unfold; cases E (T f _ cTf); simplify; intros (x y z Axy);
38 cases Axy (H H); lapply (cTf ? ? z H) as H1; cases H1; clear Axy H1;
39 [left; left|right; left|right; right|left; right] assumption]
42 (* Definition 2.2 (2) *)
43 definition eq ≝ λA:bishop_set.λa,b:A. ¬ (a # b).
45 notation "hvbox(a break ≈ b)" non associative with precedence 50
46 for @{ 'napart $a $b}.
48 interpretation "Bishop set alikeness" 'napart a b =
49 (cic:/matita/dama/bishop_set/eq.con _ a b).
51 lemma eq_reflexive:∀E:bishop_set. reflexive ? (eq E).
52 intros (E); unfold; intros (x); apply bs_coreflexive;
55 lemma eq_sym_:∀E:bishop_set.symmetric ? (eq E).
56 intros 4 (E x y H); intro T; cases (H (bs_symmetric ??? T));
59 lemma eq_sym:∀E:bishop_set.∀x,y:E.x ≈ y → y ≈ x ≝ eq_sym_.
61 lemma eq_trans_: ∀E:bishop_set.transitive ? (eq E).
62 (* bug. intros k deve fare whd quanto basta *)
63 intros 6 (E x y z Exy Eyz); intro Axy; cases (bs_cotransitive ???y Axy);
64 [apply Exy|apply Eyz] assumption.
67 coercion cic:/matita/dama/bishop_set/bishop_set_of_ordered_set.con.
69 lemma le_antisymmetric:
70 ∀E:ordered_set.antisymmetric E (le E) (eq E).
71 intros 5 (E x y Lxy Lyx); intro H;
72 cases H; [apply Lxy;|apply Lyx] assumption;
75 lemma le_le_eq: ∀E:ordered_set.∀a,b:E. a ≤ b → b ≤ a → a ≈ b.
76 intros (E x y L1 L2); intro H; cases H; [apply L1|apply L2] assumption;
79 definition lt ≝ λE:ordered_set.λa,b:E. a ≤ b ∧ a # b.
81 interpretation "ordered sets less than" 'lt a b =
82 (cic:/matita/dama/bishop_set/lt.con _ a b).
84 lemma lt_coreflexive: ∀E.coreflexive ? (lt E).
85 intros 2 (E x); intro H; cases H (_ ABS);
86 apply (bs_coreflexive ? x ABS);
89 lemma lt_transitive: ∀E.transitive ? (lt E).
90 intros (E); unfold; intros (x y z H1 H2); cases H1 (Lxy Axy); cases H2 (Lyz Ayz);
91 split; [apply (le_transitive ???? Lxy Lyz)] clear H1 H2;
92 cases Axy (H1 H1); cases Ayz (H2 H2); [1:cases (Lxy H1)|3:cases (Lyz H2)]clear Axy Ayz;
93 [1: cases (os_cotransitive ??? y H1) (X X); [cases (Lxy X)|cases (os_coreflexive ?? X)]
94 |2: cases (os_cotransitive ??? x H2) (X X); [right;assumption|cases (Lxy X)]]
97 theorem lt_to_excess: ∀E:ordered_set.∀a,b:E. (a < b) → (b ≰ a).
98 intros (E a b Lab); cases Lab (LEab Aab); cases Aab (H H);[cases (LEab H)]