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

renaming

parent c27fc703
......@@ -156,10 +156,11 @@ End MArray.
(* TODO: id outside domain *)
Module LibMaps.
Section Map.
Transparent map.
Definition LibMap_map A `{Inhab B1} `{Inhab B2} (f:A->B1->B2) (M:map A B1) : map A B2 :=
Definition 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)
......@@ -167,10 +168,10 @@ Definition LibMap_map A `{Inhab B1} `{Inhab B2} (f:A->B1->B2) (M:map A B1) : map
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].
Lemma map_update : forall A `{Inhab B1} `{Inhab B2} (f:A->B1->B2) (M:map A B1) x y,
map_ f (M[x:=y]) = (map_ f M)[x:=f x y].
Proof using.
intros. extens. intros a. unfold LibMap_map. simpl. unfold bag_update_as_union_single.
intros. extens. intros a. unfold 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 *)
......@@ -178,31 +179,31 @@ 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.
Lemma dom_map : forall A `{Inhab B1} `{Inhab B2} (f:A->B1->B2) (M:map A B1),
dom (map_ f M) = dom M.
Proof using.
intros. unfold LibMap_map. simpl. unfold dom_impl.
intros. unfold 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,
Lemma read_map : 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]).
(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.
introv Hx. unfold 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.
Axiom LibMap_extens : forall A `{Inhab B} (M1 M2:map A B),
Axiom extens : forall A `{Inhab B} (M1 M2:map A B),
dom M1 = dom M2 ->
(forall (x:A), x \indom M1 -> M1[x] = M2[x]) ->
M1 = M2.
End Map.
End LibMaps.
......
(** Functional queue represented as a pair of lists:
- the front list stores elements in order of exit
- the back list stores elements in reverse order.
The structure maintains the front list nonempty
whenever possible. *)
type 'a queue = 'a list * 'a list
......
(** Mutable queue, represented as a record with two lists,
and a size field. *)
type 'a t = {
mutable front : 'a list;
......
......@@ -10,7 +10,7 @@ Require Export CFMLAdditions.
Section UF.
Context (K : Type) `{IK:Inhab K}.
Implicit Type L : map K K.
Implicit Type P : map K K.
Implicit Type R : K->K.
Implicit Type x y z r s : K.
......@@ -19,26 +19,26 @@ Implicit Type x y z r s : K.
(*******************************************************************)
(** Union-Find Invariants *)
(** [repr L x z] asserts that [z] is the root of [x], that is,
(** [repr P x z] asserts that [z] is the root of [x], that is,
the end of the linked path that starts from [x]. *)
Inductive repr (L:map K K) : K->K->Prop :=
Inductive repr (P:map K K) : K->K->Prop :=
| repr_root : forall x,
index L x ->
x = L[x] ->
repr L x x
index P x ->
x = P[x] ->
repr P x x
| repr_next : forall x y z,
index L x ->
y = L[x] ->
index P x ->
y = P[x] ->
x <> y ->
repr L y z ->
repr L x z.
repr P y z ->
repr P x z.
(** [roots L R] captures the fact that [R] is the function
that computes the roots described by the table [L]. *)
(** [roots P R] captures the fact that [R] is the function
that computes the roots described by the table [P]. *)
Definition roots (L:map K K) (R:K->K) :=
forall x, index L x -> repr L x (R x).
Definition roots (P:map K K) (R:K->K) :=
forall x, index P x -> repr P x (R x).
(*******************************************************************)
......@@ -51,40 +51,40 @@ Implicit Type d : nat.
(** Copy-paste of the definition of [repr], plus a bound on the depth. *)
Inductive reprn L : nat->K->K->Prop :=
Inductive reprn P : nat->K->K->Prop :=
| reprn_root : forall d x,
index L x ->
x = L[x] ->
reprn L d x x
index P x ->
x = P[x] ->
reprn P d x x
| reprn_next : forall d x y z,
index L x ->
y = L[x] ->
index P x ->
y = P[x] ->
x <> y ->
reprn L d y z ->
reprn L (S d) x z.
reprn P d y z ->
reprn P (S d) x z.
Hint Constructors repr reprn.
Hint Extern 1 (_ < _) => math.
Lemma reprn_lt : forall d d' L x z,
reprn L d x z ->
Lemma reprn_lt : forall d d' P x z,
reprn P d x z ->
d < d' ->
reprn L d' x z.
reprn P d' x z.
Proof.
introv H. gen d'. induction H; introv N;
(destruct d' as [|d']; [ false; math | autos* ]).
Qed.
Lemma reprn_of_repr : forall L x z,
repr L x z ->
exists d, reprn L d x z.
Lemma reprn_of_repr : forall P x z,
repr P x z ->
exists d, reprn P d x z.
Proof.
hint reprn_lt. introv H. induction H; try induct_height.
Qed.
Lemma repr_of_reprn : forall L d x z,
reprn L d x z ->
repr L x z.
Lemma repr_of_reprn : forall P d x z,
reprn P d x z ->
repr P x z.
Proof. introv H. induction* H. Qed.
End Reprn.
......@@ -96,9 +96,9 @@ End Reprn.
(** [repr] is injective. *)
Lemma repr_inj : forall z1 z2 L x,
repr L x z1 ->
repr L x z2 ->
Lemma repr_inj : forall z1 z2 P x,
repr P x z1 ->
repr P x z2 ->
z1 = z2.
Proof using.
introv H1 H2. gen z2.
......@@ -111,9 +111,9 @@ Arguments repr_inj : clear implicits.
(** [repr] defines a function. *)
Lemma repr_functional : forall L x z1 z2,
repr L x z1 ->
repr L x z2 ->
Lemma repr_functional : forall P x z1 z2,
repr P x z1 ->
repr P x z2 ->
z1 = z2.
Proof using.
introv H1 H2. induction H1; inverts H2; try subst; auto_false.
......@@ -121,21 +121,21 @@ Qed.
(** [repr] only holds of valid nodes. *)
Lemma repr_inv_index_l : forall L x z,
repr L x z ->
index L x.
Lemma repr_inv_index_l : forall P x z,
repr P x z ->
index P x.
Proof using. introv H. inverts* H. Qed.
Lemma repr_inv_index_r : forall L x z,
repr L x z ->
index L z.
Lemma repr_inv_index_r : forall P x z,
repr P x z ->
index P z.
Proof using. introv H. induction* H. Qed.
(** [repr] relates nodes to nodes that are roots. *)
Lemma repr_inv_L : forall L x z,
repr L x z ->
L[z] = z.
Lemma repr_inv_L : forall P x z,
repr P x z ->
P[z] = z.
Proof using. introv H. induction* H. Qed.
Hint Resolve repr_inv_index_l repr_inv_index_r.
......@@ -146,10 +146,10 @@ Hint Resolve repr_inv_index_l repr_inv_index_r.
(** Parents of valid nodes are valid nodes. *)
Lemma index_L : forall L R x,
roots L R ->
index L x ->
index L (L[x]).
Lemma index_L : forall P R x,
roots P R ->
index P x ->
index P (P[x]).
Proof using.
introv HR HI. forwards M: HR HI. inverts M as.
{ introv H1 H2 H3. rewrite* <- H2. }
......@@ -160,19 +160,19 @@ Hint Resolve index_L.
(** Roots of valid nodes are valid nodes. *)
Lemma index_R : forall L R x,
roots L R ->
index L x ->
index L (R x).
Lemma index_R : forall P R x,
roots P R ->
index P x ->
index P (R x).
Proof using. introv HR Hx. forwards*: HR Hx. Qed.
(** If [R x = x] then [x] is its own parent. *)
Lemma roots_inv_L : forall x L R,
roots L R ->
Lemma roots_inv_L : forall x P R,
roots P R ->
R x = x ->
index L x ->
L[x] = x.
index P x ->
P[x] = x.
Proof using.
introv HR E Ix. forwards* Hx: HR x.
lets Ex: repr_inv_L Hx. congruence.
......@@ -181,31 +181,31 @@ 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 L R,
roots L R ->
index L x ->
L[R x] = R x.
Lemma roots_inv_L_root : forall x P R,
roots P R ->
index P x ->
P[R x] = R x.
Proof using.
introv HR Ix. forwards* Hx: HR x. applys* repr_inv_L.
Qed.
(** If [repr L x z] then [R x] is [z]. *)
(** If [repr P x z] then [R x] is [z]. *)
Lemma roots_inv_R : forall x z L R,
roots L R ->
repr L x z ->
Lemma roots_inv_R : forall x z P R,
roots P R ->
repr P x z ->
R x = z.
Proof using.
introv HR Hx. forwards* Hx': HR x.
forwards~: repr_functional Hx Hx'.
Qed.
(** If [L x = x], then [x] is a root. *)
(** If [P x = x], then [x] is a root. *)
Lemma roots_inv_R_root : forall x L R,
roots L R ->
L[x] = x ->
index L x ->
Lemma roots_inv_R_root : forall x P R,
roots P R ->
P[x] = x ->
index P x ->
R x = x.
Proof using.
introv HR Lx Ix. forwards* Hx': HR x.
......@@ -218,9 +218,9 @@ Qed.
(** Invariants hold for [create] operation. *)
Lemma roots_init : forall L,
(forall x, index L x -> L[x] = x) ->
roots L (fun x => x).
Lemma roots_init : forall P,
(forall x, index P x -> P[x] = x) ->
roots P (fun x => x).
Proof using.
introv HL. intros x Hx. applys* repr_root. rewrite* HL.
Qed.
......@@ -252,13 +252,13 @@ Qed.
(** Validity of nodes is preserved during an update operation *)
Lemma udpate_inv : forall L' L a b,
L' = L[a:=b] ->
index L a ->
(forall i, index L i -> index L' i)
/\ (forall i, index L' i -> index L i)
/\ (forall i, index L i -> i <> a -> L'[i] = L[i])
/\ (index L a -> L'[a] = b).
Lemma udpate_inv : forall L' P a b,
L' = 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).
Proof using.
introv E Da. subst L'. splits.
{ intros. rewrite index_eq_indom in *. rew_map~. }
......@@ -270,12 +270,12 @@ Qed.
(** Lemma for link operations: case of nodes that do not
belong to the two components involved. *)
(* TODO: index L a is in fact not needed *)
Lemma repr_update_neq : forall L a b L' x z,
repr L x z ->
index L a ->
L' = L[a:=b] ->
L[a] = a ->
(* TODO: index P a is in fact not needed *)
Lemma repr_update_neq : forall P a b L' x z,
repr P x z ->
index P a ->
L' = P[a:=b] ->
P[a] = a ->
z <> a ->
repr L' x z.
Proof using.
......@@ -288,11 +288,11 @@ Qed.
(** Lemma for link operations: case of nodes that do
belong to the component resulting of the link. *)
Lemma repr_update_eq : forall L a b L' x,
repr L x a ->
L' = L[a:=b] ->
index L b ->
L[b] = b ->
Lemma repr_update_eq : forall P a b L' x,
repr P x a ->
L' = P[a:=b] ->
index P b ->
P[b] = b ->
a <> b ->
repr L' x b.
Proof using.
......@@ -306,13 +306,13 @@ Qed.
(** A link operation preserves the invariants. *)
Lemma roots_link : forall L L' R R' x y,
Lemma roots_link : forall P L' R R' x y,
R' = link R x y (R y) ->
roots L R ->
L' = L [R x := R y] ->
roots P R ->
L' = P [R x := R y] ->
R x <> R y ->
index L x ->
index L y ->
index P x ->
index P y ->
roots L' R'.
Proof using. (* Note: this proof uses the hint [repr_inv_L] *)
introv M HR E N Dx Dy. intros u Du.
......@@ -328,10 +328,10 @@ Qed.
(** A path compression preserves the invariants. *)
Lemma roots_compress : forall L R a L',
roots L R ->
L' = L [a := R a] ->
index L a ->
Lemma roots_compress : forall P R a L',
roots P R ->
L' = P [a := R a] ->
index P a ->
roots L' R.
Proof using.
introv HR E Da. intros x Dx.
......@@ -355,20 +355,20 @@ Qed.
(*******************************************************************)
(** Lemmas only for UFPointer, for which the domain grows dynamically *)
Lemma index_extends : forall L x a b,
index L x ->
a \notindom L ->
index L[a:=b] x.
Lemma index_extends : forall P x a b,
index P x ->
a \notindom P ->
index P[a:=b] x.
Proof using IK.
introv Hx Ha. rewrite index_eq_indom in *.
rewrite LibMap.dom_update. rewrite* @in_union_eq. typeclass.
Qed.
Lemma repr_extends : forall L a b x r,
a \notindom L ->
x \indom L ->
repr L x r ->
repr (L[a:=b]) x r.
Lemma repr_extends : forall P a b x r,
a \notindom P ->
x \indom P ->
repr P x r ->
repr (P[a:=b]) x r.
Proof using.
introv Ha Hx HR. gen Hx. induction HR; intros.
{ applys* repr_root. { applys* index_extends. }
......
......@@ -2,7 +2,7 @@ Set Implicit Arguments.
Require Import UF.
Require Import UFArray_ml.
Implicit Type L : map int int.
Implicit Type P : map int int.
Implicit Type R : int->int.
Implicit Type x y z r s : int.
Implicit Types t : loc.
......@@ -17,7 +17,8 @@ Implicit Types t : loc.
indexed in the range [0...(n-1)]. *)
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].
Hexists (P:map int int), t ~> MArray P
\* \[conseq_dom n P /\ roots P R].
(*******************************************************************)
......@@ -33,7 +34,7 @@ Proof using.
introv Hn. xcf. xfun. xapp (fun (i:int) => i).
{ math. }
{ intros i Hi. xapp. xrets*. }
{ intros t. xpull. intros L HL HR. xunfold UF. xsimpl t (fun x => x) L.
{ intros t. xpull. intros P HL HR. xunfold UF. xsimpl t (fun x => x) P.
{ auto. } { split*. applys* roots_init. } }
Qed.
......@@ -49,17 +50,17 @@ Lemma find_spec : forall n R t x,
INV (UF n R t)
POST (fun r => \[r = R x]).
Proof using.
introv Ix. xunfold UF. xpull. intros L (Hn&HR).
introv Ix. xunfold UF. xpull. intros P (Hn&HR).
forwards* Hx: HR x.
forwards (d&Hx'): reprn_of_repr Hx.
gen L x. induction_wf IH: lt_wf d. hide IH. intros.
gen P x. induction_wf IH: lt_wf d. hide IH. intros.
xcf. xapps*. xrets. xif.
{ xrets*. forwards* Ex: roots_inv_R_root x L R. }
{ xrets*. forwards* Ex: roots_inv_R_root x P R. }
{ inverts Hx' as. { intros. false. } intros Ix' N Hy. rename d0 into d.
sets y: (L[x]). lets Ry: repr_of_reprn Hy.
sets y: (P[x]). lets Ry: repr_of_reprn Hy.
forwards* ER: roots_inv_R y (R x) HR. xapp_spec* (IH d).
{ subst. rewrites (>> conseq_dom_index_eq Hn). applys* index_L. }
clearbody y. clears L. intros Hr L (Hn&HR).
clearbody y. clears P. intros Hr P (Hn&HR).
xapp*. xrets*. splits*.
{ applys* conseq_dom_update. }
{ rewrite Hr,ER. applys* roots_compress. } }
......@@ -95,12 +96,12 @@ Lemma union_spec : forall n R t x y,
(fun z => Hexists (R':int->int), UF n R' t \* \[R' = link R x y z]).
Proof using.
introv Ix Iy. xcf. xapps*. xapps*. xrets. xif.
{ unfold UF. xpull. intros L (Hn&HR).
{ unfold 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 L R x y. } }
{ applys* roots_link P R x y. } }
{ xrets. rewrite* link_related. }
Qed.
......
......@@ -8,7 +8,7 @@ Import RefGroupSpecs.
(** Types *)
Implicit Type D : set loc.
Implicit Type L : map loc contents_.
Implicit Type P : 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 L x] maps a root to itself and a link to its destination. *)
(** [parent P 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 L] asserts that the target of a [Link] always differs
(** [no_self_link D P] 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.
Definition no_self_link (D:set loc) (P:map loc contents_) : Prop :=
forall x y, x \in D -> P[x] = Link y -> x <> y.
(** [inv D R L] captures the invariants of the structure *)
(** [inv D R P] 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
Definition inv (D:set loc) (R:loc->loc) (P:map loc contents_) : Prop :=
D = dom P
/\ roots (LibMaps.map_ parent P) R
/\ (forall y, y \notin D -> R y = y)
/\ no_self_link D L.
/\ no_self_link D P.
(** [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 \* \[inv D R L].
Hexists (P:map loc contents_), Group Ref P \* \[inv D R P].
(*******************************************************************)
(** Hints *)
Lemma index_map_parent_eq : forall L x,
index (LibMap_map parent L) x = x \indom L.
Lemma index_map_parent_eq : forall P x,
index (LibMaps.map_ parent P) x = x \indom P.
Proof using.
intros. rewrite index_eq_indom. rewrite* LibMap_dom_map.
intros. rewrite index_eq_indom. rewrite* LibMaps.dom_map.
Qed.