Commit 3241299c authored by charguer's avatar charguer
Browse files

rank_cleanup union

parent 3c95625e
......@@ -34,16 +34,20 @@ Definition parent (x:loc) (c:contents_) : loc :=
Definition no_self_link (D:set loc) (L:map loc contents_) : Prop :=
forall x y, x \in D -> L[x] = Link y -> x <> y.
(** [inv D R L] captures the invariants of the structure *)
Definition inv (D:set loc) (R:loc->loc) (L:map loc contents_) : Prop :=
D = dom L
/\ roots (LibMap_map parent L) R
/\ (forall y, y \notin D -> R y = y)
/\ no_self_link D L.
(** [UF D R] is a heap predicate that describes a pool of references,
whose locations belong do the domain [D], representing an instance
of the union-find data structure with respect to the root function [R]. *)
Definition UF (D:set loc) (R:loc->loc) : hprop :=
Hexists (L:map loc contents_), Group Ref L
\* \[D = dom L
/\ roots (LibMap_map parent L) R
/\ (forall y, y \notin D -> R y = y)
/\ no_self_link D L].
Hexists (L:map loc contents_), Group Ref L \* \[inv D R L].
(*******************************************************************)
......@@ -55,13 +59,26 @@ Proof using.
intros. rewrite index_eq_indom. rewrite~ LibMap_dom_map.
Qed.
Lemma indom_root : forall D R L x,
inv D R L ->
x \in D ->
(R x) \in D.
Proof using.
introv (HD&HR&HN&HL) Hx. subst D.
rewrites* <- index_map_parent_eq.
applys~ index_R. rewrite~ index_map_parent_eq.
Qed.
Hint Extern 1 (index (LibMap_map parent ?L) ?x) => rewrite index_map_parent_eq.
Hint Extern 1 (?x \in dom ?L) => congruence.
Hint Resolve indom_root.
(*******************************************************************)
(** Create *)
(** [roots] is preserved by creation of a fresh root. *)
Lemma roots_create : forall L R x,
roots (LibMap_map parent L) R ->
x \notindom L ->
......@@ -83,38 +100,68 @@ Proof using.
{ typeclass. } }
Qed.
(** [inv] is preserved by creation of a fresh root. *)
Lemma inv_create : forall L R D x,
inv D R L ->
x \notin D ->
inv (D \u '{x}) R L[x:=Root 0].
Proof using.
introv (HD&HR&HN&HL) Hx. splits.
{ rewrite~ dom_update. }
{ subst D. applys~ roots_create. }
{ intros y Hy. rewrite notin_union_eq in Hy. applys~ HN. }
{ intros y z Hy Hz. rewrite in_union_eq, in_single_eq in Hy.
destruct Hy.
{ rewrite read_update in Hz. case_if. applys* HL. }
{ subst y. rewrite read_update in Hz. case_if. } }
Qed.
(** [create] is correct. *)
Lemma create_spec : forall D R,
app create [tt]
PRE (UF D R)
POST (fun x => UF (D \u \{x}) R \* \[x \notin D]).
Proof using.
xcf. xunfold UF. xpull. intros L (HD&HR&HN&HL).
xapp. intros x. xsimpl.
{ congruence. }
{ splits.
{ rewrite~ dom_update. }
{ applys~ roots_create. applys~ HN. }
{ intros y Hy. rewrite notin_union_eq in Hy. applys~ HN. }
{ intros y z Hy Hz. rewrite in_union_eq, in_single_eq in Hy.
destruct Hy.
{ rewrite read_update in Hz. case_if. applys* HL. }
{ subst y. rewrite read_update in Hz. case_if. } } }
xcf. xunfold UF. xpull. intros L HI. lets (HD&HR&HN&HL): HI.
xapp. intros x. xsimpl~. applys~ inv_create.
Qed.
Hint Extern 1 (RegisterSpec create) => Provide create_spec.
(*******************************************************************)
(** Find *)
(** [inv] is preserved by path compression *)
Lemma inv_compress : forall D R L L' x r,
inv D R L ->
x \in D ->
x <> R x ->
L' = L[x := Link (R x)] ->
inv D R L'.
Proof using.
introv (HD&HR&HN&HL) Hx Nx ->. splits.
{ rewrite~ dom_update_at_index. rewrite~ index_eq_indom. }
{ applys* roots_compress.
{ rewrite* LibMap_map_update. }
{ rewrite* index_map_parent_eq. } }
{ auto. }
{ intros a b Ha Hb. rewrite read_update in Hb. case_if.
{ inverts~ Hb. } { applys~ HL. } }
Qed.
(** [find] is correct. *)
Lemma find_spec : forall D R x,
x \in D ->
app find [x]
INV (UF D R)
POST (fun r => \[r = R x]).
Proof using.
introv Ix. xunfold UF. xpull. intros L (HD&HR&HN&HL).
introv Ix. xunfold UF. xpull. intros L HI. lets (HD&HR&HN&HL): HI.
forwards* Hx: HR x.
forwards (d&Hx'): reprn_of_repr Hx. clear Hx.
gen L x. induction_wf IH: lt_wf d. hide IH. intros.
......@@ -124,10 +171,9 @@ Proof using.
{ intros y Hy. sets L':(LibMap_map parent L). inverts Hx' as.
{ intros IRx E1 E2. forwards* HLx: roots_inv_L x HR.
{ subst L'. rewrite~ index_map_parent_eq. }
subst L'.
rewrite* LibMap_map_read in E1. rewrite <- E2 in E1. rewrite Hy in E1. simpls.
unfolds in HL. false~ (>> HL x y). }
{ intros Ix' N Hy'. rename d0 into d.
subst L'. rewrite* LibMap_map_read in E1. rewrite <- E2 in E1.
rewrite Hy in E1. simpls. unfolds in HL. false~ (>> HL x y). }
{ intros Ix' N Hy'. rename d0 into d.
sets z: (L'[x]). asserts EQ: (z = y).
{ subst z L'. rewrite~ LibMap_map_read. rewrite~ Hy. }
clearbody z. subst z.
......@@ -140,14 +186,8 @@ Proof using.
asserts Ryx: (R y <> x).
{ intros E. forwards~ HL'x: roots_inv_L x HR. subst L'.
rewrite~ LibMap_map_read in HL'x. rewrite Hy in HL'x. simpls. false. }
clears L L'. clear L HN. intros Hr L (HD&HR&HN&HL).
xapp~. xrets*. splits*.
{ rewrite~ dom_update_at_index. rewrite~ index_eq_indom. }
{ rewrite Hr,ER. applys* roots_compress.
{ rewrite* LibMap_map_update. }
{ rewrite* index_map_parent_eq. } }
{ intros a b Ha Hb. rewrite read_update in Hb. case_if.
{ inverts~ Hb. } { applys~ HL. } } } }
clears L L'. clear L HN. intros Hr L HI. lets (HD&HR&HN&HL): HI.
xapp~. xrets*. applys~ inv_compress. } }
Qed.
Hint Extern 1 (RegisterSpec find) => Provide find_spec.
......@@ -156,6 +196,8 @@ Hint Extern 1 (RegisterSpec find) => Provide find_spec.
(*******************************************************************)
(** Same *)
(** [same] is correct. *)
Lemma same_spec : forall D R x y,
x \in D ->
y \in D ->
......@@ -172,27 +214,25 @@ Hint Extern 1 (RegisterSpec same) => Provide same_spec.
(*******************************************************************)
(** Union *)
Lemma link_correct : forall D R L x y,
D = dom L ->
roots (LibMap_map parent L) R ->
(forall y, y \notin D -> R y = y) ->
no_self_link D L ->
(** Invariants are preserved by a link operation. *)
Lemma link_correct : forall D R R' L L' x y,
inv D R L ->
R' = link R x y (R y) ->
L' = L[(R x) := Link (R y)] ->
x \in D ->
y \in D ->
(R x) \in D ->
(R y) \in D ->
R x <> R y ->
D = dom L[R x:=Link (R y)]
/\ roots (LibMap_map parent L[R x:=Link (R y)]) (link R x y (R y))
/\ (forall y0 : loc, y0 \notin D -> link R x y (R y) y0 = y0)
/\ no_self_link D L[R x:=Link (R y)].
inv D R' L'.
Proof using.
introv HD HR HN HL Hx Hy HRx HRy Hxy. splits.
{ rewrite~ dom_update_at_index. rewrite~ index_eq_indom. }
{ applys* roots_link R x y. rewrite~ LibMap_map_update. }
{ intros z Hz. unfold link. specializes HN Hz. case_if as Cz.
introv HI ER' EL' Hx Hy Hxy. lets (HD&HR&HN&HL): HI.
forwards* HRx: indom_root x HI. forwards* HRy: indom_root y HI.
splits.
{ subst D L'. rewrite~ dom_update_at_index. }
{ subst L'. applys* roots_link R x y. rewrite~ LibMap_map_update. }
{ intros z Hz. subst R'. unfold link. specializes HN Hz. case_if as Cz.
{ destruct Cz. { false; congruence. } { congruence. } } { auto. } }
{ intros a b Ha Hb. rewrite read_update in Hb. case_if.
{ subst L'. intros a b Ha Hb. rewrite read_update in Hb. case_if.
{ inverts~ Hb. } { applys~ HL. } }
Qed.
......@@ -212,6 +252,29 @@ Proof using.
{ eauto. } { simpls. false~ HN (R x). }
Qed.
Generalizable Variables A B.
Axiom LibMap_extens : forall A `{Inhab B} (M1 M2:map A B),
dom M1 = dom M2 ->
(forall (x:A), M1[x] = M2[x]) ->
M1 = M2.
Lemma inv_rerank : forall x D L L' R n,
inv D R L ->
x \in D ->
L' = L[R x := Root n] ->
inv D R L'.
Proof using.
introv HI Hd EL'. lets (HD&HR&HN&HL): HI.
forwards~ HRx: indom_root x HI. splits.
{ subst L'. rewrite~ dom_update_at_index. rewrite~ index_eq_indom. }
{ asserts_rewrite~ (LibMap_map parent L' = LibMap_map parent L).
{ skip. (* TODO applys LibMap_extens. by extensionality ... *) } }
{ auto. }
{ subst L'. unfolds no_self_link. intros a b Ha HLa.
rewrite read_update in HLa. case_if. applys~ HL. }
Qed.
Lemma union_spec : forall D R x y,
x \in D ->
y \in D ->
......@@ -220,25 +283,19 @@ Lemma union_spec : forall D R x y,
(fun z => Hexists R', UF D R' \* \[R' = link R x y z]).
Proof using.
introv Ix Iy. xcf. xapps*. xapps*. xapps. xif.
{ unfold UF. xpull. intros L (HD&HR&HN&HL).
asserts Rx: (R x \in D).
{ subst D. rewrites* <- index_map_parent_eq. applys~ index_R. }
asserts Ry: (R y \in D).
{ subst D. rewrites* <- index_map_parent_eq. applys~ index_R. }
xapps*. xapps*. xmatch.
{ unfold UF. xpull. intros L HI. lets (HD&HR&HN&HL): HI.
xapps~. xapps*. xmatch.
{ xif.
{ xapps~. xrets*. applys* link_correct. }
{ xif.
{ xapp~. xrets*. rewrite link_sym. applys* link_correct. }
{ xapp~. sets L': (L[R x:=Root (n + 1)%I]).
asserts ED: (dom L = dom L').
{ unfold L'. rewrite~ dom_update_at_index. rewrite~ index_eq_indom. }
asserts EP: (LibMap_map parent L' = LibMap_map parent L).
{ unfold L'. skip. (* TODO by extensionality ... *) }
xapp~. xrets*. rewrite link_sym. applys~ link_correct.
{ unfolds roots. rewrite~ EP. }
{ unfolds no_self_link. intros a b Ha HLa. unfold L' in HLa.
rewrite read_update in HLa. case_if. applys~ HL. } } } }
{ unfold L'. rewrite~ dom_update_at_index.
rewrite~ index_eq_indom. rewrite~ <- HD. }
forwards~ HRy: indom_root y HI.
xapp~. xrets*. rewrite link_sym. applys~ link_correct L'.
subst L'. applys~ inv_rerank x. } } }
{ xfail.
forwards* (n&En): roots_inv_L_Root x D.
forwards* (m&Em): roots_inv_L_Root y D.
......@@ -249,40 +306,3 @@ Qed.
Hint Extern 1 (RegisterSpec union) => Provide union_spec.
......@@ -58,8 +58,19 @@ Proof using.
intros. rewrite index_eq_indom. rewrite~ LibMap_dom_map.
Qed.
Lemma indom_root : forall D R L x,
inv D R L ->
x \in D ->
(R x) \in D.
Proof using.
introv (HD&HR&HN&HL) Hx. subst D.
rewrites* <- index_map_parent_eq.
applys~ index_R. rewrite~ index_map_parent_eq.
Qed.
Hint Extern 1 (index (LibMap_map parent ?L) ?x) => rewrite index_map_parent_eq.
Hint Extern 1 (?x \in dom ?L) => congruence.
Hint Resolve indom_root.
(*******************************************************************)
......@@ -206,17 +217,17 @@ Hint Extern 1 (RegisterSpec same) => Provide same_spec.
Lemma link_correct : forall D R R' L L' x y,
inv D R L ->
R' = link R x y (R y) ->
L' = L[(R x) := Link (R y)] ->
x \in D ->
y \in D ->
(R x) \in D ->
(R y) \in D ->
R x <> R y ->
R' = link R x y (R y) ->
L' = L[(R x) := Link (R y)] ->
inv D R' L'.
Proof using.
introv (HD&HR&HN&HL) Hx Hy HRx HRy Hxy ER' EL'. splits.
{ subst D L'. rewrite~ dom_update_at_index. (* rewrite~ index_eq_indom. *) }
introv HI ER' EL' Hx Hy Hxy. lets (HD&HR&HN&HL): HI.
forwards* HRx: indom_root x HI. forwards* HRy: indom_root y HI.
splits.
{ subst D L'. rewrite~ dom_update_at_index. }
{ subst L'. applys* roots_link R x y. rewrite~ LibMap_map_update. }
{ intros z Hz. subst R'. unfold link. specializes HN Hz. case_if as Cz.
{ destruct Cz. { false; congruence. } { congruence. } } { auto. } }
......@@ -235,10 +246,6 @@ Lemma union_spec : forall D R x y,
Proof using.
introv Ix Iy. xcf. xapps*. xapps*. xapps. xif.
{ unfold UF. xpull. intros L HI. lets (HD&HR&HN&HL): HI.
asserts Rx: (R x \in D).
{ subst D. rewrites* <- index_map_parent_eq. applys~ index_R. }
asserts Ry: (R y \in D).
{ subst D. rewrites* <- index_map_parent_eq. applys~ index_R. }
xapp~. xrets*. applys~ link_correct x y HI. }
{ xrets. rewrite~ link_related. }
Qed.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment