proposition: Lemma body_initialise_list: semax_body Vprog (@Gprog size inf) f_initialise_list (@initialise_list_spec size).
proof: Proof. start_function. assert_PROP(Zlength old_list = size). entailer!. forward_for_simple_bound size (EX i : Z, PROP () LOCAL (temp _list arr; temp _size (Vint (Int.repr size)); temp _a (Vint (Int.repr a))) SEP ( data_at Tsh (tarray tint size) (repeat (Vint (Int.repr a)) (Z.to_nat i) ++ (sublist i size old_list)) arr ))%assert. entailer!. rewrite app_nil_l. rewrite sublist_same by lia. entailer!. forward. entailer!. rewrite (sublist_split i (i+1)) by lia. replace (sublist i (i+1) old_list) with [Znth i old_list]. simpl. rewrite upd_Znth_char. rewrite <- repeat_app' by lia. rewrite <- app_assoc. simpl. auto. apply Zlength_repeat; lia. symmetry; apply sublist_one; lia. entailer!. rewrite sublist_nil. rewrite app_nil_r. entailer!. Qed.
imports: CertiGraph.prim.prim_env CertiGraph.lib.find_lemmas CertiGraph.priq.is_empty_lemmas CertiGraph.graph.MathUAdjMatGraph CertiGraph.graph.SpaceUAdjMatGraph1 CertiGraph.prim.prim_spec1