Commit 185cc0d2 authored by charguer's avatar charguer
Browse files

uf_proof

parent 0fb918f4
......@@ -12,81 +12,6 @@ Implicit Types t : loc.
Notation "'\exists' x1 , H" := (heap_is_pack (fun x1 => H))
(at level 39, x1 ident, H at level 50) : heap_scope.
Notation "'\exists' x1 x2 , H" := (Hexists x1, Hexists x2, H)
(at level 39, x1 ident, x2 ident, H at level 50) : heap_scope.
Notation "'\exists' x1 x2 x3 , H" := (Hexists x1, Hexists x2, Hexists x3, H)
(at level 39, x1 ident, x2 ident, x3 ident, H at level 50) : heap_scope.
Notation "'\exists' x1 x2 x3 x4 , H" :=
(Hexists x1, Hexists x2, Hexists x3, Hexists x4, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50) : heap_scope.
Notation "'\exists' x1 x2 x3 x4 x5 , H" :=
(Hexists x1, Hexists x2, Hexists x3, Hexists x4, Hexists x5, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50) : heap_scope.
Notation "'\exists' x1 : T1 , H" := (heap_is_pack (fun x1:T1 => H))
(at level 39, x1 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) , H" := (Hexists x1:T1,H)
(at level 39, x1 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) ( x2 : T2 ) , H" :=
(Hexists x1:T1, Hexists x2:T2, H)
(at level 39, x1 ident, x2 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) , H" :=
(Hexists x1:T1, Hexists x2:T2, Hexists x3:T3, H)
(at level 39, x1 ident, x2 ident, x3 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) ( x4 : T4 ) , H" :=
(Hexists x1:T1, Hexists x2:T2, Hexists x3:T3, Hexists x4:T4, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) ( x4 : T4 ) ( x5 : T5 ) , H" :=
(Hexists x1:T1, Hexists x2:T2, Hexists x3:T3, Hexists x4:T4, Hexists x5:T5, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 x2 : T ) , H" :=
(Hexists x1:T, Hexists x2:T, H)
(at level 39, x1 ident, x2 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 x2 x3 : T ) , H" :=
(Hexists x1:T, Hexists x2:T, Hexists x3:T, H)
(at level 39, x1 ident, x2 ident, x3 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 x2 x3 x4 : T ) , H" :=
(Hexists x1:T, Hexists x2:T, Hexists x3:T, Hexists x4:T, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 x2 x3 x4 x5 : T ) , H" :=
(Hexists x1:T, Hexists x2:T, Hexists x3:T, Hexists x4:T, Hexists x5:T, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) x2 , H" :=
(Hexists x1:T1, Hexists x2, H)
(at level 39, x1 ident, x2 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) x2 x3 , H" :=
(Hexists x1:T1, Hexists x2, Hexists x3, H)
(at level 39, x1 ident, x2 ident, x3 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) x2 x3 x4 , H" :=
(Hexists x1:T1, Hexists x2, Hexists x3, Hexists x4, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) x2 x3 x4 x5 , H" :=
(Hexists x1:T1, Hexists x2, Hexists x3, Hexists x4, Hexists x5, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) ( x2 : T2 ) x3 , H" :=
(Hexists x1:T1, Hexists x2:T2, Hexists x3, H)
(at level 39, x1 ident, x2 ident, x3 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) ( x2 : T2 ) x3 x4 , H" :=
(Hexists x1:T1, Hexists x2:T2, Hexists x3, Hexists x4, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) ( x2 : T2 ) x3 x4 x5 , H" :=
(Hexists x1:T1, Hexists x2:T2, Hexists x3, Hexists x4, Hexists x5, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) x4 , H" :=
(Hexists x1:T1, Hexists x2:T2, Hexists x3:T3, Hexists x4, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50, only parsing) : heap_scope.
Notation "'\exists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) x4 x5 , H" :=
(Hexists x1:T1, Hexists x2:T2, Hexists x3:T3, Hexists x4, Hexists x5, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.
(*******************************************************************)
(** Representation Predicate *)
......@@ -117,7 +42,7 @@ Definition roots (L:list int) (R:int->int) :=
indexed in the range [0...(n-1)]. *)
Definition UF (n:int) (R:int->int) (t:loc) : hprop :=
\exists (L:list int), t ~> Array L \* \[n = length L /\ roots L R].
Hexists (L:list int), t ~> Array L \* \[n = length L /\ roots L R].
......@@ -273,7 +198,8 @@ Proof using.
forwards~: repr_functional Hx Hx'.
Qed.
(* not used? *)
(** If [L x = x], then [x] is a root. *)
Lemma roots_inv_R_root : forall x L R,
roots L R ->
L[x] = x ->
......@@ -344,7 +270,7 @@ Proof using.
{ rewrite~ @read_update_same. }
Qed.
(** Update of [repr] during a linking operation, for nodes that do not
(** 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,
......@@ -360,7 +286,7 @@ Proof using.
{ applys~ repr_next y. rewrite~ K1. }
Qed.
(** Update of [repr] during a linking operation, for nodes that do
(** 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,
......@@ -379,7 +305,7 @@ Proof using.
{ applys~ repr_next y. rewrite~ K1. }
Qed.
(** Putting it together: invariants are preserved by a link operation. *)
(** A link operation preserves the invariants. *)
Lemma roots_link : forall L R x y L' R',
R' = link R x y ->
......@@ -401,33 +327,8 @@ Proof using. (* Note: this proof uses hint [repr_inv_L] *)
{ rew_logic in C. destruct C as [C1 C2]. applys~ repr_update_neq E. }
Qed.
(* TODO: compression *)
(** A path compression preserves the invariants. *)
Lemma roots_compress' : forall d L R a L' x,
roots L R ->
reprn L d x (R x) ->
L' = L [a := R a] ->
index L x ->
index L a ->
reprn L' d x (R x).
Proof using.
introv HR M E Dx Da.
forwards~ Ha: HR a. lets Ra: repr_inv_L Ha.
lets (I1&I2&K1&K2): udpate_inv E.
gen_eq z: (R x). induction M; introv Ez.
{ applys~ reprn_root. tests C: (x = a).
{ rewrite~ K2. }
{ rewrite~ K1. } }
{ tests C: (x = a).
{ subst z. asserts~ Na: (a <> R a).
applys~ reprn_next (R a).
{ rewrite~ K2. }
{ applys~ reprn_root. rewrite~ K1. } }
{ forwards~ Ez': roots_inv_R y z HR.
applys~ reprn_next y. { rewrite~ K1. } } }
Qed.
(* derivable from above *)
Lemma roots_compress : forall L R a L',
roots L R ->
L' = L [a := R a] ->
......@@ -459,7 +360,7 @@ Lemma create_spec : forall n,
n >= 0 ->
app create [n]
PRE \[]
POST (fun t => \exists t R, UF n R t \*
POST (fun t => Hexists t R, UF n R t \*
\[forall x, index n x -> R x = x]).
Proof using.
introv Hn. xcf. xfun.
......@@ -478,82 +379,29 @@ Qed.
Hint Extern 1 (RegisterSpec create) => Provide create_spec.
(*******************************************************************)
(** Find *)
(*
Hint Rewrite @index_map_eq : rew_array. (*--TODO move *)
Hint Resolve index_map.
Lemma triple_root : forall n R p x,
index n x ->
triple (val_root p x)
(UF n R p)
(fun r => \[r = R x] \* UF n R p).
Proof using.
introv Dx. xcf. xval as F ;=> EF.
unfold UF. xtpull ;=> L (Hn&HR).
forwards~ Ix: index_of_index_length' (rm Dx) Hn.
forwards~ Hx: HR x.
forwards (d&Hx'): reprn_of_repr Hx.
applys mklocal_erase.
gen x. induction_wf IH: lt_wf d. hide IH. intros.
rewrite EF. xcf. rewrite <- EF.
xapp as vy. rew_array~. rewrite (@read_map int _ val _); auto.
(* --todo: should be rewrite read_map. *)
intros Evy. subst vy.
xapps. xif ;=> C; inverts Hx' as; try solve [ intros; false ].
{ introv _ _ Ex. xvals~. }
{ rename d0 into d. introv _ _ Nx. sets y: (L[x]).
forwards~ ER: roots_inv_R y (R x) HR.
xapp~ (>> IH d). xsimpl~. }
Qed.
Lemma triple_compress : forall n R p x z,
index n x ->
z = R x ->
triple (val_compress p x z)
(UF n R p)
(fun r => UF n R p).
Proof using.
introv Dx Ez. xcf. xval as F ;=> EF.
unfold UF. xtpull ;=> L (Hn&HR).
forwards~ Ix: index_of_index_length' (rm Dx) Hn.
forwards~ Hx: HR x.
applys mklocal_erase. (* TODO: avoid *)
forwards (d&Hx'): reprn_of_repr Hx.
gen L x. induction_wf IH: lt_wf d. hide IH. intros.
rewrite EF. xcf. rewrite <- EF.
xapps. xif ;=> C.
{ xapps~. xapp~ ;=> ? ->. rewrite (@read_map int _ val _); auto.
(* --todo: should be rewrite read_map. *)
inverts Hx' as; try solve [ intros; false ].
introv _ Nx Ry. sets y: (L[x]). rename d0 into d.
forwards~ ER: roots_inv_R y (R x) HR.
rewrite <- map_update; auto.
sets_eq L': (L[x:=z]).
forwards~ (I1&I2&K1&K2): udpate_inv L' L x z.
subst z. forwards~ HR': roots_compress L' HR.
forwards~ Hy: HR' y.
xapp~ (>> IH d).
{ subst L'. rew_array~. }
{ applys~ roots_compress' HR. }
{ xsimpl~. } }
{ xvals~. }
Qed.
*)
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. xcf.
(* xapps~. xapps~. intros _. xvals~. *) skip. (* TODO *)
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. applys* index_L. }
{ rewrite* ER. }
clearbody y. clears L. intros Hr L (Hn&HR).
xapp*. xrets*. splits*.
{ rewrite* length_update. }
{ rewrite Hr,ER. applys* roots_compress. } }
Qed.
Hint Extern 1 (RegisterSpec find) => Provide find_spec.
......@@ -583,7 +431,7 @@ Lemma union_spec : forall n R t x y,
index n y ->
app union [t x y]
(UF n R t)
(fun (_:unit) => \exists (R':int->int), UF n R' t \* \[R' = link R x y]).
(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).
......
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