proposition: Lemma copied_vertex_pgd_reachable: forall g e to r v, sound_gc_graph g -> copied_vertex_prop g (vgeneration (dst g e)) to -> evalid g e -> raw_mark (vlabel g (dst g e)) = true -> reachable g r v -> reachable (pregraph_gen_dst g e (copied_vertex (vlabel g (dst g e)))) r v \/ raw_mark (vlabel g v) = true.
proof: Proof. intros. unfold reachable, reachable_by in H3. destruct H3 as [[s p] ?]. assert (phead (s, p) = r) by (eapply reachable_by_path_head; eauto). simpl in H4. subst s. remember (length p) as n. assert (length p <= n)%nat by lia. clear Heqn. revert r p H4 H3. induction n; intros. - destruct p. 2: simpl in H4; lia. destruct H3 as [[_ ?] [? _]]. simpl in *. subst v. left. apply reachable_refl. now simpl. - destruct (in_dec equiv_dec e p). 2: left; exists (r, p); rewrite no_edge_gen_dst_equiv; auto. 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 H5. destruct H5. rewrite app_length in H8. simpl in H8. eapply copied_vertex_reachable_by_path in H9; eauto. destruct H9. 1: right; auto. destruct H9 as [p' [? ?]]. assert (length p' <= n)%nat by lia. specialize (IHn _ _ H11 H9). destruct IHn. 2: now right. left. remember (copied_vertex (vlabel g (dst g e))) as cde. apply reachable_trans with cde; auto. assert (reachable (pregraph_gen_dst g e cde) r (src g e)) by (exists (r, p1); now rewrite no_edge_gen_dst_equiv). apply reachable_trans with (src g e); auto. exists (src g e, [e]). split; split; simpl; auto. + apply updateEdgeFunc_eq. + split; auto. red. simpl. split; auto. rewrite updateEdgeFunc_eq. apply reachable_head_valid in H12. simpl in H12. split; auto. apply reachable_foot_valid in H13. simpl in H13. auto. + red. rewrite Forall_forall. now intros. 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