]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/dama/bishop_set.ma
better doc
[helm.git] / helm / software / matita / library / 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 "dama/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 interpretation "bishop set apartness" 'apart x y = (bs_apart _ x y).
27
28 definition bishop_set_of_ordered_set: ordered_set → bishop_set.
29 intros (E); apply (mk_bishop_set E (λa,b:E. a ≰ b ∨ b ≰ a));  
30 [1: intro x; simplify; intro H; cases H; clear H;
31     apply (exc_coreflexive x H1);
32 |2: intros 3 (x y H); simplify in H ⊢ %; cases H; [right|left]assumption; 
33 |3: intros 4 (x y z H);  simplify in H ⊢ %; cases H; clear H;
34     [ cases (exc_cotransitive x y z H1); [left;left|right;left] assumption;
35     | cases (exc_cotransitive y x z H1); [right;right|left;right] assumption;]]
36 qed.
37
38 (* Definition 2.2 (2) *)
39 definition eq ≝ λA:bishop_set.λa,b:A. ¬ (a # b).
40
41 interpretation "Bishop set alikeness" 'napart a b = (eq _ a b). 
42
43 lemma eq_reflexive:∀E:bishop_set. reflexive ? (eq E).
44 intros (E); unfold; intros (x); apply bs_coreflexive; 
45 qed.
46
47 lemma eq_sym_:∀E:bishop_set.symmetric ? (eq E).
48 intros 4 (E x y H); intro T; cases (H (bs_symmetric ??? T)); 
49 qed.
50
51 lemma eq_sym:∀E:bishop_set.∀x,y:E.x ≈ y → y ≈ x ≝ eq_sym_.
52
53 lemma eq_trans_: ∀E:bishop_set.transitive ? (eq E).
54 intros 6 (E x y z Exy Eyz); intro Axy; cases (bs_cotransitive ???y Axy); 
55 [apply Exy|apply Eyz] assumption.
56 qed.
57
58 coercion bishop_set_of_ordered_set.
59
60 lemma le_antisymmetric: 
61   ∀E:ordered_set.antisymmetric E (le (os_l E)) (eq E).
62 intros 5 (E x y Lxy Lyx); intro H; 
63 cases H; [apply Lxy;|apply Lyx] assumption;
64 qed.
65
66 lemma le_le_eq: ∀E:ordered_set.∀a,b:E. a ≤ b → b ≤ a → a ≈ b.
67 intros (E x y L1 L2); intro H; cases H; [apply L1|apply L2] assumption;
68 qed.
69
70 definition bs_subset ≝ λO:bishop_set.λP,Q:O→Prop.∀x:O.P x → Q x.
71
72 interpretation "bishop set subset" 'subseteq a b = (bs_subset _ a b). 
73
74 definition square_bishop_set : bishop_set → bishop_set.
75 intro S; apply (mk_bishop_set (S × S));
76 [1: intros (x y); apply ((\fst x # \fst y) ∨ (\snd x # \snd y));
77 |2: intro x; simplify; intro; cases H (X X); clear H; apply (bs_coreflexive ?? X);   
78 |3: intros 2 (x y); simplify; intro H; cases H (X X); clear H; [left|right] apply (bs_symmetric ??? X); 
79 |4: intros 3 (x y z); simplify; intro H; cases H (X X); clear H;
80     [1: cases (bs_cotransitive ??? (\fst z) X); [left;left|right;left]assumption;
81     |2: cases (bs_cotransitive ??? (\snd z) X); [left;right|right;right]assumption;]]
82 qed.
83
84 notation "s 2 \atop \neq" non associative with precedence 90
85   for @{ 'square_bs $s }.
86 notation > "s 'squareB'" non associative with precedence 90
87   for @{ 'squareB $s }.
88 interpretation "bishop set square" 'squareB x = (square_bishop_set x).
89 interpretation "bishop set square" 'square_bs x = (square_bishop_set x).