proposition: Lemma uf_union_preserves_ufroot_same: forall (g1 g2: PreGraph Vertex Edge) (li1 : LstGraph g1 out_edge) (li2 : LstGraph g2 out_edge) (fin1: FiniteGraph g1) (fin2: FiniteGraph g2) (ma1: MathGraph g1 is_null) (ma2: MathGraph g2 is_null) u v a b, vvalid g1 u -> vvalid g1 v -> uf_union g1 u v g2 -> ufroot_same g1 a b -> ufroot_same g2 a b.
proof: Proof. intros. pose proof (uf_union_create_precons _ _ _ _ _ _ H H0). destruct H3 as [u_rt [v_rt [? [? [? [? [? ?]]]]]]]. destruct H2 as [ab_rt [? ?]]. destruct (EV ab_rt u_rt). { rewrite e in *. assert (ufroot_same g1 u a). { exists u_rt; split; trivial. } assert (ufroot_same g1 u b). { exists u_rt; split; trivial. } apply (uf_union_affected_inhabited _ _ _ _ _ _ H5 H6 H7 H8) in H1. destruct H1 as [rt [? ?]]. exists rt; split; apply H12, Union_introl; trivial. } destruct (EV ab_rt v_rt). { rewrite e in *. assert (ufroot_same g1 v a). { exists v_rt; split; trivial. } assert (ufroot_same g1 v b). { exists v_rt; split; trivial. } apply uf_union_sym in H1. apply (uf_union_affected_inhabited _ _ _ _ _ _ H6 H5 H8 H7) in H1. destruct H1 as [rt [? ?]]. exists rt; split; apply H12, Union_introl; trivial. } assert (ufroot_same g1 a a). { apply (ufroot_same_refl _ li1). apply (ufroot_vvalid_vert _ ab_rt); trivial. } assert (ufroot_same g1 a b). { exists ab_rt; split; trivial. } apply (uf_union_unaffected_inhabited _ _ _ _ a _ _ (ufroot_same g1 a) H5 H6) in H1; trivial. destruct H1 as [rt [? ?]]. exists rt; split; apply H12; trivial. - intro. apply (same_set_contra _ _ _ a H12); trivial. intro. apply (ufroot_same_false _ li1 a u ab_rt u_rt); trivial. apply ufroot_same_symm; trivial. - intro. apply (same_set_contra _ _ _ a H12); trivial. intro. apply (ufroot_same_false _ li1 a v ab_rt v_rt); trivial. apply ufroot_same_symm; trivial. - apply (ufroot_uf_set_in _ li1 a ab_rt); trivial. 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