proposition: Lemma to_tree_list_is_reachable: forall lim l n trL, Forall (vvalid G) l -> (forall x, In x (flat_map leaves trL) -> exists v, In v (forest_head trL) /\ reachable G v x) -> forall x, In x (flat_map leaves (snd (to_tree_list lim l (n, trL)))) -> exists v, In v (l ++ forest_head trL) /\ reachable G v x.
proof: Proof. intro lim. remember lim as up. rewrite Hequp. assert (lim <= up) by intuition. clear Hequp. revert lim H. induction up; intros. + assert (lim = 0) by intuition. subst. simpl in H2. specialize (H1 x H2). destruct H1 as [v [? ?]]. exists v. split; auto. apply in_or_app. right; auto. + destruct lim; simpl in H2. 1: specialize (H1 x H2); destruct H1 as [v [? ?]]; exists v; split; auto; apply in_or_app; right; auto. destruct l; simpl in H2. 1: specialize (H1 x H2); destruct H1 as [v [? ?]]; exists v; split; auto; apply in_or_app; right; auto. remember (graph_to_tree lim v). destruct p as [current tr]. destruct (eq_nat_dec current 0). 1: simpl in H2; specialize (H1 x H2); destruct H1 as [v' [? ?]]; exists v'; split; auto; apply in_or_app; right; auto. assert (lim - current <= up) by intuition. assert (Forall (vvalid G) l) by (apply Forall_tl in H0; auto). specialize (IHup _ H3 l (n + current + 1) (tr :: trL) H4). clear H3 H4. assert (forall x : Vertex, In x (flat_map leaves (tr :: trL)) -> exists v : Vertex, In v (forest_head (tr :: trL)) /\ reachable G v x). { intro y; intros. simpl in H3. simpl. apply in_app_or in H3. destruct H3. + destruct tr. 1: simpl in H3; exfalso; auto. assert (v0 = v). { clear -Heqp. destruct lim; simpl in Heqp. 1: inversion Heqp. remember (to_tree_list lim (nodup veq_dec (filter not_null_bool (map (dst G) (edge_func G v)))) (0, nil)). destruct p as [total sub_trees]. inversion Heqp. auto. } subst. exists v. simpl. split. 1: left; auto. pose proof (graph_to_tree_is_reachable lim v y). apply H4. - apply Forall_inv in H0; auto. - rewrite <- Heqp. simpl; auto. + specialize (H1 y H3). destruct tr. 1: apply H1. destruct H1 as [v1 [? ?]]. exists v1. split; auto. simpl. right; auto. } specialize (IHup H3 _ H2). clear H2 H3 n0. destruct IHup as [v' [? ?]]. exists v'. split; auto. apply in_app_or in H2. apply in_or_app. destruct H2. - left. simpl. right. auto. - simpl in H2. destruct tr. 1: right; auto. simpl in H2. destruct H2. 2: right; auto. subst. assert (v' = v). { destruct lim; simpl in Heqp. 1: inversion Heqp. remember (to_tree_list lim (nodup veq_dec (filter not_null_bool (map (dst G) (edge_func G v)))) (0, nil)). destruct p as [p1 p2]. inversion Heqp. auto. } subst. left. simpl. left; 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