proposition: Lemma fr_O_reachable_or_marked: forall (from to : nat) (p : forward_p_type) (g1 g2 : LGraph) (roots : roots_t), from <> to -> graph_has_gen g1 to -> sound_gc_graph g1 -> no_dangling_dst g1 -> roots_graph_compatible roots g1 -> copied_vertex_prop g1 from to -> forward_p_compatible p roots g1 from -> reachable_or_marked_special_cond g1 roots from to p -> forward_relation from to O (forward_p2forward_t p roots g1) g1 g2 -> forall v, reachable_or_marked from g1 roots v <-> reachable_or_marked from g2 (upd_roots from to p g1 roots) v.
proof: Proof. pose (H2 := True). intros from to p g1 g2 roots H H0 H1 Hd H3 H4 H5 Hb H6 v. assert (Hr: forall i r, 0 <= i < Zlength roots -> Znth i roots = inr r -> graph_has_v g1 r). { intros. red in H3. rewrite Forall_forall in H3. apply H3. rewrite <- filter_sum_right_In_iff, <- H8. now apply Znth_In. } unfold upd_roots, upd_root. pose proof H1. destruct H7 as [Hv _]. red in Hv. destruct p; simpl in H5, H6. - destruct (Znth z roots) eqn:? ; [destruct s|]; simpl in *; rewrite ?Heqr; inversion H6; subst; clear H6; try easy; try (rewrite <- Heqr, upd_Znth_unchanged'); auto; try easy. + rewrite if_false; auto; rewrite <- Heqr, upd_Znth_unchanged'; easy. + rewrite if_true, H10; auto. split; intros; red in H6 |-* ; destruct H6; split; auto. * destruct H7; [| right]; auto. rewrite reachable_from_roots in H7. destruct H7 as [i [r [? [? ?]]]]. pose proof I. destruct (Z.eq_dec i z). -- subst i. rewrite Heqr in H8. inversion H8. assert (vvalid g2 v) by (apply reachable_foot_valid in H9; auto). subst v0. clear H8. eapply copied_vertex_reachable in H9; eauto. destruct H9. 2: right; auto. left. rewrite reachable_from_roots. exists z, (copied_vertex (vlabel g2 r)). rewrite upd_Znth_Zlength, upd_Znth_same; auto. -- left. rewrite reachable_from_roots. exists i, r. rewrite upd_Znth_Zlength, upd_Znth_diff; auto. * destruct H7; [| right]; auto. rewrite reachable_from_roots in H7. pose proof I. rewrite upd_Znth_Zlength in H7; auto. destruct H7 as [i [r [? [? ?]]]]. destruct (Z.eq_dec i z). -- subst i. rewrite upd_Znth_same in H9; auto. inversion H9. subst r. clear H9. rename v0 into r. left. rewrite reachable_from_roots. exists z, r. do 2 (split; auto). eapply copied_vertex_reachable_inv; eauto. -- left. rewrite reachable_from_roots. exists i, r. rewrite upd_Znth_diff in H9; auto. + rewrite if_true, H9; auto. assert (Hs: sound_gc_graph (lgraph_copy_v g1 v0 to)) by (now apply lcv_sound). assert (~ vvalid g1 (new_copied_v g1 to)). { rewrite Hv. intro. now apply graph_has_v_not_eq with (to := to) in H6. } split; intros; red in H7 |-* ; destruct H7; split; auto; destruct H8. * rewrite reachable_from_roots in H8. destruct H8 as [i [r [? [? ?]]]]. pose proof I. assert (vvalid g1 r) by (now apply reachable_head_valid in H11). destruct (Z.eq_dec i z). -- rewrite e, Heqr in H10. inversion H10. subst v0. rewrite (pcv_reachable_new _ _ (new_copied_v g1 to)) in H11; auto. clear H10. destruct H11; [right | left]. ++ subst v. rewrite lcv_raw_mark_old. destruct Hs. red in H10. rewrite H10. split; auto. apply lcv_graph_has_v_old; auto. now rewrite <- Hv. ++ rewrite reachable_from_roots. exists i, (new_copied_v g1 to). subst i; rewrite upd_Znth_Zlength, upd_Znth_same; auto. do 2 (split; auto). simpl. now destruct H8. -- left. rewrite reachable_from_roots. exists i, r. rewrite upd_Znth_Zlength, upd_Znth_diff; auto. do 2 (split; auto). simpl. rewrite pcv_reachable_old; auto. * destruct H8. right. destruct Hs. red in H11. rewrite H11. assert (graph_has_v g1 v) by (destruct H1; red in H1; now rewrite <- H1). split. 1: apply lcv_graph_has_v_old; auto. rewrite <- lcv_raw_mark; auto. intro. subst v0. now rewrite H9 in H10. * rewrite reachable_from_roots in *. destruct H8 as [i [r [? [? ?]]]]. pose proof I. rewrite upd_Znth_Zlength in H8; auto. destruct (Z.eq_dec i z). -- subst i. rewrite upd_Znth_same in H10; auto. inversion H10. subst r. clear H10. simpl in H11. left. exists z, v0. rewrite (pcv_reachable_new _ _ (new_copied_v g1 to)); auto. 2: destruct H1; red in H1; rewrite H1; apply (Hr z); auto. do 2 (split; auto). right. split; auto. intro. subst v. rewrite <- H7 in H. unfold new_copied_v in H. now simpl in H. -- left. rewrite upd_Znth_diff in H10; auto. simpl in H11. rewrite pcv_reachable_old in H11; auto. 1: exists i, r; auto. rewrite Hv. eapply Hr; eauto. * destruct H8. destruct_eq_dec v v0. -- subst v0. left. rewrite reachable_from_roots. exists z, v. do 2 (split; auto). apply reachable_refl. rewrite Hv. eapply Hr; eauto. -- right. destruct Hs. red in H12. rewrite H12, lcv_graph_has_v_iff in H8; auto. destruct H8. 2: subst v; rewrite <- H7 in H; unfold new_copied_v in H; now simpl in H. split. 1: now rewrite <- Hv in H8. rewrite <- lcv_raw_mark in H10; auto. - simpl. destruct p as [x n]. destruct H5 as [? [? [? ?]]]. rewrite H8 in H6. simpl in H6. assert (forall e, Znth n (make_fields g1 x) = inr e -> fst e = x) by (intros; apply make_fields_Znth_edge in H10; auto; now subst e). assert (forall e, Znth n (make_fields g1 x) = inr e -> graph_has_e g1 e). { destruct H1 as [? [? [? _]]]. red in H1, H11, H12. intros. split; rewrite H10; auto. unfold get_edges. rewrite <- filter_sum_right_In_iff, <- H13. apply Znth_In. now rewrite make_fields_eq_length. } assert (forall e, Znth n (make_fields g1 x) = inr e -> evalid g1 e). { intros. destruct H1 as [_ [? _]]. red in H1. rewrite H1. now apply H11. } destruct (Znth n (make_fields g1 x)) eqn:? ; [destruct s |]; simpl in H6; inversion H6; subst; try easy. + split; intros; red in H13 |-* ; destruct H13; split; auto; destruct H14. * rewrite reachable_from_roots in *. destruct H14 as [i [r [? [? ?]]]]. subst new_g. simpl. assert (evalid g1 e) by (now apply H12). assert (vvalid g1 v) by (now apply reachable_foot_valid in H17). eapply copied_vertex_pgd_reachable in H17; eauto. destruct H17. 2: now right. left. exists i, r. auto. * subst new_g. simpl. now right. * rewrite reachable_from_roots in *. destruct H14 as [i [r [? [? ?]]]]. subst new_g. simpl in *. left. exists i, r. do 2 (split; auto). eapply copied_vertex_pgd_reachable_inv in H17; eauto. * subst new_g. simpl in H14. now right. + assert (Hs: sound_gc_graph (lgraph_copy_v g1 (dst g1 e) to)) by (now apply lcv_sound). assert (~ vvalid g1 (new_copied_v g1 to)). { rewrite Hv. intro. now apply graph_has_v_not_eq with (to := to) in H13. } split; intros; red in H14 |-* ; destruct H14; split; auto; destruct H16. * rewrite reachable_from_roots in *. destruct H16 as [i [r [? [? ?]]]]. subst new_g. simpl. assert (vvalid g1 r) by (now apply reachable_head_valid in H18). rewrite <- (pcv_reachable_old _ (dst g1 e) (new_copied_v g1 to)) in H18; auto. assert (reachable (lgraph_copy_v g1 (dst g1 e) to) r v) by (now simpl). assert (fst e <> new_copied_v g1 to) by (rewrite H10; auto; intro; subst x; now rewrite <- Hv in H5). apply (copied_vertex_pgd_reachable _ e to) in H20; auto; simpl in *. -- rewrite pcv_dst_old, ucov_copied_vertex in H20; auto. destruct H20. ++ left. exists i, r. auto. ++ right; split; auto. apply reachable_foot_valid in H18. auto. -- rewrite pcv_dst_old; auto. apply lcv_copied_vertex_prop; auto. -- rewrite pcv_evalid_iff. left. now apply H12. -- rewrite pcv_dst_old; auto. apply ucov_rawmark. * destruct H16. right. subst new_g. simpl. split. -- rewrite pcv_vvalid_iff. now left. -- rewrite ucov_not_eq. 2: intro; subst v; now rewrite H15 in H17. rewrite lacv_vlabel_old; auto. intro. now subst v. * rewrite reachable_from_roots in *. destruct H16 as [i [r [? [? ?]]]]. subst new_g. remember (lgraph_copy_v g1 (dst g1 e) to) as g3. assert (fst e <> new_copied_v g1 to) by (rewrite H10; auto; intro; subst x; now rewrite <- Hv in H5). assert (dst g1 e = dst g3 e) by (subst g3; simpl; rewrite pcv_dst_old; auto). assert (new_copied_v g1 to = copied_vertex (vlabel g3 (dst g3 e))). { rewrite <- H20. subst g3. simpl. rewrite ucov_copied_vertex. easy. } rewrite H21 in H18. apply copied_vertex_pgd_reachable_inv with (to := to) in H18; try (now rewrite <- H20); try (now subst g3). -- rewrite Heqg3 in H18. simpl in H18. assert (vvalid g1 r) by (rewrite Hv; apply Hr with i; auto). left. exists i, r. rewrite pcv_reachable_old in H18; auto. -- rewrite <- H20. subst g3. apply lcv_copied_vertex_prop; auto. -- subst g3. apply lcv_no_dangling_dst; auto. red in Hd. assert (graph_has_e g1 e) by (now apply H11). destruct H22. apply Hd with (fst e); auto. -- subst g3. simpl. rewrite pcv_evalid_iff. left. now apply H12. -- rewrite <- H20. subst g3. apply lcv_raw_mark_old. * destruct H16. subst new_g. simpl in *. rewrite pcv_vvalid_iff in H16. assert (v <> new_copied_v g1 to). { intro. subst. unfold new_copied_v in *. simpl in *. now rewrite <- H14 in H. } destruct H16. 2: easy. destruct_eq_dec (dst g1 e) v. -- subst v. rewrite ucov_rawmark in H17. left. destruct Hb as [He Hb]. red in Hb. assert (evalid g1 e) by (apply H12; auto). assert (vgeneration (fst e) = to). { apply make_fields_Znth_edge in Heqf; auto. subst e. now simpl. } specialize (Hb _ H19 H20 H14). rewrite reachable_from_roots in *. destruct Hb as [i [r [? [? ?]]]]. exists i, r. do 2 (split; auto). apply reachable_trans with (fst e); auto. destruct H1 as [? [? [? _]]]. red in H1, H24, H25. exists (fst e, [e]). split; split; simpl; auto. 2: red; rewrite Forall_forall; intros; auto. rewrite H25. split; auto. red. do 2 (split; auto). rewrite H25. rewrite H24 in H19. destruct H19. rewrite <- H1 in H19. easy. -- rewrite ucov_not_eq in H17; auto. rewrite lacv_vlabel_old in H17; 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