Commit 341fd592 authored by charguer's avatar charguer
Browse files

progressUF

parent 185cc0d2
Set Implicit Arguments.
Require Import CFML.CFLib.
Require Import Stdlib.
Require Import Array_proof.
Require Import UFArray_ml.
Require Import TLC.LibListZ.
Module Import MArray.
Parameter MArray : forall A, map int A -> loc -> hprop.
Require Import TLC.LibSet.
Open Scope set_scope.
Definition conseq_dom A (n:int) (M:map int A) : Prop :=
dom M = \set{ i | 0 <= i < n }.
Parameter MArray_conseq_dom : forall A (M:map int A) p,
p ~> MArray M ==+> Hexists n, \[conseq_dom n M].
(* TODO: MArray domain *)
(* -------------------------------------------------------------------------- *)
(* [Array.length].
Parameter length_spec :
curried 1%nat Array_ml.length /\
forall A (xs:list A) t,
app Array_ml.length [t]
INV (t ~> Array xs)
POST (fun n => \[n = length xs]).
Hint Extern 1 (RegisterSpec Array_ml.length) => Provide length_spec.
*)
(* -------------------------------------------------------------------------- *)
(* [Array.get]. *)
Parameter get_spec :
curried 2%nat Array_ml.get /\
forall A `{Inhab A} (xs:map int A) t i,
index xs i ->
app Array_ml.get [t i]
INV (t ~> MArray xs)
POST \[= xs[i] ].
Hint Extern 1 (RegisterSpec Array_ml.get) => Provide get_spec.
(* -------------------------------------------------------------------------- *)
(* [Array.set]. *)
Parameter set_spec :
curried 2%nat Array_ml.set /\
forall A (xs:map int A) t (i:int) (x:A),
index xs i ->
app Array_ml.set [t i x]
PRE ( t ~> MArray xs)
POST (# t ~> MArray (xs[i:=x])).
Hint Extern 1 (RegisterSpec Array_ml.set) => Provide set_spec.
(* -------------------------------------------------------------------------- *)
(* [Array.make].
Parameter make_spec :
curried 2%nat Array_ml.make /\
forall A n (x:A),
0 <= n ->
app Array_ml.make [n x]
PRE \[]
POST (fun t => Hexists xs, t ~> MArray xs \* \[xs = make n x]).
Hint Extern 1 (RegisterSpec Array_ml.make) => Provide make_spec.
*)
(* -------------------------------------------------------------------------- *)
(* [Array.init]. *)
Generalizable Variable A.
Axiom init_spec :
forall A (IA:Inhab A) (F : int -> A) (n : int) (f : func),
0 <= n ->
(forall (i : int),
index n i ->
app f [i]
PRE \[] (* simplified spec for now: no state carried through *)
POST (fun (x:A) => \[x = F i])) ->
app Array_ml.init [n f]
PRE \[]
POST (fun t =>
Hexists (xs:map int A), t ~> MArray xs \* \[conseq_dom n xs]
\* \[forall i, index xs i -> xs[i] = F i]).
Hint Extern 1 (RegisterSpec Array_ml.init) => Provide init_spec.
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.
(*******************************************************************)
(** Union-Find Invariants *)
(** [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 :=
| repr_root : forall x,
index L x ->
x = L[x] ->
repr L x x
| repr_next : forall x y z,
index L x ->
y = L[x] ->
x <> y ->
repr L y z ->
repr L x z.
(** [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) :=
forall x, index L x -> repr L x (R x).
(*******************************************************************)
(** Induction principle on the height of a [repr] derivation *)
(** Ideally, would be automatically generated by Coq *)
Section Reprn.
Implicit Type d : nat.
(** Copy-paste of the definition of [repr], plus a bound on the depth. *)
Inductive reprn L : nat->int->int->Prop :=
| reprn_root : forall d x,
index L x ->
x = L[x] ->
reprn L d x x
| reprn_next : forall d x y z,
index L x ->
y = L[x] ->
x <> y ->
reprn L d y z ->
reprn L (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 ->
d < d' ->
reprn L 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.
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.
Proof. introv H. induction* H. Qed.
End Reprn.
Hint Resolve repr_of_reprn.
(*******************************************************************)
(** Basic lemmas about [repr] *)
(** [repr] is injective. *)
Lemma repr_inj : forall z1 z2 L x,
repr L x z1 ->
repr L x z2 ->
z1 = z2.
Proof using.
introv H1 H2. gen z2.
induction H1 as [x1 HI1 HE1 | x1 y1 z1 HI1 HE1 HN1 IH]; intros.
{ inverts H2; auto_false. }
{ inverts H2; auto_false. subst y1. applys* IHIH. }
Qed.
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 ->
z1 = z2.
Proof using.
introv H1 H2. induction H1; inverts H2; try subst; auto_false.
Qed.
(** [repr] only holds of valid nodes. *)
Lemma repr_inv_index_l : forall L x z,
repr L x z ->
index L x.
Proof using. introv H. inverts* H. Qed.
Lemma repr_inv_index_r : forall L x z,
repr L x z ->
index L 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.
Proof using. introv H. induction~ H. Qed.
Hint Resolve repr_inv_index_l repr_inv_index_r.
(*******************************************************************)
(** Basic lemmas about [roots] *)
(** Parents of valid nodes are valid nodes. *)
Lemma index_L : forall L R x,
roots L R ->
index L x ->
index L (L[x]).
Proof using.
introv HR HI. forwards M: HR HI. inverts M as.
{ introv H1 H2 H3. rewrite* <- H2. }
{ intros. applys* repr_inv_index_l. }
Qed.
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).
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 ->
R x = x ->
index L x ->
L[x] = x.
Proof using.
introv HR E Ix. forwards~ Hx: HR x.
lets Ex: repr_inv_L Hx. congruence.
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.
Proof using.
introv HR Ix. forwards~ Hx: HR x. applys* repr_inv_L.
Qed.
(** If [repr L x z] then [R x] is [z]. *)
Lemma roots_inv_R : forall x z L R,
roots L R ->
repr L 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. *)
Lemma roots_inv_R_root : forall x L R,
roots L R ->
L[x] = x ->
index L x ->
R x = x.
Proof using.
introv HR Lx Ix. forwards* Hx': HR x.
inverts Hx'; congruence.
Qed.
(*******************************************************************)
(** Lemmas for specifying and justifying the operations *)
Ltac auto_tilde ::=
try solve [ jauto_set; solve [ eauto | congruence | math ] ].
Hint Resolve index_of_index_length'.
(** Invariants hold for [create] operation. *)
Lemma roots_init : forall L,
(forall x, index L x -> L[x] = x) ->
roots L (fun x => x).
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]. *)
Definition link R x y :=
fun i => If (R i = R x \/ R i = R y) then R y else R i.
(** 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.
Proof using.
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.
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,
L' = L[a:=b] ->
(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).
Proof using.
intros. subst. splits; intros.
{ rewrite index_eq_indom in *. rew_map*. typeclass. }
skip. (* TODO { rewrite index_eq_indom in *. rew_map* in H. typeclass. }*)
(*
Print LibMap.
{ rewrite~ @LibMap.update_eq. }
{ rewrite~ @index_update_eq in H. }
{ rewrite~ @read_update_neq. }
{ rewrite~ @read_update_same. }
Qed.
*)
Admitted.
(** Lemma for link operations: case of nodes that do not
belong to the two components involved. *)
Lemma repr_update_neq : forall L a b L' x z,
repr L x z ->
L' = L[a:=b] ->
L[a] = a ->
z <> a ->
repr L' x z.
Proof using.
introv M E R N. lets (I1&_&K1&_): udpate_inv (rm E).
induction M.
{ applys~ repr_root. rewrite~ K1. }
{ applys~ repr_next y. rewrite~ K1. }
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 ->
a <> b ->
repr L' x b.
Proof using.
introv M E Ib Rb N. lets (I1&_&K1&K2): udpate_inv (rm E).
lets Ra: repr_inv_L M.
gen_eq a': a. induction M; intros E.
{ subst x. applys~ repr_next b. rewrite~ K2.
applys* repr_root. rewrite~ K1. }
{ applys~ repr_next y. rewrite~ K1. }
Qed.
(** A link operation preserves the invariants. *)
Lemma roots_link : forall L R x y L' R',
R' = link R x 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.
lets (I1&I2&_&_): udpate_inv E.
rewrites (rm M). unfold link. 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.
(** 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 ->
roots L' R.
Proof using.
introv HR E Da. intros x Dx.
forwards~ Ha: HR a. lets Ra: repr_inv_L Ha.
lets (I1&I2&K1&K2): udpate_inv E. forwards~ M: HR x.
gen_eq z: (R x). induction M; introv Ez.
{ applys~ repr_root. tests C: (x = a).
{ rewrite~ K2. }
{ rewrite~ K1. } }
{ tests C: (x = a).
{ subst z. asserts~ Na: (a <> R a).
applys~ repr_next (R a).
{ rewrite~ K2. }
{ applys~ repr_root. rewrite~ K1. } }
{ forwards~ Ez': roots_inv_R y z HR.
applys~ repr_next y. { rewrite~ K1. } } }
Qed.
(*******************************************************************)
(** Representation predicate *)
(** [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
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].
(*******************************************************************)
(** Hints *)
Lemma conseq_dom_index_eq : forall A n (L:map int A),
conseq_dom n L ->
index n = index L. (* i.e. [index L x <> index n x] *)
Proof using.
introv HD. extens. intros x. rewrite int_index_eq.
rewrite index_eq_indom. unfolds in HD. rewrite HD.
rewrite* in_set_st_eq.
Qed.
Lemma conseq_dom_index_L : forall A n (L:map int A) x,
conseq_dom n L ->
index n x ->
index L x.
Proof. introv Hd Hx. rewrites* <- (>> conseq_dom_index_eq Hd). Qed.
Hint Resolve conseq_dom_index_L.
Lemma conseq_dom_update : forall n L x y,
conseq_dom n L ->
index n x ->
conseq_dom n (L[x:=y]).
Proof using.
introv HD Hx. unfolds conseq_dom.
rewrite* dom_update_at_index. typeclass.
Qed.
(*******************************************************************)
(** Create *)
Lemma create_spec : forall n,
n >= 0 ->
app create [n]
PRE \[]
POST (fun t => Hexists t R, UF n R t \*
\[forall x, index n x -> R x = x]).
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.
{ auto. } { split*. applys* roots_init. } }
Qed.
Hint Extern 1 (RegisterSpec create) => Provide create_spec.
(*******************************************************************)
(** Find *)
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]).
Proof using.
introv Ix. xunfold UF. xpull. intros L (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.
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).
{ 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. }
{ rewrite Hr,ER. applys* roots_compress. } }
Qed.
Hint Extern 1 (RegisterSpec find) => Provide find_spec.
(*******************************************************************)
(** Same *)
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)
POST (fun b => \[b = isTrue (R x = R y)]).
Proof using.
introv Ix Iy. xcf. xapps*. xapps*. xrets.
Qed.
Hint Extern 1 (RegisterSpec same) => Provide same_spec.
(*******************************************************************)
(** Union *)
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 (_:unit) => Hexists (R':int->int), UF n R' t \* \[R' = link R x y]).
Proof using.
introv Ix Iy. xcf. xapps*. xapps*. xrets. xif.
{ unfold UF. xpull. intros L (Hn&HR).
xapp*. xsimpl*. splits.
{ applys* conseq_dom_update.
rewrites (>> conseq_dom_index_eq Hn) in *; applys* index_R. }
{ applys* roots_link L R x y. } }
{ xrets. rewrite* link_related. }
Qed.
Hint Extern 1 (RegisterSpec union) => Provide union_spec.