Commit 3c95625e authored by charguer's avatar charguer
Browse files

simplify find

parent f352427e
......@@ -128,8 +128,9 @@ Proof using.
rewrite* LibMap_map_read in E1. rewrite <- E2 in E1. rewrite Hy in E1. simpls.
unfolds in HL. false~ (>> HL x y). }
{ intros Ix' N Hy'. rename d0 into d.
sets_eq z: (L'[x]). unfold L' in EQz. rewrite~ LibMap_map_read in EQz.
rewrite Hy in EQz. simpl in EQz. subst z. (* TODO: simplify *)
sets z: (L'[x]). asserts EQ: (z = y).
{ subst z L'. rewrite~ LibMap_map_read. rewrite~ Hy. }
clearbody z. subst z.
forwards* ER: roots_inv_R y (R x) HR.
{ applys* repr_of_reprn. }
xapp_spec* (IH d).
......
......@@ -122,6 +122,25 @@ Hint Extern 1 (RegisterSpec create) => Provide create_spec.
(*******************************************************************)
(** Find *)
(** [inv] is preserved by path compression *)
Lemma inv_compress : forall D R L L' x r,
inv D R L ->
x \in D ->
x <> R x ->
L' = L[x := Link (R x)] ->
inv D R L'.
Proof using.
introv (HD&HR&HN&HL) Hx Nx ->. splits.
{ rewrite~ dom_update_at_index. rewrite~ index_eq_indom. }
{ applys* roots_compress.
{ rewrite* LibMap_map_update. }
{ rewrite* index_map_parent_eq. } }
{ auto. }
{ intros a b Ha Hb. rewrite read_update in Hb. case_if.
{ inverts~ Hb. } { applys~ HL. } }
Qed.
(** [find] is correct. *)
Lemma find_spec : forall D R x,
......@@ -142,9 +161,10 @@ Proof using.
{ subst L'. rewrite~ index_map_parent_eq. }
subst L'. rewrite* LibMap_map_read in E1. rewrite <- E2 in E1.
rewrite Hy in E1. simpls. unfolds in HL. false~ (>> HL x y). }
{ intros Ix' N Hy'. rename d0 into d.
sets_eq z: (L'[x]). unfold L' in EQz. rewrite~ LibMap_map_read in EQz.
rewrite Hy in EQz. simpl in EQz. subst z. (* TODO: simplify *)
{ intros Ix' N Hy'. rename d0 into d.
sets z: (L'[x]). asserts EQ: (z = y).
{ subst z L'. rewrite~ LibMap_map_read. rewrite~ Hy. }
clearbody z. subst z.
forwards* ER: roots_inv_R y (R x) HR.
{ applys* repr_of_reprn. }
xapp_spec* (IH d).
......@@ -154,14 +174,8 @@ Proof using.
asserts Ryx: (R y <> x).
{ intros E. forwards~ HL'x: roots_inv_L x HR. subst L'.
rewrite~ LibMap_map_read in HL'x. rewrite Hy in HL'x. simpls. false. }
clears L L'. clear L HN. intros Hr L (HD&HR&HN&HL).
xapp~. xrets*. splits*.
{ rewrite~ dom_update_at_index. rewrite~ index_eq_indom. }
{ rewrite Hr,ER. applys* roots_compress.
{ rewrite* LibMap_map_update. }
{ rewrite* index_map_parent_eq. } }
{ intros a b Ha Hb. rewrite read_update in Hb. case_if.
{ inverts~ Hb. } { applys~ HL. } } } }
clears L L'. clear L HN. intros Hr L HI. lets (HD&HR&HN&HL): HI.
xapp~. xrets*. applys~ inv_compress. } }
Qed.
Hint Extern 1 (RegisterSpec find) => Provide find_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