proposition: Lemma body_find: semax_body Vprog Gprog f_find find_spec.
proof: Proof. start_function. remember (vgamma g x) as rpa eqn:?H. destruct rpa as [r pa]. localize [data_at sh node_type (vgamma2cdata (vgamma g x)) (pointer_val_val x)]. rewrite <- H0. simpl vgamma2cdata. forward. 1: entailer!; destruct pa; simpl; auto. unlocalize [whole_graph sh g]. 1: rewrite <- H0; simpl vgamma2cdata; apply (@vertices_at_ramif_1_stable _ _ _ _ SGBA_VST _ _ (SGA_VST sh) g (vvalid g) x (r, pa)); auto. assert (H_PARENT_Valid: vvalid g pa) by (eapply valid_parent; eauto). forward_if (EX g': Graph, EX rt : pointer_val, PROP (findS g x g' /\ uf_root g' x rt) LOCAL (temp _p (pointer_val_val rt); temp _x (pointer_val_val x)) SEP (whole_graph sh g')). - apply denote_tc_test_eq_split; apply graph_local_facts; auto. - forward_call (sh, g, pa). Intros vret. destruct vret as [g' root]. simpl fst in *. simpl snd in *. Opaque pointer_val_val. forward. Transparent pointer_val_val. pose proof (true_Cne_neq _ _ H1). assert ((vgamma g' x) = (r, pa)) by (apply (findS_preserves_vgamma g); auto). assert (weak_valid g' root) by (right; destruct H3; apply reachable_foot_valid in H3; auto). assert (vvalid g' x) by (destruct H2 as [_ [[? _] _]]; rewrite <- H2; apply H). assert (~ reachable g' root x) by (destruct H3; apply (vgamma_not_reachable' _ _ r pa); auto). remember (Graph_gen_redirect_parent g' x root H6 H7 H8) as g''. assert (ggrp_rel g' x root g''). { exists H6, H7, H8. trivial. } clear Heqg'' H6 H7 H8. localize [data_at sh node_type (Vint (Int.repr (Z.of_nat r)), pointer_val_val pa) (pointer_val_val x)]. forward. Exists g''. Exists root. unlocalize [vertices_at sh (vvalid g'') g''] using g'' assuming H9. + assert (root <> null). { destruct H3. apply reachable_foot_valid in H3. intro. subst root. apply (valid_not_null g' null H3). simpl. auto. } eapply derives_trans. apply (@graph_gen_redirect_parent_ramify_rel _ (sSGG_VST sh)); eauto. apply sepcon_derives. apply derives_refl. apply allp_right. intro g'''. rewrite <- imp_andp_adjoint. rewrite andp_comm. rewrite imp_andp_adjoint. apply prop_left. intro Heqg''. rewrite <- imp_andp_adjoint. rewrite TT_andp. subst g''. apply derives_refl. + entailer!. split. * apply (graph_gen_redirect_parent_findS g g' x r r pa root _ _ _); auto. * simpl. apply (uf_root_gen_dst_same g' (liGraph g') x x root); auto. -- apply (uf_root_edge _ (liGraph g') _ pa); auto. apply (vgamma_not_dst g' x r pa); auto. -- apply reachable_refl; auto. - forward. Exists g x. entailer!. apply false_Cne_eq in H1. subst pa. split; split; [|split| |]; auto. + reflexivity. + apply (uf_equiv_refl _ (liGraph g)). + repeat intro; auto. + apply uf_root_vgamma with (n := r); auto. - Intros g' rt. forward. Exists g' rt. entailer!. 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