proposition: Lemma lcv_copied_vertex_prop: forall (to : nat) (g : LGraph) (v : VType), vgeneration v <> to -> sound_gc_graph g -> graph_has_gen g to -> raw_mark (vlabel g v) = false -> no_dangling_dst g -> copied_vertex_prop g (vgeneration v) to -> copied_vertex_prop (lgraph_copy_v g v to) (vgeneration v) to.
proof: Proof. intros. unfold copied_vertex_prop in *. intro s; intros. apply lcv_graph_has_v_inv in H5; auto. destruct H5. 2: subst s; rewrite lcv_vlabel_new in H6; auto; now rewrite H2 in H6. pose proof H0. destruct H0 as [? [? [? Hels]]]. red in H0, H8, H9. assert (vvalid g s) by (now rewrite <- H0 in H5). assert (~ vvalid g (new_copied_v g to)) by (intro; rewrite H0 in H11; now apply (graph_has_v_not_eq g to) in H11). destruct_eq_dec s v. - subst s. simpl. rewrite ucov_copied_vertex. simpl. split; [|split; [|split; [|split]]]; auto. + apply lcv_graph_has_v_new; auto. + rewrite lcv_get_edges_old, lcv_lacv_get_edges; auto. symmetry. apply lacv_get_edges_new. + intros. rewrite lcv_get_edges_old in H12; auto. rewrite pcv_dst_new; auto. rewrite !pcv_dst_old. 2: simpl; intro; now subst. now left. - rewrite <- lcv_raw_mark in H6; auto. rewrite lcv_copied_vertex; auto. destruct (H4 _ H5 H6) as [? [? [? [? ?]]]]. split; [|split; [|split; [|split]]]; [apply lcv_graph_has_v_old | | | rewrite !lcv_get_edges_old |]; auto. intros. rewrite <- H0 in H13. rewrite lcv_get_edges_old in H18; auto. simpl dst. rewrite !pcv_dst_old; [|simpl; intro; now rewrite H19 in *..]. specialize (H17 _ H18). destruct H17 as [? | [? ?]]; [left|]; auto. assert (graph_has_v g (dst g (s, idx))). { red in H3. apply H3 with s; auto. rewrite get_edges_In; auto. } destruct_eq_dec (dst g (s, idx)) v. 1: now rewrite H21, H2 in H17. right. rewrite <- lcv_raw_mark; auto. rewrite lcv_copied_vertex; auto. 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