proposition: Lemma body_makeSet: semax_body Vprog Gprog f_makeSet makeSet_spec.
proof: Proof. start_function. forward_call (sh, 8). - compute. split; intros; inversion H. - Intros x. assert_PROP (x <> null) as x_not_null by (entailer !; destruct H0 as [? _]; apply H0). assert_PROP (~ vvalid g x) by (entailer; apply (@vertices_at_sepcon_unique_1x _ _ _ _ SGBA_VST _ _ (SGA_VST sh) (SGAvs_VST sh) g x (vvalid g) (O, null))). forward. forward. forward. Exists (make_set_Graph O tt tt x g x_not_null H). Exists x. entailer!. + split; simpl; [right | apply is_partial_make_set_pregraph]; auto. + assert (Coqlib.Prop_join (vvalid g) (eq x) (vvalid (make_set_Graph 0%nat tt tt x g x_not_null H))). { simpl; hnf; split; intros; [unfold graph_gen.addValidFunc | subst a]; intuition. } assert (vgamma (make_set_Graph O tt tt x g x_not_null H) x = (O, x)). { unfold vgamma, UnionFindGraph.vgamma. simpl. f_equal. - destruct (SGBA_VE x x); [| hnf in c; unfold Equivalence.equiv in c; exfalso]; auto. - unfold graph_gen.updateEdgeFunc. destruct (EquivDec.equiv_dec (x, tt) (x, tt)). 2: compute in c; exfalso; auto. destruct (SGBA_VE null null); auto. hnf in c. unfold Equivalence.equiv in c. exfalso; auto. } rewrite <- (vertices_at_sepcon_1x (make_set_Graph 0%nat tt tt x g x_not_null H) x (vvalid g) _ (O, x)); auto. apply sepcon_derives. 1: apply derives_refl. assert (vertices_at sh (vvalid g) g = vertices_at sh (vvalid g) (make_set_Graph O tt tt x g x_not_null H)). { apply vertices_at_vertices_identical. simpl. hnf. intros. destruct a as [y ?]. unfold Morphisms_ext.app_sig. simpl. unfold UnionFindGraph.vgamma. simpl. unfold graph_gen.updateEdgeFunc. f_equal. - destruct (SGBA_VE y x); [hnf in e; subst y; exfalso |]; auto. - destruct (EquivDec.equiv_dec (x, tt) (y, tt)); auto. hnf in e. inversion e. subst y. exfalso; auto. } rewrite <- H5. apply derives_refl. Qed.
imports: CertiGraph.sample_mark.env_unionfind CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.reachable_computable CertiGraph.msl_application.Graph CertiGraph.msl_application.UnionFindGraph CertiGraph.msl_application.GList CertiGraph.msl_application.GList_UnionFind CertiGraph.floyd_ext.share CertiGraph.sample_mark.spatial_graph_glist