Commit 97433982 authored by charguer's avatar charguer
Browse files

cleanup hints

parent e4b5e585
(* Union-find: array-based implementation,
simplified by omiting the union-by-rank mechanism *)
type id = int
type node = int
type t = int array
type t = node array
let create n =
Array.init n (fun i -> i)
......
type id = int
type node = int
type t
val create : int -> t
val find : t -> id -> id
val find : t -> node -> node
val union : t -> id -> id -> unit
val union : t -> node -> node -> unit
val same : t -> id -> id -> bool
val same : t -> node -> node -> bool
......@@ -6,6 +6,8 @@ Require Import UFArray_ml.
Require Import TLC.LibListZ.
Ltac auto_tilde ::=
try solve [ jauto_set; solve [ eauto | congruence | math | typeclass ] ].
Generalizable Variables B.
......@@ -152,10 +154,14 @@ End MArray.
Implicit Type L : map int int.
Implicit Type R : int->int.
Implicit Type x y z r s : int.
Implicit Types t : loc.
Section UF.
Context (K : Type) `{IK:Inhab K}.
Implicit Type L : map K K.
Implicit Type R : K->K.
Implicit Type x y z r s : K.
(*******************************************************************)
(** Union-Find Invariants *)
......@@ -163,7 +169,7 @@ Implicit Types t : loc.
(** [repr L 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 int int) : int->int->Prop :=
Inductive repr (L:map K K) : K->K->Prop :=
| repr_root : forall x,
index L x ->
x = L[x] ->
......@@ -178,7 +184,7 @@ Inductive repr (L:map int int) : int->int->Prop :=
(** [roots L R] captures the fact that [R] is the function
that computes the roots described by the table [L]. *)
Definition roots (L:map int int) (R:int->int) :=
Definition roots (L:map K K) (R:K->K) :=
forall x, index L x -> repr L x (R x).
......@@ -194,7 +200,7 @@ Implicit Type d : nat.
(** Copy-paste of the definition of [repr], plus a bound on the depth. *)
Inductive reprn L : nat->int->int->Prop :=
Inductive reprn L : nat->K->K->Prop :=
| reprn_root : forall d x,
index L x ->
x = L[x] ->
......@@ -232,7 +238,6 @@ Proof. introv H. induction* H. Qed.
End Reprn.
Hint Resolve repr_of_reprn.
(*******************************************************************)
......@@ -303,7 +308,7 @@ Qed.
Hint Resolve index_L.
(** Roots of valid nodes are valid nodes. *)
(* not needed, used onthefly by automation *)
Lemma index_R : forall L R x,
roots L R ->
index L x ->
......@@ -360,11 +365,6 @@ Qed.
(*******************************************************************)
(** Lemmas for specifying and justifying the operations *)
Ltac auto_tilde ::=
try solve [ jauto_set; solve [ eauto | congruence | math | typeclass ] ].
Hint Resolve index_of_index_length'.
(** Invariants hold for [create] operation. *)
Lemma roots_init : forall L,
......@@ -384,7 +384,7 @@ Definition link R x y :=
Lemma link_related : forall R x y,
R x = R y ->
link R x y = R.
Proof using.
Proof using IK.
introv E. applys fun_ext_1 ;=> i. unfold link. case_if as C.
{ destruct~ C. }
{ auto. }
......@@ -394,7 +394,7 @@ Qed.
Lemma link_inv_related : forall R x y,
R x = R y ->
link R x y = R.
Proof using.
Proof using IK.
introv E. extens ;=> i. unfold link. case_if as C.
{ rewrite E in C. destruct~ C. }
{ auto. }
......@@ -500,11 +500,19 @@ Proof using.
applys~ repr_next y. { rewrite~ K1. } } }
Qed.
End UF.
(*******************************************************************)
(** 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.
(** [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
......@@ -551,10 +559,9 @@ Proof using.
xcf. xapps*. xrets. xif.
{ xrets*. forwards* Ex: roots_inv_R_root x L R. congruence. }
{ inverts Hx' as. { intros. false. } intros Ix' N Hy. rename d0 into d.
sets y: (L[x]). forwards* ER: roots_inv_R y (R x) HR.
xapp_spec* (IH d).
sets y: (L[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. }
{ rewrite* ER. }
clearbody y. clears L. intros Hr L (Hn&HR).
xapp*. xrets*. splits*.
{ applys* conseq_dom_update. }
......@@ -592,11 +599,12 @@ Lemma union_spec : forall n R t x y,
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.
{ applys* conseq_dom_update.
rewrites~ (>> conseq_dom_index_eq Hn) in *. }
rewrites* (>> conseq_dom_index_eq Hn) in *. }
{ applys* roots_link L R x y. } }
{ xrets. rewrite* link_related. }
{ xrets. rewrite~ link_related. }
Qed.
Hint Extern 1 (RegisterSpec union) => Provide union_spec.
......
(* Union-find: array-based implementation,
simplified by omiting the union-by-rank mechanism *)
type node = ref contents
and contents = Root | Link of node
let create () =
ref Root
let rec find x =
match !x with
| Root -> x
| Link y ->
let r = find y in
x := Link r;
r
let same x y =
find x == find y
let union x y =
let r = find x in
let s = find y in
if r != s then r := Link s
type node
val create : unit -> node
val find : node -> node
val union : node -> node -> unit
val same : node -> node -> bool
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