proposition: Lemma graph_gen_redirect_parent_equiv': forall (g1 g2: UFGraph) x root, uf_equiv g1 g2 -> vvalid g2 x -> (~ reachable g2 root x) -> uf_root g2 x root -> uf_equiv g1 (pregraph_gen_dst g2 (out_edge x) root).
proof: Proof. intros. apply (@uf_equiv_trans _ _ _ _ g2 _ (liGraph g2) _ (maGraph g2) (finGraph g2)); auto. split; intro y; simpl; [intuition |]. intros. assert (Decidable (reachable g2 y x)) by (apply Graph_reachable_dec; left; destruct H3; apply reachable_head_valid in H3; auto). apply decidable_prop_decidable in H5. destruct H5. - pose proof (uf_root_gen_dst_same g2 (liGraph g2) _ _ _ H2 H1 H5). simpl in H6. pose proof (uf_root_unique _ (gen_dst_preserve_lst g2 (liGraph g2) _ _ H1 H0) _ _ _ H4 H6). subst r2. pose proof (uf_root_reachable _ _ _ _ H5 H2). apply (uf_root_unique g2 (liGraph g2) _ _ _ H3 H7). - apply (uf_root_unique _ (gen_dst_preserve_lst g2 (liGraph g2) _ _ H1 H0) y); auto. apply (uf_root_gen_dst_preserve g2 (liGraph g2)); auto. Qed.
imports: Coq.Sets.Ensembles Coq.Lists.List CertiGraph.lib.EquivDec_ext CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_computable CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph CertiGraph.graph.MathGraph CertiGraph.graph.LstGraph CertiGraph.graph.UnionFind