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 <- H1. simpl vgamma2cdata. forward. 1: entailer!; destruct pa; simpl; auto. unlocalize [whole_graph sh g]. 1: rewrite <- H1; simpl; 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': UFGraph, EX rt : pointer_val, PROP (uf_equiv g g' /\ uf_root g' x rt /\ uf_under_bound g' /\ rank_unchanged g g') 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. assert (pa <> x). { intro; subst; apply H2; trivial. } assert (weak_valid g' root) by (right; destruct H4; apply reachable_foot_valid in H4; auto). assert (vvalid g' x) by (destruct H3 as [? _]; rewrite <- H3; apply H). assert (~ reachable g' root x) by (apply (uf_equiv_not_reachable g g' x r pa root); auto). assert (vertices_at sh (vvalid (Graph_gen_redirect_parent g' x root H8 H9 H10)) (Graph_gen_redirect_parent g' x root H8 H9 H10) = vertices_at sh (vvalid g') (Graph_gen_redirect_parent g' x root H8 H9 H10)). { apply vertices_at_Same_set. unfold Ensembles.Same_set, Ensembles.Included, Ensembles.In. simpl. intuition. } remember (vgamma g' x) as rpa eqn:?H. destruct rpa as [r' pa']. symmetry in H12. localize [data_at sh node_type (Vint (Int.repr (Z.of_nat r')), pointer_val_val pa') (pointer_val_val x)]. forward. unlocalize [whole_graph sh (Graph_gen_redirect_parent g' x root H8 H9 H10)]. + rewrite H11. apply (@graph_gen_redirect_parent_ramify _ (sSGG_VST sh)); auto. destruct H4. apply reachable_foot_valid in H4. intro. subst root. apply (valid_not_null g' null H4). simpl. auto. + Exists (Graph_gen_redirect_parent g' x root H8 H9 H10) root. rewrite H11. entailer!. assert (uf_root g' x root). { rewrite <- (uf_equiv_root_the_same g g' x root); auto. apply (uf_root_edge _ (liGraph g) _ pa); [| apply (vgamma_not_dst g x r pa) | rewrite (uf_equiv_root_the_same g g')]; auto. } split; [|split]. * apply (graph_gen_redirect_parent_equiv g g' x r pa); auto. * simpl. apply (uf_root_gen_dst_same g' (liGraph g') x x root); auto. apply reachable_refl; auto. * apply uf_under_bound_redirect_parent; auto. - forward. Exists g x. entailer!. rename H2 into Htemp. assert (H2: pa = x). { destruct pa; destruct x; inversion Htemp; trivial. } subst pa. split. + apply (uf_equiv_refl _ (liGraph g)). + apply uf_root_vgamma with (n := r); auto. - Intros g' rt. forward. Exists g' rt. entailer!. Qed.
imports: CertiGraph.unionfind.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.unionfind.spatial_graph_glist