proposition: Lemma SpaceAdjMatGraph_unfold': forall sh g_contents (g_ptr : val) (addresses : list val) i, Zlength g_contents = size -> 0 <= i < size -> SpaceAdjMatGraph' sh g_contents g_ptr addresses = sepcon (sepcon (iter_sepcon (list_rep sh addresses g_contents) (sublist 0 i (nat_inc_list (Z.to_nat size)))) (sepcon (list_rep sh addresses g_contents i) (iter_sepcon (list_rep sh addresses g_contents) (sublist (i + 1) (Zlength g_contents) (nat_inc_list (Z.to_nat size)))))) (data_at sh (tarray (tptr tint) size) addresses g_ptr).
proof: Proof. intros. unfold SpaceAdjMatGraph'. replace (nat_inc_list (Z.to_nat size)) with (sublist 0 size (nat_inc_list (Z.to_nat size))) at 1. 2: rewrite sublist_same; trivial; rewrite nat_inc_list_Zlength; lia. rewrite (sublist_split 0 i size), (sublist_split i (i+1) size), (sublist_one i); try lia. 2, 3, 4: rewrite nat_inc_list_Zlength; rewrite Z2Nat.id; lia. rewrite nat_inc_list_i. 2: rewrite Z2Nat_id', Z.max_r; lia. repeat rewrite iter_sepcon_app. simpl. rewrite sepcon_emp. rewrite H. reflexivity. Qed.
imports: Coq.ZArith.BinInt Coq.ZArith.Zcomplements Coq.micromega.Lia Coq.ZArith.Znat VST.floyd.proofauto CertiGraph.graph.graph_model CertiGraph.lib.List_ext CertiGraph.graph.MathAdjMatGraph