proposition: Lemma lacv_generation_rep_eq: forall g v to, graph_has_v g v -> graph_has_gen g to -> no_dangling_dst g -> copy_compatible g -> generation_rep (lgraph_add_copied_v g v to) to = vertex_at (nth_sh g to) (vertex_address g (new_copied_v g to)) (make_header g v) (make_fields_vals g v) * generation_rep g to.
proof: Proof. intros. unfold generation_rep. rewrite lacv_nth_sh by assumption. remember (number_of_vertices (nth_gen g to)). unfold lgraph_add_copied_v at 1. unfold nth_gen. simpl. rewrite cvmgil_eq by assumption. simpl. unfold nth_gen in Heqn. rewrite <- Heqn. rewrite nat_inc_list_app, map_app, iter_sepcon_app_sepcon, sepcon_comm. simpl nat_seq. change (nth to (g_gen (glabel g)) null_info) with (nth_gen g to) in Heqn. f_equal. - simpl. normalize. replace (to, n) with (new_copied_v g to) by (unfold new_copied_v; subst n; reflexivity). unfold vertex_rep. f_equal. + apply lacv_vertex_address_new. assumption. + apply lacv_make_header_new. + apply lacv_make_fields_vals_new; assumption. - apply iter_sepcon_func_strong. intros. destruct x as [m x]. apply list_in_map_inv in H3. destruct H3 as [? [? ?]]. inversion H3. subst x0. subst m. clear H3. remember (nth_sh g to) as sh. subst n. rewrite nat_inc_list_In_iff in H4. unfold vertex_rep. assert (graph_has_v g (to, x)) by (split; simpl; assumption). rewrite lacv_vertex_address_old, lacv_make_header_old, lacv_make_fields_vals_old; [reflexivity | try assumption..]. unfold new_copied_v. intro. inversion H5. lia. Qed.
imports: VST.veric.compcert_rmaps VST.msl.shares VST.msl.wand_frame VST.concurrency.conclib CertiGraph.lib.List_ext CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.ramification_lemmas CertiGraph.graph.graph_model CertiGraph.CertiGC.GCGraph CertiGraph.CertiGC.env_graph_gc CertiGraph.msl_ext.iter_sepcon Coq.Lists.List