proposition: Lemma pcv_dst_new: forall g old new n, In n (map snd (get_edges g old)) -> dst (pregraph_copy_v g old new) (new, n) = dst g (old, n).
proof: Proof. intros. unfold pregraph_copy_v. rewrite flcvae_dst_new with (v := dst g (old, n)). - reflexivity. - rewrite map_fst_combine. + apply NoDup_combine_r. clear H. unfold get_edges. unfold make_fields. remember (raw_fields (vlabel g old)). clear Heql. remember 0 as m. clear Heqm. revert m. induction l; intros. simpl. 1: constructor. simpl. destruct a; [destruct s|]; simpl; try apply IHl. constructor. 2: apply IHl. clear. cut (forall a b, In a (map snd (filter_sum_right (make_fields' l old b))) -> b <= a). * repeat intro. apply H in H0. lia. * induction l; intros; simpl in H. 1: exfalso; assumption. destruct a; [destruct s|]; simpl in H; try (apply IHl in H; lia). destruct H; [|apply IHl in H]; lia. + unfold EType. rewrite combine_length, repeat_length, !map_length, Nat.min_id. reflexivity. - apply list_in_map_inv in H. destruct H as [[x ?] [? ?]]. simpl in H. subst n0. assert (x = old). { unfold get_edges in H0. rewrite <- filter_sum_right_In_iff in H0. unfold make_fields in H0. apply e_in_make_fields' in H0. destruct H0 as [s ?]. inversion H. reflexivity. } subst x. remember (get_edges g old). clear Heql. induction l; simpl in *. 1: assumption. destruct H0. + subst a. simpl. left; reflexivity. + right. apply IHl. 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