proposition: Lemma reachable_through_set_enum: forall S, EnumCovered V (reachable_through_set G S) -> forall s, incl s S -> well_defined_list G s -> Enumerable V (reachable_through_set G s).
proof: Proof. intros. induction s. - exists nil. split. 1: apply NoDup_nil. simpl. unfold reachable_through_set. unfold Ensembles.In. intros. split; intros. + exfalso; auto. + destruct H1 as [? [? ?]]. inversion H1. - spec IHs; [eapply incl_tran; [apply incl_tl, incl_refl | apply H] |]. spec IHs; [intros x HH; apply (H0 x); right; auto |]. destruct IHs as [l1 [? ?]]. destruct (reachable_set_enumcovered_single_reachable S X a) as [l2 [? ?]]. 1: apply (H a); left; auto. 1: specialize (H0 a); spec H0; [left; auto |]; destruct H0; [left | right]; auto. exists (nodup equiv_dec (l1 ++ l2)). split. 1: apply NoDup_nodup. unfold reachable_list, reachable_through_set, Ensembles.In in *. intros x; rewrite nodup_In. rewrite in_app_iff. specialize (H2 x). specialize (H3 x). split; intros. + destruct H5; [| exists a; split; [left; auto | tauto]]. rewrite H2 in H5. destruct H5 as [s0 ?H]; exists s0. split; [right|]; tauto. + destruct H5 as [s0 ?H]. destruct_eq_dec a s0; [right | left]; subst; try tauto. apply H2. exists s0; simpl in H5; tauto. Qed.
imports: Coq.Sets.Finite_sets Coq.Arith.Arith Coq.Logic.ProofIrrelevance Coq.Logic.FunctionalExtensionality Coq.Sorting.Permutation Coq.micromega.Lia CertiGraph.lib.Coqlib CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles Coq.Lists.List VST.msl.Coqlib2 CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_ind CertiGraph.graph.subgraph2 CertiGraph.graph.graph_gen CertiGraph.graph.MathGraph CertiGraph.graph.FiniteGraph