proposition: Lemma frames_shell_rep_update: forall (sh: share) (frs: list frame) (rootvals: list val), Zlength rootvals = Zlength (frames2rootpairs frs) -> frames_shell_rep sh frs = frames_shell_rep sh (update_frames frs rootvals).
proof: Proof. induction frs as [|[a r s] frs']; simpl; intros; auto. unfold frames2rootpairs in H; fold frames2rootpairs in H. change (map ?f (?A::frs')) with (f A :: map f frs') in H. change (concat (?A :: ?B)) with (A ++ concat B) in H. rewrite Zlength_app in H. unfold frame2rootpairs at 1 in H. simpl Zlength in H. rewrite Zlength_frame2rootpairs' in H. rewrite Zlength_sublist by list_solve. rewrite Z.sub_0_r. rewrite frames_p_update_frames. f_equal. apply IHfrs'. rewrite Zlength_sublist by list_solve. unfold frames2rootpairs. lia. Qed.
imports: VST.veric.compcert_rmaps VST.msl.shares VST.msl.wand_frame VST.concurrency.conclib CertiGraph.lib.List_ext CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.ramification_lemmas CertiGraph.graph.graph_model CertiGraph.CertiGC.GCGraph CertiGraph.CertiGC.env_graph_gc CertiGraph.msl_ext.iter_sepcon Coq.Lists.List