Commit 873dcea1 authored by charguer's avatar charguer
Browse files

UF rank

parent 226d5d53
(* Union-find: pointer-based implementation *)
(*
type contents = Root | Link of node
and node = contents ref
*)
type rank = int
type contents = Root of rank | Link of contents ref
type node = contents ref
let create () =
ref (Root 0)
let rec find x =
match !x with
| Root _ -> x
| Link y ->
let r = find y in
x := Link r;
r
let same x y =
find x == find y
let union x y =
let r = find x in
let s = find y in
if r != s then begin
match !r, !s with
| Root n, Root m ->
if n < m then begin
r := Link s;
s
end else if n > m then begin
s := Link r;
r
end else begin
r := Root (n+1);
s := Link r;
r
end
| _ -> assert false
end else r
Set Implicit Arguments.
Require Import CFML.CFLib.
Require Import Stdlib.
Require Import Array_proof.
Require Import UFPointerRank_ml.
Require Import TLC.LibListZ.
Require Import UFArray_map_proof.
(* TODO rename
ref_spec_group
infix_emark_spec_group
infix_colon_eq_spec_group
*)
Section Map.
Transparent map.
Generalizable Variables A B.
Definition LibMap_map A `{Inhab B1} `{Inhab B2} (f:A->B1->B2) (M:map A B1) : map A B2 :=
fun (x:A) => match M x with
| None => None
| Some y => Some (f x y)
end.
Transparent update update_inst bag_update_as_union_single single_bind single_bind_inst LibMap.union_inst LibContainer.union.
Lemma LibMap_map_update : forall A `{Inhab B1} `{Inhab B2} (f:A->B1->B2) (M:map A B1) x y,
LibMap_map f (M[x:=y]) = (LibMap_map f M)[x:=f x y].
Proof using.
intros. extens. intros a. unfold LibMap_map. simpl. unfold bag_update_as_union_single.
unfold single_bind. simpl. unfold single_bind_impl. unfold LibContainer.union. simpl.
unfold LibMap.union_impl.
case_if. autos~. destruct~ (M a). (* TODO: cleanup *)
Qed.
Transparent dom dom_inst.
Lemma LibMap_dom_map : forall A `{Inhab B1} `{Inhab B2} (f:A->B1->B2) (M:map A B1),
dom (LibMap_map f M) = dom M.
Proof using.
intros. unfold LibMap_map. simpl. unfold dom_impl.
fequal. extens. intros x. destruct (M x); auto_false.
Qed.
Transparent read LibMap.read_inst.
Lemma LibMap_map_read : forall A `{Inhab B1} `{Inhab B2} (f:A->B1->B2) (M:map A B1) x,
x \indom M ->
(LibMap_map f M)[x] = f x (M[x]).
Proof using.
introv Hx. unfold LibMap_map. simpl. unfold read, LibMap.read_inst. unfold LibMap.read_impl.
unfold dom, LibMap.dom_inst, dom_impl in Hx. rewrite in_set_st_eq in Hx.
destruct (M x); auto_false.
Qed.
End Map.
Implicit Type D : set loc.
Implicit Type L : map loc contents_.
Implicit Type R : loc->loc.
Implicit Type x y z r s : loc.
(*******************************************************************)
(** Representation predicate *)
Global Instance Inhab_contents_ : Inhab contents_.
Proof using. apply (Inhab_of_val (Root 0)). Qed.
(** [parent L x] maps a root to itself and a link to its destination. *)
Definition parent (x:loc) (c:contents_) : loc :=
match c with
| Root _ => x
| Link y => y
end.
(** [no_self_link D L] asserts that the target of a [Link] always differs
from the node itself. *)
Definition no_self_link (D:set loc) (L:map loc contents_) : Prop :=
forall x y, x \in D -> L[x] = Link y -> x <> y.
(** [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].
(*******************************************************************)
(** Hints *)
Lemma index_map_parent_eq : forall L x,
index (LibMap_map parent L) x = x \indom L.
Proof using.
intros. rewrite index_eq_indom. rewrite~ LibMap_dom_map.
Qed.
Hint Extern 1 (index (LibMap_map parent ?L) ?x) => rewrite index_map_parent_eq.
Hint Extern 1 (?x \indom ?L) => congruence.
(*******************************************************************)
(** Additional lemmas *)
Lemma index_extends : forall (L:map loc loc) x a b,
index L x ->
a \notindom L ->
index L[a:=b] x.
Proof using.
introv Hx Ha. rewrite index_eq_indom in *.
rewrite LibMap.dom_update. rewrite~ @in_union_eq.
Qed.
Hint Resolve index_extends.
Lemma repr_extends : forall (L:map loc loc) a b x r,
a \notindom L ->
x \indom L ->
repr L x r ->
repr (L[a:=b]) x r.
Proof using.
introv Ha Hx HR. gen Hx. induction HR; intros.
{ applys* repr_root. rewrite* LibMap.read_update_neq. { intro_subst. false* Ha. } }
{ applys* repr_next y.
{ rewrite* LibMap.read_update_neq. { intro_subst. false* Ha. } }
{ applys* IHHR. rewrite* <- index_eq_indom. applys* repr_inv_index_l. } }
Qed.
(* TEMPORARY TODO
Lemma no_self_link_update : forall D L x v,
no_self_link D L ->
no_self_link D L
forall y z : loc, y \in D \u '{x} -> L[x:=Root][y] = Link z -> z <> y
no_self_link D L
*)
(*******************************************************************)
(** Create *)
Lemma roots_create : forall L R x,
roots (LibMap_map parent L) R ->
x \notindom L ->
R x = x ->
roots (LibMap_map parent L[x:=Root 0]) R.
Proof using.
introv HR Hx Rx. unfolds roots.
intros y Hy.
rewrite index_eq_indom in Hy. rewrite LibMap_dom_map in Hy. rewrite dom_update in Hy.
rewrite in_union_eq in Hy. destruct Hy.
{ forwards~ Ry: HR y. rewrite LibMap_map_update. applys* repr_extends.
{ rewrite* LibMap_dom_map. }
{ rewrite* LibMap_dom_map. } }
{ rewrite~ @in_single_eq in H. subst y. rewrite LibMap_map_update. rewrite Rx.
applys repr_root.
{ rewrite index_eq_indom. rewrite LibMap.dom_update, LibMap_dom_map.
rewrite in_union_eq. right. rewrite~ @in_single_eq. } (* TODO: simpler *)
{ rewrite* LibMap.read_update_same. } }
Qed.
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_spec ref_spec_group. 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. } } }
Qed.
Hint Extern 1 (RegisterSpec create) => Provide create_spec.
(*******************************************************************)
(** Find *)
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).
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.
xcf. xapps_spec* infix_emark_spec_group. xmatch_no_intros.
{ intros n HLx. xrets*. forwards* Ex: roots_inv_R_root x R.
rewrite* LibMap_map_read. rewrite* HLx. }
{ 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.
sets_eq z: (L'[x]). unfold L' in EQz. rewrite~ LibMap_map_read in EQz.
rewrite Hy in EQz. simpl in EQz. subst z. (* TODO: simplify *)
forwards* ER: roots_inv_R y (R x) HR.
{ applys* repr_of_reprn. }
xapp_spec* (IH d).
{ lets: repr_of_reprn Hy'. subst D. rewrite <- index_map_parent_eq.
applys* repr_inv_index_l. }
{ rewrite* ER. }
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_spec* infix_colon_eq_spec_group. 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. } } } }
Qed.
Hint Extern 1 (RegisterSpec find) => Provide find_spec.
(*******************************************************************)
(** Same *)
Lemma same_spec : forall D R x y,
x \in D ->
y \in D ->
app same [x y]
INV (UF D R)
POST (fun b => \[b = isTrue (R x = R y)]).
Proof using.
introv Ix Iy. xcf. xapps*. xapps*. xapps. xsimpl*.
Qed.
Hint Extern 1 (RegisterSpec same) => Provide same_spec.
(*******************************************************************)
(** Union *)
(* TODO: inv_record *)
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 ->
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)
/\ (forall y0 : loc, y0 \notin D -> link R x y y0 = y0)
/\ no_self_link D L[R x:=Link (R y)].
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.
{ destruct Cz. { false; congruence. } { congruence. } } { auto. } }
{ intros a b Ha Hb. rewrite read_update in Hb. case_if.
{ inverts~ Hb. } { applys~ HL. } }
Qed.
Lemma roots_inv_L_Root : forall x D L R,
roots (LibMap_map parent L) R ->
D = dom L ->
no_self_link D L ->
x \in D ->
(R x) \in D ->
exists n, L[R x] = Root n.
Proof using.
introv HR HD HN Hx HRx. forwards~ EQ: roots_inv_L_root x HR.
rewrite~ LibMap_map_read in EQ. cases (L[R x]) as ERx.
{ eauto. } { simpls. false~ HN (R x). }
Qed.
Section Linkto.
Hint Resolve index_R.
Definition linkto R x y z :=
fun i => If (R i = R x \/ R i = R y) then z else R i.
Lemma linkto_sym : forall R x y z,
linkto R x y z = linkto R y x z.
Proof using.
intros. extens. intros i. unfolds linkto. repeat case_if*.
Qed.
Lemma roots_linkto : forall (L L':map loc loc) R x y R',
R' = linkto R x y (R y) ->
roots L R ->
L' = L [R x := R y] ->
R x <> R y ->
index L x ->
index L y ->
roots L' R'.
Proof using. (* Note: this proof uses hint [repr_inv_L] *)
introv M HR E N Dx Dy. intros u Du.
forwards~ Hx: roots_inv_L_root x HR.
forwards~ Hy: roots_inv_L_root y HR.
forwards~ (I1&I2&_&_): udpate_inv E.
rewrites (rm M). unfold linkto. case_if as C.
{ destruct C as [C|C].
{ rewrite <- C in E. applys~ repr_update_eq E. }
{ rewrite <- C. applys~ repr_update_neq E. } }
{ rew_logic in C. destruct C as [C1 C2]. applys* repr_update_neq E. }
Qed.
Lemma linkto_related : forall R x y,
R x = R y ->
linkto R x y (R x) = R.
Proof using.
introv E. applys fun_ext_1 ;=> i. unfold linkto. case_if as C.
{ destruct~ C. }
{ auto. }
Qed.
End Linkto.
Lemma union_spec : forall D R x y,
x \in D ->
y \in D ->
app union [x y]
(UF D R)
(fun z => Hexists R', UF D R' \* \[R' = linkto 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_spec* infix_emark_spec_group.
xapps_spec* infix_emark_spec_group.
xmatch.
{ xif.
{ xapp_spec* infix_colon_eq_spec_group.
xrets*. applys* link_correct. }
{ xif.
{ xapp_spec* infix_colon_eq_spec_group.
xrets*. rewrite linkto_sym. applys* link_correct. }
{ xapp_spec* infix_colon_eq_spec_group.
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_spec* infix_colon_eq_spec_group.
xret. xsimpl*. rewrite linkto_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. } } } }
{ xfail.
forwards* (n&En): roots_inv_L_Root x D.
forwards* (m&Em): roots_inv_L_Root y D.
(* false C0. *) } }
{ xrets. rewrite~ linkto_related. }
Qed.
Hint Extern 1 (RegisterSpec union) => Provide union_spec.
......@@ -12,6 +12,7 @@ ref_spec_group
infix_emark_spec_group
infix_colon_eq_spec_group
*)
(* TODO: id outside domain *)
Section Map.
Transparent map.
......@@ -209,9 +210,8 @@ 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. }
false C. subst L'.
rewrite* LibMap_map_read in E1. rewrite <- E2 in E1. rewrite Hy in E1. simpls.
unfolds in HL. false~ (>> HL x y). }
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_eq z: (L'[x]). unfold L' in EQz. rewrite~ LibMap_map_read in EQz.
rewrite Hy in EQz. simpl in EQz. subst z. (* TODO: simplify *)
......@@ -281,7 +281,7 @@ Hint Extern 1 (RegisterSpec union) => Provide union_spec.
(* TODO: xapps_spec *)
......
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