proposition: Lemma lgd_copied_vertex_prop: forall to g e, no_dangling_dst g -> graph_has_gen g to -> vgeneration (dst g e) <> to -> vgeneration (fst e) <> vgeneration (dst g e) -> raw_mark (vlabel g (dst g e)) = true -> evalid g e -> copied_vertex_prop g (vgeneration (dst g e)) to -> copied_vertex_prop (labeledgraph_gen_dst g e (copied_vertex (vlabel g (dst g e)))) (vgeneration (dst g e)) to.
proof: Proof. intros. unfold copied_vertex_prop in *. intro s; intros. simpl in *. rewrite <- lgd_graph_has_v in *. destruct (H5 _ H6 H7) as [? [? [? [? ?]]]]. split; [|split; [|split; [|split]]]; auto. intros. unfold get_edges in H13. rewrite lgd_make_fields_eq in H13. fold (get_edges g s) in H13. specialize (H12 _ H13). destruct_eq_dec e (s, idx). 1: subst e; simpl in H2; now rewrite H10 in H2. rewrite (updateEdgeFunc_neq _ _ _ (s, idx)); auto. destruct_eq_dec e (copied_vertex (vlabel g s), idx). 2: rewrite updateEdgeFunc_neq; auto. remember (copied_vertex (vlabel g s)) as cs. subst e. rewrite updateEdgeFunc_eq. destruct H12 as [? | [? ?]]. - right. rewrite H12 in *. auto. - simpl in H2. rewrite H9 in *. assert (graph_has_v g (dst g (s, idx))). { red in H. apply H with s; auto. rewrite get_edges_In. auto. } specialize (H5 _ H16 H12). rewrite H15 in H2. destruct H5 as [_ [? _]]. now rewrite H5 in H2. 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