proposition: Lemma uf_root_gen_dst: forall x z y root, uf_root g y root -> ~ reachable g y x -> reachable g z x -> uf_root (pregraph_gen_dst g (out_edge x) y) z root.
proof: Proof. intros. assert (vvalid g x) by (apply reachable_foot_valid in H1; auto). assert (vvalid g y) by (destruct H; apply reachable_head_valid in H; auto). split; intros. - destruct H1 as [[p l1] ?]. destruct H as [[[q l2] ?] ?]. exists (p, l1 ++ (out_edge x) :: l2). assert ((p, l1 ++ (out_edge x) :: l2) = path_glue (p, l1) (x, (out_edge x) :: l2)) by (unfold path_glue; simpl; auto). rewrite H5. clear H5. apply reachable_by_path_merge with x. + rewrite no_edge_gen_dst_equiv; auto. intro. simpl in H5. apply in_split in H5. destruct H5 as [l3 [l4 ?]]. subst l1. assert (paths_meet_at g (p, l3) (x, out_edge x :: l4) x). { hnf; split. 2: simpl; auto. destruct H1 as [_ [? _]]. apply pfoot_split in H1. pose proof (vvalid_src_evalid _ _ _ H2). destruct H5. rewrite H5 in H1. auto. } assert ((p, l3 ++ out_edge x :: l4) = path_glue (p, l3) (x, (out_edge x) :: l4)) by (unfold path_glue; simpl; auto). rewrite H6 in H1; clear H6. apply reachable_by_path_split_glue with (n := x) in H1; auto. clear H5. destruct H1. apply no_loop_path in H5. inversion H5. + assert ((x, out_edge x :: l2) = path_glue (x, out_edge x :: nil) (y, l2)) by (unfold path_glue; simpl; auto). rewrite H5; clear H5. apply reachable_by_path_merge with y. * assert (valid_path (pregraph_gen_dst g (out_edge x) y) (x, out_edge x :: nil)). { simpl. unfold strong_evalid. simpl. unfold updateEdgeFunc. destruct (equiv_dec (out_edge x) (out_edge x)). 2: compute in c; exfalso; apply c; auto. pose proof (vvalid_src_evalid _ _ _ H2). destruct H5. rewrite H5. split; [|split; [|split]]; auto. } split; split; auto. -- simpl. unfold updateEdgeFunc. destruct (equiv_dec (out_edge x) (out_edge x)); auto. compute in c; exfalso; apply c; auto. -- rewrite path_prop_equiv; auto. * assert (q = y) by (destruct H as [[? _] _]; simpl in H; auto). subst q. rewrite no_edge_gen_dst_equiv; auto. intro. simpl in H5. apply H0. apply (reachable_path_in g (y, l2) _ root); auto. right; simpl; exists (out_edge x); split; auto; left. pose proof (vvalid_src_evalid _ _ _ H2); destruct H6; auto. - destruct H. apply H5. rewrite not_reachable_gen_dst_equiv in H4; auto. pose proof (vvalid_src_evalid _ _ _ H2). destruct H6. rewrite H6. intro; apply H0. apply reachable_trans with root; auto. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.Ensembles_ext CertiGraph.lib.EnumEnsembles CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.MathGraph CertiGraph.graph.LstGraph CertiGraph.graph.FiniteGraph CertiGraph.graph.reachable_computable