proposition: Lemma graph_gen_redirect_parent_ramify: forall (g: UFGraph) x r pa root (H: weak_valid g root) (Hv: vvalid g x) (Hn: ~ reachable g root x), vgamma g x = (r, pa) -> root <> null -> (vertices_at (vvalid g) g: pred) |-- vertex_at x (r, pa) * (vertex_at x (r, root) -* vertices_at (vvalid g) (Graph_gen_redirect_parent g x root H Hv Hn)).
proof: Proof. intros. assert (vgamma (Graph_gen_redirect_parent g x root H Hv Hn) x = (r, root)). { simpl in *. remember (updateEdgeFunc (dst (lg_gg g)) (x, tt) root (x, tt)). inversion H0. unfold vgamma, UnionFindGraph.vgamma. simpl. f_equal. unfold updateEdgeFunc in *. destruct (equiv_dec (x, tt) (x, tt)). 2: compute in c; exfalso; apply c; auto. subst a. destruct (SGBA_VE root null); [exfalso| ]; auto. } apply vertices_at_ramif_1; auto. eexists. split; [|split]. - apply Ensemble_join_Intersection_Complement. + unfold Included, In; intro y. intros. subst. auto. + intros; destruct_eq_dec x x0; auto. - apply Ensemble_join_Intersection_Complement. + unfold Included, In; intro y. intros. subst. auto. + intros; destruct_eq_dec x x0; auto. - rewrite vertices_identical_spec. simpl. intros. change (lg_gg g) with (g: LGraph). rewrite Intersection_spec in H3. destruct H3. unfold Complement, In in H4. unfold vgamma, UnionFindGraph.vgamma. simpl. unfold updateEdgeFunc. destruct (equiv_dec (x, tt) (x0, tt)); auto. compute in e. exfalso. inversion e. auto. 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