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