proposition: Lemma pcv_edge: forall (g: LGraph) old_v new_v z, sound_gc_graph g -> no_dangling_dst g -> vvalid g old_v -> ~ vvalid g new_v -> g |= old_v ~> z <-> (pregraph_copy_v g old_v new_v) |= new_v ~> z.
proof: Proof. intros g old_v new_v z H0 Hd H H1. unfold edge. destruct H0 as [? [? [? Hels]]]. red in H0, H2, H3. split; intros; destruct H4 as [? [? ?]]. - split3; auto. + apply pcv_vvalid_iff. now right. + rewrite pcv_vvalid_iff. now left. + rewrite step_spec in *. destruct H6 as [e [? [? ?]]]. rewrite H2 in H6. destruct H6. rewrite get_edges_inv in H9. destruct H9 as [idx [? ?]]. destruct e as [gen i]. simpl in *. rewrite H3 in H7. simpl in *. subst gen. inversion H9. subst i. clear H9. exists (new_v, idx). split3. * rewrite pcv_evalid_iff. right. rewrite get_edges_map_map. rewrite (map_map _ (fun x : VType * nat => (new_v, snd x))). simpl. change (new_v, idx) with ((fun x : nat => (new_v, x)) idx). now apply in_map. * now apply pcv_src_new. * now rewrite pcv_dst_new. - assert (step g old_v z). { rewrite step_spec in *. destruct H6 as [e [? [? ?]]]. rewrite pcv_evalid_iff in H6. destruct H6. - exfalso. rewrite H2 in H6. destruct H6. destruct e as [gen idx]. simpl in *. rewrite <- H0 in H6. destruct_eq_dec gen new_v. 1: now subst. rewrite pcv_src_old in H7. 2: now simpl. rewrite H3 in H7. now simpl in H7. - rewrite get_edges_map_map, (map_map _ (fun x : VType * nat => (new_v, snd x))) in H6. simpl in H6. rewrite in_map_iff in H6. destruct H6 as [idx [? ?]]. destruct e. inversion H6. subst v n. clear H6. rewrite pcv_dst_new in H8; auto. exists (old_v, idx). rewrite H3. simpl. split; auto. rewrite H2. split; simpl. 1: now rewrite <- H0. now apply In_snd_get_edges. } split3; auto. eapply step_vvalid; eauto. split3; easy. 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