helm/coq-contribs/SUBSETS/tbs_base.v

   1 (** This module (Toolbox - subsets: basics) defines:
   2     - subset membership:               [Eps]  (epsilon)
   3     - empty subset:                    [SBot] (subset bottom)
   4     - full subset:                     [STop] (subset top)
   5     - singleton:                       [Sing] (singleton)
   6     - relative universal quantifier:   [RAll] (relative all)
   7     - relative existential quantifier: [REx]  (relative exists)
   8
   9     and provides:
  10     - introduction and elimination rules for the defined constants
  11     - epsilon conditions: [eps_1], [eps_2]
  12     - alternative form of epsilon with sigma: [eps2]
  13
  14 % \hrule %
  15
  16  We require the support for finite sets and finite domain functions ([xt_fin])
  17  that includes the basic type theory (the [st] package).
  18
  19  *)
  20 Require Export xt_fin.
  21
  22 Section Subset_Definitions.
  23
  24    Section subset_membership.
  25
  26 (** Epsilon: [(Eps S a U)] corresponds to $ a \e_S U $. *)
  27       Definition Eps: (S:Set) S -> (S -> Set) -> Set.
  28       Intros S a U.
  29       Exact (LAnd (U a) (Id S a a)).
  30       Defined.
  31
  32    End subset_membership.
  33
  34    Section subset_constants.
  35
  36 (** Subset bottom: [(SBot S)] corresponds to $ \sbot_S $. *)
  37       Definition SBot: (S:Set) S -> Set.
  38       Intros.
  39       Exact LBot.
  40       Defined.
  41
  42 (** Subset top: [(STop S)] corresponds to $ \stop_S $, %{\ie}% to $S$ as a subset of itself. *)
  43       Definition STop: (S:Set) S -> Set.
  44       Intros.
  45       Exact LTop.
  46       Defined.
  47
  48 (** Singleton: [(Sing S a)] corresponds to $ \subset{a} $. *)
  49       Definition Sing: (S:Set) S -> (S -> Set).
  50       Intros S a b.
  51       Exact (Id S a b).
  52       Defined.
  53
  54    End subset_constants.
  55
  56    Section relative_quantification.
  57
  58 (** Relative all: [(RAll S U P)] corresponds to $ (\lall x \e U) P(x) $. *)
  59       Definition RAll: (S:Set) (S -> Set) -> (S -> Set) -> Set.
  60       Intros S U P.
  61       Exact (a:S) (Eps S a U) -> (P a).
  62       Defined.
  63
  64 (** Relative exists: [(REx S U P)] corresponds to $ (\lex x \e U) P(x) $. *)
  65       Definition REx: (S:Set) (S -> Set) -> (S -> Set) -> Set.
  66       Intros S U P.
  67       Exact (LEx S [a](LAnd (Eps S a U) (P a))).
  68       Defined.
  69
  70    End relative_quantification.
  71
  72 End Subset_Definitions.
  73
  74 Section Subset_Results.
  75
  76    Section epsilon_conditions.
  77
  78 (** Epsilon elimination: $ a \e U \limp U(a) $. *)
  79       Theorem eps_e: (S:Set; a:S; U:S->Set) (Eps S a U) -> (U a).
  80       Unfold Eps.
  81       Intros.
  82       MApply '(land_e2 (Id S a a)).
  83       Qed.
  84
  85 (** Epsilon introduction: $ U(a) \limp a \e U $. *)
  86       Theorem eps_i: (S:Set; a:S; U:S->Set) (U a) -> (Eps S a U).
  87       Unfold Eps.
  88       Intros.
  89       MApply 'land_i.
  90       Qed.
  91
  92 (** Epsilon condition 1: $ a \e U \liff U(a) $. *)
  93       Theorem eps_1: (S:Set; U:(S -> Set)) (a:S)(LIff (Eps S a U) (U a)).
  94       Intros.
  95       MApply 'liff_i.
  96       MApply '(eps_e S a).
  97       MApply 'eps_i.
  98       Qed.
  99
 100 (** Epsilon condition 2: $ a \e_S U \limp a \in S $. *)
 101       Theorem eps_2: (S:Set; a:S; U:(S -> Set)) (Eps S a U) -> S.
 102       Intros.
 103       Exact a.
 104       Qed.
 105
 106 (** Epsilon in sigma form: $ a \e_S U \liff (\lex z \in (\Sigma x \in S) U) Id(S, p(z), a) $. *)
 107       Theorem eps2: (S:Set; a:S; U:(S -> Set)) (LIff (Eps S a U) (LEx (Sigma S U) [z](Id S (sp S U z) a))).
 108       Intros.
 109       MApply 'liff_i.
 110       MCut '(U a).
 111       MApply 'eps_e.
 112       MApply '(lex_i (Sigma S U) (pair S U a H0)).
 113       MApply 'eps_i.
 114       MElim 'H 'lex_e.
 115       MApply '(id_repl ? a (sp S U a0)).
 116       MElim 'a0 psplit.
 117       Qed.
 118
 119    End epsilon_conditions.
 120
 121    Section subset_top_bottom.
 122
 123 (** Subset top, epsilon introduction: $ a \e \stop $. *)
 124       Theorem stop_eps_i: (S:Set; a:S) (Eps S a (STop S)).
 125       Intros.
 126       MApply 'eps_i.
 127       Unfold STop.
 128       MApply 'LTop_red.
 129       Qed.
 130
 131 (** Subset bottom, epsilon elimination: $ a \e \sbot \limp \lbot $. *)
 132       Theorem sbot_eps_e: (S:Set; a:S) (Eps S a (SBot S)) -> LBot.
 133       Intros.
 134       MApply '(eps_e S a).
 135       Qed.
 136
 137    End subset_top_bottom.
 138
 139    Section singleton.
 140
 141 (** Singleton, epsilon introduction: $ Id(S, a, b) \limp b \e \subset{a} $. *)
 142       Theorem sing_eps_i: (S:Set; b,a:S) (Id S a b) -> (Eps S b (Sing S a)).
 143       Intros.
 144       MApply 'eps_i.
 145       Qed.
 146
 147 (** Singleton, epsilon elimination: $ b \e \subset{a} \limp Id(S, a, b) $. *)
 148       Theorem sing_eps_e: (S:Set; a,b:S) (Eps S b (Sing S a)) -> (Id S a b).
 149       Intros.
 150       MApply 'eps_e.
 151       Qed.
 152
 153    End singleton.
 154
 155    Section relative_universal.
 156
 157 (** Relative all introduction: $ ((\lall a \in S)\ a \e U \limp P(a)) \limp (\lall x \e U) P(x) $. *)
 158       Theorem rall_i: (S:Set; U:S->Set; P:S->Set) ((a:S) (Eps S a U) -> (P a)) -> (RAll S U P).
 159       Unfold RAll.
 160       Intros.
 161       MApply '(H a).
 162       Qed.
 163
 164 (** Relative all elimination: $ a \e U \limp (\lall x \e U) P(x) \limp P(a) $. *)
 165       Theorem rall_e: (S:Set; a:S; U:S->Set; P:S->Set) (Eps S a U) -> (RAll S U P) -> (P a).
 166       Intros.
 167       Unfold RAll in H0.
 168       MApply '(H0 a).
 169       Qed.
 170
 171    End relative_universal.
 172
 173    Section relative_existential.
 174
 175 (** Relative exists introduction: $ a \e U \limp P(a) \limp (\lex x \e U) P(x) $. *)
 176       Theorem rex_i: (S:Set; a:S; U:S->Set; P:S->Set) (Eps S a U) -> (P a) -> (REx S U P).
 177       Intros.
 178       Unfold REx.
 179       MApply '(lex_i S a).
 180       MApply 'land_i.
 181       Qed.
 182
 183 (** Relative exists elimination: $ ((\lall a \in S)\ a \e U \limp P(a) \limp T) \limp (\lex x \e U) P(x) \limp T $. *)
 184       Theorem rex_e: (S:Set; U:S->Set; P:S->Set; T:Set) ((a:S) (Eps S a U) -> (P a) -> T) -> (REx S U P) -> T.
 185       Intros.
 186       Unfold REx in H0.
 187       MElim 'H0 'lex_e.
 188       MApply '(H a).
 189       MApply '(land_e2 (P a)).
 190       MApply '(land_e1 (Eps S a U)).
 191       Qed.
 192
 193    End relative_existential.
 194
 195 End Subset_Results.