Commit 425cbaa7 authored by charguer's avatar charguer
Browse files

valid

parent 6d631152
(** Mutable queue, represented as a record with two lists,
and a size field. *)
(** Mutable queue, represented with two lists and a size field.
The items stored in the queue [q] are described by the
list [q.front ++ rev q.back]. *)
type 'a t = {
mutable front : 'a list;
......@@ -39,4 +41,4 @@ let is_empty q =
let transfer q1 q2 =
while not (is_empty q1) do
push (pop q1) q2
done
\ No newline at end of file
done
......@@ -65,12 +65,20 @@ Hint Extern 1 (RegisterClose (record_repr _)) =>
(*******************************************************************)
(** Create *)
(** Cusom notation for specifications:
[[
app f [x1 x2]
PRE H
POST (fun r => H')
]]
*)
Lemma create_spec : forall A,
app create [tt]
PRE \[]
POST (fun q => q ~> Queue (@nil A)).
Proof using.
xcf. xapp. intros r. xclose r. { auto. } { xsimpl. }
xcf. xapp. intros q. xclose q. { rew_list*. } { xsimpl*. }
Qed.
Hint Extern 1 (RegisterSpec create) => Provide create_spec.
......@@ -100,10 +108,10 @@ Lemma push_spec : forall A (L:list A) q x,
PRE (q ~> Queue L)
POST (fun (_:unit) => q ~> Queue (L ++ x::nil)).
Proof using.
xcf. xopen q. xpull. intros f b n (I1&I2).
xapps. xapp. xapps. xapp. xclose q.
{ subst. rew_list. math. }
{ xsimpl. subst. rew_list*. }
xcf. xopen q. xpull. intros f b n (IL&In).
xapps. xapp. xapps. xapp. intros _.
xclose q. { subst. rew_list. math. }
{ xsimpl. subst. rew_list. auto. }
Qed.
Hint Extern 1 (RegisterSpec push) => Provide push_spec.
......
......@@ -183,7 +183,6 @@ Proof using.
Qed.
(** As corrolary, the parent of [R x] is always [R x]. *)
(* TODO: use directly roots_inv_L *)
Lemma roots_inv_L_root : forall x P R,
roots P R ->
......
......@@ -51,8 +51,8 @@ Hint Extern 1 (RegisterSpec create) => Provide create_spec.
Lemma find_spec : forall n R t x,
index n x ->
app find [t x]
INV (UF n R t)
POST (fun r => \[r = R x]).
PRE (UF n R t)
POST (fun r => \[r = R x] \* UF n R t).
Proof using.
introv Ix. xunfold UF. xpull. intros P (Hn&HR).
forwards* Hx: HR x.
......
......@@ -8,7 +8,7 @@ Import RefGroupSpecs.
(** Types *)
Implicit Type D : set loc.
Implicit Type P : map loc contents_.
Implicit Type M : map loc contents_.
Implicit Type R : loc->loc.
Implicit Type x y z r s : loc.
......@@ -20,7 +20,7 @@ Proof using. apply (Inhab_of_val (Root 0)). Qed.
(** Representation predicate *)
(** [parent P x] maps a root to itself and a link to its destination. *)
(** [parent M x] maps a root to itself and a link to its destination. *)
Definition parent (x:loc) (c:contents_) : loc :=
match c with
......@@ -28,39 +28,39 @@ Definition parent (x:loc) (c:contents_) : loc :=
| Link y => y
end.
(** [no_self_link D P] asserts that the target of a [Link]
(** [no_self_link D M] asserts that the target of a [Link]
always differs from the node itself. *)
Definition no_self_link (D:set loc) (P:map loc contents_) : Prop :=
forall x y, x \in D -> P[x] = Link y -> x <> y.
Definition no_self_link (D:set loc) (M:map loc contents_) : Prop :=
forall x y, x \in D -> M[x] = Link y -> x <> y.
(** [inv D R P] captures the invariants of the structure *)
(** [inv D R M] captures the invariants of the structure *)
Definition inv (D:set loc) (R:loc->loc) (P:map loc contents_) : Prop :=
D = dom P
/\ roots (LibMaps.map_ parent P) R
Definition inv (D:set loc) (R:loc->loc) (M:map loc contents_) : Prop :=
D = dom M
/\ roots (LibMaps.map_ parent M) R
/\ (forall y, y \notin D -> R y = y)
/\ no_self_link D P.
/\ no_self_link D M.
(** [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 (P:map loc contents_), Group Ref P \* \[inv D R P].
Hexists (M:map loc contents_), Group Ref M \* \[inv D R M].
(*******************************************************************)
(** Hints *)
Lemma index_map_parent_eq : forall P x,
index (LibMaps.map_ parent P) x = x \indom P.
Lemma index_map_parent_eq : forall M x,
index (LibMaps.map_ parent M) x = x \indom M.
Proof using.
intros. rewrite index_eq_indom. rewrite* LibMaps.dom_map.
Qed.
Lemma indom_root : forall D R P x,
inv D R P ->
Lemma indom_root : forall D R M x,
inv D R M ->
x \in D ->
(R x) \in D.
Proof using.
......@@ -80,17 +80,17 @@ Hint Resolve indom_root.
(** [roots] is preserved by creation of a fresh root. *)
Lemma roots_create : forall P R x,
roots (LibMaps.map_ parent P) R ->
x \notindom P ->
Lemma roots_create : forall M R x,
roots (LibMaps.map_ parent M) R ->
x \notindom M ->
R x = x ->
roots (LibMaps.map_ parent P[x:=Root 0]) R.
roots (LibMaps.map_ parent M[x:=Root 0]) R.
Proof using.
introv HR Hx Rx. unfolds roots.
intros y Hy.
rewrite index_eq_indom in Hy. rewrite LibMaps.dom_map in Hy.
rewrite dom_update in Hy. rewrite in_union_eq in Hy. destruct Hy.
{ forwards* Ry: HR y. rewrite LibMaps.map_update.
{ forwards* Ry: HR y. rewrite LibMaps.map_update.
applys* repr_extends.
{ rewrite* LibMaps.dom_map. }
{ rewrite* LibMaps.dom_map. } }
......@@ -104,10 +104,10 @@ Qed.
(** [inv] is preserved by creation of a fresh root. *)
Lemma inv_create : forall P R D x,
inv D R P ->
Lemma inv_create : forall M R D x,
inv D R M ->
x \notin D ->
inv (D \u '{x}) R P[x:=Root 0].
inv (D \u '{x}) R M[x:=Root 0].
Proof using.
introv (HD&HR&HN&HL) Hx. splits.
{ rewrite* dom_update. }
......@@ -126,7 +126,7 @@ 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 P HI. lets (HD&HR&HN&HL): HI.
xcf. xunfold UF. xpull. intros M HI. lets (HD&HR&HN&HL): HI.
xapp. intros x. xsimpl*. applys* inv_create.
Qed.
......@@ -138,12 +138,12 @@ Hint Extern 1 (RegisterSpec create) => Provide create_spec.
(** [inv] is preserved by path compression *)
Lemma inv_compress : forall D R P P' x r,
inv D R P ->
Lemma inv_compress : forall D R M M' x r,
inv D R M ->
x \in D ->
x <> R x ->
P' = P[x := Link (R x)] ->
inv D R P'.
M' = M[x := Link (R x)] ->
inv D R M'.
Proof using.
introv (HD&HR&HN&HL) Hx Nx ->. splits.
{ rewrite* dom_update_at_index. rewrite* index_eq_indom. }
......@@ -163,32 +163,32 @@ Lemma find_spec : forall D R x,
INV (UF D R)
POST (fun r => \[r = R x]).
Proof using.
introv Ix. xunfold UF. xpull. intros P HI. lets (HD&HR&HN&HL): HI.
introv Ix. xunfold UF. xpull. intros M HI. lets (HD&HR&HN&HL): HI.
forwards* Hx: HR x.
forwards (d&Hx'): reprn_of_repr Hx. clear Hx.
gen P x. induction_wf IH: lt_wf d. hide IH. intros.
gen M x. induction_wf IH: lt_wf d. hide IH. intros.
xcf. xapps*. xmatch_no_intros.
{ intros n HLx. xrets*. forwards* Ex: roots_inv_R_root x R.
rewrite* LibMaps.read_map. rewrite* HLx. }
{ intros y Hy. sets P':(LibMaps.map_ parent P). inverts Hx' as.
{ intros y Hy. sets M':(LibMaps.map_ parent M). inverts Hx' as.
{ intros IRx E1 E2. forwards* HLx: roots_inv_L x HR.
{ subst P'. rewrite* index_map_parent_eq. }
subst P'. rewrite* LibMaps.read_map in E1. rewrite <- E2 in E1.
{ subst M'. rewrite* index_map_parent_eq. }
subst M'. rewrite* LibMaps.read_map 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: (P'[x]). asserts EQ: (z = y).
{ subst z P'. rewrite* LibMaps.read_map. rewrite* Hy. }
sets z: (M'[x]). asserts EQ: (z = y).
{ subst z M'. rewrite* LibMaps.read_map. rewrite* Hy. }
clearbody z. subst z.
forwards* ER: roots_inv_R y (R x) HR.
{ applys* repr_of_reprn. }
xapp_spec* (IH d); try solve [ subst P'; autos* ].
{ subst P'. lets: repr_of_reprn Hy'. subst D.
xapp_spec* (IH d); try solve [ subst M'; autos* ].
{ subst M'. lets: repr_of_reprn Hy'. subst D.
rewrite <- index_map_parent_eq. applys* repr_inv_index_l. }
asserts Ryx: (R y <> x).
{ intros E. forwards* HL'x: roots_inv_L x HR. subst P'.
rewrite* LibMaps.read_map in HL'x. rewrite Hy in HL'x.
{ intros E. forwards* HL'x: roots_inv_L x HR. subst M'.
rewrite* LibMaps.read_map in HL'x. rewrite Hy in HL'x.
simpls. false. }
clears P P'. clear P HN. intros Hr P HI. lets (HD&HR&HN&HL): HI.
clears M M'. clear M HN. intros Hr M HI. lets (HD&HR&HN&HL): HI.
xapp*. xrets*. applys* inv_compress. } }
Qed.
......@@ -218,65 +218,65 @@ Hint Extern 1 (RegisterSpec same) => Provide same_spec.
(** Invariants are preserved by a link operation. *)
Lemma link_correct : forall D R R' P P' x y,
Lemma link_correct : forall D R R' M M' x y,
R' = link R x y (R y) ->
P' = P[(R x) := Link (R y)] ->
inv D R P ->
M' = M[(R x) := Link (R y)] ->
inv D R M ->
x \in D ->
y \in D ->
R x <> R y ->
inv D R' P'.
inv D R' M'.
Proof using.
introv ER' EL' HI Hx Hy Hxy. lets (HD&HR&HN&HL): HI.
forwards* HRx: indom_root x HI. forwards* HRy: indom_root y HI.
splits.
{ subst D P'. rewrite* dom_update_at_index. }
{ subst P'. applys* roots_link R x y. rewrite* LibMaps.map_update. }
{ subst D M'. rewrite* dom_update_at_index. }
{ subst M'. applys* roots_link R x y. rewrite* LibMaps.map_update. }
{ intros z Hz. subst R'. unfold link. specializes HN Hz. case_if as Cz.
{ destruct Cz. { false; congruence. } { congruence. } } { auto. } }
{ subst P'. intros a b Ha Hb. rewrite read_update in Hb. case_if.
{ subst M'. intros a b Ha Hb. rewrite read_update in Hb. case_if.
{ 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 P R,
inv D R P ->
Lemma roots_inv_L_Root : forall x D M R,
inv D R M ->
x \in D ->
(R x) \in D ->
exists n, P[R x] = Root n.
exists n, M[R x] = Root n.
Proof using.
introv (HD&HR&HN&HL) Hx HRx. forwards* EQ: roots_inv_L_root x HR.
rewrite* LibMaps.read_map in EQ. cases (P[R x]) as ERx.
rewrite* LibMaps.read_map in EQ. cases (M[R x]) as ERx.
{ eauto. } { simpls. false* HL (R x). }
Qed.
(** [inv] is preserved by updating the rank information. *)
Lemma inv_rerank : forall x D P P' R n,
P' = P[R x := Root n] ->
inv D R P ->
Lemma inv_rerank : forall x D M M' R n,
M' = M[R x := Root n] ->
inv D R M ->
x \in D ->
inv D R P'.
inv D R M'.
Proof using.
introv Hd HI EL'. lets (HD&HR&HN&HL): HI.
asserts ED: (dom P = dom P').
{ subst P'. rewrite* dom_update_at_index.
asserts ED: (dom M = dom M').
{ subst M'. rewrite* dom_update_at_index.
rewrite* index_eq_indom. rewrite* <- HD. }
forwards* HRx: indom_root x HI. splits.
{ subst P'. rewrite* dom_update_at_index. rewrite* index_eq_indom. }
{ asserts_rewrite* (LibMaps.map_ parent P' = LibMaps.map_ parent P).
{ subst M'. rewrite* dom_update_at_index. rewrite* index_eq_indom. }
{ asserts_rewrite* (LibMaps.map_ parent M' = LibMaps.map_ parent M).
{ applys LibMaps.extens. { repeat rewrite LibMaps.dom_map. auto. }
{ intros a Ha. rewrite LibMaps.dom_map in Ha.
rewrite* LibMaps.read_map.
rewrite* LibMaps.read_map.
rewrite* LibMaps.read_map; [| rewrite* ED].
subst P'. rewrite read_update. case_if.
{ forwards* (m&Hm): roots_inv_L_Root x HI.
subst M'. rewrite read_update. case_if.
{ forwards* (m&Hm): roots_inv_L_Root x HI.
subst a. rewrite Hm. simple*. }
{ auto. } } } }
{ auto. }
{ subst P'. unfolds no_self_link. intros a b Ha HLa.
{ subst M'. unfolds no_self_link. intros a b Ha HLa.
rewrite read_update in HLa. case_if. applys* HL. }
Qed.
......@@ -288,22 +288,22 @@ 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 P HI. lets (HD&HR&HN&HL): HI.
{ unfold UF.
xpull. intros M HI. lets (HD&HR&HN&HL): HI.
xapps*. xapps*. xmatch.
{ xif.
{ xapps*. xrets*. applys* link_correct. }
{ xif.
{ xapp*. xrets*. rewrite link_sym.
{ xapp*. xrets*. rewrite link_sym.
applys* link_correct. }
{ xapp*. sets P': (P[R x:=Root (n + 1)%I]).
asserts ED: (dom P = dom P').
{ unfold P'. rewrite* dom_update_at_index.
{ 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.
xapp*. xrets*. rewrite link_sym.
applys* link_correct.
subst P'. applys* inv_rerank. } } }
subst M'. applys* inv_rerank. } } }
{ xfail. (* false C0 *)
forwards* (n&En): roots_inv_L_Root x D.
forwards* (m&Em): roots_inv_L_Root y D. } }
......
......@@ -8,7 +8,7 @@ Import RefGroupSpecs.
(** Types *)
Implicit Type D : set loc.
Implicit Type P : map loc contents_.
Implicit Type M : map loc contents_.
Implicit Type R : loc->loc.
Implicit Type x y z r s : loc.
......@@ -19,7 +19,7 @@ Proof using. apply (Inhab_of_val Root). Qed.
(*******************************************************************)
(** Representation predicate *)
(** [parent P x] maps a root to itself and a link to its destination. *)
(** [parent M x] maps a root to itself and a link to its destination. *)
Definition parent (x:loc) (c:contents_) : loc :=
match c with
......@@ -27,39 +27,39 @@ Definition parent (x:loc) (c:contents_) : loc :=
| Link y => y
end.
(** [no_self_link D P] asserts that the target of a [Link] always differs
(** [no_self_link D M] asserts that the target of a [Link] always differs
from the node itself. *)
Definition no_self_link (D:set loc) (P:map loc contents_) : Prop :=
forall x y, x \in D -> P[x] = Link y -> x <> y.
Definition no_self_link (D:set loc) (M:map loc contents_) : Prop :=
forall x y, x \in D -> M[x] = Link y -> x <> y.
(** [inv D R P] captures the invariants of the structure *)
(** [inv D R M] captures the invariants of the structure *)
Definition inv (D:set loc) (R:loc->loc) (P:map loc contents_) : Prop :=
D = dom P
/\ roots (LibMaps.map_ parent P) R
Definition inv (D:set loc) (R:loc->loc) (M:map loc contents_) : Prop :=
D = dom M
/\ roots (LibMaps.map_ parent M) R
/\ (forall y, y \notin D -> R y = y)
/\ no_self_link D P.
/\ no_self_link D M.
(** [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 (P:map loc contents_), Group Ref P \* \[inv D R P].
Hexists (M:map loc contents_), Group Ref M \* \[inv D R M].
(*******************************************************************)
(** Hints *)
Lemma index_map_parent_eq : forall P x,
index (LibMaps.map_ parent P) x = x \indom P.
Lemma index_map_parent_eq : forall M x,
index (LibMaps.map_ parent M) x = x \indom M.
Proof using.
intros. rewrite index_eq_indom. rewrite* LibMaps.dom_map.
Qed.
Lemma indom_root : forall D R P x,
inv D R P ->
Lemma indom_root : forall D R M x,
inv D R M ->
x \in D ->
(R x) \in D.
Proof using.
......@@ -78,11 +78,11 @@ Hint Resolve indom_root.
(** [roots] is preserved by creation of a fresh root. *)
Lemma roots_create : forall P R x,
roots (LibMaps.map_ parent P) R ->
x \notindom P ->
Lemma roots_create : forall M R x,
roots (LibMaps.map_ parent M) R ->
x \notindom M ->
R x = x ->
roots (LibMaps.map_ parent P[x:=Root]) R.
roots (LibMaps.map_ parent M[x:=Root]) R.
Proof using.
introv HR Hx Rx. unfolds roots.
intros y Hy.
......@@ -101,10 +101,10 @@ Qed.
(** [inv] is preserved by creation of a fresh root. *)
Lemma inv_create : forall P R D x,
inv D R P ->
Lemma inv_create : forall M R D x,
inv D R M ->
x \notin D ->
inv (D \u '{x}) R P[x:=Root].
inv (D \u '{x}) R M[x:=Root].
Proof using.
introv (HD&HR&HN&HL) Hx. splits.
{ rewrite* dom_update. }
......@@ -123,7 +123,7 @@ 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 P HI. lets (HD&HR&HN&HL): HI.
xcf. xunfold UF. xpull. intros M HI. lets (HD&HR&HN&HL): HI.
xapp. intros x. xsimpl*. applys* inv_create.
Qed.
......@@ -135,12 +135,12 @@ Hint Extern 1 (RegisterSpec create) => Provide create_spec.
(** [inv] is preserved by path compression *)
Lemma inv_compress : forall D R P P' x r,
inv D R P ->
Lemma inv_compress : forall D R M M' x r,
inv D R M ->
x \in D ->
x <> R x ->
P' = P[x := Link (R x)] ->
inv D R P'.
M' = M[x := Link (R x)] ->
inv D R M'.
Proof using.
introv (HD&HR&HN&HL) Hx Nx ->. splits.
{ rewrite* dom_update_at_index. rewrite* index_eq_indom. }
......@@ -160,31 +160,31 @@ Lemma find_spec : forall D R x,
INV (UF D R)
POST (fun r => \[r = R x]).
Proof using.
introv Ix. xunfold UF. xpull. intros P HI. lets (HD&HR&HN&HL): HI.
introv Ix. xunfold UF. xpull. intros M HI. lets (HD&HR&HN&HL): HI.
forwards* Hx: HR x.
forwards (d&Hx'): reprn_of_repr Hx. clear Hx.
gen P x. induction_wf IH: lt_wf d. hide IH. intros.
gen M x. induction_wf IH: lt_wf d. hide IH. intros.
xcf. xapps*. xmatch_no_intros.
{ intros HLx. xrets*. forwards* Ex: roots_inv_R_root x R.
rewrite* LibMaps.read_map. rewrite* HLx. }
{ intros y Hy. sets P':(LibMaps.map_ parent P). inverts Hx' as.
{ intros y Hy. sets M':(LibMaps.map_ parent M). inverts Hx' as.
{ intros IRx E1 E2. forwards* HLx: roots_inv_L x HR.
{ subst P'. rewrite* index_map_parent_eq. }
subst P'. rewrite* LibMaps.read_map in E1. rewrite <- E2 in E1.
{ subst M'. rewrite* index_map_parent_eq. }
subst M'. rewrite* LibMaps.read_map 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: (P'[x]). asserts EQ: (z = y).
{ subst z P'. rewrite* LibMaps.read_map. rewrite* Hy. }
sets z: (M'[x]). asserts EQ: (z = y).
{ subst z M'. rewrite* LibMaps.read_map. rewrite* Hy. }
clearbody z. subst z.
forwards* ER: roots_inv_R y (R x) HR.
{ applys* repr_of_reprn. }
xapp_spec (IH d); try solve [ subst P'; autos* ].
{ subst P'. lets: repr_of_reprn Hy'. subst D. rewrite <- index_map_parent_eq.
xapp_spec (IH d); try solve [ subst M'; autos* ].
{ subst M'. lets: repr_of_reprn Hy'. subst D. rewrite <- index_map_parent_eq.
applys* repr_inv_index_l. }
asserts Ryx: (R y <> x).
{ intros E. forwards* HL'x: roots_inv_L x HR. subst P'.
{ intros E. forwards* HL'x: roots_inv_L x HR. subst M'.
rewrite* LibMaps.read_map in HL'x. rewrite Hy in HL'x. simpls. false. }
clears P P'. clear P HN. intros Hr P HI. lets (HD&HR&HN&HL): HI.
clears M M'. clear M HN. intros Hr M HI. lets (HD&HR&HN&HL): HI.
xapp*. xrets*. applys* inv_compress. } }
Qed.
......@@ -214,23 +214,23 @@ Hint Extern 1 (RegisterSpec same) => Provide same_spec.
(** Invariants are preserved by a link operation. *)
Lemma link_correct : forall D R R' P P' x y,
Lemma link_correct : forall D R R' M M' x y,
R' = link R x y (R y) ->
P' = P[(R x) := Link (R y)] ->
inv D R P ->
M' = M[(R x) := Link (R y)] ->
inv D R M ->
x \in D ->
y \in D ->
R x <> R y ->
inv D R' P'.
inv D R' M'.
Proof using.
introv ER' EL' HI Hx Hy Hxy. lets (HD&HR&HN&HL): HI.
forwards* HRx: indom_root x HI. forwards* HRy: indom_root y HI.
splits.
{ subst D P'. rewrite* dom_update_at_index. }
{ subst P'. applys* roots_link R x y. rewrite* LibMaps.map_update. }
{ subst D M'. rewrite* dom_update_at_index. }
{ subst M'. applys* roots_link R x y. rewrite* LibMaps.map_update. }
{ intros z Hz. subst R'. unfold link. specializes HN Hz. case_if as Cz.
{ destruct Cz. { false; congruence. } { congruence. } } { auto. } }
{ subst P'. intros a b Ha Hb. rewrite read_update in Hb. case_if.
{ subst M'. intros a b Ha Hb. rewrite read_update in Hb. case_if.
{ inverts* Hb. } { applys* HL. } }
Qed.
......@@ -244,7 +244,7 @@ Lemma union_spec : forall D R x y,
(fun z => Hexists R', UF D R' \* \[R' = link R x y z]).