a contribution about subset theory in an intuitionistic and predicative foundation

[helm.git] / helm / coq-contribs / SUBSETS / tbs_rop.v

diff --git a/helm/coq-contribs/SUBSETS/tbs_rop.v b/helm/coq-contribs/SUBSETS/tbs_rop.v
new file mode 100644 (file)
index 0000000..2abccd6
--- /dev/null
+++ b/helm/coq-contribs/SUBSETS/tbs_rop.v
@@ -0,0 +1,130 @@
+Require Export tbs_op.
+
+Section Subset_Relative_Operations_Definitions.
+
+   Section relative_membership.
+   
+      Definition REps: (I,S:Set) S -> (I -> S -> Set) -> Set := [I,S;a;F](LEx I [i](Eps S a (F i))).
+   
+   End relative_membership.
+
+   Section infinitary_subset_relative_operations.
+
+      Definition SRAll: (I:Set; T:I->Set; S:Set) ((i:I) (T i) -> (S -> Set)) -> (S -> Set) := [I;T;S;R;a](RAll I T [i](REps (T i) S a (R i))).
+      
+      Definition SREx: (I:Set; T:I->Set; S:Set) ((i:I) (T i) -> (S -> Set)) -> (S -> Set) := [I;T;S;R;a](REx I T [i](REps (T i) S a (R i))).
+
+   End infinitary_subset_relative_operations.
+
+End Subset_Relative_Operations_Definitions.
+
+Section Subset_Relative_Operations_Results.
+
+   Section relative_epsilon_conditions.
+   
+      Theorem reps_i: (I:Set; i:I; S:Set; a:S; F:I->S->Set) (Eps S a (F i)) -> (REps I S a F).
+      Intros.
+      Unfold REps.
+      MApply '(lex_i I i).
+      Qed.
+      
+      Theorem reps_e: (I,S:Set; a:S; F:I->S->Set; P:Set) ((i:I) (Eps S a (F i)) -> P) -> (REps I S a F) -> P.
+      Intros.
+      Unfold REps in H0.
+      MElim 'H0 'lex_e.
+      MApply '(H a0).
+      Qed.
+      
+   End relative_epsilon_conditions.
+
+   Section infinitary_relative_intersection.
+   
+      Theorem srall_eps_i: (I:Set; T:I->Set; S:Set; a:S; R:(i:I)(T i)->(S->Set)) ((i:I) (REps (T i) S a (R i))) -> (Eps S a (SRAll I T S R)).
+      Intros.
+      MApply 'eps_i.
+      Unfold SRAll.
+      MApply 'rall_i.
+      MApply '(H a0).
+      Qed.
+      
+      Theorem srall_eps_e: (I:Set; i:I; T:I->Set) (T i) -> (S:Set; a:S; R:(i:I)(T i)->(S->Set)) (Eps S a (SRAll I T S R)) -> (REps (T i) S a (R i)). 
+      Intros.
+      MCut '(SRAll I T S R a).
+      MApply 'eps_e.
+      Unfold SRAll in H1.
+      MApply '(rall_e I i T).
+      MApply 'eps_i.
+      Qed.
+      
+   End infinitary_relative_intersection.
+
+   Section infinitary_relative_union.
+   
+      Theorem srex_eps_i: (I:Set; i:I; S:Set; a:S; T:I->Set; R:(i:I)(T i)->(S->Set)) (REps (T i) S a (R i)) -> (Eps S a (SREx I T S R)).
+      Intros.
+      MApply 'eps_i.
+      Unfold SREx.
+      MApply '(rex_i I i).
+      MApply 'eps_i.
+      MApply '(reps_e (T i) S a (R i)).
+      Qed.
+      
+      Theorem srex_eps_e: (I:Set; T:I->Set; S:Set; a:S; R:(i:I)(T i)->(S->Set)) (Eps S a (SREx I T S R)) -> (LEx I [i](REps (T i) S a (R i))).
+      Intros.
+      MCut '(SREx I T S R a).
+      MApply 'eps_e.
+      Unfold SREx in H0.
+      MApply '(rex_e I T [i:I](REps (T i) S a (R i))).
+      MApply '(lex_i I a0).
+      Qed.
+
+      Theorem srex_sbe: (I:Set; V,W:I->Set; S:Set; F:I->S->Set) (SbE I V W) -> (SbE S (SREx I V S [i;_](F i)) (SREx I W S [i;_](F i))).
+      Intros.
+      MApply 'sbe_i.
+      MCut '(LEx I [i:?](REps (V i) S a [_:?](F i))).
+      MApply '(srex_eps_e I V S a [i:?; _:(V i)](F i)).
+      MElim 'H1 'lex_e.
+      MApply '(srex_eps_i I a0).
+      MCut '(W a0).
+      MApply 'eps_e.
+      MApply '(sbe_e I V).
+      MApply 'eps_i.
+      MApply '(reps_e (V a0) S a [_:(V a0)](F a0)).
+      MApply '(reps_i (W a0) H2).
+      MApply '(reps_e (V a0) S a [_:(V a0)](F a0)).
+      Qed.
+      
+      Theorem srex_sing_e: (S:Set; U:S->Set) (SbE S (SREx S U S [a;_](Sing S a)) U).
+      Intros.
+      MApply 'sbe_i.
+      MCut '(LEx S [b:?](REps (U b) S a [_:?](Sing S b))).
+      MApply '(srex_eps_e S U S a [a0:S; _:(U a0)](Sing S a0)).
+      MElim 'H0 'lex_e.
+      MApply '(reps_e (U a0) S a [_:(U a0)](Sing S a0)).
+      MCut '(Id S a0 a).
+      MApply 'sing_eps_e.
+      MApply '(id_repl S a a0).
+      MApply 'eps_i.
+      Qed.
+
+      Theorem srex_sing_i: (S:Set; U:S->Set) (SbE S U (SREx S U S [a;_](Sing S a))).
+      Intros.
+      MApply 'sbe_i.
+      MApply '(srex_eps_i S a).
+      MCut '(U a).
+      MApply 'eps_e.
+      MApply '(reps_i (U a) H0).
+      MApply 'sing_eps_i.
+      Qed.
+
+      Theorem srex_sing: (S:Set; U:S->Set) (SEq S (SREx S U S [a;_](Sing S a)) U).
+      Intros.
+      MApply 'seq_sbe_i.
+      MApply 'srex_sing_e.
+      MApply 'srex_sing_i.
+      Qed.
+      
+   End infinitary_relative_union.
+
+End Subset_Relative_Operations_Results.
+