proposition: Lemma fr_O_backward_edge_prop: forall from to p g1 g2 roots, from <> to -> graph_has_gen g1 to -> sound_gc_graph g1 -> no_dangling_dst g1 -> forward_p_compatible p roots g1 from -> forward_relation from to O (forward_p2forward_t p roots g1) g1 g2 -> copied_vertex_prop g1 from to -> gen_unmarked g1 to -> edge_from_gen_cond p to -> backward_edge_prop g1 roots from to -> backward_edge_prop g2 (upd_roots from to p g1 roots) from to.
proof: Proof. pose (H3:=True). intros from to p g1 g2 roots H H0 H1 H2 H4 H5 H6 Hu Hc H7. assert (He: forall e, evalid g1 e -> fst e <> new_copied_v g1 to). { intros. destruct H1 as [_ [? _]]. red in H1. rewrite H1 in H8. destruct H8. eapply graph_has_v_not_eq in H8; eauto. } unfold upd_roots, upd_root. pose proof H1. destruct H8 as [Hv _]. red in Hv. destruct p; simpl in H4, H5. - destruct (Znth z roots) eqn:? ; [destruct s|]; simpl in *; rewrite ?Heqr; inversion H5; subst; clear H5; try (rewrite <- Heqr, upd_Znth_unchanged'); auto. + rewrite if_false; auto. rewrite <- Heqr, upd_Znth_unchanged'; auto. + rewrite if_true, H11; auto. red in H7 |-* ; intros. specialize (H7 _ H5 H8 H9). rewrite reachable_from_roots in *. destruct H7 as [i [r [? [? ?]]]]. pose proof I. rewrite upd_Znth_Zlength; auto. destruct (Z.eq_dec i z). * exists i, (copied_vertex (vlabel g2 v)). subst i. rewrite upd_Znth_same; auto. do 2 (split; auto). rewrite Heqr in H10. inversion H10. subst v. pose proof H12. apply reachable_foot_valid in H14. eapply copied_vertex_reachable in H12; eauto. destruct H12; auto. rewrite Hv in H14. specialize (H6 _ H14 H12). destruct H6 as [_ [_ [? _]]]. rewrite H6 in H8. now rewrite H8 in H. * exists i, r. split3; auto. clear - n H10. list_solve. + rewrite if_true, H10; auto. red in H7 |-* ; intros. simpl in H5. rewrite pcv_evalid_iff in H5. simpl in H9. assert (Hi: ~ vvalid g1 (new_copied_v g1 to)). { rewrite Hv. intro. now apply (graph_has_v_not_eq _ to) in H11. } destruct H5. * rewrite pcv_dst_old in H9. 2: apply He; auto. specialize (H7 _ H5 H8 H9). rewrite reachable_from_roots in *. destruct H7 as [i [r [? [? ?]]]]. pose proof I. pose proof H12. rewrite upd_Znth_Zlength; auto. apply reachable_head_valid in H14. destruct (Z.eq_dec i z). -- exists i, (new_copied_v g1 to). subst i. rewrite upd_Znth_same; auto. do 2 (split; auto). rewrite Heqr in H11. inversion H11. subst v. simpl. pose proof H12. apply reachable_head_valid in H15. rewrite (pcv_reachable_new _ _ (new_copied_v g1 to)) in H12; auto. destruct H12 as [? | [? ?]]; auto. now rewrite <- H12, H8 in H. -- exists i, r. rewrite upd_Znth_diff; auto. do 2 (split; auto). simpl. rewrite pcv_reachable_old; auto. * rewrite reachable_from_roots. pose proof I. rewrite upd_Znth_Zlength; auto. exists z, (new_copied_v g1 to). rewrite upd_Znth_same; auto. do 2 (split; auto). simpl. rewrite in_map_iff in H5. destruct H5 as [ve [? ?]]. subst e. simpl. apply reachable_refl. rewrite pcv_vvalid_iff. now right. - simpl. destruct p as [x n]. destruct H4 as [? [? [? ?]]]. rewrite H9 in H5. simpl in H5. assert (forall e, Znth n (make_fields g1 x) = inr e -> fst e = x) by (intros; apply make_fields_Znth_edge in H11; auto; now subst e). assert (forall e, Znth n (make_fields g1 x) = inr e -> graph_has_e g1 e). { destruct H1 as [? [? [? _]]]. red in H1, H12, H13. intros. split; rewrite H11; auto. unfold get_edges. rewrite <- filter_sum_right_In_iff, <- H14. apply Znth_In. now rewrite make_fields_eq_length. } assert (forall e, Znth n (make_fields g1 x) = inr e -> evalid g1 e). { intros. destruct H1 as [_ [? _]]. red in H1. rewrite H1. now apply H12. } assert (Ht: forall e, evalid g1 e -> vgeneration (fst e) = to -> raw_mark (vlabel g1 (fst e)) = false). { intros. red in Hu. destruct e as [v ?]. simpl in *. destruct H1 as [_ [? _]]. red in H1. rewrite H1 in H14. destruct H14. simpl in H14. destruct v as [gen idx]. simpl in *. subst gen. destruct H14. simpl in *. now specialize (Hu H14 _ H15). } destruct (Znth n (make_fields g1 x)) eqn:?; [destruct s |]; simpl in H5; inversion H5; subst; clear H5; try easy. + red in H7 |-* ; intros. subst new_g. destruct_eq_dec e0 e. * exfalso. subst e0. simpl in H15. rewrite updateEdgeFunc_eq in H15. assert (graph_has_e g1 e) by (now apply H12). red in H2. destruct H16. specialize (H2 _ H16 _ H18). specialize (H6 _ H2 H17). destruct H6 as [_ [? _]]. now rewrite <- H15, H6 in H. * rewrite reachable_from_roots. simpl in *. rewrite updateEdgeFunc_neq in H15; auto. specialize (H7 _ H5 H14 H15). rewrite reachable_from_roots in H7. destruct H7 as [i [r [? [? ?]]]]. eapply copied_vertex_pgd_reachable in H19; eauto. exists i, r. do 2 (split; auto). destruct H19; auto. rewrite Ht in H19; auto. easy. + red in H7 |-* ; intros. subst new_g. simpl in H5, H15. destruct_eq_dec e0 e. * exfalso. subst e0. rewrite updateEdgeFunc_eq in H15. unfold new_copied_v in H15. simpl in H15. now rewrite <- H15 in H. * rewrite updateEdgeFunc_neq in H15; auto. rewrite reachable_from_roots. simpl. rewrite pcv_evalid_iff in H5. assert (Hi: ~ vvalid g1 (new_copied_v g1 to)). { rewrite Hv. intro. now apply (graph_has_v_not_eq _ to) in H18. } assert (He': fst e <> new_copied_v g1 to) by (apply He, H13; auto). destruct H5. -- rewrite pcv_dst_old in H15. 2: apply He; auto. specialize (H7 _ H5 H14 H15). rewrite reachable_from_roots in H7. destruct H7 as [i [r [? [? ?]]]]. exists i, r. do 2 (split; auto). pose proof H19. apply reachable_head_valid in H20. rewrite <- (pcv_reachable_old _ (dst g1 e) (new_copied_v g1 to)) in H19; auto. assert (reachable (lgraph_copy_v g1 (dst g1 e) to) r (fst e0)) by easy. apply (copied_vertex_pgd_reachable _ e to) in H21; simpl in *. ++ rewrite pcv_dst_old in H21; auto. rewrite ucov_copied_vertex in H21. destruct H21; auto. rewrite ucov_not_eq in H21. 2: intro; now rewrite H22, H14 in H. rewrite lacv_vlabel_old in H21. 2: apply He; auto. rewrite Ht in H21; auto. easy. ++ apply lcv_sound; auto. ++ rewrite pcv_dst_old; auto. apply lcv_copied_vertex_prop; auto. ++ rewrite pcv_evalid_iff. left. apply H13; auto. ++ rewrite pcv_dst_old; auto. apply ucov_rawmark. -- rewrite in_map_iff in H5. destruct H5 as [ve [? ?]]. subst e0. simpl in *. assert (evalid g1 e) by (apply H13; auto). assert (vgeneration (fst e) = to). { apply make_fields_Znth_edge in Heqf; auto. subst e. now simpl. } specialize (H7 _ H5 H19 (eq_refl (vgeneration (dst g1 e)))). rewrite reachable_from_roots in H7. destruct H7 as [i [r [? [? ?]]]]. exists i, r. do 2 (split; auto). pose proof H21. apply reachable_head_valid in H22. rewrite <- (pcv_reachable_old _ (dst g1 e) (new_copied_v g1 to)) in H21; auto. assert (reachable (lgraph_copy_v g1 (dst g1 e) to) r (fst e)) by easy. apply (copied_vertex_pgd_reachable _ e to) in H23; simpl in *. ++ rewrite pcv_dst_old in H23; auto. rewrite ucov_copied_vertex, ucov_not_eq in H23. 2: intro; now rewrite H24, H19 in H. rewrite lacv_vlabel_old in H23; auto. rewrite Ht in H23; auto. destruct H23; [|easy]. apply reachable_trans with (fst e); auto. exists (fst e, [e]). split; split; simpl; auto. 3: red; rewrite Forall_forall; intros; auto. 1: rewrite updateEdgeFunc_eq; auto. destruct H1 as [? [? [? _]]]. red in H25. split. 1: rewrite pcv_src_old; auto. red. simpl. red in H1, H24. rewrite updateEdgeFunc_eq. rewrite pcv_src_old; auto. split3. ** rewrite pcv_evalid_iff. now left. ** rewrite pcv_vvalid_iff, H25. left. rewrite H1. rewrite H24 in H5. now destruct H5. ** rewrite pcv_vvalid_iff. now right. ++ apply lcv_sound; auto. ++ rewrite pcv_dst_old; auto. apply lcv_copied_vertex_prop; auto. ++ rewrite pcv_evalid_iff. now left. ++ rewrite pcv_dst_old; auto. apply ucov_rawmark. Qed.
imports: Coq.ZArith.ZArith Coq.Program.Basics compcert.lib.Integers compcert.common.Values VST.veric.base VST.veric.Clight_lemmas VST.veric.val_lemmas VST.veric.shares VST.msl.seplog VST.msl.shares VST.zlist.sublist VST.floyd.coqlib3 VST.floyd.functional_base VST.floyd.data_at_rec_lemmas CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.graph_isomorphism CertiGraph.graph.reachable_ind CertiGraph.CertiGC.GCGraph