proposition: Lemma graph_to_tree_nodup': forall lim root, vvalid G root -> is_tree G root -> NoDup (leaves (snd (graph_to_tree lim root))) /\ (forall l n trL, (forall x, In x l -> step G root x /\ vvalid G x) -> NoDup (flat_map leaves trL) -> (forall x v m, In x l -> In v (leaves (snd (graph_to_tree m x))) -> ~ In v (flat_map leaves trL)) -> NoDup l -> NoDup (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; simpl; split; intros. + assert (lim = 0) by intuition. subst. simpl. apply NoDup_nil. + assert (lim = 0) by intuition. subst. simpl. auto. + destruct lim; simpl. 1: apply NoDup_nil. pose proof (to_tree_list_is_reachable lim (nodup veq_dec (filter not_null_bool (map (dst G) (edge_func G root)))) 0 nil). remember (nodup veq_dec (filter not_null_bool (map (dst G) (edge_func G root)))). simpl in H2. rewrite app_nil_r in H2. assert (Forall (vvalid G) l). { clear H2; rewrite Forall_forall. intros. subst. rewrite nodup_In in H2. apply in_edge_func_edge in H2. destruct H2 as [? [? ?]]. apply H3. } assert (forall x : Vertex, False -> exists v : Vertex, False /\ reachable G v x) by (intros; exfalso; auto). specialize (H2 H3 H4). clear H4. remember (to_tree_list lim l (0, nil)). destruct p as [total sub_trees]. simpl in *. constructor. - intro. specialize (H2 _ H4). destruct H2 as [v [? ?]]. rewrite Heql in H2. rewrite nodup_In in H2. apply in_edge_func_edge in H2. apply (is_tree_not_to_root _ _ _ H1 H2 H5); auto. - assert (lim <= up) by intuition. destruct (IHup _ H4 _ H0 H1) as [_ ?]. clear IHup. specialize (H5 l 0 nil). rewrite <- Heqp in H5. simpl in H5. apply H5. * intros. subst l. rewrite nodup_In in H6. apply in_edge_func_edge in H6. destruct H6 as [? [? ?]]. split; auto. * apply NoDup_nil. * intros. intro; auto. * rewrite Heql. apply NoDup_nodup. + destruct lim; simpl; auto. destruct l; simpl; auto. remember (graph_to_tree lim v). destruct p as [current tr]. destruct (eq_nat_dec current 0). 1: simpl; auto. assert (lim <= up) by intuition. assert (In v (v :: l)) by (simpl; left; auto). destruct (H2 _ H7). assert (is_tree G v) by (apply is_tree_sub_is_tree with root; auto). destruct (IHup _ H6 _ H9 H10) as [? _]. rewrite <- Heqp in H11. simpl in H11. assert (lim - current <= up) by intuition. destruct (IHup _ H12 _ H0 H1) as [_ ?]. clear IHup. specialize (H13 l (n + current + 1) (tr :: trL)). simpl in H13. apply H13; clear H13. - intros. apply H2. simpl; right; auto. - apply NoDup_app_inv; auto. intros. specialize (H4 v x lim). rewrite <- Heqp in H4. simpl in H4. apply H4; auto. - intros x v' m; intros. intro. apply in_app_or in H15. assert (In x (v :: l)) by (simpl; right; auto). destruct H15. 2: specialize (H4 x v' m H16 H14); apply H4; auto. pose proof (graph_to_tree_is_reachable lim v v' H9). rewrite <- Heqp in H17. simpl in H17. specialize (H17 H15). specialize (H2 _ H16). destruct H2. apply (graph_to_tree_is_reachable m x v' H18) in H14. assert (x <> v) by (apply NoDup_cons_2 in H5; intro; subst x; exfalso; auto). clear -H0 H1 H2 H8 H14 H17 H19. assert (x = v) by (apply (is_tree_step_eq root x v v'); auto). auto. - apply NoDup_cons_1 with v; 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