]> matita.cs.unibo.it Git - helm.git/blob - helm/coq-contribs/SUBSETS/tbs_fin.v
reorganization continues ...
[helm.git] / helm / coq-contribs / SUBSETS / tbs_fin.v
1 Require Export tbs_fun.
2
3 Section Subset_Finite_Definitions.
4
5    Section subsets_from_lists.
6
7       Definition SList: (S:Set) (List S) -> (S -> Set) := [S](ListFam S [_](S->Set) (SBot S) [_;p;a](SOr S p (Sing S a))).
8
9    End subsets_from_lists.
10
11    Section subset_finite_predicate.
12
13       Definition WFin: (S:Set) (S -> Set) -> Set := [S;U](LEx (FDF S) [z](SbE S U (FDFImg S z))).
14 (*      
15 Definition SFin: (S:Set) (S -> Set) -> Set := [S;U](Ex (FDF S) [z](SEq S U (FDFImg S z))).
16 *)
17    End subset_finite_predicate.
18 (*
19 Section subset_finite_quantification.
20    
21 Definition FAll: (S:Set) ((Part S) -> Set) -> Set := [S;P](z:(FDF S))(P (SFImg S z)).
22       
23 Definition FEx: (S:Set) ((Part S) -> Set) -> Set := [S;P](Ex (FDF S) [z](P (SFImg S z))).
24    
25 End subset_finite_quantification.
26 *)
27 End Subset_Finite_Definitions.
28
29 Section Subset_Finite_Results.
30
31    Section subset_list.
32
33       Theorem slist_eps_i: (S:Set; a:S; l:(List S)) (LIn S a l) -> (Eps S a (SList S l)).
34       Intros S a l.
35       MElim l listrec.
36       MCut Empty.
37       Apply (lin_e S a (empty S)).
38       Assumption.
39       Intros v w.
40       MElim w listrec.
41       MApply '(list_p4 S v a).
42       MApply '(list_p4 S (app S (fr S v a) l0) s).
43       MElim H0 efq.
44       Apply (lin_e S a (fr S l0 s)).
45       Assumption.
46       Intros v w.
47       MElim w listrec.
48       MApply 'sor_eps_i1.
49       MApply 'sing_eps_i.
50       MApply '(fr_ini2 S l0 v).
51       MApply 'sor_eps_i2.
52       MApply 'H.
53       MApply '(lin_i S v l1).
54       MApply '(fr_ini1 S s0 s).
55       Qed.
56
57
58       Theorem slist_xfdfl: (S:Set; n:N; v:(Fin n)->S) (SbE S (Img (Fin n) S v) (SList S (xfdf_list S n v))).
59       Intros.
60       MApply 'sbe_i.
61       MApply 'slist_eps_i.
62       MApply '(img_eps_e (Fin n) S v a).
63       MApply '(id_repl S a (v i)).
64       MApply 'xfdfl_lin.
65       Qed.
66
67       Theorem slist_fdfl: (S:Set; v:(FDF S)) (SbE S (FDFImg S v) (SList S (fdfl S v))).
68       Intros.
69       MApply '(id_repl (List S) (fdfl S v) (xfdf_list S (fdf_n S v) (fdf_f S v))).
70       MElim 'v '(fdf_e S).
71       Unfold FDFImg.
72       MApply 'slist_xfdfl.
73       Qed.
74
75    End subset_list.
76    
77    Section weakly_finite.
78
79       Theorem wfin_i: (S:Set; v:(FDF S); U:S->Set) (SbE S U (FDFImg S v)) -> (WFin S U).
80       Intros.
81       Unfold WFin.
82       MApply '(lex_i (FDF S) v).
83       Qed.
84       
85       Theorem wfin_e: (S:Set; U:S->Set; P:Set) (WFin S U) -> ((v:(FDF S)) (SbE S U (FDFImg S v)) -> P) -> P.
86       Intros.
87       MElim 'H 'lex_e.
88       MApply '(H0 a).
89       Qed.
90
91       Theorem wfin_sand: (S:Set; U,V:S->Set) (WFin S U) -> (WFin S (SAnd S U V)).
92       Intros.
93       MApply '(wfin_e S U).
94       MApply '(wfin_i S v).
95       MApply '(sbe_t S U).
96       MApply 'sand_sbe_e2.
97       Qed.
98
99       Theorem wfin_sor: (S:Set; U,V:S->Set) (WFin S U) -> (WFin S V) -> (WFin S (SOr S U V)).
100       Intros.
101       MApply '(wfin_e S U).
102       MApply '(wfin_e S V).
103       MApply '(wfin_i S (fdf_add S v v0)).
104       MApply '(sbe_t S (SOr S (FDFImg S v) (FDFImg S v0))).
105       MApply 'sor_sbe_c.
106       MApply 'img_fdf_add_i.
107       Qed.
108
109       Theorem wfin_list: (S:Set; U:S->Set) (WFin S U) -> (LEx (List S) [v](SbE S U (SList S v))). 
110       Intros.
111       MApply '(wfin_e S U).
112       MApply '(lex_i (List S) (fdfl S v)).
113       MApply '(sbe_t S (FDFImg S v)).
114       MApply 'slist_fdfl.
115       Qed.      
116
117    End weakly_finite.
118
119 End Subset_Finite_Results.