proposition: Lemma graph_to_tree_edge': forall lim, (forall s d t root, tree_match_graph_edges s d (snd (graph_to_tree lim root)) t) /\ (forall s d t root l n trL, (forall m, In m l -> G |= root ~> m) -> (forall m, In m (forest_head trL) -> G |= root ~> m) -> tree_match_graph_edges s d (T root trL) t -> tree_match_graph_edges s d (T root (snd (to_tree_list lim l (n, trL)))) t).
proof: Proof. intro lim. remember lim as up. rewrite Hequp. assert (lim <= up) by intuition. clear Hequp. revert lim H. induction up; split; intros; hnf; intros. + assert (lim = 0) by intuition; subst; simpl in H0; inversion H0. + assert (lim = 0) by intuition; subst. simpl in H3. apply H2; auto. + destruct lim; simpl in H0. 1: inversion H0. destruct lim; simpl in H0. 1: inversion H0; [| inversion H5]; clear v t0 H2 H5; subst s; subst t; simpl in H1; exfalso; auto. remember (nodup veq_dec (filter not_null_bool (map (dst G) (edge_func G root)))). destruct l; simpl in H0. 1: inversion H0; [| inversion H5]; clear v t0 H2 H5; subst s; subst t; simpl in H1; exfalso; auto. remember (graph_to_tree lim v). destruct p as [current tr]. destruct (eq_nat_dec current 0). 1: inversion H0; subst; [simpl in H1 | simpl in H5]; exfalso; auto. remember (to_tree_list (lim - current) l (current + 1, tr :: nil)). destruct p as [total sub_trees]. simpl in H0. assert (lim - current <= up) by intuition. destruct (IHup _ H2) as [_ ?]. specialize (H3 s d t root l (current + 1) (tr :: nil)). assert (forall m : Vertex, In m (v :: l) -> G |= root ~> m). { intros. rewrite Heql in H4. rewrite nodup_In in H4; apply in_edge_func_edge; auto. } assert (forall m : Vertex, In m (forest_head (tr :: nil)) -> G |= root ~> m). { intros. clear H1 H2 H3. destruct lim; simpl in Heqp. 1: inversion Heqp; subst; simpl in H5; exfalso; auto. remember (to_tree_list lim (nodup veq_dec (filter not_null_bool (map (dst G) (edge_func G v)))) (0, nil)). destruct p as [total1 sub_trees1]. inversion Heqp. subst. simpl in H5. destruct H5. 2: exfalso; auto. subst. apply H4. simpl; left; auto. } apply H3; auto. - intros. apply H4. apply in_cons; auto. - repeat intro. assert (lim <= up) by intuition. destruct (IHup _ H8) as [? _]. specialize (H9 s d t v). rewrite <- Heqp in H9. simpl in H9. inversion H6. * subst. unfold subtrees in H1. apply H5; auto. * subst. destruct H13. 2: exfalso; auto. rewrite <- H10 in *. apply H9; auto. - rewrite <- Heqp0. simpl. auto. + destruct lim; simpl in H3. 1: apply H2; auto. destruct l. 1: simpl in H3; apply H2; auto. remember (graph_to_tree lim v). destruct p as [current tr]. destruct (eq_nat_dec current 0). 1: simpl in H3; apply H2; auto. assert (lim - current <= up) by intuition. destruct (IHup _ H5) as [_ ?]. assert (forall m : Vertex, In m (forest_head (tr :: trL)) -> G |= root ~> m). { intros. destruct lim; simpl in Heqp; inversion Heqp; subst. 1: simpl in H7; apply H1; auto. remember (to_tree_list lim (nodup veq_dec (filter not_null_bool (map (dst G) (edge_func G v)))) (0, nil)). destruct p as [total1 sub_trees1]. inversion H9. subst. simpl in H7. destruct H7. 2: apply H1; auto. subst v. apply H0. simpl; left; auto. } specialize (H6 s d t root l (n + current + 1) (tr :: trL)). apply H6; auto. 1: intros; apply H0; simpl; right; auto. repeat intro. clear H3 H4 H5 H6. inversion H8. - subst. unfold subtrees in H9. apply H7; auto. - subst. simpl in H6. destruct H6. * rewrite <- H3 in *. assert (lim <= up) by intuition. destruct (IHup _ H4) as [? _]. specialize (H5 s d t v). apply H5; auto. rewrite <- Heqp. simpl; auto. * apply H2; auto. apply FT_succ with tr'; 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