proposition: Lemma heap_head_cut_thread_info: forall h i s (H1: 0 <= i < Zlength (spaces h)) (H2: has_space (Znth i (spaces h)) s), i <> 0 -> heap_head (cut_heap h i s H1 H2) = heap_head h.
proof: Proof. intros. destruct (heap_head_cons h) as [hs1 [l1 [? ?]]]. destruct (heap_head_cons (cut_heap h i s H1 H2)) as [hs2 [l2 [? ?]]]. rewrite H3, H5. simpl in H4. pose proof (split3_full_length_list 0 i _ _ H1 (Zminus_0_l_reverse (Zlength (spaces h)))). replace (i - 0) with i in H6 by lia. simpl in H6. remember (firstn (Z.to_nat i) (spaces h)) as ls1. remember (skipn (Z.to_nat (i + 1)) (spaces h)) as ls2. assert (Zlength ls1 = i). { rewrite Zlength_length by lia. subst ls1. apply firstn_length_le. clear H5. rewrite Zlength_correct in H1. rep_lia. } rewrite H6 in H4 at 1. rewrite (upd_Znth_char _ _ _ _ _ H7) in H4. rewrite H6 in H0. clear -H0 H4 H H7. destruct ls1. - rewrite Zlength_nil in H7. exfalso. apply H. subst i. reflexivity. - simpl in H0, H4. inversion H0. subst hs1. inversion H4. reflexivity. 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