Commit 0e01d34e authored by charguer's avatar charguer
Browse files

polish

parent 425cbaa7
......@@ -49,12 +49,7 @@ Proof using. intros. xunfolds* Queue. Qed.
Arguments Queue_close : clear implicits.
(** Customization of [xopen] and [xclose] tactics for [Queue].
These tactics avoid the need to call [hchange] or [xchange]
by providing explicitly the lemmas [Queue_open] and [Queue_close].
Note that the number of underscores avec [Queue] after the [RegisterOpen]
needs to match the number of arguments of the representation predicate
[Queue], excluding the pointer. (Here, we have one underscore for [L].) *)
(** Customization of [xopen] and [xclose] tactics for [Queue]. *)
Hint Extern 1 (RegisterOpen (Queue _)) =>
Provide Queue_open.
......@@ -78,7 +73,9 @@ Lemma create_spec : forall A,
PRE \[]
POST (fun q => q ~> Queue (@nil A)).
Proof using.
xcf. xapp. intros q. xclose q. { rew_list*. } { xsimpl*. }
xcf. xapp. intros q. xclose q.
{ rew_list. auto. }
{ xsimpl. }
Qed.
Hint Extern 1 (RegisterSpec create) => Provide create_spec.
......
......@@ -8,11 +8,14 @@ Require Export CFMLAdditions.
Section UF.
(** [K] denotes the types of nodes. *)
Context (K : Type) `{IK:Inhab K}.
Implicit Type P : map K K.
Implicit Type R : K->K.
Implicit Type x y z r s : K.
(*******************************************************************)
(** Union-Find Invariants *)
......@@ -255,15 +258,15 @@ Qed.
(** Validity of nodes is preserved during an update operation *)
Lemma udpate_inv : forall L' P a b,
L' = P[a:=b] ->
Lemma udpate_inv : forall P' P a b,
P' = P[a:=b] ->
index P a ->
(forall i, index P i -> index L' i)
/\ (forall i, index L' i -> index P i)
/\ (forall i, index P i -> i <> a -> L'[i] = P[i])
/\ (index P a -> L'[a] = b).
(forall i, index P i -> index P' i)
/\ (forall i, index P' i -> index P i)
/\ (forall i, index P i -> i <> a -> P'[i] = P[i])
/\ (index P a -> P'[a] = b).
Proof using.
introv E Da. subst L'. splits.
introv E Da. subst P'. splits.
{ intros. rewrite index_eq_indom in *. rew_map~. }
{ introv H. applys* index_update_inv Da. }
{ introv H N. rewrite* LibMap.read_update_neq. }
......@@ -273,13 +276,13 @@ Qed.
(** Lemma for link operations: case of nodes that do not
belong to the two components involved. *)
Lemma repr_update_neq : forall P a b L' x z,
Lemma repr_update_neq : forall P a b P' x z,
repr P x z ->
index P a -> (* technically not needed *)
L' = P[a:=b] ->
P' = P[a:=b] ->
P[a] = a ->
z <> a ->
repr L' x z.
repr P' x z.
Proof using.
introv M Ia E R N. forwards* (I1&_&K1&_): udpate_inv (rm E).
induction M.
......@@ -290,13 +293,13 @@ Qed.
(** Lemma for link operations: case of nodes that do
belong to the component resulting of the link. *)
Lemma repr_update_eq : forall P a b L' x,
Lemma repr_update_eq : forall P a b P' x,
repr P x a ->
L' = P[a:=b] ->
P' = P[a:=b] ->
index P b ->
P[b] = b ->
a <> b ->
repr L' x b.
repr P' x b.
Proof using.
introv M E Ib Rb N. forwards* (I1&_&K1&K2): udpate_inv (rm E).
lets Ra: repr_inv_L M.
......@@ -308,14 +311,14 @@ Qed.
(** A link operation preserves the invariants. *)
Lemma roots_link : forall P L' R R' x y,
Lemma roots_link : forall P P' R R' x y,
R' = link R x y (R y) ->
roots P R ->
L' = P [R x := R y] ->
P' = P [R x := R y] ->
R x <> R y ->
index P x ->
index P y ->
roots L' R'.
roots P' R'.
Proof using. (* Note: this proof uses the hint [repr_inv_L] *)
introv M HR E N Dx Dy. intros u Du.
forwards* Hx: roots_inv_L_root x HR.
......@@ -331,11 +334,11 @@ Qed.
(** A path compression preserves the invariants. *)
Lemma roots_compress : forall P R a L',
Lemma roots_compress : forall P R a P',
roots P R ->
L' = P [a := R a] ->
P' = P [a := R a] ->
index P a ->
roots L' R.
roots P' R.
Proof using.
introv HR E Da. intros x Dx.
forwards* Ha: HR a. lets Ra: repr_inv_L Ha.
......
(* Union-find: array-based implementation,
simplified by omiting the union-by-rank mechanism *)
without the union-by-rank mechanism *)
type node = int
......
......@@ -12,7 +12,7 @@ Implicit Types t : loc.
(*******************************************************************)
(** Representation predicate *)
(** [UF n R t] is a heap predicate that describes an array [t]
(** [t ~> UF n R] 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 indexed in the range [0...(n-1)]. *)
......@@ -32,7 +32,7 @@ Lemma create_spec : forall n,
n >= 0 ->
app create [n]
PRE \[]
POST (fun t => Hexists t R, UF n R t \*
POST (fun t => Hexists t R, t ~> UF n R \*
\[forall x, index n x -> R x = x]).
Proof using.
introv Hn. xcf. xfun. xapp (fun (i:int) => i).
......@@ -51,8 +51,18 @@ Hint Extern 1 (RegisterSpec create) => Provide create_spec.
Lemma find_spec : forall n R t x,
index n x ->
app find [t x]
PRE (UF n R t)
POST (fun r => \[r = R x] \* UF n R t).
PRE (t ~> UF n R)
POST (fun r => \[r = R x] \* t ~> UF n R).
(* Syntactic sugar to avoid repeating the precondition
in the postcondition:
[[
app find [t x]
INV (t ~> UF n R)
POST (fun r => \[r = R x]).
]]
*)
Proof using.
introv Ix. xunfold UF. xpull. intros P (Hn&HR).
forwards* Hx: HR x.
......@@ -80,7 +90,7 @@ Lemma same_spec : forall n R t x y,
index n x ->
index n y ->
app same [t x y]
INV (UF n R t)
INV (t ~> UF n R)
POST (fun b => \[b = isTrue (R x = R y)]).
Proof using.
introv Ix Iy. xcf. xapps*. xapps*. xrets.
......@@ -96,16 +106,16 @@ Lemma union_spec : forall n R t x y,
index n x ->
index n y ->
app union [t x y]
(UF n R t)
(fun z => Hexists (R':int->int), UF n R' t \* \[R' = link R x y z]).
PRE (t ~> UF n R)
POST (fun z => Hexists R', t ~> UF n R' \* \[R' = link R x y z]).
Proof using.
introv Ix Iy. xcf. xapps*. xapps*. xrets. xif.
{ unfold UF. xpull. intros P (Hn&HR).
{ xunfold UF. xpull. intros P (Hn&HR).
forwards* IRx: index_R x HR.
xapp*. xrets*. splits.
{ applys* conseq_dom_update.
rewrites* (>> conseq_dom_index_eq Hn) in *. }
{ applys* roots_link P R x y. } }
{ applys* roots_link. } }
{ xrets. rewrite* link_related. }
Qed.
......
(* Union-find: pointer-based implementation,
simplified by omiting the union-by-rank mechanism *)
without the union-by-rank mechanism *)
type contents = Root | Link of contents ref
......
(* Union-find: pointer-based implementation
including union-by-rank *)
including the union-by-rank mechanism *)
type contents = Root of int | Link of contents ref
......
......@@ -20,7 +20,7 @@ Proof using. apply (Inhab_of_val (Root 0)). Qed.
(** Representation predicate *)
(** [parent M x] maps a root to itself and a link to its destination. *)
(** [parent M x c] maps a root to itself and a link to its destination. *)
Definition parent (x:loc) (c:contents_) : loc :=
match c with
......@@ -44,7 +44,8 @@ Definition inv (D:set loc) (R:loc->loc) (M:map loc contents_) : Prop :=
(** [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]. *)
of the union-find data structure with respect to the root
function [R]. *)
Definition UF (D:set loc) (R:loc->loc) : hprop :=
Hexists (M:map loc contents_), Group Ref M \* \[inv D R M].
......@@ -96,8 +97,9 @@ Proof using.
{ rewrite* LibMaps.dom_map. } }
{ rewrite* @in_single_eq in H. subst y. rewrite LibMaps.map_update.
rewrite Rx. applys repr_root.
{ rewrite index_eq_indom. rewrite LibMap.dom_update, LibMaps.dom_map.
rewrite in_union_eq. right. rewrite* @in_single_eq. typeclass. }
{ rewrite index_eq_indom.
rewrite LibMap.dom_update, LibMaps.dom_map. rewrite in_union_eq.
right. rewrite* @in_single_eq. typeclass. }
{ rewrite* LibMap.read_update_same. }
{ typeclass. } }
Qed.
......@@ -218,7 +220,7 @@ Hint Extern 1 (RegisterSpec same) => Provide same_spec.
(** Invariants are preserved by a link operation. *)
Lemma link_correct : forall D R R' M M' x y,
Lemma inv_link : forall D R R' M M' x y,
R' = link R x y (R y) ->
M' = M[(R x) := Link (R y)] ->
inv D R M ->
......@@ -292,17 +294,17 @@ Proof using.
xpull. intros M HI. lets (HD&HR&HN&HL): HI.
xapps*. xapps*. xmatch.
{ xif.
{ xapps*. xrets*. applys* link_correct. }
{ xapps*. xrets*. applys* inv_link. }
{ xif.
{ xapp*. xrets*. rewrite link_sym.
applys* link_correct. }
applys* inv_link. }
{ xapp*. sets M': (M[R x:=Root (n + 1)%I]).
asserts ED: (dom M = dom M').
{ unfold M'. 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.
applys* inv_link.
subst M'. applys* inv_rerank. } } }
{ xfail. (* false C0 *)
forwards* (n&En): roots_inv_L_Root x D.
......
......@@ -19,7 +19,7 @@ Proof using. apply (Inhab_of_val Root). Qed.
(*******************************************************************)
(** Representation predicate *)
(** [parent M x] maps a root to itself and a link to its destination. *)
(** [parent M x c] maps a root to itself and a link to its destination. *)
Definition parent (x:loc) (c:contents_) : loc :=
match c with
......@@ -94,7 +94,7 @@ Proof using.
{ rewrite* @in_single_eq in H. subst y. rewrite LibMaps.map_update.
rewrite Rx. applys repr_root.
{ rewrite index_eq_indom. rewrite LibMap.dom_update, LibMaps.dom_map.
rewrite in_union_eq. right. rewrite* @in_single_eq. typeclass. } (* TODO: simpler *)
rewrite in_union_eq. right. rewrite* @in_single_eq. typeclass. }
{ rewrite* LibMap.read_update_same. }
{ typeclass. } }
Qed.
......@@ -214,7 +214,7 @@ Hint Extern 1 (RegisterSpec same) => Provide same_spec.
(** Invariants are preserved by a link operation. *)
Lemma link_correct : forall D R R' M M' x y,
Lemma inv_link : forall D R R' M M' x y,
R' = link R x y (R y) ->
M' = M[(R x) := Link (R y)] ->
inv D R M ->
......@@ -245,7 +245,7 @@ Lemma union_spec : forall D R x y,
Proof using.
introv Ix Iy. xcf. xapps*. xapps*. xapps. xif.
{ unfold UF. xpull. intros M HI. lets (HD&HR&HN&HL): HI.
xapp*. xrets*. applys* link_correct. }
xapp*. xrets*. applys* inv_link. }
{ 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