Commit ee4bdb24 authored by charguer's avatar charguer
Browse files

rank cleanup

parent d417b9c8
......@@ -202,3 +202,11 @@ Proof using.
Qed.
End Map.
(* TODO rename
ref_spec_group
infix_emark_spec_group
infix_colon_eq_spec_group
*)
......@@ -41,8 +41,6 @@ Definition roots (L:map K K) (R:K->K) :=
forall x, index L x -> repr L x (R x).
(*******************************************************************)
(** Induction principle on the height of a [repr] derivation *)
......@@ -227,32 +225,31 @@ Proof using.
introv HL. intros x Hx. applys* repr_root. rewrite* HL.
Qed.
(** Update to [R] when the root of [x] is set to point to the root of [y]. *)
(** Update to [R] when the components of [x] and [y] are unified and
[z] denotes the new root---[z] being either [x] or [y]. *)
Definition link (R:K->K) (x y z:K) : K->K :=
fun i => If (R i = R x \/ R i = R y) then z else R i.
Definition link R x y :=
fun i => If (R i = R x \/ R i = R y) then R y else R i.
(** Linking is symmetric in [x] and [y]. *)
Lemma link_sym : forall R x y z,
link R x y z = link R y x z.
Proof using.
intros. extens. intros i. unfolds link. repeat case_if*.
Qed.
(** Linking of nodes in the same component is idempotent. *)
Lemma link_related : forall R x y,
R x = R y ->
link R x y = R.
link R x y (R y) = R.
Proof using IK.
introv E. applys fun_ext_1 ;=> i. unfold link. case_if as C.
{ destruct~ C. }
{ auto. }
Qed.
(* TODO: not used? *)
Lemma link_inv_related : forall R x y,
R x = R y ->
link R x y = R.
Proof using IK.
introv E. extens ;=> i. unfold link. case_if as C.
{ rewrite E in C. destruct~ C. }
{ auto. }
Qed.
(** Validity of nodes is preserved during an update operation *)
Lemma udpate_inv : forall L' L a b,
......@@ -309,15 +306,15 @@ Qed.
(** A link operation preserves the invariants. *)
Lemma roots_link : forall L R x y L' R',
R' = link R x y ->
Lemma roots_link : forall L L' R R' x y,
R' = link R x y (R y) ->
roots L R ->
L' = L [R x := R y] ->
R x <> R y ->
index L x ->
index L y ->
roots L' R'.
Proof using. (* Note: this proof uses hint [repr_inv_L] *)
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.
forwards~ Hy: roots_inv_L_root y HR.
......@@ -326,7 +323,7 @@ Proof using. (* Note: this proof uses hint [repr_inv_L] *)
{ destruct C as [C|C].
{ rewrite <- C in E. applys~ repr_update_eq E. }
{ rewrite <- C. applys~ repr_update_neq E. } }
{ rew_logic in C. destruct C as [C1 C2]. applys~ repr_update_neq E. }
{ rew_logic in C. destruct C as [C1 C2]. applys* repr_update_neq E. }
Qed.
(** A path compression preserves the invariants. *)
......@@ -354,4 +351,32 @@ Proof using.
applys~ repr_next y. { rewrite~ K1. } } }
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.
Proof using IK.
introv Hx Ha. rewrite index_eq_indom in *.
rewrite LibMap.dom_update. rewrite~ @in_union_eq. typeclass.
Qed.
Hint Resolve index_extends.
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.
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.
End UF.
......@@ -22,4 +22,7 @@ let same t x y =
let union t x y =
let r = find t x in
let s = find t y in
if r <> s then t.(r) <- s
if r <> s
then (t.(r) <- s; s)
else s
......@@ -8,7 +8,7 @@ val create : int -> t
val find : t -> node -> node
val union : t -> node -> node -> unit
val union : t -> node -> node -> node
val same : t -> node -> node -> bool
......
......@@ -95,12 +95,12 @@ Lemma union_spec : forall n R t x y,
index n y ->
app union [t x y]
(UF n R t)
(fun (_:unit) => Hexists (R':int->int), UF n R' t \* \[R' = link R 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).
forwards* IRx: index_R x HR.
xapp*. xsimpl*. splits.
xapp*. xrets*. splits.
{ applys* conseq_dom_update.
rewrites* (>> conseq_dom_index_eq Hn) in *. }
{ applys* roots_link L R x y. } }
......
......@@ -27,6 +27,8 @@ let same x y =
let union x y =
let r = find x in
let s = find y in
if r != s then r := Link s
if r != s
then (r := Link s; s)
else s
......@@ -5,7 +5,7 @@ val create : unit -> node
val find : node -> node
val union : node -> node -> unit
val union : node -> node -> node
val same : node -> node -> bool
Set Implicit Arguments.
Require Import CFML.CFLib.
Require Import Stdlib.
Require Import Array_proof.
Require Import UF.
Require Import UFPointerRank_ml.
Require Import TLC.LibListZ.
Require Import UFArray_proof.
(* TODO rename
ref_spec_group
infix_emark_spec_group
infix_colon_eq_spec_group
*)
Section Map.
Transparent map.
Generalizable Variables A B.
Definition LibMap_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)
end.
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].
Proof using.
intros. extens. intros a. unfold LibMap_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 *)
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.
Proof using.
intros. unfold LibMap_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,
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.
(*******************************************************************)
(** Types *)
Implicit Type D : set loc.
Implicit Type L : map loc contents_.
Implicit Type R : loc->loc.
Implicit Type x y z r s : loc.
Global Instance Inhab_contents_ : Inhab contents_.
Proof using. apply (Inhab_of_val (Root 0)). Qed.
(*******************************************************************)
(** Representation predicate *)
Global Instance Inhab_contents_ : Inhab contents_.
Proof using. apply (Inhab_of_val (Root 0)). Qed.
(** [parent L x] maps a root to itself and a link to its destination. *)
......@@ -106,43 +55,8 @@ Proof using.
Qed.
Hint Extern 1 (index (LibMap_map parent ?L) ?x) => rewrite index_map_parent_eq.
Hint Extern 1 (?x \indom ?L) => congruence.
Hint Extern 1 (?x \in dom ?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 *)
......@@ -163,8 +77,9 @@ Proof using.
{ 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. } }
rewrite in_union_eq. right. rewrite~ @in_single_eq. typeclass. } (* TODO: simpler *)
{ rewrite* LibMap.read_update_same. }
{ typeclass. } }
Qed.
Lemma create_spec : forall D R,
......@@ -255,8 +170,6 @@ Hint Extern 1 (RegisterSpec same) => Provide same_spec.
(*******************************************************************)
(** Union *)
(* TODO: inv_record *)
Lemma link_correct : forall D R L x y,
D = dom L ->
roots (LibMap_map parent L) R ->
......@@ -268,8 +181,8 @@ Lemma link_correct : forall D R L x y,
(R y) \in D ->
R x <> R y ->
D = dom L[R x:=Link (R y)]
/\ roots (LibMap_map parent L[R x:=Link (R y)]) (link R x y)
/\ (forall y0 : loc, y0 \notin D -> link R x y y0 = y0)
/\ roots (LibMap_map parent L[R x:=Link (R y)]) (link R x y (R y))
/\ (forall y0 : loc, y0 \notin D -> link R x y (R y) y0 = y0)
/\ no_self_link D L[R x:=Link (R y)].
Proof using.
introv HD HR HN HL Hx Hy HRx HRy Hxy. splits.
......@@ -294,56 +207,12 @@ Proof using.
{ eauto. } { simpls. false~ HN (R x). }
Qed.
Section Linkto.
Hint Resolve index_R.
Definition linkto R x y z :=
fun i => If (R i = R x \/ R i = R y) then z else R i.
Lemma linkto_sym : forall R x y z,
linkto R x y z = linkto R y x z.
Proof using.
intros. extens. intros i. unfolds linkto. repeat case_if*.
Qed.
Lemma roots_linkto : forall (L L':map loc loc) R x y R',
R' = linkto R x y (R y) ->
roots L R ->
L' = L [R x := R y] ->
R x <> R y ->
index L x ->
index L y ->
roots L' R'.
Proof using. (* Note: this proof uses hint [repr_inv_L] *)
introv M HR E N Dx Dy. intros u Du.
forwards~ Hx: roots_inv_L_root x HR.
forwards~ Hy: roots_inv_L_root y HR.
forwards~ (I1&I2&_&_): udpate_inv E.
rewrites (rm M). unfold linkto. case_if as C.
{ destruct C as [C|C].
{ rewrite <- C in E. applys~ repr_update_eq E. }
{ rewrite <- C. applys~ repr_update_neq E. } }
{ rew_logic in C. destruct C as [C1 C2]. applys* repr_update_neq E. }
Qed.
Lemma linkto_related : forall R x y,
R x = R y ->
linkto R x y (R x) = R.
Proof using.
introv E. applys fun_ext_1 ;=> i. unfold linkto. case_if as C.
{ destruct~ C. }
{ auto. }
Qed.
End Linkto.
Lemma union_spec : forall D R x y,
x \in D ->
y \in D ->
app union [x y]
(UF D R)
(fun z => Hexists R', UF D R' \* \[R' = linkto R x y z]).
(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).
......@@ -359,7 +228,7 @@ Proof using.
xrets*. applys* link_correct. }
{ xif.
{ xapp_spec* infix_colon_eq_spec_group.
xrets*. rewrite linkto_sym. applys* link_correct. }
xrets*. rewrite link_sym. applys* link_correct. }
{ xapp_spec* infix_colon_eq_spec_group.
sets L': (L[R x:=Root (n + 1)%I]).
asserts ED: (dom L = dom L').
......@@ -367,7 +236,7 @@ Proof using.
asserts EP: (LibMap_map parent L' = LibMap_map parent L).
{ unfold L'. skip. (* TODO by extensionality ... *) }
xapp_spec* infix_colon_eq_spec_group.
xret. xsimpl*. rewrite linkto_sym. applys~ link_correct.
xret. xsimpl*. rewrite link_sym. applys~ link_correct.
{ unfolds roots. rewrite~ EP. }
{ unfolds no_self_link. intros a b Ha HLa. unfold L' in HLa.
rewrite read_update in HLa. case_if. applys~ HL. } } } }
......@@ -375,7 +244,7 @@ Proof using.
forwards* (n&En): roots_inv_L_Root x D.
forwards* (m&Em): roots_inv_L_Root y D.
(* false C0. *) } }
{ xrets. rewrite~ linkto_related. }
{ xrets. rewrite link_sym. rewrite~ link_related. }
Qed.
Hint Extern 1 (RegisterSpec union) => Provide union_spec.
......
......@@ -54,44 +54,9 @@ Proof using.
Qed.
Hint Extern 1 (index (LibMap_map parent ?L) ?x) => rewrite index_map_parent_eq.
Hint Extern 1 (?x \indom ?L) => congruence.
Hint Extern 1 (?x \in dom ?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. typeclass.
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 *)
......@@ -208,13 +173,13 @@ Lemma union_spec : forall D R x y,
y \in D ->
app union [x y]
(UF D R)
(fun (_:unit) => Hexists R', UF D R' \* \[R' = link 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).
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.
xapp_spec* infix_colon_eq_spec_group. 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.
......@@ -228,7 +193,6 @@ Hint Extern 1 (RegisterSpec union) => Provide union_spec.
(* TODO: xapps_spec *)
......@@ -237,6 +201,7 @@ 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