proposition: Lemma pcv_src_edge: forall (g: LGraph) v new, src_edge g -> src_edge (pregraph_copy_v g v new).
proof: Proof. intros. unfold src_edge in *. intros. unfold pregraph_copy_v. replace (length (get_edges g v)) with (length (map snd (get_edges g v))) by (rewrite map_length; reflexivity). remember (get_edges g v) as el. remember (combine (combine (repeat new (Datatypes.length (map snd el))) (map snd el)) (map (dst g) el)) as l. destruct (in_dec equiv_dec e (map fst l)). - rewrite flcvae_src_new; auto. rewrite combine_repeat_eq_map, map_map, combine_map_join in Heql. apply list_in_map_inv in i. destruct i as [x [? ?]]. subst l. apply list_in_map_inv in H1. destruct H1 as [x0 [? ?]]. subst x e. simpl. auto. - rewrite flcvae_src_old; auto. simpl. apply H. Qed.
imports: Coq.ZArith.ZArith Coq.Program.Basics 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 CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.graph_isomorphism CertiGraph.graph.reachable_ind CertiGraph.CertiGC.GCGraph