proposition: Lemma findS_preserves_vgamma: forall (g1 g2: UFGraph) x r pa, vvalid g1 x -> vgamma g1 x = (r, pa) -> pa <> x -> findS g1 pa g2 -> vgamma g2 x = (r, pa).
proof: Proof. intros. assert (Hr: ~ reachable g1 pa x) by (apply vgamma_not_reachable with r; auto). unfold vgamma in *. destruct (projT2 isNullDec (dst g1 (out_edge x))). 1: inversion H0; exfalso; auto. rewrite <- H0. destruct H2 as [? [[? ?] ?]]. f_equal. - assert (vvalid g2 x) by (rewrite <- H3; auto). specialize (H5 x H H6). unfold UFGraph_LGraph. rewrite H5. auto. - assert (evalid (predicate_partialgraph (lg_gg g1) (fun n : V => ~ reachable (lg_gg g1) pa n)) (out_edge x)). { simpl. hnf. pose proof (vvalid_src_evalid _ (liGraph g1) _ H). unfold UFGraph_LGraph in H6. destruct H6. rewrite H6. split; auto. } destruct H2 as [_ [? [_ ?]]]. pose proof H6. rewrite H2 in H8. clear H2. specialize (H7 _ H6 H8). simpl in H7. unfold UFGraph_LGraph. rewrite <- H7. destruct (projT2 isNullDec (dst (lg_gg g1) (out_edge x))); [exfalso |]; auto. Qed.
imports: Coq.Sets.Ensembles Coq.Lists.List CertiGraph.lib.EquivDec_ext CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_computable CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph CertiGraph.graph.MathGraph CertiGraph.graph.LstGraph CertiGraph.graph.UnionFind