Commit 226d5d53 authored by charguer's avatar charguer
Browse files

URpointers done

parent 5216e427
...@@ -199,28 +199,39 @@ Lemma find_spec : forall D R x, ...@@ -199,28 +199,39 @@ Lemma find_spec : forall D R x,
INV (UF D R) INV (UF D R)
POST (fun r => \[r = R x]). POST (fun r => \[r = R x]).
Proof using. Proof using.
(* introv Ix. xunfold UF. xpull. intros L (HD&HR&HN&HL).
introv Ix. xunfold UF. xpull. intros L (HD&HR&HN).
forwards* Hx: HR x. forwards* Hx: HR x.
forwards (d&Hx'): reprn_of_repr Hx. forwards (d&Hx'): reprn_of_repr Hx. clear Hx.
gen L x. induction_wf IH: lt_wf d. hide IH. intros. gen L x. induction_wf IH: lt_wf d. hide IH. intros.
xcf. xapps_spec* infix_emark_spec_group. xmatch_no_intros. xcf. xapps_spec* infix_emark_spec_group. xmatch_no_intros.
{ intros HLx. xrets*. forwards* Ex: roots_inv_R_root x R. { intros HLx. xrets*. forwards* Ex: roots_inv_R_root x R.
rewrite* LibMap_map_read. rewrite* HLx. } rewrite* LibMap_map_read. rewrite* HLx. }
{ intros y Hy. sets L':(LibMap_map parent L). inverts Hx' as. { intros y Hy. sets L':(LibMap_map parent L). inverts Hx' as.
{ intros IRx E1 E2. false C. subst L'. { intros IRx E1 E2. forwards* HLx: roots_inv_L x HR.
rewrite* LibMap_map_read in E1. rewrite <- E2 in E1. rewrite Hy in E1. simpls. false. } { subst L'. rewrite~ index_map_parent_eq. }
intros Ix' N Hy. rename d0 into d. false C. subst L'.
sets y: (L[x]). forwards* ER: roots_inv_R y (R x) HR. rewrite* LibMap_map_read in E1. rewrite <- E2 in E1. rewrite Hy in E1. simpls.
xapp_spec* (IH d). unfolds in HL. false~ (>> HL x y). }
{ subst. rewrites (>> conseq_dom_index_eq Hn). applys* index_L. } { intros Ix' N Hy'. rename d0 into d.
{ rewrite* ER. } sets_eq z: (L'[x]). unfold L' in EQz. rewrite~ LibMap_map_read in EQz.
clearbody y. clears L. intros Hr L (Hn&HR). rewrite Hy in EQz. simpl in EQz. subst z. (* TODO: simplify *)
xapp*. xrets*. splits*. forwards* ER: roots_inv_R y (R x) HR.
{ applys* conseq_dom_update. } { applys* repr_of_reprn. }
{ rewrite Hr,ER. applys* roots_compress. } } xapp_spec* (IH d).
*) { lets: repr_of_reprn Hy'. subst D. rewrite <- index_map_parent_eq.
skip. applys* repr_inv_index_l. }
{ rewrite* ER. }
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_spec* infix_colon_eq_spec_group. 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. } } } }
Qed. Qed.
Hint Extern 1 (RegisterSpec find) => Provide find_spec. 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