proposition: Lemma upd_roots_not_pointing: forall from to i g roots roots', copy_compatible g -> roots_graph_compatible roots g -> from <> to -> 0 <= i < Zlength roots -> roots' = upd_roots from to (inl i) g roots -> np_roots_rel from roots roots' [i].
proof: Proof. intros * ? ? ? ?. pose proof I. intros. unfold np_roots_rel. intros. simpl. unfold flip. assert (Zlength roots' = Zlength roots) by (rewrite H4; apply upd_roots_Zlength). assert (0 <= j < Zlength roots). { rewrite <- H6. destruct (Z_lt_le_dec j (Zlength roots')). 2: rewrite Znth_outofbounds in H5 by lia; inversion H5. split; auto. destruct (Z_lt_le_dec j 0); auto. rewrite Znth_outofbounds in H5 by lia. inversion H5. } unfold upd_roots, upd_root in *. simpl in H4. destruct (Znth i roots) eqn:? . - assert (roots' = roots) by (rewrite <- Heqr, upd_Znth_unchanged in H4; auto). clear H4. subst roots'. split; intros; auto. destruct H4; auto. congruence. - if_tac in H4. + destruct (raw_mark (vlabel g v0)) eqn: ?; subst; split; intros. * destruct H4; auto. subst. rewrite upd_Znth_same in H5 by auto. inversion H5. red in H0. rewrite Forall_forall in H0. assert (graph_has_v g v0). { apply H0. rewrite <- filter_sum_right_In_iff, <- Heqr. apply Znth_In; assumption. } hnf in H. destruct (H _ H4 Heqb) as [_ ?]. auto. * assert (i<>j) by tauto. rewrite upd_Znth_diff in H5 by auto. auto. * destruct H4; auto. subst j. rewrite upd_Znth_same in H5 by assumption. inversion H5. unfold new_copied_v. simpl. auto. * assert (i<>j) by tauto. rewrite upd_Znth_diff in H5 by auto; auto. + rewrite <- Heqr in H4. rewrite upd_Znth_unchanged in H4 by auto. subst roots'. split; intros; auto. destruct H4; auto. congruence. 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