X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FSUBSETS%2Ftbs_base.v;fp=helm%2Fcoq-contribs%2FSUBSETS%2Ftbs_base.v;h=88e083b332ebad43cfabd18de71c30c928d0d75f;hb=65f400affe20fa3fe66b9a998ced5d6f64a23b45;hp=0000000000000000000000000000000000000000;hpb=50377dde5b5b1a8e5c7b2fb48b47defde9508b50;p=helm.git diff --git a/helm/coq-contribs/SUBSETS/tbs_base.v b/helm/coq-contribs/SUBSETS/tbs_base.v new file mode 100644 index 000000000..88e083b33 --- /dev/null +++ b/helm/coq-contribs/SUBSETS/tbs_base.v @@ -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.