proposition: Lemma copied_vertex_pgd_reachable_inv: forall g e to r v, sound_gc_graph g -> copied_vertex_prop g (vgeneration (dst g e)) to -> no_dangling_dst g -> evalid g e -> raw_mark (vlabel g (dst g e)) = true -> vgeneration v = vgeneration (dst g e) -> vgeneration (dst g e) <> to -> reachable (pregraph_gen_dst g e (copied_vertex (vlabel g (dst g e)))) r v -> reachable g r v.
proof: Proof. intros. unfold reachable, reachable_by in H6. destruct H6 as [[s p] ?]. pose proof H6. apply reachable_by_path_head in H7. simpl in H7. subst s. destruct (in_dec equiv_dec e p). - change p with (snd (r, p)) in i. eapply reachable_path_unique_edge in i; eauto. destruct i as [p1 [p2 [? [? [? _]]]]]. apply reachable_by_path_app_cons in H7. simpl in *. destruct H7. rewrite updateEdgeFunc_eq in H10. rewrite no_edge_gen_dst_equiv in H7, H10; simpl; auto. assert (graph_has_v g (dst g e)). { red in H1. destruct H as [? [? ?]]. red in H11. rewrite H11 in H2. destruct H2. apply H1 with (fst e); auto. } eapply copied_vertex_reachable_by_path_inv in H10; eauto. destruct H10 as [p' [? _]]. assert (reachable g r (src g e)) by (now exists (r, p1)). assert (reachable g (dst g e) v) by (now exists (dst g e, p')). apply reachable_trans with (src g e); auto. apply reachable_trans with (dst g e); auto. exists (src g e, [e]). split; split; simpl; auto. + split; auto. red. apply reachable_foot_valid in H12. apply reachable_head_valid in H13. auto. + red. rewrite Forall_forall. intros; auto. - exists (r, p). rewrite no_edge_gen_dst_equiv in H6; 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