proposition: Lemma gti_compatible_add: forall g h gi sp i (Hs: 0 <= i < MAX_SPACES), graph_heap_compatible g h-> ~ graph_has_gen g (Z.to_nat i) -> graph_has_gen g (Z.to_nat (i - 1)) -> (forall (gr: LGraph), generation_space_compatible gr (Z.to_nat i, gi, sp)) -> graph_heap_compatible (lgraph_add_new_gen g gi) (add_new_space h sp i Hs).
proof: Proof. intros. unfold graph_heap_compatible in *. destruct H as [? [? ?]]. assert (length (g_gen (glabel g)) = Z.to_nat i). { clear -H0 H1. unfold graph_has_gen in *. rewrite Z2Nat.inj_sub in H1 by lia. simpl in H1. lia. } pose proof (spaces_size h). assert (length (g_gen (glabel (lgraph_add_new_gen g gi))) <= length (spaces (add_new_space h sp i Hs)))%nat. { simpl. rewrite <- !ZtoNat_Zlength, upd_Znth_Zlength by lia. rewrite H6, ZtoNat_Zlength, app_length, H5. simpl. change (S O) with (Z.to_nat 1). rewrite <- Z2Nat.inj_add, <- Z2Nat.inj_le by lia. lia. } split; [|split]; auto. - rewrite gsc_iff in H |- * by assumption. intros. apply ang_graph_has_gen in H8. destruct H8. + rewrite ang_nth_old by assumption. rewrite ans_nth_old. 1: apply H; assumption. red in H8. rewrite H5 in H8. lia. + subst gen. rewrite ang_nth_new, H5, ans_nth_new. apply H2. - simpl. rewrite <- upd_Znth_map. rewrite app_length. rewrite H5 in *. simpl. change (S O) with (Z.to_nat 1). rewrite <- Z2Nat.inj_add, <- sublist_skip in * by lia. rewrite upd_Znth_Zlength; rewrite Zlength_map, spaces_size in *. 2: assumption. rewrite sublist_upd_Znth_r. 2: lia. 2: rewrite Zlength_map, spaces_size; lia. apply Forall_incl with (sublist i MAX_SPACES (map space_start (spaces h))). 2: assumption. rewrite Z.add_comm. replace MAX_SPACES with (MAX_SPACES - i + i) at 1 by (clear; lia). rewrite <- sublist_sublist with (j := MAX_SPACES) by lia. unfold incl. intro a. apply sublist_In. 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