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.