proposition: Lemma graph_thread_info_compatible_reset: forall g h gen, graph_heap_compatible g h -> graph_heap_compatible (reset_graph gen g) (reset_nth_heap gen h).
proof: Proof. intros. destruct H as [? [? ?]]. split; [|split]; [|simpl; rewrite reset_nth_gen_info_length..]. - rewrite gsc_iff by (simpl; rewrite remove_ve_glabel_unchanged, reset_nth_space_length, reset_nth_gen_info_length; assumption). intros n ?. rewrite gsc_iff in H by assumption. rewrite graph_has_gen_reset in H2. specialize (H _ H2). red in H. simpl. unfold nth_gen, nth_space in *. simpl. rewrite remove_ve_glabel_unchanged. destruct (Nat.eq_dec n gen). + subst gen. red in H2. rewrite reset_nth_gen_info_same. rewrite reset_nth_space_same by lia. intuition auto. + rewrite reset_nth_gen_info_diff, reset_nth_space_diff by assumption. destruct H as [? [? ?]]. split. 1: assumption. split. 1: assumption. rewrite pvs_reset_unchanged. assumption. - rewrite remove_ve_glabel_unchanged. destruct (le_lt_dec (length (spaces h)) gen). + rewrite reset_nth_space_overflow; assumption. + rewrite reset_nth_space_Znth by assumption. rewrite <- upd_Znth_map. simpl. remember (spaces h). assert (0 <= Z.of_nat gen < Zlength l0) by (rewrite Zlength_correct; lia). replace (space_start (Znth (Z.of_nat gen) l0)) with (Znth (Z.of_nat gen) (map space_start l0)) by (rewrite Znth_map; auto). rewrite upd_Znth_unchanged; [|rewrite Zlength_map]; assumption. - rewrite remove_ve_glabel_unchanged, reset_nth_space_length. assumption. 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