proposition: Lemma body_union: semax_body Vprog Gprog f_Union union_spec.
proof: Proof. start_function. forward_call (sh, g, subsets, 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, subsets, y). Intros vret. destruct vret as [g2 y_root]. simpl fst in *. simpl snd in *. forward_if (PROP (x_root <> y_root) LOCAL (temp _yroot (Vint (Int.repr y_root)); temp _xroot (Vint (Int.repr x_root)); temp _subsets (pointer_val_val subsets); temp _x (Vint (Int.repr x)); temp _y (Vint (Int.repr y))) SEP (whole_graph sh g2 subsets)). - forward. apply (exp_right g2). entailer. rewrite whole_graph_unfold. Intros n. apply prop_right. apply (the_same_root_union g g1 g2 x y y_root); auto. assert (x_root = y_root). { assert (Int.signed (Int.repr x_root) = Int.signed (Int.repr y_root)) by (rewrite H6; auto). rewrite !Int.signed_repr in H10; auto. - apply (bounded_vertex _ (Z.of_nat n)); auto. destruct H5. apply reachable_foot_valid in H5. rewrite <- H8 in H5; auto. - apply (bounded_vertex _ (Z.of_nat n)); auto. destruct H4. destruct H2. apply reachable_foot_valid in H2. rewrite H4 in H2. rewrite <- H8 in H2; auto. } subst y_root. apply H2. - forward. entailer!. - rewrite whole_graph_unfold. Intros n. assert (0 <= x_root < Z.of_nat n) by (destruct H4; destruct H2; apply reachable_foot_valid in H2; rewrite H4 in H2; rewrite <- H7 in H2; auto). assert (H_XROOT_BOUND: 0 <= x_root < Zlength (nat_inc_list n)) by (rewrite Zlength_correct, nat_inc_list_length; apply H9). assert (Hxroot: Int.min_signed <= x_root <= Int.max_signed). { split; try rep_lia. transitivity (Z.of_nat n); try lia. transitivity (Int.max_signed / 8). 1: lia. apply Z.lt_le_incl. apply Z.div_lt; rep_lia. } forward. rewrite <- (map_id (nat_inc_list n)) at 1. rewrite Znth_nat_inc_list; auto. simpl id. unfold vgamma2cdata at 1. unfold vgamma at 1. unfold UnionFindGraph.vgamma. assert (0 <= y_root < Z.of_nat n) by (destruct H5; apply reachable_foot_valid in H5; rewrite <- H7 in H5; auto). assert (H_YROOT_BOUND: 0 <= y_root < Zlength (nat_inc_list n)) by (rewrite Zlength_correct, nat_inc_list_length; apply H10). assert (Hyroot: Int.min_signed <= y_root <= Int.max_signed). { split; try rep_lia. transitivity (Z.of_nat n); try lia. transitivity (Int.max_signed / 8). 1: lia. apply Z.lt_le_incl. apply Z.div_lt; rep_lia. } forward. rewrite <- (map_id (nat_inc_list n)) at 1. rewrite Znth_nat_inc_list; auto. unfold vgamma2cdata at 1. unfold vgamma at 1. unfold UnionFindGraph.vgamma. simpl id. forward_if (EX g': UFGraph, PROP (uf_union g x y g') LOCAL (temp _yRank (Vint (Int.repr (Z.of_nat (vlabel (lg_gg g2) y_root)))); temp _xRank (Vint (Int.repr (Z.of_nat (vlabel (lg_gg g2) x_root)))); temp _yroot (Vint (Int.repr y_root)); temp _xroot (Vint (Int.repr x_root)); temp _subsets (pointer_val_val subsets); temp _x (Vint (Int.repr x)); temp _y (Vint (Int.repr y))) SEP (whole_graph sh g' subsets)). + Opaque Znth. forward. rewrite Znth_nat_inc_list; auto. assert (weak_valid g2 y_root) by (right; rewrite <- H7; auto). assert (vvalid g2 x_root) by (rewrite <- H7; auto). assert (~ reachable g2 y_root x_root) by (intro; destruct H5; specialize (H15 _ H14); auto). apply (exp_right (Graph_gen_redirect_parent g2 x_root y_root H12 H13 H14)). unfold vgamma2cdata at 2. unfold vgamma at 2. unfold UnionFindGraph.vgamma. Opaque vgamma2cdata. Opaque vgamma. entailer !. Transparent vgamma. Transparent vgamma2cdata. * apply (diff_root_union_1 g g1 g2 x y x_root y_root); auto. * rewrite whole_graph_unfold. apply (exp_right n). rewrite <- upd_Znth_Graph_redirect_parent; auto. entailer!. + assert (weak_valid g2 x_root) by (right; rewrite <- H7; auto). assert (vvalid g2 y_root) by (rewrite <- H7; auto). assert (~ reachable g2 x_root y_root) by (intro; rewrite (uf_equiv_root_the_same g1 g2) in H2; auto; destruct H2; specialize (H15 _ H14); auto). forward_if (EX g': UFGraph, PROP (uf_union g x y g') LOCAL (temp _yRank (Vint (Int.repr (Z.of_nat (vlabel (lg_gg g2) y_root)))); temp _xRank (Vint (Int.repr (Z.of_nat (vlabel (lg_gg g2) x_root)))); temp _yroot (Vint (Int.repr y_root)); temp _xroot (Vint (Int.repr x_root)); temp _subsets (pointer_val_val subsets); temp _x (Vint (Int.repr x)); temp _y (Vint (Int.repr y))) SEP (whole_graph sh g' subsets)). * forward. rewrite Znth_nat_inc_list; auto. apply (exp_right (Graph_gen_redirect_parent g2 y_root x_root H12 H13 H14)). unfold vgamma2cdata at 2. unfold vgamma at 2. unfold UnionFindGraph.vgamma. Opaque vgamma2cdata. Opaque vgamma. entailer!. Transparent vgamma. Transparent vgamma2cdata. -- apply (diff_root_union_2 g g1 g2 x y x_root y_root); auto. -- rewrite whole_graph_unfold. apply (exp_right n). rewrite <- upd_Znth_Graph_redirect_parent; auto. entailer!. * forward. rewrite Znth_nat_inc_list; auto. remember (Graph_gen_redirect_parent g2 y_root x_root H12 H13 H14) as g3. assert (uf_union g x y g3) by (rewrite Heqg3; simpl; apply (diff_root_union_2 g g1 g2 x y x_root y_root); auto). unfold vgamma2cdata at 2. unfold vgamma at 2. unfold UnionFindGraph.vgamma. forward. apply (exp_right (Graph_vgen g3 x_root ((vlabel (lg_gg g2) x_root) + 1)%nat)). Opaque vgamma2cdata. Opaque vgamma. entailer !. Transparent vgamma. Transparent vgamma2cdata. rewrite upd_Znth_diff; auto; [|rewrite Zlength_map, Zlength_correct, nat_inc_list_length; auto..]. rewrite Znth_nat_inc_list; auto. rewrite whole_graph_unfold. apply (exp_right n). entailer !. cut (upd_Znth x_root (upd_Znth y_root (map (fun x0 : Z => vgamma2cdata (vgamma (lg_gg g2) x0)) (nat_inc_list n)) (Vint (Int.repr x_root), Vint (Int.repr (Z.of_nat (vlabel (lg_gg g2) y_root))))) (let (x0, _) := vgamma2cdata (vgamma (lg_gg g2) x_root) in x0, Vint (Int.repr (Z.of_nat (vlabel (lg_gg g2) x_root) + 1))) = map (fun x0 : Z => vgamma2cdata (vgamma (lg_gg (Graph_vgen (Graph_gen_redirect_parent g2 y_root x_root H12 H13 H14) x_root (vlabel (lg_gg g2) x_root + 1)%nat)) x0)) (nat_inc_list n)); intros. -- rewrite <- H23. apply derives_refl. -- clear -H6 H9 H10. assert (Zlength (map (fun m : Z => vgamma2cdata (vgamma (lg_gg g2) m)) (nat_inc_list n)) = Z.of_nat n) by (rewrite Zlength_map, Zlength_correct, nat_inc_list_length; auto). assert (Zlength (upd_Znth y_root (map (fun x0 : Z => vgamma2cdata (vgamma (lg_gg g2) x0)) (nat_inc_list n)) (Vint (Int.repr x_root), Vint (Int.repr (Z.of_nat (vlabel (lg_gg g2) y_root))))) = Z.of_nat n) by (rewrite upd_Znth_Zlength; auto; rewrite <- H in H10; auto). apply (list_eq_Znth _ _ n). ++ rewrite <- (Nat2Z.id n) at 2. rewrite <- Zlength_length. 2: lia. rewrite <- H in H10, H9. rewrite upd_Znth_Zlength; auto; rewrite upd_Znth_Zlength; auto. ++ rewrite list_length_map, nat_inc_list_length; auto. ++ intros. rewrite Znth_nat_inc_list; auto. rewrite (upd_Znth_lookup' (Z.of_nat n)); auto. rewrite (upd_Znth_lookup' (Z.of_nat n)); auto. rewrite Znth_nat_inc_list; auto. unfold vgamma2cdata, vgamma, UnionFindGraph.vgamma. simpl. unfold graph_gen.updateEdgeFunc, graph_gen.update_vlabel, EquivDec.equiv_dec, Z_EqDec, zeq. destruct (Z.eq_dec j x_root). ** subst j. destruct (Z.eq_dec y_root x_root). 1: exfalso; auto. destruct (Z.eq_dec x_root x_root). 2: exfalso; apply n1; auto. do 3 f_equal. transitivity (Z.succ (Z.of_nat (vlabel (lg_gg g2) x_root))). 2: rewrite <- Nat2Z.inj_succ; f_equal; unfold Z_EqDec; lia. rewrite Z.add_1_r. auto. ** destruct (Z.eq_dec j y_root). --- subst j. destruct (Z.eq_dec y_root y_root). 2: exfalso; apply n1; auto. destruct (Z.eq_dec x_root y_root). 1: exfalso; auto. destruct (Z_lt_dec x_root 0). 1: destruct H9; exfalso; lia. auto. --- destruct (Z.eq_dec y_root j). 1: exfalso; apply n1; auto. destruct (Z.eq_dec x_root j). 1: exfalso; auto. auto. + Intros g'. Exists g'. entailer!. Qed.
imports: CertiGraph.lib.List_ext CertiGraph.unionfind.env_unionfind_arr CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.reachable_computable CertiGraph.graph.UnionFind CertiGraph.msl_application.ArrayGraph CertiGraph.floyd_ext.share CertiGraph.unionfind.spatial_array_graph Coq.Lists.List CertiGraph.unionfind.uf_arr_specs VST.floyd.library