proposition: Lemma body_unionS: semax_body Vprog Gprog f_unionS unionS_spec.
proof: Proof. start_function. forward_call (sh, g, x). Intros vret. destruct vret as [g1 x_root]. simpl fst in *. simpl snd in *. apply rank_unchanged_in_bound in H6; auto. assert (vvalid g1 y) by (destruct H3 as [? _]; rewrite <- H3; apply H0). forward_call (sh, g1, y). Intros vret. destruct vret as [g2 y_root]. simpl fst in *. simpl snd in *. apply rank_unchanged_in_bound in H11; auto. assert (H_VALID_XROOT: vvalid g2 x_root) by (destruct H8 as [? _]; rewrite <- H8; destruct H4; apply reachable_foot_valid in H4; apply H4). assert (H_VALID_YROOT: vvalid g2 y_root) by (destruct H9; apply reachable_foot_valid in H9; apply H9). 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_tac (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. rename H12 into Htemp. assert (H12: x_root = y_root). { destruct x_root; destruct y_root; inversion Htemp; trivial. } Exists g2. subst y_root. entailer!. apply (the_same_root_union g g1 g2 x y x_root); auto. - forward. rename H12 into Htemp. assert (x_root <> y_root). { intro; subst; apply Htemp; trivial. } entailer!. - Intros. remember (vgamma g2 x_root) as rpa eqn:?H. destruct rpa as [rankXRoot paXRoot]. symmetry in H13. localize [data_at sh node_type (vgamma2cdata (vgamma g2 x_root)) (pointer_val_val x_root)]. rewrite H13. simpl vgamma2cdata. forward. unlocalize [whole_graph sh g2]. 1: rewrite H13; 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 H14. localize [data_at sh node_type (vgamma2cdata (vgamma g2 y_root)) (pointer_val_val y_root)]. rewrite H14. simpl vgamma2cdata. forward. unlocalize [whole_graph sh g2]. 1: rewrite H14; simpl; apply (@vertices_at_ramif_1_stable _ _ _ _ SGBA_VST _ _ (SGA_VST sh) g2 (vvalid g2) y_root (rankYRoot, paYRoot)); auto. rename H_VALID_XROOT into H15. clear H1 H2 H5 H6. assert (Int.unsigned (Int.repr (Z.of_nat rankXRoot)) = Z.of_nat (vlabel g2 x_root)). { simpl vgamma in H13. inversion H13. apply Int.unsigned_repr. split; [apply Zle_0_nat | specialize (H11 x_root H15); auto]. } assert (Int.unsigned (Int.repr (Z.of_nat rankYRoot)) = Z.of_nat (vlabel g2 y_root)). { simpl vgamma in H14. inversion H14. apply Int.unsigned_repr. split; [apply Zle_0_nat | specialize (H11 y_root H_VALID_YROOT); auto]. } clear H11. forward_if (EX g': UFGraph, PROP (uf_union g x y g' /\ uf_under_bound 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). assert (~ reachable g2 y_root x_root) by (intro; destruct H9; specialize (H16 _ H11); auto). assert (vertices_at sh (vvalid (Graph_gen_redirect_parent g2 x_root y_root H6 H15 H11)) (Graph_gen_redirect_parent g2 x_root y_root H6 H15 H11) = vertices_at sh (vvalid g2) (Graph_gen_redirect_parent g2 x_root y_root H6 H15 H11)). { 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 H13. simpl vgamma2cdata. forward. unlocalize [whole_graph sh (Graph_gen_redirect_parent g2 x_root y_root H6 H15 H11)]. 1: rewrite H13; simpl vgamma2cdata; rewrite H16; apply (@graph_gen_redirect_parent_ramify _ (sSGG_VST sh)); auto. Exists (Graph_gen_redirect_parent g2 x_root y_root H6 H15 H11). entailer !. split. * apply (diff_root_union_1 g g1 g2 x y x_root y_root); auto. * rewrite H1 in *. rewrite H2 in *. rewrite <- Nat2Z.inj_lt in H5. destruct H9. apply uf_under_bound_redirect_parent_lt; 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 H4; auto; destruct H4; specialize (H17 _ H16); auto). assert (vertices_at sh (vvalid (Graph_gen_redirect_parent g2 y_root x_root H6 H11 H16)) (Graph_gen_redirect_parent g2 y_root x_root H6 H11 H16) = vertices_at sh (vvalid g2) (Graph_gen_redirect_parent g2 y_root x_root H6 H11 H16)). { apply vertices_at_Same_set. unfold Ensembles.Same_set, Ensembles.Included, Ensembles.In. simpl. intuition. } forward_if (EX g': UFGraph, PROP (uf_union g x y g' /\ uf_under_bound 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 H14. simpl vgamma2cdata. forward. unlocalize [whole_graph sh (Graph_gen_redirect_parent g2 y_root x_root H6 H11 H16)]. 1: rewrite H14; simpl vgamma2cdata; rewrite H17; apply (@graph_gen_redirect_parent_ramify _ (sSGG_VST sh)); auto. Exists (Graph_gen_redirect_parent g2 y_root x_root H6 H11 H16). entailer!. split. -- apply (diff_root_union_2 g g1 g2 x y x_root y_root); auto. -- rewrite H1 in *. rewrite H2 in *. rewrite <- Nat2Z.inj_lt in H18. apply uf_under_bound_redirect_parent_lt; auto. rewrite (uf_equiv_root_the_same g1 g2) in H4; auto. destruct H4. auto. * localize [data_at sh node_type (vgamma2cdata (vgamma g2 y_root)) (pointer_val_val y_root)]. rewrite H14. simpl vgamma2cdata. forward. unlocalize [whole_graph sh (Graph_gen_redirect_parent g2 y_root x_root H6 H11 H16)]. 1: rewrite H14; simpl vgamma2cdata; rewrite H17; apply (@graph_gen_redirect_parent_ramify _ (sSGG_VST sh)); auto. set (g3 := Graph_gen_redirect_parent g2 y_root x_root H6 H11 H16). 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 H13. simpl vgamma2cdata. forward. rewrite add_repr. replace (Z.of_nat rankXRoot + 1) with (Z.of_nat (rankXRoot + 1)). 2: 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 H20. clear H20. rewrite H13. simpl vgamma2cdata. apply (@graph_vgen_ramify _ (sSGG_VST sh)). ++ subst g3. simpl. destruct H8 as [? _]. rewrite <- H8. destruct H4; apply reachable_foot_valid in H4; apply H4. ++ subst g3. remember (Graph_gen_redirect_parent g2 y_root x_root H6 H11 H16) as g3. apply (graph_gen_redirect_parent_vgamma _ _ _ rankXRoot paXRoot) in Heqg3; auto. intros. inversion H20; auto. -- Exists (Graph_vgen g3 x_root (rankXRoot + 1)%nat). entailer!. rewrite H1 in *; rewrite H2 in *. assert (Z.of_nat (vlabel g2 x_root) = Z.of_nat (vlabel g2 y_root)) by (clear -H5 H18; intuition auto with *). apply Nat2Z.inj in H24. simpl in H13. inversion H13. apply uf_under_bound_redirect_parent_eq; auto. rewrite (uf_equiv_root_the_same g1 g2) in H4; auto. destruct H4. auto. + Intros g'. Exists g'. 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