proposition: Lemma upd_rootpairs_compatible: forall g rootpairs roots z, rootpairs_compatible g rootpairs roots -> forall (v : VType) (HB : 0 <= z < Zlength roots), rootpairs_compatible g (update_rootpairs rootpairs (upd_Znth z (map rp_val rootpairs) (vertex_address g v))) (upd_Znth z roots (inr v)).
proof: Proof. intros. red in H |-* . assert (0 <= z < Zlength (map (root2val g) roots)) by (list_solve). clear HB. rewrite <- upd_Znth_map. set (r := map _ roots) in *. clearbody r; clear roots. subst r. simpl root2val. set (u := vertex_address g v). clearbody u. clear g v. revert z H0; induction rootpairs as [ | [a r] rest]; simpl; intros. - rewrite Zlength_nil in H0; lia. - destruct (zeq z 0). + subst. rewrite upd_Znth0. simpl; f_equal. rewrite update_rootpairs_same; auto. + rewrite upd_Znth_cons by rep_lia. simpl. f_equal. apply IHrest. list_solve. 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