Require Export tbs_rop.

Section Subset_From_Functions_Definitions.

   Section image_subset.

      Definition Img: (I,S:Set) (I -> S) -> (S -> Set) := [I,S;f;a] (LEx I [i](Id S (f i) a)).
      
      Definition FDFImg: (S:Set) (FDF S) -> (S -> Set) := [S;v](Img (Fin (fdf_n S v)) S (fdf_f S v)).

   End image_subset.

   Section relative_image_domain_subset.
   
      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)).
      
      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)).

   End relative_image_domain_subset.

End Subset_From_Functions_Definitions.

Section Subset_From_Functions_Results.

   Section image.

      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)). 
      Intros.
      MApply 'eps_i.
      Unfold Img.
      MApply '(lex_i I i).
      Qed.

      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.
      Intros.
      MCut '(LEx I [i](Id S (f i) a)).
      Fold (Img I S f a).
      MApply 'eps_e.
      MElim 'H1 'lex_e.
      MApply '(H0 a0).
      Qed.
      
      Theorem img_seq: (S:Set; U:(S -> Set)) (SEq S U (Img (Sigma S U) S (sp S U))).
      Intros.
      MApply 'seq_i.
      MCut '(U a).
      MApply 'eps_e.
      MApply '(img_eps_i (Sigma S U) (pair S U a H0)).
      MApply 'eps_i.
      MApply '(img_eps_e (Sigma S U) S (sp S U) a).
      MApply '(id_repl S a (sp S U i)).
      MElim 'i 'psplit.
      Qed.

      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)).
      Intros.
      MElim 'H 'lex_e.
      MApply 'sbe_i.
      MApply '(img_eps_e I S f a0).
      MApply '(img_eps_i J (a i)).
      MApply '(id_repl S a0 (f i)).
      MApply 'id_comm.
      MApply '(y i).
      Qed.

      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))).
      Intros.
      MApply 'sor_sbe_e.
      MApply 'img_sbe_i.
      MApply '(lex_i (Fin m)->(Fin (add m n)) (fil m n)).
      MApply 'id_comm.
      MApply 'xfdfa_fil.
      MApply 'img_sbe_i.
      MApply '(lex_i (Fin n)->(Fin (add m n)) (fir m n)).
      MApply 'id_comm.
      MApply 'xfdfa_fir.
      Qed.

   End image.
   
   Section fdf_image.

      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)).
      Intros.
      Unfold FDFImg.
      MApply '(img_eps_i (Fin (fdf_n S v)) i).
      Qed.

      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.
      Intros.
      MApply '(img_eps_e (Fin (fdf_n S v)) S (fdf_f S v) a).
      MApply '(H0 i).
      Qed.

      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))).
      Intros.
      Unfold FDFImg fdf_add.
      MSimpl.
      MApply 'img_xfdf_add_i.
      Qed.

   End fdf_image.
   
   Section relative_image.
   
      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)).
      Intros.
      MApply 'eps_i.
      Unfold RImg.
      MApply '(rex_i I i).
      Qed.
      
      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.
      Intros.
      Unfold RImg in H0.
      MCut '(REx I T [i:I](Id S (f i) a)).
      MApply '(eps_e S a).
      MApply '(rex_e I T [i:I](Id S (f i) a)).
      MApply '(H a0).
      Qed.
      
      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)).
      Intros.
      MApply 'sbe_i.
      MApply '(rimg_eps_e I S a U f).
      MApply '(rimg_eps_i I i).
      MApply '(sbe_e I U).
      Qed.
      
      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))).
      Intros.
      MApply 'sbe_i.
      MCut '(LEx I [i:I](REps (T i) S a [_:?](Sing S (f i)))).
      MApply '(srex_eps_e I T S a [i:I; _:(T i)](Sing S (f i))).
      MElim 'H0 'lex_e.
      MApply '(srex_eps_i S (f a0)).
      MApply '(reps_e (T a0) S a [_:(T a0)](Sing S (f a0))).
      MCut '(RImg I S f T (f a0)).
      MApply 'eps_e.
      MApply '(rimg_eps_i I a0).
      MApply 'eps_i.
      MApply '(reps_i (RImg I S f T (f a0)) H2).
      Qed.
      
      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)))).
      Intros.
      MApply 'sbe_i.
      MCut '(LEx S [a0:?](REps (RImg I S f T a0) S a [_:?](Sing S a0))).
      MApply '(srex_eps_e S (RImg I S f T) S a [a0:S; _:(RImg I S f T a0)](Sing S a0)).
      MElim 'H0 'lex_e.
      MApply '(reps_e (RImg I S f T a0) S a [_:(RImg I S f T a0)](Sing S a0)).
      MCut '(Eps S a0 (RImg I S f T)).
      MApply 'eps_i.
      MApply '(rimg_eps_e I S a0 T f).
      MApply '(srex_eps_i I i0).
      MCut '(T i0).
      MApply 'eps_e.
      MApply '(reps_i (T i0) H5).
      MApply 'sing_eps_i.
      MApply '(id_repl S (f i0) a0).
      MApply 'sing_eps_e.
      Qed.
      
      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))).
      Intros.
      MApply 'seq_sbe_i.
      MApply 'rimg_sing_i.
      MApply 'rimg_sing_e.
      Qed.
      
      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)).
      Intros.
      MApply '(seq_t S (SREx S (RImg I S f T) S [a:S; _:(RImg I S f T a)](Sing S a))).
      MApply 'rimg_sing.
      MApply 'srex_sing.
      Qed.

      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)).
      Intros.
      MApply 'sbe_i.
      Apply (img_eps_e (Sigma I T) S [x:(Sigma I T)](f (sp I T x)) a).
      Assumption.
      Intros p.
      MElim 'p 'psplit.
      MApply '(rimg_eps_i I a0).
      MApply 'eps_i.
      Qed.
      
      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)))).
      Intros.
      MApply 'sbe_i.
      MApply '(rimg_eps_e I S a T f).
      MCut '(T i).
      MApply 'eps_e.
      MApply '(img_eps_i (Sigma I T) (pair I T i H2)).
      Qed.
      
      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)).
      Intros.
      MApply 'seq_sbe_i.
      MApply 'rimg_img_i.
      MApply 'rimg_img_e.
      Qed.
      
   End relative_image.
   
End Subset_From_Functions_Results.