helm/coq-contribs/SUBSETS/tbs_op.v

   1 (** This module (Toolbox - subsets: operations) defines:
   2     - subset binary intersection:     [SAnd] (subset and)
   3     - subset binary union:            [SOr]  (subset or)
   4     - subset implication:             [SImp] (subset implies)
   5     - subset opposite:                [SNot] (subset not)
   6     - subset infinitary intersection: [SAll] (subset all)
   7     - subset infinitary union:        [SEx]  (subset exists)
   8
   9     and provides:
  10     - introduction and elimination rules for the defined constants
  11     - standard properties (idempotency, commutativity, associativity, compatibility, distributivity) for the defined constants
  12     - Cantor's diagonalization theorem: [cantor_diag]
  13
  14 % \hrule %
  15
  16  We require Toolbox relations and the underlying theory.
  17
  18  *)
  19 Require Export tbs_rel.
  20
  21 Section Subset_Operations_Definitions.
  22
  23    Section finitary_subset_operations.
  24
  25 (** Subset and: [(SAnd S U V)] corresponds to $ U \sand_S V $. *)
  26       Definition SAnd: (S:Set) (S -> Set) -> (S -> Set) -> (S -> Set).
  27       Intros S U V a.
  28       Exact (LAnd (U a) (V a)).
  29       Defined.
  30
  31 (** Subset or: [(SOr S U V)] corresponds to $ U \sor_S V $. *)
  32       Definition SOr: (S:Set) (S -> Set) -> (S -> Set) -> (S -> Set).
  33       Intros S U V a.
  34       Exact (LOr (U a) (V a)).
  35       Defined.
  36
  37 (** Subset implies: [(SImp S U V)] corresponds to $ U \simp_S V $. *)
  38       Definition SImp: (S:Set) (S -> Set) -> (S -> Set) -> (S -> Set).
  39       Intros S U V a.
  40       Exact (U a)->(V a).
  41       Defined.
  42
  43 (** Subset not: [(SNot S U)] corresponds to $ \snot_S U $. *)
  44       Definition SNot: (S:Set) (S -> Set) -> (S -> Set).
  45       Intros S U a.
  46       Exact (LNot (U a)).
  47       Defined.
  48
  49    End finitary_subset_operations.
  50
  51    Section infinitary_subset_operations.
  52
  53 (** Subset all: [(SAll I S F)] corresponds to $ \bigsand_S\subset{F(i) \st i \in I} $. *)
  54       Definition SAll: (I,S:Set) (I -> S -> Set) -> (S -> Set).
  55       Intros I S F a.
  56       Exact (i:I)(F i a).
  57       Defined.
  58
  59 (** Subset exists: [(SEx I S F)] corresponds to $ \bigsor_S\subset{F(i) \st i \in I} $. *)
  60       Definition SEx: (I,S:Set) (I -> S -> Set) -> (S -> Set).
  61       Intros I S F a.
  62       Exact (LEx I [i](F i a)).
  63       Defined.
  64
  65    End infinitary_subset_operations.
  66
  67 End Subset_Operations_Definitions.
  68
  69 Section Subset_Operations_Results.
  70
  71    Section subset_binary_intersection.
  72
  73 (** Subset and, epsilon introduction: $ a \e U \limp a \e V \limp a \e U \sand V $. *)
  74       Theorem sand_eps_i: (S:Set; U,V:S->Set; a:S) (Eps S a U) -> (Eps S a V) -> (Eps S a (SAnd S U V)).
  75       Intros.
  76       MApply 'eps_i.
  77       Unfold SAnd.
  78       MApply 'land_i.
  79       MApply 'eps_e.
  80       MApply 'eps_e.
  81       Qed.
  82
  83 (** Subset and, epsilon elimination 2: $ a \e U \sand V \limp a \e U $. *)
  84       Theorem sand_eps_e2: (S:Set; V,U:S->Set; a:S) (Eps S a (SAnd S U V)) -> (Eps S a U).
  85       Intros.
  86       MApply 'eps_i.
  87       MApply '(land_e2 (V a)).
  88       Fold (SAnd S U V a).
  89       MApply 'eps_e.
  90       Qed.
  91
  92 (** Subset and, epsilon elimination 1: $ a \e U \sand V \limp a \e V $. *)
  93       Theorem sand_eps_e1: (S:Set; U,V:S->Set; a:S) (Eps S a (SAnd S U V)) -> (Eps S a V).
  94       Intros.
  95       MApply 'eps_i.
  96       MApply '(land_e1 (U a)).
  97       Fold (SAnd S U V a).
  98       MApply 'eps_e.
  99       Qed.
 100
 101 (** Subset and, epsilon criterion: $ a \e U \land a \e V \liff a \e U \sand V $ *)
 102       Theorem sand_eps: (S:Set; U,V:S->Set; a:S) (LIff (LAnd (Eps S a U) (Eps S a V)) (Eps S a (SAnd S U V))).
 103       Intros.
 104       MApply 'liff_i.
 105       MApply 'sand_eps_i.
 106       MApply '(land_e2 (Eps S a V)).
 107       MApply '(land_e1 (Eps S a U)).
 108       MApply 'land_i.
 109       MApply '(sand_eps_e2 S V).
 110       MApply '(sand_eps_e1 S U).
 111       Qed.
 112
 113 (** Subset and, sub or equal elimination 2: $ U \sand V \sub U $. *)
 114       Theorem sand_sbe_e2: (S:Set; U,V:S->Set) (SbE S (SAnd S U V) U).
 115       Intros.
 116       MApply 'sbe_i.
 117       MApply '(sand_eps_e2 S V).
 118       Qed.
 119
 120 (** Subset and, sub or equal elimination 1: $ U \sand V \sub V $. *)
 121       Theorem sand_sbe_e1: (S:Set; U,V:S->Set) (SbE S (SAnd S U V) V).
 122       Intros.
 123       MApply 'sbe_i.
 124       MApply '(sand_eps_e1 S U).
 125       Qed.
 126
 127 (** Subset and, sub or equal introduction: $ W \sub U \limp W \sub V \limp W \sub U \sand V $. *)
 128       Theorem sand_sbe_i: (S:Set; W,U,V:S->Set) (SbE S W U) -> (SbE S W V) -> (SbE S W (SAnd S U V)).
 129       Intros.
 130       MApply 'sbe_i.
 131       MApply 'sand_eps_i.
 132       MApply '(sbe_e S W).
 133       MApply '(sbe_e S W).
 134       Qed.
 135
 136 (** Subset and, sub or equal compatibility 2: $ U \sub V \limp U \sand W \sub V \sand W $. *)
 137       Theorem sand_sbe_c2: (S:Set; U,V,W:S->Set) (SbE S U V) -> (SbE S (SAnd S U W) (SAnd S V W)).
 138       Intros.
 139       MApply 'sand_sbe_i.
 140       MApply '(sbe_t S U).
 141       MApply 'sand_sbe_e2.
 142       MApply 'sand_sbe_e1.
 143       Qed.
 144
 145 (** Subset and, sub or equal subset top: $ U \sub \stop \sand U $. *)
 146       Theorem sand_sbe_stop: (S:Set; U:S->Set) (SbE S U (SAnd S (STop S) U)).
 147       Intros.
 148       MApply 'sand_sbe_i.
 149       MApply 'stop_sbe_i.
 150       MApply 'sbe_r.
 151       Qed.
 152
 153 (** Subset and, sub or equal idempotency: $ U \sub U \sand U $. *)
 154       Theorem sand_sbe_r: (S:Set; U:S->Set) (SbE S U (SAnd S U U)).
 155       Intros.
 156       MApply 'sand_sbe_i.
 157       MApply 'sbe_r.
 158       MApply 'sbe_r.
 159       Qed.
 160
 161 (** Subset and, idempotency $ U \sand U = U $. *)
 162       Theorem sand_r: (S:Set; U:S->Set) (SEq S (SAnd S U U) U).
 163       Intros.
 164       MApply 'seq_sbe_i.
 165       MApply 'sand_sbe_e2.
 166       MApply 'sand_sbe_r.
 167       Qed.
 168
 169 (** Subset and, sub or equal commutativity: $ V \sand U \sub U \sand V $. *)
 170       Theorem sand_sbe_s: (S:Set; U,V:S->Set) (SbE S (SAnd S V U) (SAnd S U V)).
 171       Intros.
 172       MApply 'sand_sbe_i.
 173       MApply 'sand_sbe_e1.
 174       MApply 'sand_sbe_e2.
 175       Qed.
 176
 177 (** Subset and, commutativity: $ V \sand U = U \sand V $. *)
 178       Theorem sand_s: (S:Set; U,V:S->Set) (SEq S (SAnd S V U) (SAnd S U V)).
 179       Intros.
 180       MApply 'seq_sbe_i.
 181       MApply 'sand_sbe_s.
 182       MApply 'sand_sbe_s.
 183       Qed.
 184
 185 (** Subset and, sub or equal associativity 1: $ U \sand (V \sand W) \sub (U \sand V) \sand W $. *)
 186       Theorem sand_sbe_a1: (S:Set; U,V,W:S->Set) (SbE S (SAnd S U (SAnd S V W)) (SAnd S (SAnd S U V) W)).
 187       Intros.
 188       MApply 'sand_sbe_i.
 189       MApply 'sand_sbe_i.
 190       MApply 'sand_sbe_e2.
 191       MApply '(sbe_t S (SAnd S V W)).
 192       MApply 'sand_sbe_e1.
 193       MApply 'sand_sbe_e2.
 194       MApply '(sbe_t S (SAnd S V W)).
 195       MApply 'sand_sbe_e1.
 196       MApply 'sand_sbe_e1.
 197       Qed.
 198
 199 (** Subset and, sub or equal associativity 2: $ (U \sand V) \sand W \sub U \sand (V \sand W) $. *)
 200       Theorem sand_sbe_a2: (S:Set; U,V,W:S->Set) (SbE S (SAnd S (SAnd S U V) W) (SAnd S U (SAnd S V W))).
 201       Intros.
 202       MApply '(sbe_t S (SAnd S W (SAnd S U V))).
 203       MApply 'sand_sbe_s.
 204       MApply '(sbe_t S (SAnd S (SAnd S V W) U)).
 205       MApply '(sbe_t S (SAnd S (SAnd S W U) V)).
 206       MApply 'sand_sbe_a1.
 207       MApply '(sbe_t S (SAnd S V (SAnd S W U))).
 208       MApply 'sand_sbe_s.
 209       MApply 'sand_sbe_a1.
 210       MApply 'sand_sbe_s.
 211       Qed.
 212
 213 (** Subset and, associativity: $ U \sand (V \sand W) = (U \sand V) \sand W $. *)
 214       Theorem sand_a: (S:Set; U,V,W:S->Set) (SEq S (SAnd S U (SAnd S V W)) (SAnd S (SAnd S U V) W)).
 215       Intros.
 216       MApply 'seq_sbe_i.
 217       MApply 'sand_sbe_a1.
 218       MApply 'sand_sbe_a2.
 219       Qed.
 220
 221 (** Subset and, sub or equal compatibility 1: $ U \sub V \limp W \sand U \sub W \sand V $. *)
 222       Theorem sand_sbe_c1: (S:Set; U,V,W:S->Set) (SbE S U V) -> (SbE S (SAnd S W U) (SAnd S W V)).
 223       Intros.
 224       MApply '(sbe_t S (SAnd S U W)).
 225       MApply 'sand_sbe_s.
 226       MApply '(sbe_t S (SAnd S V W)).
 227       MApply 'sand_sbe_c2.
 228       MApply 'sand_sbe_s.
 229       Qed.
 230
 231 (** Subset and, sub or equal compatibility: $ U \sub V \limp W \sub X \limp U \sand W \sub V \sand X $. *)
 232       Theorem sand_sbe_c: (S:Set; U,V,W,X:S->Set) (SbE S U V) -> (SbE S W X) -> (SbE S (SAnd S U W) (SAnd S V X)).
 233       Intros.
 234       MApply '(sbe_t S (SAnd S V W)).
 235       MApply 'sand_sbe_c2.
 236       MApply 'sand_sbe_c1.
 237       Qed.
 238
 239    End subset_binary_intersection.
 240
 241    Section subset_binary_union.
 242
 243 (** Subset or, epsilon introduction 2: $ a \e U \limp a \e U \sor V $. *)
 244       Theorem sor_eps_i2: (S:Set; U,V:S->Set; a:S) (Eps S a U) -> (Eps S a (SOr S U V)).
 245       Intros.
 246       MApply 'eps_i.
 247       Unfold SOr.
 248       MApply 'in_l.
 249       MApply 'eps_e.
 250       Qed.
 251
 252 (** Subset or, epsilon introduction 1: $ a \e V \limp a \e U \sor V $. *)
 253       Theorem sor_eps_i1: (S:Set; U,V:S->Set; a:S) (Eps S a V) -> (Eps S a (SOr S U V)).
 254       Intros.
 255       MApply 'eps_i.
 256       Unfold SOr.
 257       MApply 'in_r.
 258       MApply 'eps_e.
 259       Qed.
 260
 261 (** Subset or, epsilon elimination: $ (a \e U \limp T) \limp (a \e V \limp T) \limp a \e U \sor V \limp T $. *)
 262       Theorem sor_eps_e: (S:Set; a:S; U,V:S->Set; T:Set) ((Eps S a U) -> T) -> ((Eps S a V) -> T) -> (Eps S a (SOr S U V)) -> T.
 263       Intros.
 264       MCut '(SOr S U V a).
 265       MApply 'eps_e.
 266       MApply '(lor_e (U a) (V a)).
 267       MApply 'H.
 268       MApply 'eps_i.
 269       MApply 'H0.
 270       MApply 'eps_i.
 271       Qed.
 272
 273 (** Subset or, epsilon criterion: $ a \e U \lor a \e V \liff a \e U \sor V $. *)
 274       Theorem sor_eps: (S:Set; U,V:S->Set; a:S) (LIff (LOr (Eps S a U) (Eps S a V)) (Eps S a (SOr S U V))).
 275       Intros.
 276       MApply 'liff_i.
 277       MApply '(lor_e (Eps S a U) (Eps S a V)).
 278       MApply 'sor_eps_i2.
 279       MApply 'sor_eps_i1.
 280       MApply '(sor_eps_e S a U V).
 281       MApply 'in_l.
 282       MApply 'in_r.
 283       Qed.
 284
 285 (** Subset or, sub or equal introduction 2: $ U \sub U \sor V $. *)
 286       Theorem sor_sbe_i2: (S:Set; U,V:S->Set) (SbE S U (SOr S U V)).
 287       Intros.
 288       MApply 'sbe_i.
 289       MApply 'sor_eps_i2.
 290       Qed.
 291
 292 (** Subset or, sub or equal introduction 1: $ V \sub U \sor V $. *)
 293       Theorem sor_sbe_i1: (S:Set; U,V:S->Set) (SbE S V (SOr S U V)).
 294       Intros.
 295       MApply 'sbe_i.
 296       MApply 'sor_eps_i1.
 297       Qed.
 298
 299 (** Subset or, sub or equal elimination: $ U \sub W \limp V \sub W \limp U \sor V \sub W $. *)
 300       Theorem sor_sbe_e: (S:Set; W,U,V:S->Set) (SbE S U W) -> (SbE S V W) -> (SbE S (SOr S U V) W).
 301       Intros.
 302       MApply 'sbe_i.
 303       MApply '(sor_eps_e S a U V).
 304       MApply '(sbe_e S U).
 305       MApply '(sbe_e S V).
 306       Qed.
 307
 308 (** Subset or, sub or equal compatibility 2: $ U \sub V \limp U \sor W \sub V \sor W $. *)
 309       Theorem sor_sbe_c2: (S:Set; U,V,W:S->Set) (SbE S U V) -> (SbE S (SOr S U W) (SOr S V W)).
 310       Intros.
 311       MApply 'sor_sbe_e.
 312       MApply '(sbe_t S V).
 313       MApply 'sor_sbe_i2.
 314       MApply 'sor_sbe_i1.
 315       Qed.
 316
 317 (** Subset or, sub or equal idempotency: $ U \sor U \sub U $. *)
 318       Theorem sor_sbe_r: (S:Set; U:S->Set) (SbE S (SOr S U U) U).
 319       Intros.
 320       MApply 'sor_sbe_e.
 321       MApply 'sbe_r.
 322       MApply 'sbe_r.
 323       Qed.
 324
 325 (** Subset or, idempotency: $ U \sor U = U $. *)
 326       Theorem sor_r: (S:Set; U:S->Set) (SEq S (SOr S U U) U).
 327       Intros.
 328       MApply 'seq_sbe_i.
 329       MApply 'sor_sbe_r.
 330       MApply 'sor_sbe_i2.
 331       Qed.
 332
 333 (** Subset or, sub or equal commutativity: $ V \sor U \sub U \sor V $. *)
 334       Theorem sor_sbe_s: (S:Set; U,V:S->Set) (SbE S (SOr S V U) (SOr S U V)).
 335       Intros.
 336       MApply 'sor_sbe_e.
 337       MApply 'sor_sbe_i1.
 338       MApply 'sor_sbe_i2.
 339       Qed.
 340
 341 (** Subset or, commutativity: $ V \sor U = U \sor V $. *)
 342       Theorem sor_s: (S:Set; U,V:S->Set) (SEq S (SOr S V U) (SOr S U V)).
 343       Intros.
 344       MApply 'seq_sbe_i.
 345       MApply 'sor_sbe_s.
 346       MApply 'sor_sbe_s.
 347       Qed.
 348
 349 (** Subset or, sub or equal associativity 1: $ U \sor (V \sor W) \sub (U \sor V) \sor W $. *)
 350       Theorem sor_sbe_a1: (S:Set; U,V,W:S->Set) (SbE S (SOr S U (SOr S V W)) (SOr S (SOr S U V) W)).
 351       Intros.
 352       MApply 'sor_sbe_e.
 353       MApply '(sbe_t S (SOr S U V)).
 354       MApply 'sor_sbe_i2.
 355       MApply 'sor_sbe_i2.
 356       MApply 'sor_sbe_e.
 357       MApply '(sbe_t S (SOr S U V)).
 358       MApply 'sor_sbe_i1.
 359       MApply 'sor_sbe_i2.
 360       MApply 'sor_sbe_i1.
 361       Qed.
 362
 363 (** Subset or, sub or equal associativity 2: $ (U \sor V) \sor W \sub U \sor (V \sor W) $. *)
 364       Theorem sor_sbe_a2: (S:Set; U,V,W:S->Set) (SbE S (SOr S (SOr S U V) W) (SOr S U (SOr S V W))).
 365       Intros.
 366       MApply '(sbe_t S (SOr S W (SOr S U V))).
 367       MApply 'sor_sbe_s.
 368       MApply '(sbe_t S (SOr S (SOr S V W) U)).
 369       MApply '(sbe_t S (SOr S (SOr S W U) V)).
 370       MApply 'sor_sbe_a1.
 371       MApply '(sbe_t S (SOr S V (SOr S W U))).
 372       MApply 'sor_sbe_s.
 373       MApply 'sor_sbe_a1.
 374       MApply 'sor_sbe_s.
 375       Qed.
 376
 377 (** Subset or, associativity: $ U \sor (V \sor W) = (U \sor V) \sor W $. *)
 378       Theorem sor_a: (S:Set; U,V,W:S->Set) (SEq S (SOr S U (SOr S V W)) (SOr S (SOr S U V) W)).
 379       Intros.
 380       MApply 'seq_sbe_i.
 381       MApply 'sor_sbe_a1.
 382       MApply 'sor_sbe_a2.
 383       Qed.
 384
 385 (** Subset or, sub or equal compatibility 1: $ U \sub V \limp W \sor U \sub W \sor V $. *)
 386       Theorem sor_sbe_c1: (S:Set; U,V,W:S->Set) (SbE S U V) -> (SbE S (SOr S W U) (SOr S W V)).
 387       Intros.
 388       MApply '(sbe_t S (SOr S U W)).
 389       MApply 'sor_sbe_s.
 390       MApply '(sbe_t S (SOr S V W)).
 391       MApply 'sor_sbe_c2.
 392       MApply 'sor_sbe_s.
 393       Qed.
 394
 395 (** Subset or, sub or equal compatibility: $ U \sub V \limp W \sub X \limp U \sor W \sub V \sor X $. *)
 396       Theorem sor_sbe_c: (S:Set; U,V,W,X:S->Set) (SbE S U V) -> (SbE S W X) -> (SbE S (SOr S U W) (SOr S V X)).
 397       Intros.
 398       MApply '(sbe_t S (SOr S V W)).
 399       MApply 'sor_sbe_c2.
 400       MApply 'sor_sbe_c1.
 401       Qed.
 402
 403    End subset_binary_union.
 404
 405    Section subset_implication.
 406
 407 (** Subset implies, epsilon introduction: $ (a \e U \limp a \e V) \limp a \e U \simp V $. *)
 408       Theorem simp_eps_i: (S:Set; U,V:S->Set; a:S) ((Eps S a U) -> (Eps S a V)) -> (Eps S a (SImp S U V)).
 409       Intros.
 410       MApply 'eps_i.
 411       Unfold SImp.
 412       Intros.
 413       MApply 'eps_e.
 414       MApply 'H.
 415       MApply 'eps_i.
 416       Qed.
 417
 418 (** Subset implies, epsilon elimination: $ a \e U \simp V \limp a \e U \limp a \e V $. *)
 419       Theorem simp_eps_e: (S:Set; U,V:S->Set; a:S) (Eps S a (SImp S U V)) -> (Eps S a U) -> (Eps S a V).
 420       Intros.
 421       MApply 'eps_i.
 422       Apply (mcut (U a)).
 423       MApply 'eps_e.
 424       MApply '(eps_e S a).
 425       Qed.
 426
 427 (** Subset implies, epsilon criterion: $ a \e U \simp V \liff (a \e U \limp a \e V) $. *)
 428       Theorem simp_eps: (S:Set; U,V:S->Set; a:S) (LIff (Eps S a (SImp S U V)) (Eps S a U) -> (Eps S a V)).
 429       Intros.
 430       MApply 'liff_i.
 431       MApply '(simp_eps_e S U).
 432       MApply 'simp_eps_i.
 433       MApply 'H.
 434       Qed.
 435
 436 (** Subset implies, sub or equal elimination: $ W \sub U \simp V \limp W \sand U \sub V $. *)
 437       Theorem simp_sbe_e: (S:Set; U,V,W:S->Set) (SbE S W (SImp S U V)) -> (SbE S (SAnd S W U) V).
 438       Intros.
 439       MApply 'sbe_i.
 440       MApply '(simp_eps_e S U).
 441       MApply '(sbe_e S W).
 442       MApply '(sand_eps_e2 S U).
 443       MApply '(sand_eps_e1 S W).
 444       Qed.
 445
 446 (** Subset implies, sub or equal introduction: $ W \sand U \sub V \limp W \sub U \simp V $. *)
 447       Theorem simp_sbe_i: (S:Set; U,V,W:S->Set) (SbE S (SAnd S W U) V) -> (SbE S W (SImp S U V)).
 448       Intros.
 449       MApply 'sbe_i.
 450       MApply 'simp_eps_i.
 451       MApply '(sbe_e S (SAnd S W U)).
 452       MApply 'sand_eps_i.
 453       Qed.
 454
 455 (** Subset implies, sub or equal compatibility 2: $ V \sub U \limp U \simp W \sub V \simp W $. *)
 456       Theorem simp_sbe_c2: (S:Set; U,V,W:S->Set) (SbE S V U) -> (SbE S (SImp S U W) (SImp S V W)).
 457       Intros.
 458       MApply 'simp_sbe_i.
 459       MApply '(sbe_t S (SAnd S (SImp S U W) U)).
 460       MApply 'sand_sbe_c1.
 461       MApply 'simp_sbe_e.
 462       MApply 'sbe_r.
 463       Qed.
 464
 465 (** Subset implies, sub or equal compatibility 2: $ U \sub V \limp W \simp U \sub W \simp V $. *)
 466       Theorem simp_sbe_c1: (S:Set; U,V,W:S->Set) (SbE S U V) -> (SbE S (SImp S W U) (SImp S W V)).
 467       Intros.
 468       MApply 'simp_sbe_i.
 469       MApply '(sbe_t S U).
 470       MApply 'simp_sbe_e.
 471       MApply 'sbe_r.
 472       Qed.
 473
 474 (** Subset implies, subset top elimination: $ \stop \sub U \simp V \limp U \sub V $. *)
 475       Theorem simp_stop_e: (S:Set; U,V:S->Set) (SbE S (STop S) (SImp S U V)) -> (SbE S U V).
 476       Intros.
 477       MApply '(sbe_t S (SAnd S (STop S) U)).
 478       MApply 'sand_sbe_stop.
 479       MApply 'simp_sbe_e.
 480       Qed.
 481
 482 (** Subset implies, subset top introduction: $ U \sub V \limp \stop \sub U \simp V $. *)
 483       Theorem simp_stop_i: (S:Set; U,V:S->Set) (SbE S U V) -> (SbE S (STop S) (SImp S U V)).
 484       Intros.
 485       MApply 'simp_sbe_i.
 486       MApply '(sbe_t S U).
 487       MApply 'sand_sbe_e1.
 488       Qed.
 489
 490 (** Subset implies, subset top criterion: $ \stop \sub U \simp V \liff U \sub V $. *)
 491       Theorem simp_stop: (S:Set; U,V:S->Set) (LIff (SbE S (STop S) (SImp S U V)) (SbE S U V)).
 492       Intros.
 493       MApply 'liff_i.
 494       MApply 'simp_stop_e.
 495       MApply 'simp_stop_i.
 496       Qed.
 497
 498    End subset_implication.
 499
 500    Section subset_negation.
 501
 502 (** Subset not, epsilon introduction: $ \lnot (a \e U) \limp a \e \snot U $. *)
 503       Theorem snot_eps_i: (S:Set; U:S->Set; a:S) (LNot (Eps S a U)) -> (Eps S a (SNot S U)).
 504       Intros.
 505       MApply 'eps_i.
 506       Unfold SNot.
 507       MApply 'lnot_i.
 508       MApply '(lnot_e (Eps S a U)).
 509       MApply 'eps_i.
 510       Qed.
 511
 512 (** Subset not, epsilon elimination: $ a \e \snot U \limp \lnot (a \e U) $. *)
 513       Theorem snot_eps_e: (S:Set; U:S->Set; a:S) (Eps S a (SNot S U)) -> (LNot (Eps S a U)).
 514       Unfold SNot.
 515       Intros.
 516       MApply 'lnot_i.
 517       MApply '(lnot_e (U a)).
 518       MApply '(eps_e S a [a0:S](LNot (U a0))).
 519       MApply 'eps_e.
 520       Qed.
 521
 522 (** Subset not, epsilon criterion: $ \lnot (a \e U) \liff a \e \snot U $. *)
 523       Theorem snot_eps: (S:Set; U:S->Set; a:S) (LIff (LNot (Eps S a U)) (Eps S a (SNot S U))).
 524       Intros.
 525       MApply 'liff_i.
 526       MApply 'snot_eps_i.
 527       MApply 'snot_eps_e.
 528       Qed.
 529
 530 (** Subset not, subset implication compatibility: $ \snot U = U \simp \sbot $. *)
 531       Theorem snot_simp_c: (S:Set; U:S->Set) (SEq S (SNot S U) (SImp S U (SBot S))).
 532       Intros.
 533       MApply 'seq_i.
 534       MApply 'simp_eps_i.
 535       MCut 'Empty.
 536       MApply '(lnot_e (Eps S a U)).
 537       MApply 'snot_eps_e.
 538       MElim 'H1 'efq.
 539       MApply 'snot_eps_i.
 540       MApply 'lnot_i.
 541       MApply '(sbot_eps_e S a).
 542       MApply '(simp_eps_e S U).
 543       Qed.
 544
 545    End subset_negation.
 546
 547    Section subset_infinitary_intersection.
 548
 549 (** Subset all, epsilon introduction: $ ((\lall i \in I)\ a \e F(i)) \limp a \e \bigsand\subset{F(i) \st i \in I} $. *)
 550       Theorem sall_eps_i: (I,S:Set; F:(I->S->Set); a:S) ((i:I) (Eps S a (F i))) -> (Eps S a (SAll I S F)).
 551       Intros.
 552       MApply 'eps_i.
 553       Unfold SAll.
 554       Intros.
 555       MApply 'eps_e.
 556       MApply '(H i).
 557       Qed.
 558
 559 (** Subset all, epsilon elimination: $ a \e \bigsand\subset{F(i) \st i \in I} \limp (\lall i \in I)\ a \e F(i) $. *)
 560       Theorem sall_eps_e: (I,S:Set; F:(I->S->Set); a:S) (Eps S a (SAll I S F)) -> (i:I) (Eps S a (F i)).
 561       Intros.
 562       MApply 'eps_i.
 563       Apply (mcut (i:I)(F i a)).
 564       MApply '(eps_e S a).
 565       Intros.
 566       MApply '(H0 i).
 567       Qed.
 568
 569 (** Subset all, epsilon criterion: $ a \e \bigsand\subset{F(i) \st i \in I} \liff (\lall i \in I)\ a \e F(i) $. *)
 570       Theorem sall_eps: (I,S:Set; F:(I->S->Set); a:S) (LIff (Eps S a (SAll I S F)) (i:I) (Eps S a (F i))).
 571       Intros.
 572       MApply 'liff_i.
 573       MApply '(sall_eps_e I).
 574       MApply 'sall_eps_i.
 575       MApply '(H i).
 576       Qed.
 577
 578 (** Subset all, sub or equal elimination: $ (\lall i \in I)\ \bigsand\subset{F(i) \st i \in I} \sub F(i) $. *)
 579       Theorem sall_sbe_e: (I,S:Set; F:(I->S->Set); i:I) (SbE S (SAll I S F) (F i)).
 580       Intros.
 581       MApply 'sbe_i.
 582       MApply '(sall_eps_e I).
 583       Qed.
 584
 585 (** Subset all, sub or equal introduction: $ ((\lall i \in I)\ W \sub F(i)) \limp W \sub \bigsand\subset{F(i) \st i \in I} $. *)
 586       Theorem sall_sbe_i: (I,S:Set; F:(I->S->Set); W:S->Set) ((i:I)(SbE S W (F i))) -> (SbE S W (SAll I S F)).
 587       Intros.
 588       MApply 'sbe_i.
 589       MApply 'sall_eps_i.
 590       MApply '(sbe_e S W).
 591       MApply 'H.
 592       Qed.
 593
 594    End subset_infinitary_intersection.
 595
 596    Section subset_infinitary_union.
 597
 598 (** Subset exists, epsilon introduction: $ ((\lex i \in I)\ a \e F(i)) \limp a \e \bigsor\subset{F(i) \st i \in I} $. *)
 599       Theorem sex_eps_i: (I,S:Set; F:(I->S->Set); a:S) (LEx I [i](Eps S a (F i))) -> (Eps S a (SEx I S F)).
 600       Intros.
 601       MApply 'eps_i.
 602       Unfold SEx.
 603       MElim 'H 'lex_e.
 604       MApply '(lex_i I a0).
 605       MApply 'eps_e.
 606       Qed.
 607
 608 (** Subset exists, epsilon elimination: $ a \e \bigsor\subset{F(i) \st i \in I} \limp (\lex i \in I)\ a \e F(i) $. *)
 609       Theorem sex_eps_e: (I,S:Set; F:(I->S->Set); a:S) (Eps S a (SEx I S F)) -> (LEx I [i](Eps S a (F i))).
 610       Intros.
 611       MCut '(SEx I S F a).
 612       MApply 'eps_e.
 613       MElim 'H0 'lex_e.
 614       MApply '(lex_i I a0).
 615       MApply 'eps_i.
 616       Qed.
 617
 618 (** Subset exists, epsilon elimination: $ a \e \bigsor\subset{F(i) \st i \in I} \liff (\lex i \in I)\ a \e F(i) $. *)
 619       Theorem sex_eps: (I,S:Set; F:(I->S->Set); a:S) (LIff (Eps S a (SEx I S F)) (LEx I [i](Eps S a (F i)))).
 620       Intros.
 621       MApply 'liff_i.
 622       MApply 'sex_eps_e.
 623       MApply 'sex_eps_i.
 624       Qed.
 625
 626 (** Subset exists, sub or equal introduction: $ (\lall i \in I)\ F(i) \sub \bigsor\subset{F(i) \st i \in I} $. *)
 627       Theorem sex_sbe_i: (I,S:Set; F:(I->S->Set); i:I) (SbE S (F i) (SEx I S F)).
 628       Intros.
 629       MApply 'sbe_i.
 630       MApply 'sex_eps_i.
 631       MApply '(lex_i I i).
 632       Qed.
 633
 634 (** Subset exists, sub or equal elimination: $ ((\lall i \in I)\ F(i) \sub W) \limp \bigsor\subset{F(i) \st i \in I} \sub W $. *)
 635       Theorem sex_sbe_e: (I,S:Set; F:(I->S->Set); W:S->Set) ((i:I)(SbE S (F i) W)) -> (SbE S (SEx I S F) W).
 636       Intros.
 637       MApply 'sbe_i.
 638       MCut '(LEx I [i:I](Eps S a (F i))).
 639       MApply 'sex_eps_e.
 640       MElim 'H1 'lex_e.
 641       MApply '(sbe_e S (F a0)).
 642       MApply 'H.
 643       Qed.
 644
 645    End subset_infinitary_union.
 646
 647    Section subset_frame.
 648
 649 (** Frame, subset and introduction: $ U \sub V \limp U \sand V = U $. *)
 650       Theorem frame_sand_i: (S:Set; U,V:S->Set) (SbE S U V) -> (SEq S (SAnd S U V) U).
 651       Intros.
 652       MApply 'seq_sbe_i.
 653       MApply 'sand_sbe_e2.
 654       MApply '(sbe_t S (SAnd S U U)).
 655       MApply 'sand_sbe_r.
 656       MApply 'sand_sbe_c1.
 657       Qed.
 658
 659 (** Frame, subset and elimination: $ U \sand V = U \limp U \sub V $. *)
 660       Theorem frame_sand_e: (S:Set; U,V:S->Set) (SEq S (SAnd S U V) U) -> (SbE S U V).
 661       Intros.
 662       MApply '(sbe_t S (SAnd S U V)).
 663       MApply '(land_e1 (SbE S (SAnd S U V) U)).
 664       MApply 'seq_sbe_e.
 665       MApply 'sand_sbe_e1.
 666       Qed.
 667
 668 (** Frame, subset or introduction: $ U \sub V \limp U \sor V = V $. *)
 669       Theorem frame_sor_i: (S:Set; U,V:S->Set) (SbE S U V) -> (SEq S (SOr S U V) V).
 670       Intros.
 671       MApply 'seq_sbe_i.
 672       MApply '(sbe_t S (SOr S V V)).
 673       MApply 'sor_sbe_c2.
 674       MApply 'sor_sbe_r.
 675       MApply 'sor_sbe_i1.
 676       Qed.
 677
 678 (** Frame, subset or elimination: $ U \sor V = V \limp U \sub V $. *)
 679       Theorem frame_sor_e: (S:Set; U,V:S->Set) (SEq S (SOr S U V) V) -> (SbE S U V).
 680       Intros.
 681       MApply '(sbe_t S (SOr S U V)).
 682       MApply 'sor_sbe_i2.
 683       MApply '(land_e2 (SbE S V (SOr S U V))).
 684       MApply 'seq_sbe_e.
 685       Qed.
 686
 687 (** Frame, subset exists introduction: $ \bigsor\subset{F(i) \st i \in I} \sand W \sub \bigsor\subset{F(i) \sand W \st i \in I} $. *)
 688       Theorem frame_sex_i: (I,S:Set; F:(I->S->Set); W:S->Set) (SbE S (SAnd S (SEx I S F) W) (SEx I S [i](SAnd S (F i) W))).
 689       Intros.
 690       MApply 'sbe_i.
 691       MApply 'sex_eps_i.
 692       MCut '(Eps S a (SEx I S F)).
 693       MApply '(sand_eps_e2 S W).
 694       MCut '(LEx I [i:I](Eps S a (F i))).
 695       MApply 'sex_eps_e.
 696       MElim 'H1 'lex_e.
 697       MApply '(lex_i I a0).
 698       MApply 'sand_eps_i.
 699       MApply '(sand_eps_e1 S (SEx I S F)).
 700       Qed.
 701
 702 (** Frame, subset exists elimination: $ \bigsor\subset{F(i) \sand W \st i \in I} \sub \bigsor\subset{F(i) \st i \in I} \sand W $. *)
 703       Theorem frame_sex_e: (I,S:Set; F:(I->S->Set); W:S->Set) (SbE S (SEx I S [i]
 704 (SAnd S (F i) W)) (SAnd S (SEx I S F) W)).
 705       Intros.
 706       MApply 'sand_sbe_i.
 707       MApply 'sex_sbe_e.
 708       MApply '(sbe_t S (F i)).
 709       MApply 'sand_sbe_e2.
 710       MApply 'sex_sbe_i.
 711       MApply 'sex_sbe_e.
 712       MApply 'sand_sbe_e1.
 713       Qed.
 714
 715 (** Frame, subset exists distributivity: $ \bigsor\subset{F(i) \st i \in I} \sand W = \bigsor\subset{F(i) \sand W \st i \in I} $. *)
 716       Theorem frame_sex_d: (I,S:Set; F:(I->S->Set); W:S->Set) (SEq S (SAnd S (SEx I S F) W) (SEx I S [i](SAnd S (F i) W))).
 717       Intros.
 718       MApply 'seq_sbe_i.
 719       MApply 'frame_sex_i.
 720       MApply 'frame_sex_e.
 721       Qed.
 722
 723 (** Frame, subset implies elimination: $ \bigsor\subset{F(i) \st i \in I} \simp W \sub \bigsand\subset{F(i) \simp W \st i \in I} $. *)
 724       Theorem frame_simp_e: (I,S:Set; F:(I->S->Set); W:S->Set) (SbE S (SImp S (SEx I S F) W) (SAll I S [i](SImp S (F i) W))).
 725       Intros.
 726       MApply 'sall_sbe_i.
 727       MApply 'simp_sbe_c2.
 728       MApply 'sex_sbe_i.
 729       Qed.
 730
 731 (** Frame, subset implies introduction: $ \bigsand\subset{F(i) \simp W \st i \in I} \sub \bigsor\subset{F(i) \st i \in I} \simp W $. *)
 732       Theorem frame_simp_i: (I,S:Set; F:(I->S->Set); W:S->Set) (SbE S (SAll I S [i](SImp S (F i) W)) (SImp S (SEx I S F) W)).
 733       Intros.
 734       MApply 'sbe_i.
 735       MApply 'simp_eps_i.
 736       MCut '(LEx I [i:I](Eps S a (F i))).
 737       MApply 'sex_eps_e.
 738       MElim 'H1 'lex_e.
 739       MApply '(simp_eps_e S (F a0)).
 740       MApply '(sall_eps_e I S [i:I](SImp S (F i) W)).
 741       Qed.
 742
 743 (** Frame, subset implies compatibility: $ \bigsor\subset{F(i) \st i \in I} \simp W = \bigsand\subset{F(i) \simp W \st i \in I} $. *)
 744       Theorem frame_simp_c: (I,S:Set; F:(I->S->Set); W:S->Set) (SEq S (SImp S (SEx I S F) W) (SAll I S [i](SImp S (F i) W))).
 745       Intros.
 746       MApply 'seq_sbe_i.
 747       MApply 'frame_simp_e.
 748       MApply 'frame_simp_i.
 749       Qed.
 750
 751    End subset_frame.
 752
 753    Section cantor_diagonalization.
 754
 755 (** [(D S F)] is Cantor's subset $ D_F $. *)
 756       Local D: (S:Set) (S -> S -> Set) -> (S -> Set).
 757       Intros S F.
 758       Exact (SNot S [a:S](F a a)).
 759       Defined.
 760
 761 (** Cantor's diagonalization: $ (\lall b \in S)\ \lnot (F(b) = D_F) $. *)
 762       Theorem cantor_diag: (S:Set; F:S->S->Set) (b:S) (LNot (SEq S (F b) (D S F))).
 763       Intros.
 764       MApply 'lnot_i.
 765       MCut '(LIff (Eps S b (F b)) (LNot (Eps S b (F b)))).
 766       MApply 'liff_i.
 767       MApply 'snot_eps_e.
 768       Change (Eps S b (D S F)).
 769       MApply '(seq_e1 S (F b)).
 770       MApply '(seq_e2 S (D S F)).
 771       Change (Eps S b (SNot S (F b))).
 772       MApply 'snot_eps_i.
 773       MApply '(lnot_liff_lbot (Eps S b (F b))).
 774       Qed.
 775
 776    End cantor_diagonalization.
 777
 778 End Subset_Operations_Results.