proposition: Lemma graph_to_tree_contains_all_edges': forall lim root s d, vvalid G root -> is_tree G root -> reachable G root s -> reachable G root d -> G |= s ~> d -> (forall H: Enumerable Vertex (reachable G root), 2 * sizeOfEnum H - 1 <= lim -> graph_match_tree_edges s d (snd (graph_to_tree lim root))) /\ (forall n l trL (H: Enumerable Vertex (reachable_through_set G l)), 2 * sizeOfEnum H <= lim -> (forall y, In y l -> step G root y /\ vvalid G y) -> (reachable_through_set G l d \/ graph_match_tree_edges s d (T root trL)) -> NoDup l -> graph_match_tree_edges s d (T root (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 H5 as XX; destruct H5 as [? [? ?]]; unfold sizeOfEnum in H6; simpl in H6; unfold Ensembles.In in i. + assert (lim = 0) by intuition. subst. rewrite <- i in H2. destruct x. inversion H2. simpl in H6; exfalso; intuition. + assert (lim = 0) by intuition. subst. simpl. destruct H8; auto. rewrite <- i in H5. destruct x. inversion H5. simpl in H6. exfalso; intuition. + remember (graph_to_tree lim root). destruct p as [num t]. simpl. destruct lim. 1: rewrite <- i in H2; destruct x; [inversion H2 | simpl in H6; 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 _ _ x); auto). destruct (IHup _ H5 _ _ _ H0 H1 H2 H3 H4) as [_ ?]. specialize (H8 0 _ nil X H7). rewrite <- Heql in H8. 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 *. apply H8. - intros. rewrite Heql in H9. rewrite nodup_In in H9. apply in_edge_func_edge in H9. destruct H9 as [? [? ?]]. split; auto. - left. rewrite Heql. rewrite <- reachable_through_set_nonull_nodup. apply (reachable_ind.step_list_step_reachable _ root s); auto. - rewrite Heql. apply NoDup_nodup. + destruct lim. 1: simpl; destruct H8; auto; rewrite <- i in H5; destruct x; [inversion H5 | simpl in H6; exfalso; intuition]. destruct l. 1: simpl; destruct H8; auto; destruct H5 as [? [? ?]]; inversion H5. 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 x = 0) by intuition. assert (x = nil) by (destruct x; auto; inversion H8). subst. assert (reachable_through_set G (v :: l) v) by (assert (In v (v :: l)) by apply in_eq; exists v; split; auto; apply reachable_by_refl; auto; destruct (H7 _ H10); auto). rewrite <- i in H10. inversion H10. - assert (In v (v :: l)) by apply in_eq. pose proof (H7 _ H5); destruct H10. 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 x; split; auto; unfold Ensembles.In; intros; rewrite i; exists v; split; auto). assert (2 * sizeOfEnum X - 1 <= lim). { clear -n0 i H6 X H5. destruct X as [l' [? ?]]. unfold sizeOfEnum. simpl. unfold Ensembles.In in i0. assert (incl l' x) by (intro; rewrite i, i0; intros; exists v; split; auto). assert (length l' <= length x) by (apply NoDup_incl_length; auto). intuition. } assert (reachable G v d -> graph_match_tree_edges s d (T root ((snd (graph_to_tree lim v)) :: nil))). { assert (EnumCovered Vertex (reachable G v)) by (apply Enumerable_is_EnumCovered; auto). intros. destruct (reachable_decidable_prime G v H11 X0 s). + assert (lim <= up) by intuition. destruct (IHup _ H15 v s d H11 H12 r H14 H4) as [? _]. clear IHup. specialize (H16 X H13). apply (graph_match_tree_edges_in _ _ _ _ H16). apply in_eq. + clear IHup. apply reachable_ind.reachable_ind in H2. destruct H2. - subst s. assert (d = v) by (destruct H4 as [? [? ?]]; apply (is_tree_step_eq root d v d); auto; apply reachable_refl; auto). subst d. exists (T root (snd (graph_to_tree lim v) :: nil)). split. 1: apply FT_base. rewrite <- Heqp0. unfold snd. clear -Heqp0 n1. destruct lim; simpl in Heqp0. inversion Heqp0. 1: exfalso; auto. remember (nodup veq_dec (filter not_null_bool (map (dst G) (edge_func G v)))). destruct (to_tree_list lim l (0, nil)). inversion Heqp0. simpl. left; auto. - exfalso. apply n2. destruct H2 as [z [? [? ?]]]. assert (z = v) by (apply (is_tree_step_eq root z v d); auto; [destruct H2 as [? [? ?]] | apply reachable_edge with s]; auto). subst z; auto. } assert (Hs: forall y : Vertex, reachable G v y <-> In y (leaves tr)). { intro. split; intros. + apply (graph_to_tree_contains_reachable lim _ X) in H15; auto. rewrite <- Heqp0 in H15. simpl in H15; auto. + apply (graph_to_tree_is_reachable lim); auto. rewrite <- Heqp0. simpl; auto. } clear X H13. assert (lim - current <= up) by intuition. destruct (IHup _ H13 _ _ _ H0 H1 H2 H3 H4) as [_ ?]. specialize (H15 (n + current + 1) l (tr :: trL)). clear H13 IHup. assert (Enumerable Vertex (reachable_through_set G l)). { apply (reachable_through_set_enum _ (v :: l)); [apply Enumerable_is_EnumCovered; exists x; split; auto | apply incl_tl, incl_refl |]. hnf. intros. assert (In x0 (v :: l)) by (right; auto). apply H7 in H16. destruct H16. hnf. right; auto. } assert (2 * sizeOfEnum X <= lim - current) by (apply (sizeOfEnum_cons root l X v x lim current tr); auto). specialize (H15 X H13). rewrite Heqp. apply H15; [intros; apply H7; right | | apply NoDup_cons_1 in H9]; auto. clear H15 X H13. rewrite reachable_through_set_eq in H8. destruct H8 as [[? | ?] | ?]. 2: left; auto. * specialize (H14 H8). right. rewrite <- Heqp0 in H14. simpl in H14. apply graph_match_tree_edges_cons_1; auto. * right. apply graph_match_tree_edges_cons_2; 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