]> matita.cs.unibo.it Git - helm.git/blob - helm/coq-contribs/SUBSETS/tbs_rel.v
Added aliases and notation.
[helm.git] / helm / coq-contribs / SUBSETS / tbs_rel.v
1 (** This module (Toolbox - subsets: relations) defines:
2     - subset inclusion:        [SbE] (sub or equal)
3     - subset overlap:          [SOv] (subset overlap)  not used in %\cite{SV}%
4     - subset equality          [SEq] (subset equal) 
5     
6     and provides:
7     - introduction and elimination rules for [SbE] and [SEq]
8     - standard properties (reflexiivity, symmetry, transitivity) for [SbE] and [SEq]
9
10 % \hrule %
11  
12  We require Toolbox basics and the underlying theory.
13   
14  *)
15 Require Export tbs_base.
16
17 Section Subset_Relations_Definitions.
18
19    Section subset_inclusion_overlap_equality.
20    
21 (** Sub or equal: [(SbE S U V)] means $ U \sub_S V $. *)
22       Definition SbE: (S:Set) (S -> Set) -> (S -> Set) -> Set.
23       Intros S U V.
24       Exact (a:S)(Eps S a U)->(Eps S a V).
25       Defined.
26
27 (** Subset overlap: [(SOv S U V)] means $ U \meet_S V $ that is $ (\lex a \in S)\ a \e U \land a \e V $. *)
28       Definition SOv: (S:Set) (S -> Set) -> (S -> Set) -> Set.
29       Intros S U V. 
30       Exact (LEx S [a](LAnd (Eps S a U) (Eps S a V))).
31       Defined.      
32 (*
33 (** Sup or equal: [(SpE S U V)] means $ U \sup_S V $. *)
34 Definition SpE: (S:Set) (S -> Set) -> (S -> Set) -> Set.
35 Intros S U V. 
36 Exact (SbE S V U).
37 Defined.
38 *)
39
40 (** Subset equal: [(SEq S U V)] means $ U =_S V $. *)   
41       Definition SEq: (S:Set) (S -> Set) -> (S -> Set) -> Set.
42       Intros S U V. 
43       Exact (a:S)(LIff (Eps S a U) (Eps S a V)).
44       Defined.
45
46    End subset_inclusion_overlap_equality.
47 (*   
48 Section subset_completion.
49
50 (** Subset complete: [(SCm S U V)] means $ (\lall a \in S)\ a \e U \lor a \e V $. *)
51 Definition SCm: (S:Set) (S -> Set) -> (S -> Set) -> Set.
52 Intros S U V.
53 Exact (a:S)(LOr (Eps S a U) (Eps S a V)).
54 Defined.
55
56 End subset_completion.
57 *)
58 End Subset_Relations_Definitions.
59
60 Section Subset_Relations_Results.
61
62    Section subset_inclusion.
63
64 (** Sub or equal introduction: $ ((\lall a \in S)\ a \e U \limp a \e V) \limp U \sub V $. *)
65       Theorem sbe_i: (S:Set; U,V:S-> Set) ((a:S) (Eps S a U) -> (Eps S a V)) -> (SbE S U V).
66       Unfold SbE.      
67       Intros.
68       MApply '(H a).
69       Qed.
70
71 (** Sub or equal elimination: $ a \e U \limp U \sub V \limp a \e V $. *)
72       Theorem sbe_e: (S:Set; U,V:S -> Set; a:S) (Eps S a U) -> (SbE S U V) -> (Eps S a V).
73       Unfold SbE.
74       Intros.
75       MApply '(H0 a).
76       Qed.
77
78 (*      
79 Theorem sbe_i2: (S:Set; U,V:(S -> Set)) ((a:S) (U a) -> (V a)) -> (SbE S U V).
80 Intros.
81 MApply 'sbe_i.
82 MApply 'eps_c1_l.
83 MApply '(H a).
84 MApply 'eps_c1_r.
85 Qed.
86
87 Theorem sbe_e2: (S:Set; U,V:(S -> Set); a:S) (U a) -> (SbE S U V) -> (V a).
88 Intros.
89 MApply 'eps_c1_r.
90 MApply '(sbe_e S U).
91 MApply 'eps_c1_l.
92 Qed.
93 *)
94 (** Sub or equal reflexivity: $ U \sub U $. *) 
95       Theorem sbe_r: (S:Set; U:S->Set) (SbE S U U).
96       Intros.
97       MApply 'sbe_i.
98       Qed.
99
100 (** Sub or equal transitivity: $ U \sub W \limp W \sub V \limp U \sub V $. *) 
101       Theorem sbe_t: (S:Set; W,U,V:S->Set) (SbE S U W) -> (SbE S W V) -> (SbE S U V).
102       Intros.
103       MApply 'sbe_i.
104       MApply '(sbe_e S W).
105       MApply '(sbe_e S U).
106       Qed.
107       
108    End subset_inclusion.
109
110    Section stop_sbot_sing_inclusion.
111
112 (** Subset top, sub or equal introduction: $ U \sub \stop $. *) 
113       Theorem stop_sbe_i: (S:Set; U:S->Set) (SbE S U (STop S)).
114       Intros.
115       MApply 'sbe_i.
116       MApply 'stop_eps_i.
117       Qed.
118
119 (** Subset bottom, sub or equal introduction: $ \sbot \sub U $. *)
120       Theorem sbot_sbe_i: (S:Set; U:S->Set) (SbE S (SBot S) U).
121       Intros.
122       MApply 'sbe_i.
123       MCut 'Empty.
124       Intros.
125       MApply '(sbot_eps_e S a).
126       MElim 'H0 'efq.
127       Qed.
128
129 (** Singleton, sub or equal introduction: $ a \e U \limp \subset{a} \sub U $. *)
130       Theorem sing_sbe_i: (S:Set; a:S; U:S->Set) (Eps S a U) -> (SbE S (Sing S a) U).
131       Intros.
132       MApply 'sbe_i.
133       MCut '(Id S a a0).
134       MApply 'sing_eps_e.
135       MApply '(id_repl S a0 a).
136       Qed.
137
138 (** Singleton, sub or equal elimination: $ \subset{a} \sub U \limp a \e U $. *)
139       Theorem sing_sbe_e: (S:Set; a:S; U:S->Set) (SbE S (Sing S a) U) -> (Eps S a U).
140       Intros.
141       MApply '(sbe_e S (Sing S a)).
142       MApply 'sing_eps_i.
143       Qed.
144
145 (** Singleton, sub or equal criterion: $ a \e U \liff \subset{a} \sub U $. *)
146       Theorem sing_sbe: (S:Set; a:S; U:S->Set) (LIff (Eps S a U) (SbE S (Sing S a) U)).
147       Intros.
148       MApply 'liff_i.
149       MApply 'sing_sbe_i.
150       MApply 'sing_sbe_e.
151       Qed.
152
153    End stop_sbot_sing_inclusion.
154    
155    Section subset_equality.
156
157 (** Set equal introduction: $ ((\lall a \in S)\ a \e U \limp a \e V) \limp ((\lall a \in S)\ a \e V \limp a \e U) \limp U = V $. *)
158       Theorem seq_i: (S:Set; U,V:S->Set) ((a:S) (Eps S a U) -> (Eps S a V)) -> ((a:S) (Eps S a V) -> (Eps S a U)) -> (SEq S U V).
159       Unfold SEq.
160       Intros.
161       MApply 'liff_i.
162       MApply '(H a).
163       MApply '(H0 a).
164       Qed.
165
166 (** Set equal elimination 1: $ a \e U \limp U = V \limp a \e V $. *)
167       Theorem seq_e1: (S:Set; U,V:S->Set; a:S) (Eps S a U) -> (SEq S U V) -> (Eps S a V).
168       Unfold SEq.
169       Intros.
170       MApply '(liff_e1 (Eps S a U)).
171       MApply '(H0 a).
172       Qed.
173
174 (** Set equal elimination 2: $ a \e V \limp U = V \limp a \e U $. *)
175       Theorem seq_e2: (S:Set; V,U:(S -> Set); a:S) (Eps S a V) -> (SEq S U V) -> (Eps S a U).
176       Unfold SEq.
177       Intros.
178       MApply '(liff_e2 (Eps S a V)).
179       MApply '(H0 a).
180       Qed.
181
182 (*
183 Theorem seq_i2: (S:Set; U,V:(S -> Set)) ((a:S) (U a) -> (V a)) -> ((a:S) (V a) -> (U a)) -> (SEq S U V).
184 Intros.
185 MApply 'seq_i.
186 MApply 'eps_c1_l.
187 MApply '(H a).
188 MApply 'eps_c1_r.
189 MApply 'eps_c1_l.
190 MApply '(H0 a).
191 MApply 'eps_c1_r.
192 Qed.
193 *)
194 (** Set equal, sub or equal introduction: $ U \sub V \limp V \sub U \limp U = V $. *)
195       Theorem seq_sbe_i: (S:Set; U,V:S->Set) (SbE S U V) -> (SbE S V U) -> (SEq S U V).
196       Intros.
197       MApply 'seq_i.
198       MApply '(sbe_e S U).
199       MApply '(sbe_e S V).
200       Qed.
201
202 (** Set equal, sub or equal elimination: $ U = V \limp U \sub V \land V \sub U $. *)
203       Theorem seq_sbe_e: (S:Set; U,V:S->Set) (SEq S U V) -> (LAnd (SbE S U V) (SbE S V U)).
204       Intros.
205       MApply 'land_i.
206       MApply 'sbe_i.
207       MApply '(seq_e1 S U).
208       MApply 'sbe_i.
209       MApply '(seq_e2 S V).
210       Qed.
211
212 (** Set equal, sub or equal criterion: $ U = V \liff U \sub V \land V \sub U $. *)
213       Theorem seq_sbe: (S:Set; U,V:S->Set) (LIff (SEq S U V) (LAnd (SbE S U V) (SbE S V U))).
214       Intros.
215       MApply 'liff_i.
216       MApply 'seq_sbe_e.
217       MApply 'seq_sbe_i.
218       MApply '(land_e2 (SbE S V U)).
219       MApply '(land_e1 (SbE S U V)).
220       Qed.
221
222 (** Subset equal reflexivity: $ U = U $. *) 
223       Theorem seq_r: (S:Set; U:S->Set) (SEq S U U).
224       Intros.
225       MApply 'seq_i.
226       Qed.
227
228 (** Subset equal transitivity: $ U = W \limp W = V \limp U = V $. *) 
229       Theorem seq_t: (S:Set; W,U,V:S->Set) (SEq S U W) -> (SEq S W V) -> (SEq S U V).
230       Intros.
231       MApply 'seq_i.
232       MApply '(seq_e1 S W).
233       MApply '(seq_e1 S U).
234       MApply '(seq_e2 S W).
235       MApply '(seq_e2 S V).
236       Qed.
237
238 (** Subset equal symmetry: $ U = V \limp V = U $. *) 
239       Theorem seq_s: (S:Set; U,V:S-> Set) (SEq S U V) -> (SEq S V U).
240       Intros.
241       MApply 'seq_i.
242       MApply '(seq_e2 S V).
243       MApply '(seq_e1 S U).
244       Qed.
245
246    End subset_equality.
247
248 End Subset_Relations_Results.
249