proposition: Theorem is_tree_is_tree: forall root, vvalid G root -> EnumCovered Vertex (reachable G root) -> is_tree G root -> {tree | graph_tree_isomorphism_v G tree root}.
proof: Proof. intros. pose proof X as XX. destruct X as [ul [? ?]]. unfold Ensembles.In in H2. remember (graph_to_tree (2 * (length ul)) root) as nT. destruct nT as [n tree]. exists tree. split; [|split]; intros. + split; intro. - pose proof (finite_reachable_enumcovered_enumerable _ _ H XX). destruct H3 as [? [? ?]]. pose proof (graph_to_tree_contains_all_edges (2 * length ul) _ _ _ X H H0 H3 H4 H5). rewrite <- HeqnT in H6. apply H6. clear H6. destruct X as [l [? ?]]. unfold sizeOfEnum. simpl. unfold Ensembles.In in i. cut (length l <= length ul). 1: intuition. apply NoDup_incl_length; auto. repeat intro. apply H2. rewrite <- i. auto. - destruct H3 as [t' [? ?]]. assert (G |= s ~> d) by (apply (graph_to_tree_edge (2 * length ul) s d t' root); auto; rewrite <- HeqnT; simpl; auto). split; [|split]; auto. * apply find_tree_in_leaves in H3. apply (graph_to_tree_is_reachable (2 * length ul) root s); auto. rewrite <- HeqnT; simpl; auto. * apply forest_head_in_leaves in H4. pose proof (find_tree_in_leaves' _ _ _ H3 d H4). apply (graph_to_tree_is_reachable (2 * length ul) root d); auto. rewrite <- HeqnT; simpl; auto. + split; intros. - pose proof (finite_reachable_enumcovered_enumerable _ _ H XX). change (leaves tree) with (leaves (snd (n, tree))). rewrite HeqnT. apply (graph_to_tree_contains_reachable _ _ X); auto. destruct X as [l [? ?]]. unfold sizeOfEnum. simpl. unfold Ensembles.In in i. cut (length l <= length ul). 1: intuition. apply NoDup_incl_length; auto. repeat intro. apply H2. rewrite <- i. auto. - apply (graph_to_tree_is_reachable (2 * length ul)); auto. rewrite <- HeqnT; simpl; auto. + pose proof (graph_to_tree_nodup (2 * length ul) root H H0). rewrite <- HeqnT in H3. simpl in H3. 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