proposition: Lemma reachable_uf_equiv_connected: forall (g1 g2: UFGraph) u v, uf_equiv g1 g2 -> reachable g1 u v -> connected g2 u v.
proof: Proof. intros. pose proof (reachable_foot_valid _ _ _ H0). pose proof (reachable_head_valid _ _ _ H0). destruct H. assert (EnumEnsembles.EnumCovered Z (evalid g2)). { apply EnumEnsembles.Enumerable_is_EnumCovered, finiteE. } assert (EnumEnsembles.EnumCovered Z (evalid g1)). { apply EnumEnsembles.Enumerable_is_EnumCovered, finiteE. } assert (vvalid g2 u). { apply H; trivial. } assert (vvalid g2 v). { apply H; trivial. } pose proof (uf_root_always_exists g1 (liGraph g1) u X0 H2). pose proof (uf_root_always_exists g1 (liGraph g1) v X0 H1). pose proof (uf_root_always_exists g2 (liGraph g2) u X H4). pose proof (uf_root_always_exists g2 (liGraph g2) v X H5). destruct H6 as [ur1 ?]. destruct H7 as [vr1 ?]. destruct H8 as [ur2 ?]. destruct H9 as [vr2 ?]. pose proof (H3 _ _ _ H6 H8). pose proof (H3 _ _ _ H7 H9). pose proof (uf_root_reachable _ _ _ _ H0 H7). pose proof (uf_root_unique _ _ _ _ _ H6 H12). subst ur1. subst vr1. subst vr2. clear H6 H7. destruct H8 as [? _]. destruct H9 as [? _]. apply reachable_implies_connected in H6. apply reachable_implies_connected in H7. apply connected_symm in H7. apply (connected_trans _ _ _ _ H6 H7). Qed.
imports: CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.UnionFind CertiGraph.msl_application.ArrayGraph CertiGraph.unionfind.env_unionfind_arr CertiGraph.graph.undirected_graph