helm/coq-contribs/SUBSETS/tbs_rop.v

   1 Require Export tbs_op.
   2
   3 Section Subset_Relative_Operations_Definitions.
   4
   5    Section relative_membership.
   6
   7       Definition REps: (I,S:Set) S -> (I -> S -> Set) -> Set := [I,S;a;F](LEx I [i](Eps S a (F i))).
   8
   9    End relative_membership.
  10
  11    Section infinitary_subset_relative_operations.
  12
  13       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))).
  14
  15       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))).
  16
  17    End infinitary_subset_relative_operations.
  18
  19 End Subset_Relative_Operations_Definitions.
  20
  21 Section Subset_Relative_Operations_Results.
  22
  23    Section relative_epsilon_conditions.
  24
  25       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).
  26       Intros.
  27       Unfold REps.
  28       MApply '(lex_i I i).
  29       Qed.
  30
  31       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.
  32       Intros.
  33       Unfold REps in H0.
  34       MElim 'H0 'lex_e.
  35       MApply '(H a0).
  36       Qed.
  37
  38    End relative_epsilon_conditions.
  39
  40    Section infinitary_relative_intersection.
  41
  42       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)).
  43       Intros.
  44       MApply 'eps_i.
  45       Unfold SRAll.
  46       MApply 'rall_i.
  47       MApply '(H a0).
  48       Qed.
  49
  50       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)).
  51       Intros.
  52       MCut '(SRAll I T S R a).
  53       MApply 'eps_e.
  54       Unfold SRAll in H1.
  55       MApply '(rall_e I i T).
  56       MApply 'eps_i.
  57       Qed.
  58
  59    End infinitary_relative_intersection.
  60
  61    Section infinitary_relative_union.
  62
  63       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)).
  64       Intros.
  65       MApply 'eps_i.
  66       Unfold SREx.
  67       MApply '(rex_i I i).
  68       MApply 'eps_i.
  69       MApply '(reps_e (T i) S a (R i)).
  70       Qed.
  71
  72       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))).
  73       Intros.
  74       MCut '(SREx I T S R a).
  75       MApply 'eps_e.
  76       Unfold SREx in H0.
  77       MApply '(rex_e I T [i:I](REps (T i) S a (R i))).
  78       MApply '(lex_i I a0).
  79       Qed.
  80
  81       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))).
  82       Intros.
  83       MApply 'sbe_i.
  84       MCut '(LEx I [i:?](REps (V i) S a [_:?](F i))).
  85       MApply '(srex_eps_e I V S a [i:?; _:(V i)](F i)).
  86       MElim 'H1 'lex_e.
  87       MApply '(srex_eps_i I a0).
  88       MCut '(W a0).
  89       MApply 'eps_e.
  90       MApply '(sbe_e I V).
  91       MApply 'eps_i.
  92       MApply '(reps_e (V a0) S a [_:(V a0)](F a0)).
  93       MApply '(reps_i (W a0) H2).
  94       MApply '(reps_e (V a0) S a [_:(V a0)](F a0)).
  95       Qed.
  96
  97       Theorem srex_sing_e: (S:Set; U:S->Set) (SbE S (SREx S U S [a;_](Sing S a)) U).
  98       Intros.
  99       MApply 'sbe_i.
 100       MCut '(LEx S [b:?](REps (U b) S a [_:?](Sing S b))).
 101       MApply '(srex_eps_e S U S a [a0:S; _:(U a0)](Sing S a0)).
 102       MElim 'H0 'lex_e.
 103       MApply '(reps_e (U a0) S a [_:(U a0)](Sing S a0)).
 104       MCut '(Id S a0 a).
 105       MApply 'sing_eps_e.
 106       MApply '(id_repl S a a0).
 107       MApply 'eps_i.
 108       Qed.
 109
 110       Theorem srex_sing_i: (S:Set; U:S->Set) (SbE S U (SREx S U S [a;_](Sing S a))).
 111       Intros.
 112       MApply 'sbe_i.
 113       MApply '(srex_eps_i S a).
 114       MCut '(U a).
 115       MApply 'eps_e.
 116       MApply '(reps_i (U a) H0).
 117       MApply 'sing_eps_i.
 118       Qed.
 119
 120       Theorem srex_sing: (S:Set; U:S->Set) (SEq S (SREx S U S [a;_](Sing S a)) U).
 121       Intros.
 122       MApply 'seq_sbe_i.
 123       MApply 'srex_sing_e.
 124       MApply 'srex_sing_i.
 125       Qed.
 126
 127    End infinitary_relative_union.
 128
 129 End Subset_Relative_Operations_Results.
 130