proposition: Lemma roots_rep_update_frames: forall (sh: share) (frs: list frame) (roots: list rootpair), map rp_adr (frames2rootpairs frs) = map rp_adr roots -> roots_rep sh (frames2rootpairs (update_frames frs (map rp_val roots))) = roots_rep sh roots.
proof: Proof. unfold frames2rootpairs. intros. symmetry in H|-*. revert roots H; induction frs as [|[a r s] frs']; intros. simpl in *. destruct roots; inv H; auto. simpl update_frames. change (map ?f (?A:: ?B)) with (f A :: map f B) in *. change (concat (?A :: ?B)) with (A ++ concat B) in *. unfold frame2rootpairs at 1. unfold frame2rootpairs at 1 in H. simpl frame2rootpairs' in *. rewrite map_app in *. assert (Zlength s <= Zlength roots). apply (f_equal (@Zlength val)) in H. rewrite Zlength_app, !Zlength_map, Zlength_frame2rootpairs' in H. list_solve. assert (roots = sublist 0 (Zlength s) roots ++ sublist (Zlength s) (Zlength roots) roots) by list_solve. rewrite H1. unfold roots_rep. rewrite !iter_sepcon_app_sepcon. rewrite sublist_map. rewrite sublist_app1 by list_solve. rewrite sublist_sublist by list_solve. rewrite !Z.add_0_r. f_equal. + assert (map rp_adr (sublist 0 (Zlength s) roots) = map rp_adr (frame2rootpairs' r 0 s)). rewrite map_sublist. rewrite H. rewrite sublist_app1 by (rewrite ?Zlength_map, ?Zlength_frame2rootpairs'; list_solve). rewrite sublist_map. f_equal. rewrite sublist_same by (rewrite ?Zlength_map, ?Zlength_frame2rootpairs'; list_solve); auto. clear - H0 H2. f_equal. pose (k := 0%Z). change (frame2rootpairs' r 0) with (frame2rootpairs' r k) in *. clearbody k. revert roots H0 k H2; induction s; destruct roots; simpl; intros; try list_solve. rewrite (sublist_split 0 1) in H2|-* by list_solve. simpl in H2|-*. inv H2. f_equal. destruct r0; simpl in *; f_equal; auto. change (r0::roots) with ([r0]++roots) in H3|-*. rewrite sublist_app2 in H3|-* by list_solve. change (1 - _) with 0 in *. autorewrite with sublist. replace (_ - _) with (Zlength s) by lia. replace (_ - _)%Z with (Zlength s) in H3 by list_solve. apply IHs. list_solve. auto. + etransitivity. apply IHfrs'. rewrite map_sublist at 1. rewrite H. rewrite sublist_app2 by (rewrite ?Zlength_map, ?Zlength_frame2rootpairs'; list_solve). rewrite ?Zlength_map. rewrite ?Zlength_frame2rootpairs'. rewrite sublist_same; auto. lia. rewrite Zlength_map. apply (f_equal (@Zlength val)) in H. autorewrite with sublist in H. lia. unfold roots_rep. f_equal. autorewrite with sublist. replace (_ + (_ - _)) with (Zlength roots) by lia. rewrite <- map_sublist. autorewrite with sublist. auto. 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