proposition: Lemma space_start_isnull: forall (g: LGraph) (h: heap) i, graph_heap_compatible g h -> 0 <= i < Zlength (spaces h) -> ~ graph_has_gen g (Z.to_nat i) -> space_start (Znth i (spaces h)) = nullval.
proof: Proof. intros. unfold graph_has_gen in H1. destruct H as [_ [? ?]]. rewrite Forall_forall in H. symmetry. apply H. rewrite <- map_skipn. apply List.in_map. remember (g_gen (glabel g)). replace i with (i - Zlength l + Zlength l) by lia. assert (length l <= Z.to_nat i)%nat by lia. clear H1. assert (0 <= i - Zlength l) by (rewrite <- ZtoNat_Zlength, <- Z2Nat.inj_le in H3; rep_lia). rewrite <- Znth_skipn by rep_lia. rewrite ZtoNat_Zlength. apply Znth_In. split. 1: assumption. rewrite <- ZtoNat_Zlength, Zlength_skipn. rewrite (Z.max_r 0 (Zlength l)) by rep_lia. rewrite Z.max_r; rep_lia. 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