proposition: Lemma copied_vertex_reachable_by_path_inv: forall (g: LGraph) (r v: VType) from to p, sound_gc_graph g -> copied_vertex_prop g from to -> raw_mark (vlabel g r) = true -> vgeneration v = from -> from <> to -> no_dangling_dst g -> graph_has_v g r -> g |= (copied_vertex (vlabel g r), p) is (copied_vertex (vlabel g r)) ~o~> v satisfying (fun _ => True) -> exists p', g |= (r, p') is r ~o~> v satisfying (fun _ => True) /\ length p = length p'.
proof: Proof. intros g r v from to p H H0 H1 H2 H3 Hd H4 H5. remember (length p) as n. assert (length p <= n)%nat by lia. rewrite Heqn. clear Heqn. revert r p H6 H1 H4 H5. induction n; intros. - destruct p. 2: simpl in H6; lia. destruct H5 as [[_ ?] _]. simpl in H5. red in H0. specialize (H0 _ H4 H1). destruct H0 as [_ [? _]]. rewrite H5, H2 in H0. now rewrite H0 in H3. - red in H0. specialize (H0 _ H4 H1). destruct H0 as [? [? [? [? ?]]]]. remember (copied_vertex (vlabel g r)) as cr. destruct p. + destruct H5 as [[_ ?] _]. simpl in H5. rewrite H5, H2 in H7. now rewrite H7 in H3. + assert (g |= (dst g e, p) is dst g e ~o~> v satisfying (fun _ => True)). { change (e :: p) with ([] ++ e :: p) in H5. apply reachable_by_path_app_cons in H5. now destruct H5. } destruct H5 as [_ [? _]]. rewrite valid_path_cons_iff in H5. destruct H5 as [? [[? [? ?]] ?]]. destruct H as [? [? [? _]]]. red in H, H16, H17. rewrite H17 in H5. destruct e as [cr' idx]. simpl in H5. subst cr'. rewrite H16 in H12. destruct H12. simpl fst in *. rewrite get_edges_In in H12. rewrite <- H9 in H12. specialize (H10 _ H12). assert (vvalid g (dst g (r, idx)) -> g |= (r, [(r, idx)]) is r ~o~> (dst g (r, idx)) satisfying (fun _ => True)). { split; split; simpl; auto. 2: red; rewrite Forall_forall; intros; auto. rewrite H17. split; auto. split3; [| rewrite H17; simpl; rewrite H |]; auto. rewrite H16. split; simpl; auto. now rewrite get_edges_In. } destruct H10. * rewrite H10 in H11. exists ((r, idx) :: p). split. 2: simpl; auto. assert ((r, (r, idx) :: p) = path_glue (r, [(r, idx)]) (dst g (r, idx), p)) by (now unfold path_glue). unfold EType. rewrite H19. apply reachable_by_path_merge with (dst g (r, idx)); auto. apply H18. now rewrite <- H10. * destruct H10. assert (length p <= n)%nat by (simpl in H6; lia). assert (graph_has_v g (dst g (r, idx))). { red in Hd. apply Hd with r; auto. now rewrite get_edges_In. } rewrite H19 in H11. specialize (IHn _ _ H20 H10 H21 H11). destruct IHn as [p' [? ?]]. exists ((r, idx) :: p'). split. 2: simpl; auto. assert ((r, (r, idx) :: p') = path_glue (r, [(r, idx)]) (dst g (r, idx), p')) by (now unfold path_glue). unfold EType. rewrite H24. apply reachable_by_path_merge with (dst g (r, idx)). 2: apply H22; auto. apply H18. now rewrite H. 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