]> matita.cs.unibo.it Git - helm.git/blob - helm/coq-contribs/SUBSETS/tbs_fun.v
1. change_tac moved from PrimitiveTactics to ReductionTactics
[helm.git] / 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