proposition: Lemma uf_under_bound_redirect_parent: forall (g: UFGraph) root x (Hw : weak_valid g root) (Hv : vvalid g x) (Hr: ~ reachable g root x), uf_root g x root -> uf_under_bound id g -> uf_under_bound id (Graph_gen_redirect_parent g x root Hw Hv Hr).
proof: Proof. intros. hnf in H0 |-* . simpl. unfold uf_bound, id in *. intros. destruct p as [p l]. destruct H. destruct (redirect_to_root g (liGraph g) _ _ _ _ _ Hv Hr H4 H2 H3). - destruct H5. apply H0; auto. - destruct H5 as [? [l1 [? ?]]]. subst l. subst v. simpl. destruct H as [l2 ?]. destruct l2 as [? l2]. assert (a = x) by (destruct H as [[? _] ?]; simpl in H; auto). subst a. destruct l2. 1: destruct H as [[_ ?] ?]; simpl in H; subst root; exfalso; apply Hr; apply reachable_refl; auto. pose proof (reachable_by_path_merge _ _ _ _ _ _ _ H7 H). unfold path_glue in H3. simpl in H3. destruct H3 as [[_ ?] [? _]]. rewrite <- H5 in H3. pose proof (H0 _ H1 _ H6 H3). simpl in H8. clear -H8. rewrite app_length in *. simpl in *. intuition. Qed.
imports: Coq.Logic.Classical Coq.Lists.List Coq.Sets.Ensembles VST.msl.seplog VST.msl.log_normalize CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.Relation_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.reachable_computable CertiGraph.msl_application.Graph CertiGraph.msl_application.UnionFindGraph CertiGraph.msl_application.GList