Commit 5216e427 authored by charguer's avatar charguer
Browse files

pointerUF_no seelf link

parent e0fd56f9
(* Union-find: array-based implementation,
(* Union-find: pointer-based implementation,
simplified by omiting the union-by-rank mechanism *)
(*
......@@ -28,3 +28,5 @@ let union x y =
let r = find x in
let s = find y in
if r != s then r := Link s
(* Union-find: pointer-based implementation,
simplified by omiting the union-by-rank mechanism *)
(*
open NullPointers
type node = node ref
(*{ mutable contents : node }*)
let create () =
let rec r = ref r in
r
(*
let r = ref null in
r := r,
r*)
let rec find x =
if !x = x then x else begin
let r = find y in
x := r;
r
end
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 r := s
*)
\ No newline at end of file
......@@ -44,6 +44,17 @@ Proof using.
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.
......@@ -68,6 +79,12 @@ Definition parent (x:loc) (c:contents_) : loc :=
| 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]. *)
......@@ -76,7 +93,8 @@ 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)].
/\ (forall y, y \notin D -> R y = y)
/\ no_self_link D L].
(*******************************************************************)
......@@ -92,19 +110,44 @@ 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 *)
(* TO REFINE *)
Lemma repr_update_neq' : forall (L:map loc loc) a b (L':map loc loc) x z,
repr L x z ->
L' = L[a:=b] ->
L[a] = a ->
z <> a ->
repr L' x z.
Admitted.
Lemma roots_create : forall L R x,
roots (LibMap_map parent L) R ->
x \notindom L ->
......@@ -112,16 +155,17 @@ Lemma roots_create : forall L R x,
roots (LibMap_map parent L[x:=Root]) R.
Proof using.
introv HR Hx Rx. unfolds roots.
intros y Hy.
(*TODO*)
skip_rewrite (index (LibMap_map parent L[x:=Root]) y = (index L y \/ x = y)) in Hy.
destruct Hy.
{ forwards Ry: HR y. skip. (* TODO *)
applys repr_update_neq' x x Ry. (* TODO: need to prove R y \in D , thus <> x. *)
skip. skip. skip. }
{ subst y. rewrite LibMap_map_update. rewrite Rx.
applys repr_root. skip. (* TODO *)
rewrite* LibMap.read_update_same. }
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,
......@@ -129,13 +173,17 @@ Lemma create_spec : forall D R,
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).
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 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.
......@@ -152,13 +200,17 @@ Lemma find_spec : forall D R x,
POST (fun r => \[r = R x]).
Proof using.
(*
introv Ix. xunfold UF. xpull. intros L (Hn&HR).
introv Ix. xunfold UF. xpull. intros L (HD&HR&HN).
forwards* Hx: HR x.
forwards (d&Hx'): reprn_of_repr Hx.
gen L x. induction_wf IH: lt_wf d. hide IH. intros.
xcf. xapps*. xrets. xif.
{ xrets*. forwards* Ex: roots_inv_R_root x L R. congruence. }
{ inverts Hx' as. { intros. false. } intros Ix' N Hy. rename d0 into d.
xcf. xapps_spec* infix_emark_spec_group. xmatch_no_intros.
{ intros 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. false C. subst L'.
rewrite* LibMap_map_read in E1. rewrite <- E2 in E1. rewrite Hy in E1. simpls. false. }
intros Ix' N Hy. rename d0 into d.
sets y: (L[x]). forwards* ER: roots_inv_R y (R x) HR.
xapp_spec* (IH d).
{ subst. rewrites (>> conseq_dom_index_eq Hn). applys* index_L. }
......@@ -201,14 +253,16 @@ Lemma union_spec : forall D R x y,
(fun (_:unit) => Hexists R', UF D R' \* \[R' = link R x y]).
Proof using.
introv Ix Iy. xcf. xapps*. xapps*. xapps. xif.
{ unfold UF. xpull. intros L (HD&HR&HN).
{ 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. }
xapp_spec* infix_colon_eq_spec_group. xsimpl*. 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. } } }
{ destruct Cz. { false; congruence. } { congruence. } } { auto. } }
{ intros a b Ha Hb. rewrite read_update in Hb. case_if.
{ inverts~ Hb. } { applys~ HL. } } }
{ xrets. rewrite~ link_related. }
Qed.
......@@ -250,5 +304,6 @@ Hint Extern 1 (RegisterSpec union) => Provide union_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