proposition: Lemma whole_graph_fold: forall n sh g p, (forall v : Z, 0 <= v < Z.of_nat n <-> vvalid (lg_gg g) v) -> Z.of_nat n <= Int.max_signed / 8 -> data_at sh (tarray vertex_type (Z.of_nat n)) (map (fun x : Z => vgamma2cdata (vgamma (lg_gg g) x)) (nat_inc_list n)) (pointer_val_val p) = whole_graph sh g p.
proof: Proof. intros. apply pred_ext; unfold whole_graph, full_graph_at, vcell_array_at, SAG_VST; [apply (exp_right n)|Intros n']; rewrite map_length, nat_inc_list_length, list_map_compose. - apply andp_right; auto. apply andp_right; apply prop_right; auto. - destruct (lt_eq_lt_dec n n') as [[? | ?] | ?]; [exfalso | subst n' | exfalso]; auto. + assert (vvalid (lg_gg g) (Z.of_nat n)) by (rewrite <- H1; intuition). rewrite <- H in H3. intuition. + assert (vvalid (lg_gg g) (Z.of_nat n')) by (rewrite <- H; intuition). rewrite <- H1 in H3. intuition. Qed.
imports: CertiGraph.lib.List_ext CertiGraph.unionfind.env_unionfind_arr CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.reachable_computable CertiGraph.graph.UnionFind CertiGraph.msl_application.ArrayGraph CertiGraph.floyd_ext.share CertiGraph.unionfind.spatial_array_graph Coq.Lists.List CertiGraph.unionfind.uf_arr_specs VST.floyd.library