proposition: Lemma lacv_field2val_make_fields_old: forall (tag: Z) (g : LGraph) (v : VType) (to : nat) x, graph_has_v g x -> 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) x) = map (field2val tag g) (make_fields g x).
proof: Proof. intros. unfold make_fields. pose proof (graph_has_v_not_eq _ to _ H). rewrite lacv_vlabel_old by assumption. apply map_ext_in. intros [[? | ?] | ?] ?; simpl; try reflexivity. unfold new_copied_v. rewrite pcv_dst_old. - apply lacv_vertex_address_old. 2: assumption. specialize (H1 _ H). apply H1. unfold get_edges. rewrite <- filter_sum_right_In_iff. assumption. - apply e_in_make_fields' in H3. destruct H3 as [s ?]. subst e. simpl. intro. unfold new_copied_v in H2. contradiction. 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