helm/coq-contribs/SUBSETS/tbs_fun.v

   1 Require Export tbs_rop.
   2
   3 Section Subset_From_Functions_Definitions.
   4
   5    Section image_subset.
   6
   7       Definition Img: (I,S:Set) (I -> S) -> (S -> Set) := [I,S;f;a] (LEx I [i](Id S (f i) a)).
   8
   9       Definition FDFImg: (S:Set) (FDF S) -> (S -> Set) := [S;v](Img (Fin (fdf_n S v)) S (fdf_f S v)).
  10
  11    End image_subset.
  12
  13    Section relative_image_domain_subset.
  14
  15       Definition RImg: (I,S:Set) (I -> S) -> (I -> Set) -> (S -> Set) := [I,S;f;T;a](REx I T [i](Id S  (f i) a)).
  16
  17       Definition RDom: (I,S:Set) (I -> S) -> (S -> Set) -> (I -> Set) := [I,S;f;U;i](REx S U [a](Id S (f i) a)).
  18
  19    End relative_image_domain_subset.
  20
  21 End Subset_From_Functions_Definitions.
  22
  23 Section Subset_From_Functions_Results.
  24
  25    Section image.
  26
  27       Theorem img_eps_i: (I:Set; i:I; S:Set; a:S; f:I->S) (Id S (f i) a) -> (Eps S a (Img I S f)).
  28       Intros.
  29       MApply 'eps_i.
  30       Unfold Img.
  31       MApply '(lex_i I i).
  32       Qed.
  33
  34       Theorem img_eps_e: (I,S:Set; f:I->S; a:S; P:Set) (Eps S a (Img I S f)) -> ((i:I) (Id S (f i) a) -> P) -> P.
  35       Intros.
  36       MCut '(LEx I [i](Id S (f i) a)).
  37       Fold (Img I S f a).
  38       MApply 'eps_e.
  39       MElim 'H1 'lex_e.
  40       MApply '(H0 a0).
  41       Qed.
  42
  43       Theorem img_seq: (S:Set; U:(S -> Set)) (SEq S U (Img (Sigma S U) S (sp S U))).
  44       Intros.
  45       MApply 'seq_i.
  46       MCut '(U a).
  47       MApply 'eps_e.
  48       MApply '(img_eps_i (Sigma S U) (pair S U a H0)).
  49       MApply 'eps_i.
  50       MApply '(img_eps_e (Sigma S U) S (sp S U) a).
  51       MApply '(id_repl S a (sp S U i)).
  52       MElim 'i 'psplit.
  53       Qed.
  54
  55       Theorem img_sbe_i: (I,J,S:Set; f:I->S; g:J->S) (LEx I->J [h](i:I)(Id S (f i) (g (h i)))) -> (SbE S (Img I S f) (Img J S g)).
  56       Intros.
  57       MElim 'H 'lex_e.
  58       MApply 'sbe_i.
  59       MApply '(img_eps_e I S f a0).
  60       MApply '(img_eps_i J (a i)).
  61       MApply '(id_repl S a0 (f i)).
  62       MApply 'id_comm.
  63       MApply '(y i).
  64       Qed.
  65
  66       Theorem img_xfdf_add_i: (S:Set; m:N; v:(Fin m)->S; n:N; w:(Fin n)->S) (SbE S (SOr S (Img (Fin m) S v) (Img (Fin n) S w)) (Img (Fin (add m n)) S (xfdf_add S m v n w))).
  67       Intros.
  68       MApply 'sor_sbe_e.
  69       MApply 'img_sbe_i.
  70       MApply '(lex_i (Fin m)->(Fin (add m n)) (fil m n)).
  71       MApply 'id_comm.
  72       MApply 'xfdfa_fil.
  73       MApply 'img_sbe_i.
  74       MApply '(lex_i (Fin n)->(Fin (add m n)) (fir m n)).
  75       MApply 'id_comm.
  76       MApply 'xfdfa_fir.
  77       Qed.
  78
  79    End image.
  80
  81    Section fdf_image.
  82
  83       Theorem fdfimg_eps_i: (S:Set; v:(FDF S); i:(Fin (fdf_n S v)); a:S) (Id S (fdf_f S v i) a) -> (Eps S a (FDFImg S v)).
  84       Intros.
  85       Unfold FDFImg.
  86       MApply '(img_eps_i (Fin (fdf_n S v)) i).
  87       Qed.
  88
  89       Theorem fdfimg_eps_e: (S:Set; v:(FDF S); a:S; P:Set) (Eps S a (FDFImg S v)) -> ((i:(Fin (fdf_n S v))) (Id S (fdf_f S v i) a) -> P) -> P.
  90       Intros.
  91       MApply '(img_eps_e (Fin (fdf_n S v)) S (fdf_f S v) a).
  92       MApply '(H0 i).
  93       Qed.
  94
  95       Theorem img_fdf_add_i: (S:Set; v,w:(FDF S)) (SbE S (SOr S (FDFImg S v) (FDFImg S w)) (FDFImg S (fdf_add S v w))).
  96       Intros.
  97       Unfold FDFImg fdf_add.
  98       MSimpl.
  99       MApply 'img_xfdf_add_i.
 100       Qed.
 101
 102    End fdf_image.
 103
 104    Section relative_image.
 105
 106       Theorem rimg_eps_i: (I:Set; i:I; T:I->Set) (Eps I i T) -> (S:Set; a:S; f:I->S) (Id S (f i) a) -> (Eps S a (RImg I S f T)).
 107       Intros.
 108       MApply 'eps_i.
 109       Unfold RImg.
 110       MApply '(rex_i I i).
 111       Qed.
 112
 113       Theorem rimg_eps_e: (I,S:Set; a:S; T:I->Set; f:I->S; P:Set) ((i:I) (Eps I i T) -> (Id S (f i) a) -> P) -> (Eps S a (RImg I S f T)) -> P.
 114       Intros.
 115       Unfold RImg in H0.
 116       MCut '(REx I T [i:I](Id S (f i) a)).
 117       MApply '(eps_e S a).
 118       MApply '(rex_e I T [i:I](Id S (f i) a)).
 119       MApply '(H a0).
 120       Qed.
 121
 122       Theorem rimg_sbe: (I,S:Set; f:I->S; U,V:I->Set) (SbE I U V) -> (SbE S (RImg I S f U) (RImg I S f V)).
 123       Intros.
 124       MApply 'sbe_i.
 125       MApply '(rimg_eps_e I S a U f).
 126       MApply '(rimg_eps_i I i).
 127       MApply '(sbe_e I U).
 128       Qed.
 129
 130       Theorem rimg_sing_i: (I,S:Set; f:I->S; T:I->Set) (SbE S (SREx I T S [i;_](Sing S (f i))) (SREx S (RImg I S f T) S [a;_](Sing S a))).
 131       Intros.
 132       MApply 'sbe_i.
 133       MCut '(LEx I [i:I](REps (T i) S a [_:?](Sing S (f i)))).
 134       MApply '(srex_eps_e I T S a [i:I; _:(T i)](Sing S (f i))).
 135       MElim 'H0 'lex_e.
 136       MApply '(srex_eps_i S (f a0)).
 137       MApply '(reps_e (T a0) S a [_:(T a0)](Sing S (f a0))).
 138       MCut '(RImg I S f T (f a0)).
 139       MApply 'eps_e.
 140       MApply '(rimg_eps_i I a0).
 141       MApply 'eps_i.
 142       MApply '(reps_i (RImg I S f T (f a0)) H2).
 143       Qed.
 144
 145       Theorem rimg_sing_e: (I,S:Set; f:I->S; T:I->Set) (SbE S (SREx S (RImg I S f T) S [a;_](Sing S a)) (SREx I T S [i;_](Sing S (f i)))).
 146       Intros.
 147       MApply 'sbe_i.
 148       MCut '(LEx S [a0:?](REps (RImg I S f T a0) S a [_:?](Sing S a0))).
 149       MApply '(srex_eps_e S (RImg I S f T) S a [a0:S; _:(RImg I S f T a0)](Sing S a0)).
 150       MElim 'H0 'lex_e.
 151       MApply '(reps_e (RImg I S f T a0) S a [_:(RImg I S f T a0)](Sing S a0)).
 152       MCut '(Eps S a0 (RImg I S f T)).
 153       MApply 'eps_i.
 154       MApply '(rimg_eps_e I S a0 T f).
 155       MApply '(srex_eps_i I i0).
 156       MCut '(T i0).
 157       MApply 'eps_e.
 158       MApply '(reps_i (T i0) H5).
 159       MApply 'sing_eps_i.
 160       MApply '(id_repl S (f i0) a0).
 161       MApply 'sing_eps_e.
 162       Qed.
 163
 164       Theorem rimg_sing: (I,S:Set; f:I->S; T:I->Set) (SEq S (SREx I T S [i;_](Sing S (f i))) (SREx S (RImg I S f T) S [a;_](Sing S a))).
 165       Intros.
 166       MApply 'seq_sbe_i.
 167       MApply 'rimg_sing_i.
 168       MApply 'rimg_sing_e.
 169       Qed.
 170
 171       Theorem rimg_srex: (I,S:Set; f:I->S; T:I->Set) (SEq S (SREx I T S [i;_](Sing S (f i))) (RImg I S f T)).
 172       Intros.
 173       MApply '(seq_t S (SREx S (RImg I S f T) S [a:S; _:(RImg I S f T a)](Sing S a))).
 174       MApply 'rimg_sing.
 175       MApply 'srex_sing.
 176       Qed.
 177
 178       Theorem rimg_img_i: (I,S:Set; f:I->S; T:I->Set) (SbE S (Img (Sigma I T) S [x](f (sp I T x))) (RImg I S f T)).
 179       Intros.
 180       MApply 'sbe_i.
 181       Apply (img_eps_e (Sigma I T) S [x:(Sigma I T)](f (sp I T x)) a).
 182       Assumption.
 183       Intros p.
 184       MElim 'p 'psplit.
 185       MApply '(rimg_eps_i I a0).
 186       MApply 'eps_i.
 187       Qed.
 188
 189       Theorem rimg_img_e: (I,S:Set; f:I->S; T:I->Set) (SbE S (RImg I S f T) (Img (Sigma I T) S [x](f (sp I T x)))).
 190       Intros.
 191       MApply 'sbe_i.
 192       MApply '(rimg_eps_e I S a T f).
 193       MCut '(T i).
 194       MApply 'eps_e.
 195       MApply '(img_eps_i (Sigma I T) (pair I T i H2)).
 196       Qed.
 197
 198       Theorem rimg_img: (I,S:Set; f:I->S; T:I->Set) (SEq S (Img (Sigma I T) S [x](f (sp I T x))) (RImg I S f T)).
 199       Intros.
 200       MApply 'seq_sbe_i.
 201       MApply 'rimg_img_i.
 202       MApply 'rimg_img_e.
 203       Qed.
 204
 205    End relative_image.
 206
 207 End Subset_From_Functions_Results.
 208