proposition: Lemma matrix_unfold: forall sh size contents ptr i, 0 <= i < (Zlength contents) -> matrix_rep sh size contents ptr = iter_sepcon (list_rep sh size ptr contents) (sublist 0 i (Z_inc_list (Z.to_nat (Zlength contents)))) * (list_rep sh size ptr contents i * emp * iter_sepcon (list_rep sh size ptr contents) (sublist (i + 1) (Zlength contents) (Z_inc_list (Z.to_nat (Zlength contents))))).
proof: Proof. intros. unfold matrix_rep. replace (Z_inc_list (Z.to_nat (Zlength contents))) with (sublist 0 (Zlength contents) (Z_inc_list (Z.to_nat (Zlength contents)))) at 1. 2: { rewrite sublist_same; trivial. rewrite Z_inc_list_length, Z2Nat_id', Z.max_r; trivial. apply Zlength_nonneg. } rewrite (sublist_split 0 i (Zlength contents)), (sublist_split i (i+1) (Zlength contents)), (sublist_one i); try lia. 2, 3, 4: rewrite Z_inc_list_length; rewrite Z2Nat.id; lia. rewrite <- (Z_inc_list_eq i (Z.to_nat (Zlength contents))). 2: rewrite Z2Nat_id', Z.max_r; trivial; apply Zlength_nonneg. repeat rewrite iter_sepcon_app. reflexivity. Qed.
imports: VST.floyd.proofauto CertiGraph.summatrix.summatrix VST.msl.iter_sepcon