proposition: Lemma body_getCell: semax_body Vprog (@Gprog size inf) f_getCell (@getCell_spec size inf).
proof: Proof. start_function. rewrite (SpaceAdjMatGraph_unfold' _ _ _ addresses u); trivial. assert ((Zlength (map Int.repr (Znth u (@graph_to_symm_mat size g)))) = size). { unfold graph_to_symm_mat, graph_to_mat, vert_to_list. rewrite Znth_map; repeat rewrite Zlength_map by rep_lia. all: rewrite nat_inc_list_Zlength, Z2Nat.id; lia. } assert (0 <= i < Zlength (map Int.repr (Znth u (@graph_to_symm_mat size g)))) by lia. assert (0 <= i < Zlength (Znth u (@graph_to_symm_mat size g))). { rewrite Zlength_map in H2. lia. } Intros. freeze FR := (iter_sepcon _ _) (iter_sepcon _ _). unfold list_rep. forward. forward. forward. thaw FR. rewrite (SpaceAdjMatGraph_unfold' _ _ _ addresses u); trivial. entailer!. all: unfold graph_to_symm_mat; rewrite graph_to_mat_Zlength; rep_lia. 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