proposition: Lemma fr_O_copied_vertex_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 -> copied_vertex_prop g2 from to.
proof: Proof. intros. destruct p; simpl in H3, H4. - destruct (Znth z roots) eqn:? ; [destruct s |]; inversion H4; subst; try easy. apply lcv_copied_vertex_prop; auto. - destruct p as [v n]. destruct H3 as [? [? [? [H7' ?]]]]. rewrite H7 in H4. simpl in H4. destruct (Znth n (make_fields g1 v)) eqn:? ; [destruct s|]; simpl in H4; inversion H4; subst; try easy. + subst new_g. assert (fst e = v) by (apply make_fields_Znth_edge in Heqf; auto; now subst e). assert (evalid g1 e). { destruct H1 as [? [? [? _]]]. red in H1, H10, H11. rewrite H10. split; rewrite H9. 1: easy. unfold get_edges. rewrite <- filter_sum_right_In_iff, <- Heqf. apply Znth_In. now rewrite make_fields_eq_length. } apply lgd_copied_vertex_prop; auto. rewrite H9; auto. + subst new_g. eapply lcv_copied_vertex_prop in H5; eauto. remember (lgraph_copy_v g1 (dst g1 e) to) as g3. assert (fst e = v) by (apply make_fields_Znth_edge in Heqf; auto; now subst e). assert (dst g1 e = dst g3 e). { subst g3. simpl. rewrite pcv_dst_old; auto. rewrite H9. now apply graph_has_v_not_eq with (to := to) in H3. } assert (new_copied_v g1 to = copied_vertex (vlabel g3 (dst g3 e))). { rewrite <- H10. subst g3. simpl. rewrite ucov_copied_vertex. easy. } assert (graph_has_e g1 e). { split; rewrite H9. 1: easy. unfold get_edges. rewrite <- filter_sum_right_In_iff, <- Heqf. apply Znth_In. now rewrite make_fields_eq_length. } assert (evalid g1 e). { destruct H1 as [? [? [? _]]]. red in H1, H14, H15. now rewrite H14. } rewrite H12, H10. apply lgd_copied_vertex_prop; try (now rewrite <- H10). * subst g3. apply lcv_no_dangling_dst; auto. red in H2. apply H2 with v; auto. destruct H13. now rewrite H9 in H15. * subst g3. rewrite <- lcv_graph_has_gen; auto. * now rewrite H9, <- H10. * rewrite <- H10. subst g3. apply lcv_raw_mark_old. * subst g3. destruct H1 as [? [? [? _]]]. pose proof H0. apply (lcv_edge_valid _ (dst g1 e)) in H0; auto. red in H0. rewrite H0. split; rewrite H9. 1: apply lcv_graph_has_v_old; auto. unfold get_edges, make_fields. rewrite <- lcv_raw_fields; auto. fold (make_fields g1 v). fold (get_edges g1 v). destruct H13. now rewrite <- H9. 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