proposition: Lemma fr_roots_graph_compatible: forall depth from to p g g' roots, graph_has_gen g to -> forward_p_compatible p roots g from -> copy_compatible g -> forward_relation from to depth (forward_p2forward_t p roots g) g g' -> from <> to -> roots_graph_compatible roots g -> roots_graph_compatible (upd_roots from to p g roots) g'.
proof: Proof. intros. unfold upd_roots, upd_root in *. destruct p. - simpl in *. destruct (Znth z roots) eqn: ?; simpl in H2. + rewrite <- Heqr. rewrite upd_Znth_unchanged'. destruct s; inversion H2; subst; assumption. + assert (graph_has_v g v). { red in H4. rewrite Forall_forall in H4. apply H4. rewrite <- filter_sum_right_In_iff. rewrite <- Heqr. apply Znth_In. assumption. } inversion H2; destruct (Nat.eq_dec (vgeneration v) from); try contradiction; subst; try assumption. * rewrite <- Heqr, upd_Znth_unchanged'; auto. * rewrite H9. apply upd_Znth_graph_compatible. 1: assumption. specialize (H1 _ H5 H9). destruct H1; assumption. * destruct (raw_mark (vlabel g v)) eqn:? . 1: inversion H9. apply lcv_roots_graph_compatible; assumption. * destruct (raw_mark (vlabel g v)) eqn:? . 1: inversion H8. remember (upd_Znth z roots (inr (new_copied_v g to))) as roots'. assert (roots_graph_compatible roots' new_g) by (subst; subst new_g; apply lcv_roots_graph_compatible; assumption). assert (raw_mark (vlabel new_g (new_copied_v g to)) = false). { subst new_g. unfold lgraph_copy_v. rewrite <- lmc_raw_mark. - rewrite lacv_vlabel_new. assumption. - unfold new_copied_v. destruct v. destruct H5. simpl in H7. red in H7. intro HS. inversion HS. lia. } assert (graph_has_v new_g (new_copied_v g to)) by (subst new_g; apply lcv_graph_has_v_new; assumption). unfold vertex_pos_pairs in H11. remember (nat_inc_list (length (raw_fields (vlabel new_g (new_copied_v g to))))). eapply (fl_edge_roots_graph_compatible depth0 (vgeneration v) to l new_g); try eassumption. -- unfold new_copied_v. simpl; auto. -- subst new_g. rewrite <- lcv_graph_has_gen; assumption. -- clear H11 e H8 roots' Heqroots' H6 Heql l. subst new_g. unfold lgraph_copy_v. rewrite <- lmc_raw_tag. rewrite lacv_vlabel_new; auto. unfold new_copied_v. destruct v. destruct H5. simpl in H6. red in H6. intro HS. inversion HS. lia. -- intros. subst l. rewrite nat_inc_list_In_iff in H12. assumption. * rewrite H8. apply lcv_roots_graph_compatible; assumption. - simpl. eapply fr_right_roots_graph_compatible; eauto. Qed.
imports: Coq.ZArith.ZArith Coq.Program.Basics Coq.micromega.Lia 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 VST.zlist.list_solver CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen