a contribution about subset theory in an intuitionistic and predicative foundation

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

diff --git a/helm/coq-contribs/SUBSETS/tbs_fun.v b/helm/coq-contribs/SUBSETS/tbs_fun.v
new file mode 100644 (file)
index 0000000..7d03a1b
--- /dev/null
+++ b/helm/coq-contribs/SUBSETS/tbs_fun.v
@@ -0,0 +1,208 @@
+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.
+