proposition: Lemma body_unionS: semax_body Vprog Gprog f_unionS unionS_spec.
proof: Proof. start_function. destruct H. forward_call (sh, g, x). Intros vret. destruct vret as [g1 x_root]. simpl fst in *. simpl snd in *. assert (vvalid g1 y) by (destruct H1 as [_ [[? _] _]]; rewrite <- H1; apply H0). forward_call (sh, g1, y). Intros vret. destruct vret as [g2 y_root]. simpl fst in *. simpl snd in *. destruct H1 as [_ [? _]]. destruct H4 as [_ [? _]]. assert (H_VALID_XROOT: vvalid g2 x_root) by (destruct H4 as [? _]; rewrite <- H4; destruct H2; apply reachable_foot_valid in H2; apply H2). assert (H_VALID_YROOT: vvalid g2 y_root) by (destruct H5; apply reachable_foot_valid in H5; apply H5). assert (H_XROOT_NOT_NULL: x_root <> null) by (intro; subst x_root; apply (valid_not_null g2 null H_VALID_XROOT); simpl; auto). assert (H_YROOT_NOT_NULL: y_root <> null) by (intro; subst y_root; apply (valid_not_null g2 null H_VALID_YROOT); simpl; auto). forward_if (PROP (x_root <> y_root) LOCAL (temp _yRoot (pointer_val_val y_root); temp _xRoot (pointer_val_val x_root); temp _x (pointer_val_val x); temp _y (pointer_val_val y)) SEP (vertices_at sh (vvalid g2) g2)). - apply denote_tc_test_eq_split; apply graph_local_facts; auto. - forward. Exists g2. entailer !; auto. apply true_Ceq_eq in H6. subst y_root. apply (the_same_root_union g g1 g2 x y x_root); auto. - forward. apply false_Ceq_neq in H6. entailer!. - Intros. remember (vgamma g2 x_root) as rpa eqn:?H. destruct rpa as [rankXRoot paXRoot]. symmetry in H7. localize [data_at sh node_type (vgamma2cdata (vgamma g2 x_root)) (pointer_val_val x_root)]. rewrite H7. simpl vgamma2cdata. forward. unlocalize [whole_graph sh g2]. 1: rewrite H7; simpl; apply (@vertices_at_ramif_1_stable _ _ _ _ SGBA_VST _ _ (SGA_VST sh) g2 (vvalid g2) x_root (rankXRoot, paXRoot)); auto. remember (vgamma g2 y_root) as rpa eqn:?H. destruct rpa as [rankYRoot paYRoot]. symmetry in H8. localize [data_at sh node_type (vgamma2cdata (vgamma g2 y_root)) (pointer_val_val y_root)]. rewrite H8. simpl vgamma2cdata. forward. unlocalize [whole_graph sh g2]. 1: rewrite H8; simpl; apply (@vertices_at_ramif_1_stable _ _ _ _ SGBA_VST _ _ (SGA_VST sh) g2 (vvalid g2) y_root (rankYRoot, paYRoot)); auto. forward_if (EX g': Graph, PROP (uf_union g x y g') LOCAL (temp _xRank (Vint (Int.repr (Z.of_nat rankXRoot))); temp _yRank (Vint (Int.repr (Z.of_nat rankYRoot))); temp _xRoot (pointer_val_val x_root); temp _yRoot (pointer_val_val y_root); temp _x (pointer_val_val x); temp _y (pointer_val_val y)) SEP (whole_graph sh g')). + assert (weak_valid g2 y_root) by (right; auto). rename H_VALID_XROOT into H11. assert (~ reachable g2 y_root x_root) by (intro; destruct H5; specialize (H13 _ H12); auto). assert (vertices_at sh (vvalid (Graph_gen_redirect_parent g2 x_root y_root H10 H11 H12)) (Graph_gen_redirect_parent g2 x_root y_root H10 H11 H12) = vertices_at sh (vvalid g2) (Graph_gen_redirect_parent g2 x_root y_root H10 H11 H12)). { apply vertices_at_Same_set. unfold Ensembles.Same_set, Ensembles.Included, Ensembles.In. simpl. intuition. } localize [data_at sh node_type (vgamma2cdata (vgamma g2 x_root)) (pointer_val_val x_root)]. rewrite H7. simpl vgamma2cdata. forward. unlocalize [whole_graph sh (Graph_gen_redirect_parent g2 x_root y_root H10 H11 H12)]. 1: rewrite H7; simpl vgamma2cdata; rewrite H13; apply (@graph_gen_redirect_parent_ramify _ (sSGG_VST sh)); auto. Exists (Graph_gen_redirect_parent g2 x_root y_root H10 H11 H12). rewrite H13. entailer!. apply (diff_root_union_1 g g1 g2 x y x_root y_root); auto. + assert (weak_valid g2 x_root) by (right; auto). rename H_VALID_YROOT into H11. assert (~ reachable g2 x_root y_root) by (intro; rewrite (uf_equiv_root_the_same g1 g2) in H2; auto; destruct H2; specialize (H13 _ H12); auto). assert (vertices_at sh (vvalid (Graph_gen_redirect_parent g2 y_root x_root H10 H11 H12)) (Graph_gen_redirect_parent g2 y_root x_root H10 H11 H12) = vertices_at sh (vvalid g2) (Graph_gen_redirect_parent g2 y_root x_root H10 H11 H12)). { apply vertices_at_Same_set. unfold Ensembles.Same_set, Ensembles.Included, Ensembles.In. simpl. intuition. } forward_if (EX g': Graph, PROP (uf_union g x y g') LOCAL (temp _xRank (Vint (Int.repr (Z.of_nat rankXRoot))); temp _yRank (Vint (Int.repr (Z.of_nat rankYRoot))); temp _xRoot (pointer_val_val x_root); temp _yRoot (pointer_val_val y_root); temp _x (pointer_val_val x); temp _y (pointer_val_val y)) SEP (whole_graph sh g')). * localize [data_at sh node_type (vgamma2cdata (vgamma g2 y_root)) (pointer_val_val y_root)]. rewrite H8. simpl vgamma2cdata. forward. unlocalize [whole_graph sh (Graph_gen_redirect_parent g2 y_root x_root H10 H11 H12)]. 1: rewrite H8; simpl vgamma2cdata; rewrite H13; apply (@graph_gen_redirect_parent_ramify _ (sSGG_VST sh)); auto. Exists (Graph_gen_redirect_parent g2 y_root x_root H10 H11 H12). rewrite H13. entailer!. apply (diff_root_union_2 g g1 g2 x y x_root y_root); auto. * localize [data_at sh node_type (vgamma2cdata (vgamma g2 y_root)) (pointer_val_val y_root)]. rewrite H8. simpl vgamma2cdata. forward. unlocalize [whole_graph sh (Graph_gen_redirect_parent g2 y_root x_root H10 H11 H12)]. 1: rewrite H8; simpl vgamma2cdata; rewrite H13; apply (@graph_gen_redirect_parent_ramify _ (sSGG_VST sh)); auto. set (g3 := (Graph_gen_redirect_parent g2 y_root x_root H10 H11 H12)). assert (uf_union g x y g3) by (subst g3; simpl; apply (diff_root_union_2 g g1 g2 x y x_root y_root); auto). localize [data_at sh node_type (vgamma2cdata (vgamma g2 x_root)) (pointer_val_val x_root)]. rewrite H7. simpl vgamma2cdata. forward. rewrite add_repr. replace (Z.of_nat rankXRoot + 1) with (Z.of_nat (rankXRoot + 1)) by (rewrite Nat2Z.inj_add; simpl; auto). unlocalize [whole_graph sh (Graph_vgen g3 x_root (rankXRoot + 1)%nat)]. -- assert (vertices_at sh (vvalid (Graph_vgen g3 x_root (rankXRoot + 1)%nat)) (Graph_vgen g3 x_root (rankXRoot + 1)%nat) = vertices_at sh (vvalid g3) (Graph_vgen g3 x_root (rankXRoot + 1)%nat)). { apply vertices_at_Same_set. unfold Ensembles.Same_set, Ensembles.Included, Ensembles.In. simpl. intuition. } rewrite H16. clear H16. rewrite H7. simpl vgamma2cdata. apply (@graph_vgen_ramify _ (sSGG_VST sh)). ++ subst g3. simpl. auto. ++ subst g3. remember (Graph_gen_redirect_parent g2 y_root x_root H10 H11 H12) as g3. apply (graph_gen_redirect_parent_vgamma _ _ _ rankXRoot paXRoot) in Heqg3; auto. intros. inversion H16; auto. -- Exists (Graph_vgen g3 x_root (rankXRoot + 1)%nat). entailer!. + Intros g3. forward. Exists g3. 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