proposition: Lemma pcv_reachable_old: forall g old_v new_v s t, sound_gc_graph g -> no_dangling_dst g -> ~ vvalid g new_v -> vvalid g s -> reachable (pregraph_copy_v g old_v new_v) s t <-> reachable g s t.
proof: Proof. intros g old_v new_v s t Hg Hn H H0. split; intros. - unfold reachable, reachable_by in *. destruct H1 as [p [[? ?] [? ?]]]. destruct p as [? p]. simpl in H1. subst v. exists (s, p). assert (valid_path g (s, p)). { clear H4 H2. revert s H0 H3. induction p; intros. 1: simpl; easy. rewrite valid_path_cons_iff in *. destruct H3 as [? [? ?]]. destruct Hg as [? [? [? Hels]]]. pose proof (pcv_src_edge g old_v new_v H6). red in H7. destruct H2 as [? [? ?]]. rewrite H7 in *. rewrite pcv_evalid_iff in H2. rewrite H6. split; auto. destruct H2. - clear H8. assert (fst a <> new_v) by (intro; rewrite H8 in H1; now subst s). rewrite pcv_dst_old in H9, H3; auto. unfold strong_evalid. rewrite H6, <- H1. rewrite pcv_vvalid_iff in H9. destruct H9. 1: intuition. exfalso. red in H5. rewrite H5 in H2. destruct H2. red in Hn. apply Hn in H10; auto. red in H4. now rewrite <- H4, H9 in H10. - rewrite in_map_iff in H2. destruct H2 as [x [? _]]. destruct a. inversion H2. subst v. simpl in H1. now subst s. } split; split; auto. destruct p. 1: now simpl in *. assert (e :: p <> nil) by (intro HS; inversion HS). apply exists_last in H5. destruct H5 as [l' [a ?]]. rewrite e0 in *. rewrite pfoot_last in *. rewrite pcv_dst_old in H2; auto. assert (evalid g a) by (eapply valid_path_evalid; eauto; rewrite in_app_iff; now right; left). destruct Hg as [? [? ?]]. red in H6, H7. rewrite H7 in H5. destruct H5. rewrite <- H6 in H5. intro. now rewrite H10 in H5. - apply is_partial_graph_reachable with (g1 := g); auto. apply pcv_is_partial_graph; 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