proposition: Lemma copied_v_derives_new_g: forall g v to, graph_has_gen g to -> no_dangling_dst g -> copy_compatible g -> graph_has_v g v -> vertex_at (nth_sh g to) (vertex_address g (new_copied_v g to)) (make_header g v) (make_fields_vals g v) * graph_rep g = graph_rep (lgraph_add_copied_v g v to).
proof: Proof. intros. unfold graph_rep. unfold lgraph_add_copied_v at 1. simpl. red in H. rewrite cvmgil_length by assumption. remember (length (g_gen (glabel g))). assert (n = to + (n - to))%nat by lia. assert (0 < n - to)%nat by lia. remember (n - to)%nat as m. rewrite H3, nat_inc_list_app, !iter_sepcon_app_sepcon. rewrite (lacv_icgr_not_eq (nat_inc_list to) g v to); try assumption. 3: subst n; apply H. 2: intro; rewrite nat_inc_list_In_iff in H5; lia. rewrite sepcon_comm, sepcon_assoc. f_equal. assert (m = 1 + (m - 1))%nat by lia. rewrite H5, nat_seq_app, !iter_sepcon_app_sepcon. assert (nat_seq to 1 = [to]) by reflexivity. rewrite H6. clear H6. rewrite (lacv_icgr_not_eq (nat_seq (to + 1) (m - 1)) g v to); try assumption. 3: subst n; apply H. 2: intro; rewrite nat_seq_In_iff in H6; lia. rewrite sepcon_assoc, sepcon_comm, sepcon_assoc, sepcon_comm. f_equal. simpl iter_sepcon. normalize. clear m Heqm H3 H4 H5. subst n. rewrite <- lacv_generation_rep_eq; [reflexivity | assumption..]. 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