Commit e0fd56f9 authored by charguer's avatar charguer
Browse files

UF_pointer union

parent b53aa687
......@@ -35,6 +35,15 @@ Proof using.
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.
End Map.
......@@ -70,6 +79,19 @@ Definition UF (D:set loc) (R:loc->loc) : hprop :=
/\ (forall y, y \notin D -> R y = y)].
(*******************************************************************)
(** Hints *)
Lemma index_map_parent_eq : forall L x,
index (LibMap_map parent L) x = x \indom L.
Proof using.
intros. rewrite index_eq_indom. rewrite~ LibMap_dom_map.
Qed.
Hint Extern 1 (index (LibMap_map parent ?L) ?x) => rewrite index_map_parent_eq.
Hint Extern 1 (?x \indom ?L) => congruence.
(*******************************************************************)
(** Create *)
......@@ -170,27 +192,56 @@ 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]).
(fun (_:unit) => Hexists R', UF D R' \* \[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. }
introv Ix Iy. xcf. xapps*. xapps*. xapps. xif.
{ unfold UF. xpull. intros L (HD&HR&HN).
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.
{ 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.
{ destruct Cz. { false; congruence. } { congruence. } } { auto. } } }
{ 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