proposition: Lemma graph_gen_redirect_parent_findS: forall (g1 g2: UFGraph) x r1 r2 pa pa' (H: weak_valid g2 pa') (Hv: vvalid g2 x) (Hn: ~ reachable g2 pa' x), vvalid g1 x -> vgamma g1 x = (r1, pa) -> pa <> x -> vgamma g2 x = (r2, pa) -> findS g1 pa g2 -> uf_root g2 pa pa' -> findS g1 x (Graph_gen_redirect_parent g2 x pa' H Hv Hn).
proof: Proof. intros. hnf. simpl. destruct H4 as [? [? ?]]. hnf in H4. simpl in H4. unfold predicate_vvalid, predicate_weak_evalid in H4. split; [|split]. - assert (forall v, ~ reachable (lg_gg g1) x v -> ~ reachable (lg_gg g1) pa v). { intros. intro. apply H8. pose proof (gamma_parent_reachable_included g1 x r1 pa H0 H1). apply H10. auto. } assert (forall v, ~ reachable (lg_gg g1) pa v <-> ~ reachable (lg_gg g1) x v \/ x = v). { intros. split; intros. - destruct_eq_dec x v; [right | left]; auto. intro. apply H9. apply reachable_ind.reachable_ind in H11. destruct H11. 1: exfalso; auto. destruct H11 as [z [[_ [_ ?]] [? ?]]]. rewrite (dst_step g1 (liGraph g1) x pa) in H11; auto; [subst pa | apply (vgamma_not_dst g1 x r1)]; auto. - destruct H9. + apply H8; auto. + subst v. apply vgamma_not_reachable with r1; auto. } hnf. simpl. unfold predicate_vvalid, predicate_weak_evalid. simpl. destruct H4 as [? [? [? ?]]]. split; [|split; [|split]]; intros. + split; intros; destruct H13; split; auto; apply H8 in H14; pose proof (conj H13 H14); [rewrite H4 in H15 | rewrite <- H4 in H15]; destruct H15; auto. + split; intros; destruct H13. * pose proof (H8 _ H14). pose proof (conj H13 H15). rewrite H10 in H16. destruct H16. rewrite H9 in H17. destruct H17. 1: split; auto. symmetry in H17. pose proof (conj H17 H16). rewrite (@only_one_edge _ _ _ _ g2 _ (liGraph g2)) in H18; auto. subst e. pose proof (vvalid_src_evalid _ (liGraph g1) _ H0). destruct H18 as [? _]. unfold UFGraph_LGraph in H18. rewrite H18 in H14. exfalso. apply H14. apply reachable_refl. auto. * pose proof (H8 _ H14). pose proof (conj H13 H15). rewrite <- H10 in H16. destruct H16. rewrite H9 in H17. destruct H17. 1: split; auto. symmetry in H17. pose proof (conj H17 H16). rewrite (@only_one_edge _ _ _ _ g1 _ (liGraph g1)) in H18; auto. subst e. pose proof (vvalid_src_evalid _ (liGraph g2) _ Hv). destruct H18 as [? _]. unfold UFGraph_LGraph in H18. rewrite H18 in H14. exfalso. apply H14. apply reachable_refl. auto. + destruct H13, H14. apply H8 in H15. apply H8 in H16. apply H11; auto. + unfold updateEdgeFunc. destruct (equiv_dec (out_edge x) e). * unfold Equivalence.equiv in e0. subst e. pose proof (vvalid_src_evalid _ (liGraph g1) _ H0). destruct H15. unfold UFGraph_LGraph in H15. destruct H13. exfalso. apply H17. rewrite H15. apply reachable_refl; auto. * destruct H13, H14. apply H8 in H15. apply H8 in H16. apply H12; auto. - apply (graph_gen_redirect_parent_equiv _ _ _ r1 pa); auto. - apply H7. 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