proposition: Lemma graph_to_tree_contains_reachable': forall lim root, vvalid G root -> is_tree G root -> forall x, reachable G root x -> (forall (H: Enumerable Vertex (reachable G root)), 2 * sizeOfEnum H - 1 <= lim -> In x (leaves (snd (graph_to_tree lim root)))) /\ (forall n l trL (H: Enumerable Vertex (reachable_through_set G l)), 2 * sizeOfEnum H <= lim -> x <> root -> NoDup l -> (forall y, In y l -> step G root y /\ vvalid G y) -> ((exists i, In i l /\ reachable G i x) \/ In x (flat_map leaves trL)) -> In x (flat_map leaves (snd (to_tree_list lim l (n, trL))))).
proof: Proof. intro lim. remember lim as up. rewrite Hequp. assert (lim <= up) by intuition. clear Hequp. revert lim H. induction up; intros; split; intros; pose proof H3 as XX; destruct H3 as [? [? ?]]; unfold sizeOfEnum in H4; simpl in H4; unfold Ensembles.In in i. + assert (lim = 0) by intuition. subst. rewrite <- i in H2. destruct x0. inversion H2. simpl in H4. exfalso; intuition. + assert (lim = 0) by intuition. subst. simpl. destruct H8; auto. assert (reachable_through_set G l x) by (apply H3). rewrite <- i in H8. destruct x0. inversion H8. simpl in H4. exfalso; intuition. + remember (graph_to_tree lim root). destruct p as [num t]. simpl. destruct lim. 1: rewrite <- i in H2; destruct x0; [inversion H2 | simpl in H4; exfalso; intuition]. simpl in Heqp. remember (nodup veq_dec (filter not_null_bool (map (dst G) (edge_func G root)))). assert (lim <= up) by intuition. clear H. assert (step_list G root (map (dst G) (edge_func G root))) by (subst l; clear; intro y; rewrite edge_func_step; intuition). assert (Enumerable Vertex (reachable_through_set G l)) by (subst l; apply (Enumerable_step_list_enum root); auto). rewrite Heql in X. assert (2 * sizeOfEnum X <= lim) by (apply (sizeOfEnum_step_list root _ _ x0); auto). destruct (IHup _ H3 _ H0 H1 _ H2) as [_ ?]. specialize (H6 0 _ nil X H5). rewrite <- Heql in H6. remember (to_tree_list lim l (0, nil)). destruct p as [total sub_trees]. inversion Heqp. subst num t. clear Heqp. clear IHup. simpl in *. destruct_eq_dec x root; [left | right]; auto. apply H6; auto. - rewrite Heql. apply NoDup_nodup. - intros. rewrite Heql in H8. rewrite nodup_In in H8. apply in_edge_func_edge in H8. destruct H8 as [? [? ?]]. split; auto. - left; clear -MA H2 Heql H7. apply reachable_by_ind in H2. destruct H2. 1: exfalso; auto. destruct H as [z [? ?]]. exists z. apply reachable_by_is_reachable in H0. split; auto. rewrite Heql. rewrite nodup_In, in_edge_func_edge; auto. + destruct lim. 1: simpl; destruct H8; auto; unfold reachable_through_set in i; rewrite <- i in H3; assert (length x0 = 0) by intuition; destruct x0; [inversion H3 | inversion H8]. destruct l. 1: simpl; destruct H8; auto; destruct H3 as [i' [? _]]; inversion H3. remember (to_tree_list (S lim) (v :: l) (n, trL)). destruct p as [num t]. simpl in Heqp. remember (graph_to_tree lim v). destruct p as [current tr]. destruct (eq_nat_dec current 0). - inversion Heqp. subst. simpl. clear Heqp. destruct H8; auto. assert (lim = 0) by (apply (graph_to_tree_zero lim v); rewrite <- Heqp0; simpl; auto). subst. assert (length x0 = 0) by intuition. assert (x0 = nil) by (destruct x0; auto; inversion H8). subst. assert (reachable_through_set G (v :: l) x) by apply H3. rewrite <- i in H9. inversion H9. - assert (In v (v :: l)) by apply in_eq. pose proof (H7 _ H3); destruct H9. assert (is_tree G v) by (apply is_tree_sub_is_tree with root; auto). assert (Enumerable Vertex (reachable G v)) by (apply (@finite_reachable_enumcovered_enumerable _ _ _ _ _ is_null); auto; exists x0; split; auto; unfold Ensembles.In; intros; rewrite i; exists v; split; auto). assert (2 * sizeOfEnum X - 1 <= lim). { clear -n0 i H4 X H3. destruct X as [l' [? ?]]. unfold sizeOfEnum. simpl. unfold Ensembles.In in i0. assert (incl l' x0) by (intro; rewrite i, i0; intros; exists v; split; auto). assert (length l' <= length x0) by (apply NoDup_incl_length; auto). intuition. } assert (forall y, reachable G v y -> In y (leaves tr)). { intros. assert (lim <= up) by intuition. destruct (IHup _ H14 _ H10 H11 _ H13) as [? _]. specialize (H15 X H12). rewrite <- Heqp0 in H15. simpl in H15; auto. } clear X H12. assert (lim - current <= up) by intuition. destruct (IHup _ H12 _ H0 H1 _ H2) as [_ ?]. specialize (H14 (n + current + 1) l (tr :: trL)). clear H12 IHup. assert (Enumerable Vertex (reachable_through_set G l)). { apply (reachable_through_set_enum _ (v :: l)); [apply Enumerable_is_EnumCovered; exists x0; split; auto | apply incl_tl, incl_refl |]. hnf. intros. assert (In x1 (v :: l)) by (right; auto). apply H7 in H15. destruct H15. hnf. right; auto. } assert (2 * sizeOfEnum X <= lim - current) by (apply (sizeOfEnum_cons root l X v x0 lim current tr); auto; intros; split; auto; intros; apply (graph_to_tree_is_reachable lim); auto; rewrite <- Heqp0; auto). specialize (H14 X H12). rewrite Heqp. apply H14; auto. 1: apply NoDup_cons_1 in H6; auto. 1: intros; apply H7; right; auto. clear H14. simpl. rewrite in_app_iff. destruct H8 as [[v' [? ?]]| ?]. * simpl in H8. destruct H8. 1: subst v'; right; left; apply H13; auto. left. exists v'. split; auto. * right; right; auto. Qed.
imports: Coq.Arith.Arith CertiGraph.lib.Coqlib CertiGraph.lib.EnumEnsembles CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.MathGraph CertiGraph.graph.FiniteGraph CertiGraph.graph.reachable_computable Coq.Lists.List