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