proposition: Lemma lacv_field2val_make_fields_new: forall (tag: Z) g v to, graph_has_v g v -> graph_has_gen g to -> no_dangling_dst g -> map (field2val tag (lgraph_add_copied_v g v to)) (make_fields (lgraph_add_copied_v g v to) (new_copied_v g to)) = map (field2val tag g) (make_fields g v).
proof: Proof. intros. unfold make_fields. rewrite lacv_vlabel_new. remember (raw_fields (vlabel g v)). remember 0 as n. assert (forall m, In m (map snd (filter_sum_right (make_fields' l v n))) -> In m (map snd (get_edges g v))). { unfold get_edges, make_fields. subst. intuition auto. } clear Heql Heqn. revert n H2. induction l; intros; simpl. 1: reflexivity. destruct a; [destruct s|]. - simpl in *. rewrite IHl; [reflexivity | assumption]. - simpl in *. rewrite IHl; [reflexivity | assumption]. - simpl in *. rewrite IHl. + assert (In n (map snd (get_edges g v))) by (apply H2; left; reflexivity). f_equal. rewrite pcv_dst_new by assumption. apply lacv_vertex_address_old. 2: assumption. red in H1. apply (H1 v). 1: assumption. apply in_map_iff in H3. destruct H3 as [[x ?] [? ?]]. simpl in H3. subst n0. clear -H4. pose proof H4. unfold get_edges in H4. rewrite <- filter_sum_right_In_iff in H4. unfold make_fields in H4. apply e_in_make_fields' in H4. destruct H4 as [s ?]. inversion H0. subst. assumption. + intros. apply H2. right; assumption. Qed.
imports: Coq.ZArith.ZArith Coq.Program.Basics Coq.micromega.Lia 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 VST.zlist.list_solver CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen