proposition: Lemma diff_root_union: forall (g: Graph) x y x_root y_root, uf_root g x x_root -> uf_root g y y_root -> x_root <> y_root -> uf_union g x y (pregraph_gen_dst g (out_edge x_root) y_root).
proof: Proof. repeat intro. destruct H4; [pose proof (app_same_set H4); rewrite H6 in H2; inversion H2 |]. destruct H5; [pose proof (app_same_set H5); rewrite H6 in H3; inversion H3 |]. pose proof (P_Lst g (sound_gg g)). rename H6 into gLst. destruct H4 as [rt1 [? ?]]. assert (rt1 = x_root) by (rewrite H6 in H2; apply (@uf_root_unique _ _ _ _ g _ gLst x); auto). subst rt1. destruct H5 as [rt2 [? ?]]. assert (rt2 = y_root) by (rewrite H7 in H3; apply (@uf_root_unique _ _ _ _ g _ gLst y); auto). subst rt2. assert (forall z, Union Vertex S1 S2 z <-> uf_root (pregraph_gen_dst g (out_edge x_root) y_root) z y_root). { intro z; split; intro. - inversion H8; subst x0; unfold In in H9. + rewrite H6 in H9. apply (uf_root_gen_dst_diff _ gLst x y); auto. + rewrite H7 in H9. apply (uf_root_gen_dst_diff_preserve _ gLst x y); auto. - assert (~ reachable g y_root x_root) by (intro; apply H1; symmetry; destruct H0; apply H10; auto). assert (vvalid g x_root) by (destruct H; apply reachable_foot_valid in H; auto). apply gen_dst_uf_root in H8; auto. destruct H8; [left | right; rewrite H7; auto]. rewrite H6. split; auto. destruct H. apply H11. } assert (vvalid g x_root) by (destruct H; apply reachable_foot_valid in H; auto). assert (LstGraph (pregraph_gen_dst g (out_edge x_root) y_root) out_edge). apply gen_dst_preserve_lst; auto; intro; apply H1; destruct H0; symmetry. apply H11; auto. split; [|split]; intros. - right. exists y_root. split. 1: apply Union_intror; unfold In; auto. apply H8. - unfold uf_set_in in *. destruct H13; [left | right]; auto. destruct H13 as [rt [? ?]]. exists rt; split; auto. intro z. rewrite H14. assert (forall m, uf_root g m rt -> ~ reachable g m x_root). { repeat intro. pose proof (uf_root_reachable2 _ _ _ _ H H16). pose proof (uf_root_unique g gLst _ _ _ H15 H17). subst rt. clear H17 H16. apply H11. rewrite Same_set_spec. hnf. intro. rewrite H14. rewrite H6. intuition. } split; intro. + apply uf_root_gen_dst_preserve; auto. + pose proof H16. apply gen_dst_uf_root in H16; auto. 2: apply H15; rewrite H14 in H13; auto. destruct H16; auto. exfalso. pose proof (uf_root_reachable2 _ _ _ _ H H16). assert (uf_root (pregraph_gen_dst g (out_edge x_root) y_root) z y_root) by (apply (uf_root_gen_dst_diff _ gLst x y); auto). pose proof (uf_root_unique _ H10 _ _ _ H17 H19). subst rt. clear H18 H19. apply H12. rewrite Same_set_spec. hnf. intro. rewrite H14. rewrite H7. intuition. - unfold uf_set_in in H11. destruct H11. 1: right; left; auto. destruct H11 as [rt [? ?]]. destruct_eq_dec rt y_root; [left | right]. + subst rt. rewrite Same_set_spec. hnf. intro z. rewrite H8, H12. intuition. + right. exists rt. split; auto. intro z. rewrite H12. assert (forall m, uf_root (pregraph_gen_dst g (out_edge x_root) y_root) m rt -> ~ reachable g m x_root). { repeat intro. pose proof (uf_root_reachable2 _ _ _ _ H H15). pose proof (uf_root_gen_dst_diff g gLst _ _ _ _ _ H H0 H1 H16). pose proof (uf_root_unique _ H10 _ _ _ H14 H17). auto. } split; intro. * pose proof H15. apply gen_dst_uf_root in H15; auto. 2: rewrite H12 in H11; apply H14; auto. destruct H15; auto. exfalso. apply H14 in H16. auto. * apply uf_root_gen_dst_preserve; auto. intro. pose proof (uf_root_reachable2 _ _ _ _ H H16). pose proof (uf_root_unique g gLst _ _ _ H15 H17). subst rt. clear H14 H16 H17. rewrite H12 in H11. assert (uf_root g x_root x_root) by (destruct H; split; [apply reachable_refl | apply H14]; auto). pose proof (uf_root_gen_dst_diff g gLst _ _ _ _ _ H H0 H1 H14). pose proof (uf_root_unique _ H10 _ _ _ H11 H16). 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