Commit b53aa687 authored by charguer's avatar charguer
Browse files

pointer_proof

parent 634fc54e
Set Implicit Arguments.
Require Import CFML.CFLib.
Require Import Stdlib.
Require Import Array_proof.
Require Import UFPointer_ml.
Require Import TLC.LibListZ.
Require Import UFArray_map_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.
End Map.
Implicit Type D : set loc.
Implicit Type L : map loc contents_.
Implicit Type R : loc->loc.
Implicit Type x y z r s : loc.
(*******************************************************************)
(** Representation predicate *)
Global Instance Inhab_contents_ : Inhab contents_.
Proof using. apply (Inhab_of_val Root). Qed.
(** [parent L x] maps a root to itself and a link to its destination. *)
Definition parent (x:loc) (c:contents_) : loc :=
match c with
| Root => x
| Link y => y
end.
(** [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
\* \[D = dom L
/\ roots (LibMap_map parent L) R
/\ (forall y, y \notin D -> R y = y)].
(*******************************************************************)
(** Create *)
(* TO REFINE *)
Lemma repr_update_neq' : forall (L:map loc loc) a b (L':map loc loc) x z,
repr L x z ->
L' = L[a:=b] ->
L[a] = a ->
z <> a ->
repr L' x z.
Admitted.
Lemma roots_create : forall L R x,
roots (LibMap_map parent L) R ->
x \notindom L ->
R x = x ->
roots (LibMap_map parent L[x:=Root]) R.
Proof using.
introv HR Hx Rx. unfolds roots.
intros y Hy.
(*TODO*)
skip_rewrite (index (LibMap_map parent L[x:=Root]) y = (index L y \/ x = y)) in Hy.
destruct Hy.
{ forwards Ry: HR y. skip. (* TODO *)
applys repr_update_neq' x x Ry. (* TODO: need to prove R y \in D , thus <> x. *)
skip. skip. skip. }
{ subst y. rewrite LibMap_map_update. rewrite Rx.
applys repr_root. skip. (* TODO *)
rewrite* LibMap.read_update_same. }
Qed.
Lemma create_spec : forall D R,
app create [tt]
PRE (UF D R)
POST (fun x => UF (D \u \{x}) R \* \[x \notin D]).
Proof using.
xcf. xunfold UF. xpull. intros L (HD&HR&HN).
xapp_spec ref_spec_group. intros x. xsimpl.
{ congruence. }
{ splits.
{ rewrite~ dom_update. }
{ applys~ roots_create. applys~ HN. }
{ intros y Hy. rewrite notin_union_eq in Hy. applys~ HN. } }
Qed.
Hint Extern 1 (RegisterSpec create) => Provide create_spec.
(*******************************************************************)
(** Find *)
Lemma find_spec : forall D R x,
x \in D ->
app find [x]
INV (UF D R)
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. } }
*)
skip.
Qed.
Hint Extern 1 (RegisterSpec find) => Provide find_spec.
(*******************************************************************)
(** Same *)
Lemma same_spec : forall D R x y,
x \in D ->
y \in D ->
app same [x y]
INV (UF D R)
POST (fun b => \[b = isTrue (R x = R y)]).
Proof using.
introv Ix Iy. xcf. xapps*. xapps*. xapps. xsimpl*.
Qed.
Hint Extern 1 (RegisterSpec same) => Provide same_spec.
(*******************************************************************)
(** Union *)
(*
Lemma union_spec : forall D R x y,
x \in D ->
y \in D ->
app union [x y]
(UF D R)
(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* roots_link L R x y. } }
{ xrets. rewrite* link_related. }
Qed.
Hint Extern 1 (RegisterSpec union) => Provide union_spec.
*)
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