proposition: Lemma graph_to_tree_is_reachable': forall lim, (forall root x, vvalid G root -> In x (leaves (snd (graph_to_tree lim root))) -> reachable G root x) /\ (forall root l n trL, Forall (reachable G root) l -> (forall x, In x (flat_map leaves trL) -> reachable G root x) -> forall x, In x (flat_map leaves (snd (to_tree_list lim l (n, trL)))) -> reachable G root x).
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. + assert (lim = 0) by intuition; subst; simpl in H1; exfalso; auto. + assert (lim = 0) by intuition; subst; simpl in H2; apply H1; auto. + destruct lim. 1: simpl in H1; exfalso; auto. simpl in H1. destruct lim; simpl in H1. 1: destruct H1; [subst | exfalso; auto]; apply reachable_refl; auto. remember (nodup veq_dec (filter not_null_bool (map (dst G) (edge_func G root)))). destruct l. 1: simpl in H1; destruct H1; [subst | exfalso; auto]; apply reachable_refl; auto. remember (graph_to_tree lim v). destruct p as [current tr]. destruct (eq_nat_dec current 0). 1: simpl in H1; destruct H1; [subst; apply reachable_refl | exfalso]; auto. remember (to_tree_list (lim - current) l (current + 1, tr :: nil)). destruct p as [total sub_trees]. simpl in H1. destruct H1. 1: subst; apply reachable_refl; auto. assert (Forall (reachable G root) (v :: l)). { rewrite Forall_forall. intro y; intros. rewrite Heql in H2. rewrite nodup_In in H2. apply in_edge_func_edge in H2. apply reachable_edge with root; auto. apply reachable_refl; auto. } assert (lim - current <= up) by intuition. destruct (IHup _ H3) as [_ ?]. apply (H4 root l (current + 1) (tr :: nil)); clear H4. - apply Forall_tl in H2; auto. - simpl. intro y; intros. rewrite app_nil_r in H4. assert (lim <= up) by intuition. destruct (IHup _ H5) as [? _]. apply reachable_trans with v. * apply Forall_inv in H2; auto. * apply (H6 v). 1: apply Forall_inv in H2; apply reachable_foot_valid in H2; auto. rewrite <- Heqp. simpl. auto. - rewrite <- Heqp0. simpl. auto. + destruct lim; simpl in H2. 1: apply H1; auto. destruct l. 1: simpl in H2; apply H1; auto. remember (graph_to_tree lim v). destruct p as [current tr]. assert (lim - current <= up) by intuition. destruct (eq_nat_dec current 0). 1: simpl in H2; apply H1; auto. destruct (IHup _ H3) as [_ ?]. apply (H4 root l (n + current + 1) (tr :: trL)); auto; clear H4 H3. - apply Forall_tl in H0; auto. - intro y; intros. simpl in H3. apply in_app_or in H3. destruct H3. 2: apply H1; auto. assert (lim <= up) by intuition. destruct (IHup _ H4) as [? _]. apply reachable_trans with v. * apply Forall_inv in H0; auto. * apply (H5 v). 1: apply Forall_inv in H0; apply reachable_foot_valid in H0; auto. rewrite <- Heqp. simpl. 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