proposition: Lemma EnumStrengthen: forall U (P Q: Ensemble U), (forall x, P x -> Decidable (Q x)) -> Included Q P -> Enumerable U P -> Enumerable U Q.
proof: Proof. intros. destruct X0 as [l [? ?]]. unfold Included, Ensembles.In in H, H1. assert (forall x : U, In x l -> Decidable (Q x)) by firstorder. assert (forall x : U, Q x -> In x l) by firstorder. clear X H H1 P. assert ({l' | NoDup l' /\ (forall x, In x l' <-> Q x /\ In x l)}). + clear H2. induction l; intros. - exists nil. split; [constructor |]. intros x; simpl; tauto. - spec IHl; [inversion H0; auto |]. spec IHl; [intros; apply X0; simpl; auto |]. destruct IHl as [l0 [? ?]]. destruct (X0 a (or_introl eq_refl)) as [?H | ?H]; [exists (a :: l0) | exists l0]; split. * constructor; auto. specialize (H1 a). inversion H0; tauto. * intros. simpl. specialize (H1 x). assert (a = x -> Q x) by (intros; subst; auto). tauto. * auto. * intros; simpl. specialize (H1 x). assert (a = x -> ~ Q x) by (intros; subst; auto). tauto. + destruct X as [l' [? ?]]; exists l'. split; [auto |]. intros; unfold Ensembles.In; specialize (H1 x); specialize (H2 x). tauto. Qed.
imports: Coq.Sorting.Permutation Coq.Classes.EquivDec CertiGraph.lib.Coqlib CertiGraph.lib.List_ext CertiGraph.lib.Ensembles_ext Coq.Lists.List