Commit f352427e authored by charguer's avatar charguer
Browse files

cleanup ufpointer

parent 97c64ab2
......@@ -2,17 +2,15 @@ Set Implicit Arguments.
Require Import UF.
Require Import UFArray_ml.
(*******************************************************************)
(** Representation predicate *)
Hint Resolve index_of_index_length'.
Implicit Type L : map int int.
Implicit Type R : int->int.
Implicit Type x y z r s : int.
Implicit Types t : loc.
(*******************************************************************)
(** Representation predicate *)
(** [UF n R t] is a heap predicate that describes an array [t]
of size [n] representing an instance of the union-find data
structure with respect to the root function [R], with elements
......@@ -22,7 +20,6 @@ Definition UF (n:int) (R:int->int) (t:loc) : hprop :=
Hexists (L:map int int), t ~> MArray L \* \[conseq_dom n L /\ roots L R].
(*******************************************************************)
(** Create *)
......
......@@ -118,7 +118,7 @@ Proof using.
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.
xcf. xapps*. 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.
......@@ -195,6 +195,9 @@ Proof using.
{ inverts~ Hb. } { applys~ HL. } }
Qed.
(** Additional lemma to prove that if a node [R x] is necessarily
represented as [Root n] for some [n]. *)
Lemma roots_inv_L_Root : forall x D L R,
roots (LibMap_map parent L) R ->
D = dom L ->
......
......@@ -33,16 +33,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].
(*******************************************************************)
......@@ -61,6 +65,8 @@ Hint Extern 1 (?x \in dom ?L) => congruence.
(*******************************************************************)
(** 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 ->
......@@ -82,42 +88,53 @@ 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].
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 *)
(** [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.
xcf. xapps_spec* infix_emark_spec_group. xmatch_no_intros.
xcf. xapps*. 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.
......@@ -153,6 +170,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 ->
......@@ -169,6 +188,30 @@ Hint Extern 1 (RegisterSpec same) => Provide same_spec.
(*******************************************************************)
(** Union *)
(** Invariants are preserved by a link operation. *)
Lemma link_correct : forall D R R' L L' x y,
inv D R L ->
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. *) }
{ 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. } }
{ subst L'. intros a b Ha Hb. rewrite read_update in Hb. case_if.
{ inverts~ Hb. } { applys~ HL. } }
Qed.
(** [union] is correct. *)
Lemma union_spec : forall D R x y,
x \in D ->
y \in D ->
......@@ -177,57 +220,14 @@ 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).
{ 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. }
xapp~. xrets*. 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. } } }
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.
Hint Extern 1 (RegisterSpec union) => Provide union_spec.
(* TODO: inv_record *)
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