]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/coq-contribs/SUBSETS/tbs_base.v
a contribution about subset theory in an intuitionistic and predicative foundation
[helm.git] / helm / coq-contribs / SUBSETS / tbs_base.v
diff --git a/helm/coq-contribs/SUBSETS/tbs_base.v b/helm/coq-contribs/SUBSETS/tbs_base.v
new file mode 100644 (file)
index 0000000..88e083b
--- /dev/null
@@ -0,0 +1,195 @@
+(** This module (Toolbox - subsets: basics) defines:
+    - subset membership:               [Eps]  (epsilon)
+    - empty subset:                    [SBot] (subset bottom)
+    - full subset:                     [STop] (subset top)
+    - singleton:                       [Sing] (singleton)
+    - relative universal quantifier:   [RAll] (relative all)
+    - relative existential quantifier: [REx]  (relative exists)
+    
+    and provides:
+    - introduction and elimination rules for the defined constants
+    - epsilon conditions: [eps_1], [eps_2]
+    - alternative form of epsilon with sigma: [eps2]
+
+% \hrule %
+
+ We require the support for finite sets and finite domain functions ([xt_fin])
+ that includes the basic type theory (the [st] package).
+ *)
+Require Export xt_fin.
+
+Section Subset_Definitions.
+
+   Section subset_membership.
+   
+(** Epsilon: [(Eps S a U)] corresponds to $ a \e_S U $. *) 
+      Definition Eps: (S:Set) S -> (S -> Set) -> Set.
+      Intros S a U.
+      Exact (LAnd (U a) (Id S a a)).
+      Defined.
+
+   End subset_membership.
+
+   Section subset_constants.
+
+(** Subset bottom: [(SBot S)] corresponds to $ \sbot_S $. *) 
+      Definition SBot: (S:Set) S -> Set.
+      Intros.
+      Exact LBot.
+      Defined.
+
+(** Subset top: [(STop S)] corresponds to $ \stop_S $, %{\ie}% to $S$ as a subset of itself. *) 
+      Definition STop: (S:Set) S -> Set.
+      Intros.
+      Exact LTop.
+      Defined.
+
+(** Singleton: [(Sing S a)] corresponds to $ \subset{a} $. *) 
+      Definition Sing: (S:Set) S -> (S -> Set).
+      Intros S a b.
+      Exact (Id S a b).
+      Defined.
+
+   End subset_constants.
+
+   Section relative_quantification.
+
+(** Relative all: [(RAll S U P)] corresponds to $ (\lall x \e U) P(x) $. *) 
+      Definition RAll: (S:Set) (S -> Set) -> (S -> Set) -> Set.
+      Intros S U P.
+      Exact (a:S) (Eps S a U) -> (P a).
+      Defined.
+
+(** Relative exists: [(REx S U P)] corresponds to $ (\lex x \e U) P(x) $. *) 
+      Definition REx: (S:Set) (S -> Set) -> (S -> Set) -> Set.
+      Intros S U P.
+      Exact (LEx S [a](LAnd (Eps S a U) (P a))).
+      Defined.
+   
+   End relative_quantification.
+
+End Subset_Definitions.
+
+Section Subset_Results.
+
+   Section epsilon_conditions.
+
+(** Epsilon elimination: $ a \e U \limp U(a) $. *)  
+      Theorem eps_e: (S:Set; a:S; U:S->Set) (Eps S a U) -> (U a).
+      Unfold Eps.
+      Intros.
+      MApply '(land_e2 (Id S a a)).
+      Qed.
+
+(** Epsilon introduction: $ U(a) \limp a \e U $. *)  
+      Theorem eps_i: (S:Set; a:S; U:S->Set) (U a) -> (Eps S a U).
+      Unfold Eps.
+      Intros.
+      MApply 'land_i.
+      Qed.
+
+(** Epsilon condition 1: $ a \e U \liff U(a) $. *)
+      Theorem eps_1: (S:Set; U:(S -> Set)) (a:S)(LIff (Eps S a U) (U a)).
+      Intros.
+      MApply 'liff_i.
+      MApply '(eps_e S a).
+      MApply 'eps_i.
+      Qed.
+
+(** Epsilon condition 2: $ a \e_S U \limp a \in S $. *)
+      Theorem eps_2: (S:Set; a:S; U:(S -> Set)) (Eps S a U) -> S.
+      Intros.
+      Exact a.
+      Qed.
+
+(** Epsilon in sigma form: $ a \e_S U \liff (\lex z \in (\Sigma x \in S) U) Id(S, p(z), a) $. *)
+      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))).
+      Intros.
+      MApply 'liff_i.
+      MCut '(U a).
+      MApply 'eps_e.
+      MApply '(lex_i (Sigma S U) (pair S U a H0)).
+      MApply 'eps_i.
+      MElim 'H 'lex_e.
+      MApply '(id_repl ? a (sp S U a0)).
+      MElim 'a0 psplit.
+      Qed.
+
+   End epsilon_conditions.
+
+   Section subset_top_bottom.
+
+(** Subset top, epsilon introduction: $ a \e \stop $. *)    
+      Theorem stop_eps_i: (S:Set; a:S) (Eps S a (STop S)).
+      Intros.
+      MApply 'eps_i.
+      Unfold STop.
+      MApply 'LTop_red.
+      Qed.
+   
+(** Subset bottom, epsilon elimination: $ a \e \sbot \limp \lbot $. *)   
+      Theorem sbot_eps_e: (S:Set; a:S) (Eps S a (SBot S)) -> LBot.
+      Intros.
+      MApply '(eps_e S a).
+      Qed.
+   
+   End subset_top_bottom.
+
+   Section singleton.
+
+(** Singleton, epsilon introduction: $ Id(S, a, b) \limp b \e \subset{a} $. *)    
+      Theorem sing_eps_i: (S:Set; b,a:S) (Id S a b) -> (Eps S b (Sing S a)).
+      Intros.
+      MApply 'eps_i.
+      Qed.
+
+(** Singleton, epsilon elimination: $ b \e \subset{a} \limp Id(S, a, b) $. *)    
+      Theorem sing_eps_e: (S:Set; a,b:S) (Eps S b (Sing S a)) -> (Id S a b).
+      Intros.
+      MApply 'eps_e.
+      Qed.
+
+   End singleton.
+
+   Section relative_universal.
+
+(** Relative all introduction: $ ((\lall a \in S)\ a \e U \limp P(a)) \limp (\lall x \e U) P(x) $. *)
+      Theorem rall_i: (S:Set; U:S->Set; P:S->Set) ((a:S) (Eps S a U) -> (P a)) -> (RAll S U P).
+      Unfold RAll.
+      Intros.
+      MApply '(H a).
+      Qed.
+
+(** Relative all elimination: $ a \e U \limp (\lall x \e U) P(x) \limp P(a) $. *)
+      Theorem rall_e: (S:Set; a:S; U:S->Set; P:S->Set) (Eps S a U) -> (RAll S U P) -> (P a).
+      Intros.
+      Unfold RAll in H0.
+      MApply '(H0 a).
+      Qed.
+
+   End relative_universal.
+
+   Section relative_existential.
+
+(** Relative exists introduction: $ a \e U \limp P(a) \limp (\lex x \e U) P(x) $. *)
+      Theorem rex_i: (S:Set; a:S; U:S->Set; P:S->Set) (Eps S a U) -> (P a) -> (REx S U P).
+      Intros.
+      Unfold REx.
+      MApply '(lex_i S a).
+      MApply 'land_i.
+      Qed.
+
+(** Relative exists elimination: $ ((\lall a \in S)\ a \e U \limp P(a) \limp T) \limp (\lex x \e U) P(x) \limp T $. *)
+      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.
+      Intros.
+      Unfold REx in H0.
+      MElim 'H0 'lex_e.
+      MApply '(H a).
+      MApply '(land_e2 (P a)).
+      MApply '(land_e1 (Eps S a U)).
+      Qed.
+
+   End relative_existential.
+
+End Subset_Results.