Commit c27fc703 authored by charguer's avatar charguer
Browse files

simplifyauto

parent 9d0fb880
......@@ -10,7 +10,7 @@ Generalizable Variables A B.
Ltac auto_typeclass :=
match goal with |- Inhab _ => typeclass end.
Ltac auto_tilde ::=
Ltac auto_star ::=
try solve [ jauto_set; solve [ eauto | congruence | math | auto_typeclass ] ].
......@@ -65,7 +65,7 @@ Lemma conseq_dom_update : forall A n (L:map int A) x y,
conseq_dom n (L[x:=y]).
Proof using.
introv HD Hx. unfolds conseq_dom.
rewrite* dom_update_at_index. typeclass.
rewrite* dom_update_at_index. (* typeclass. *)
Qed.
......@@ -173,7 +173,7 @@ 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 *)
case_if. autos*. destruct* (M a). (* TODO: cleanup *)
Qed.
Transparent dom dom_inst.
......
......@@ -136,7 +136,7 @@ Proof using. introv H. induction* H. Qed.
Lemma repr_inv_L : forall L x z,
repr L x z ->
L[z] = z.
Proof using. introv H. induction~ H. Qed.
Proof using. introv H. induction* H. Qed.
Hint Resolve repr_inv_index_l repr_inv_index_r.
......@@ -174,7 +174,7 @@ Lemma roots_inv_L : forall x L R,
index L x ->
L[x] = x.
Proof using.
introv HR E Ix. forwards~ Hx: HR x.
introv HR E Ix. forwards* Hx: HR x.
lets Ex: repr_inv_L Hx. congruence.
Qed.
......@@ -186,7 +186,7 @@ Lemma roots_inv_L_root : forall x L R,
index L x ->
L[R x] = R x.
Proof using.
introv HR Ix. forwards~ Hx: HR x. applys* repr_inv_L.
introv HR Ix. forwards* Hx: HR x. applys* repr_inv_L.
Qed.
(** If [repr L x z] then [R x] is [z]. *)
......@@ -236,7 +236,7 @@ Definition link (R:K->K) (x y z:K) : K->K :=
Lemma link_sym : forall R x y z,
link R x y z = link R y x z.
Proof using.
intros. extens. intros i. unfolds link. repeat case_if*.
intros. extens. intros i. unfolds link. repeat case_if; tauto.
Qed.
(** Linking of nodes in the same component is idempotent. *)
......@@ -246,7 +246,7 @@ Lemma link_related : forall R x y,
link R x y (R y) = R.
Proof using IK.
introv E. applys fun_ext_1 ;=> i. unfold link. case_if as C.
{ destruct~ C. }
{ destruct* C. }
{ auto. }
Qed.
......@@ -262,7 +262,7 @@ Lemma udpate_inv : forall L' L a b,
Proof using.
introv E Da. subst L'. splits.
{ intros. rewrite index_eq_indom in *. rew_map~. }
{ introv H. applys~ index_update_inv Da. }
{ introv H. applys* index_update_inv Da. }
{ introv H N. rewrite* LibMap.read_update_neq. }
{ introv H. rewrite* LibMap.read_update_same. }
Qed.
......@@ -279,10 +279,10 @@ Lemma repr_update_neq : forall L a b L' x z,
z <> a ->
repr L' x z.
Proof using.
introv M Ia E R N. forwards~ (I1&_&K1&_): udpate_inv (rm E).
introv M Ia E R N. forwards* (I1&_&K1&_): udpate_inv (rm E).
induction M.
{ applys~ repr_root. rewrite~ K1. }
{ applys~ repr_next y. rewrite~ K1. }
{ applys* repr_root. rewrite* K1. }
{ applys* repr_next y. rewrite* K1. }
Qed.
(** Lemma for link operations: case of nodes that do
......@@ -296,12 +296,12 @@ Lemma repr_update_eq : forall L a b L' x,
a <> b ->
repr L' x b.
Proof using.
introv M E Ib Rb N. forwards~ (I1&_&K1&K2): udpate_inv (rm E).
introv M E Ib Rb N. forwards* (I1&_&K1&K2): udpate_inv (rm E).
lets Ra: repr_inv_L M.
gen_eq a': a. induction M; intros E.
{ subst x. applys~ repr_next b. rewrite~ K2.
applys* repr_root. rewrite~ K1. }
{ applys~ repr_next y. rewrite~ K1. }
{ subst x. applys* repr_next b. rewrite* K2.
applys* repr_root. rewrite* K1. }
{ applys* repr_next y. rewrite* K1. }
Qed.
(** A link operation preserves the invariants. *)
......@@ -316,13 +316,13 @@ Lemma roots_link : forall L L' R R' x y,
roots L' R'.
Proof using. (* Note: this proof uses the hint [repr_inv_L] *)
introv M HR E N Dx Dy. intros u Du.
forwards~ Hx: roots_inv_L_root x HR.
forwards~ Hy: roots_inv_L_root y HR.
forwards~ (I1&I2&_&_): udpate_inv E.
forwards* Hx: roots_inv_L_root x HR.
forwards* Hy: roots_inv_L_root y HR.
forwards* (I1&I2&_&_): udpate_inv E.
rewrites (rm M). unfold link. case_if as C.
{ destruct C as [C|C].
{ rewrite <- C in E. applys~ repr_update_eq E. }
{ rewrite <- C. applys~ repr_update_neq E. } }
{ rewrite <- C in E. applys* repr_update_eq E. }
{ rewrite <- C. applys* repr_update_neq E. } }
{ rew_logic in C. destruct C as [C1 C2]. applys* repr_update_neq E. }
Qed.
......@@ -335,20 +335,20 @@ Lemma roots_compress : forall L R a L',
roots L' R.
Proof using.
introv HR E Da. intros x Dx.
forwards~ Ha: HR a. lets Ra: repr_inv_L Ha.
forwards~ (I1&I2&K1&K2): udpate_inv E.
forwards~ M: HR x.
forwards* Ha: HR a. lets Ra: repr_inv_L Ha.
forwards* (I1&I2&K1&K2): udpate_inv E.
forwards* M: HR x.
gen_eq z: (R x). induction M; introv Ez.
{ applys~ repr_root. tests C: (x = a).
{ rewrite~ K2. }
{ rewrite~ K1. } }
{ applys* repr_root. tests C: (x = a).
{ rewrite* K2. }
{ rewrite* K1. } }
{ tests C: (x = a).
{ subst z. asserts~ Na: (a <> R a).
applys~ repr_next (R a).
{ rewrite~ K2. }
{ applys~ repr_root. rewrite~ K1. } }
{ forwards~ Ez': roots_inv_R y z HR.
applys~ repr_next y. { rewrite~ K1. } } }
{ subst z. asserts* Na: (a <> R a).
applys* repr_next (R a).
{ rewrite* K2. }
{ applys* repr_root. rewrite* K1. } }
{ forwards* Ez': roots_inv_R y z HR.
applys* repr_next y. { rewrite* K1. } } }
Qed.
......@@ -361,11 +361,9 @@ Lemma index_extends : forall L x a b,
index L[a:=b] x.
Proof using IK.
introv Hx Ha. rewrite index_eq_indom in *.
rewrite LibMap.dom_update. rewrite~ @in_union_eq. typeclass.
rewrite LibMap.dom_update. rewrite* @in_union_eq. typeclass.
Qed.
Hint Resolve index_extends.
Lemma repr_extends : forall L a b x r,
a \notindom L ->
x \indom L ->
......@@ -373,8 +371,10 @@ Lemma repr_extends : forall L a b x r,
repr (L[a:=b]) x r.
Proof using.
introv Ha Hx HR. gen Hx. induction HR; intros.
{ applys* repr_root. rewrite* LibMap.read_update_neq. { intro_subst. false* Ha. } }
{ applys* repr_root. { applys* index_extends. }
rewrite* LibMap.read_update_neq. { intro_subst. false* Ha. } }
{ applys* repr_next y.
{ applys* index_extends. }
{ rewrite* LibMap.read_update_neq. { intro_subst. false* Ha. } }
{ applys* IHHR. rewrite* <- index_eq_indom. (* applys* repr_inv_index_l. *) } }
Qed.
......
......@@ -54,10 +54,10 @@ Proof using.
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. }
{ xrets*. forwards* Ex: roots_inv_R_root x L R. }
{ inverts Hx' as. { intros. false. } intros Ix' N Hy. rename d0 into d.
sets y: (L[x]). lets Ry: repr_of_reprn Hy.
forwards* ER: roots_inv_R y (R x) HR. xapp_spec~ (IH d).
forwards* ER: roots_inv_R y (R x) HR. xapp_spec* (IH d).
{ subst. rewrites (>> conseq_dom_index_eq Hn). applys* index_L. }
clearbody y. clears L. intros Hr L (Hn&HR).
xapp*. xrets*. splits*.
......@@ -101,7 +101,7 @@ Proof using.
{ applys* conseq_dom_update.
rewrites* (>> conseq_dom_index_eq Hn) in *. }
{ applys* roots_link L R x y. } }
{ xrets. rewrite~ link_related. }
{ xrets. rewrite* link_related. }
Qed.
Hint Extern 1 (RegisterSpec union) => Provide union_spec.
......
......@@ -56,7 +56,7 @@ Definition UF (D:set loc) (R:loc->loc) : hprop :=
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.
intros. rewrite index_eq_indom. rewrite* LibMap_dom_map.
Qed.
Lemma indom_root : forall D R L x,
......@@ -65,8 +65,8 @@ Lemma indom_root : forall D R L x,
(R x) \in D.
Proof using.
introv (HD&HR&HN&HL) Hx. subst D.
rewrites* <- index_map_parent_eq.
applys~ index_R. rewrite~ index_map_parent_eq.
rewrites* <- index_map_parent_eq.
applys* index_R. rewrite* index_map_parent_eq.
Qed.
Hint Extern 1 (index (LibMap_map parent ?L) ?x) => rewrite index_map_parent_eq.
......@@ -89,13 +89,13 @@ Proof using.
intros y Hy.
rewrite index_eq_indom in Hy. rewrite LibMap_dom_map in Hy. rewrite dom_update in Hy.
rewrite in_union_eq in Hy. destruct Hy.
{ forwards~ Ry: HR y. rewrite LibMap_map_update. applys* repr_extends.
{ forwards* Ry: HR y. rewrite LibMap_map_update. applys* repr_extends.
{ rewrite* LibMap_dom_map. }
{ rewrite* LibMap_dom_map. } }
{ rewrite~ @in_single_eq in H. subst y. rewrite LibMap_map_update. rewrite Rx.
{ rewrite* @in_single_eq in H. subst y. rewrite LibMap_map_update. rewrite Rx.
applys repr_root.
{ rewrite index_eq_indom. rewrite LibMap.dom_update, LibMap_dom_map.
rewrite in_union_eq. right. rewrite~ @in_single_eq. typeclass. } (* TODO: simpler *)
rewrite in_union_eq. right. rewrite* @in_single_eq. typeclass. } (* TODO: simpler *)
{ rewrite* LibMap.read_update_same. }
{ typeclass. } }
Qed.
......@@ -108,9 +108,9 @@ Lemma inv_create : forall L R D x,
inv (D \u '{x}) R L[x:=Root 0].
Proof using.
introv (HD&HR&HN&HL) Hx. splits.
{ rewrite~ dom_update. }
{ subst D. applys~ roots_create. }
{ intros y Hy. rewrite notin_union_eq in Hy. applys~ HN. }
{ rewrite* dom_update. }
{ subst D. applys* roots_create. }
{ intros y Hy. rewrite notin_union_eq in Hy. applys* HN. }
{ intros y z Hy Hz. rewrite in_union_eq, in_single_eq in Hy.
destruct Hy.
{ rewrite read_update in Hz. case_if. applys* HL. }
......@@ -125,7 +125,7 @@ Lemma create_spec : forall D R,
POST (fun x => UF (D \u \{x}) R \* \[x \notin D]).
Proof using.
xcf. xunfold UF. xpull. intros L HI. lets (HD&HR&HN&HL): HI.
xapp. intros x. xsimpl~. applys~ inv_create.
xapp. intros x. xsimpl*. applys* inv_create.
Qed.
Hint Extern 1 (RegisterSpec create) => Provide create_spec.
......@@ -144,13 +144,13 @@ Lemma inv_compress : forall D R L L' x r,
inv D R L'.
Proof using.
introv (HD&HR&HN&HL) Hx Nx ->. splits.
{ rewrite~ dom_update_at_index. rewrite~ index_eq_indom. }
{ 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. } }
{ inverts* Hb. } { applys* HL. } }
Qed.
(** [find] is correct. *)
......@@ -170,24 +170,23 @@ Proof using.
rewrite* LibMap_map_read. rewrite* HLx. }
{ intros y Hy. sets L':(LibMap_map parent L). inverts Hx' as.
{ intros IRx E1 E2. forwards* HLx: roots_inv_L x HR.
{ subst L'. rewrite~ index_map_parent_eq. }
{ 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.
rewrite Hy in E1. simpls. unfolds in HL. false* (>> HL x y). }
{ 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. }
{ 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).
{ lets: repr_of_reprn Hy'. subst D. rewrite <- index_map_parent_eq.
xapp_spec* (IH d); try solve [ subst L'; autos* ].
{ subst L'. lets: repr_of_reprn Hy'. subst D. rewrite <- index_map_parent_eq.
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. }
{ 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 HI. lets (HD&HR&HN&HL): HI.
xapp~. xrets*. applys~ inv_compress. } }
xapp*. xrets*. applys* inv_compress. } }
Qed.
Hint Extern 1 (RegisterSpec find) => Provide find_spec.
......@@ -228,12 +227,12 @@ Proof using.
introv HI ER' EL' Hx Hy Hxy. lets (HD&HR&HN&HL): HI.
forwards* HRx: indom_root x HI. forwards* HRy: indom_root y HI.
splits.
{ subst D L'. rewrite~ dom_update_at_index. }
{ subst L'. applys* roots_link R x y. rewrite~ LibMap_map_update. }
{ subst D L'. rewrite* dom_update_at_index. }
{ subst L'. applys* roots_link R x y. rewrite* LibMap_map_update. }
{ intros z Hz. subst R'. unfold link. specializes HN Hz. case_if as Cz.
{ destruct Cz. { false; congruence. } { congruence. } } { auto. } }
{ subst L'. intros a b Ha Hb. rewrite read_update in Hb. case_if.
{ inverts~ Hb. } { applys~ HL. } }
{ inverts* Hb. } { applys* HL. } }
Qed.
(** Additional lemma to prove that if a node [R x] is necessarily
......@@ -245,9 +244,9 @@ Lemma roots_inv_L_Root : forall x D L R,
(R x) \in D ->
exists n, L[R x] = Root n.
Proof using.
introv (HD&HR&HN&HL) Hx HRx. forwards~ EQ: roots_inv_L_root x HR.
rewrite~ LibMap_map_read in EQ. cases (L[R x]) as ERx.
{ eauto. } { simpls. false~ HL (R x). }
introv (HD&HR&HN&HL) Hx HRx. forwards* EQ: roots_inv_L_root x HR.
rewrite* LibMap_map_read in EQ. cases (L[R x]) as ERx.
{ eauto. } { simpls. false* HL (R x). }
Qed.
(** [inv] is preserved by updating the rank information. *)
......@@ -260,20 +259,20 @@ Lemma inv_rerank : forall x D L L' R n,
Proof using.
introv HI Hd EL'. lets (HD&HR&HN&HL): HI.
asserts ED: (dom L = dom L').
{ subst L'. rewrite~ dom_update_at_index.
rewrite~ index_eq_indom. rewrite~ <- HD. }
forwards~ HRx: indom_root x HI. splits.
{ subst L'. rewrite~ dom_update_at_index. rewrite~ index_eq_indom. }
{ asserts_rewrite~ (LibMap_map parent L' = LibMap_map parent L).
{ subst L'. rewrite* dom_update_at_index.
rewrite* index_eq_indom. rewrite* <- HD. }
forwards* HRx: indom_root x HI. splits.
{ subst L'. rewrite* dom_update_at_index. rewrite* index_eq_indom. }
{ asserts_rewrite* (LibMap_map parent L' = LibMap_map parent L).
{ applys LibMap_extens. { repeat rewrite LibMap_dom_map. auto. }
{ intros a Ha. rewrite LibMap_dom_map in Ha.
rewrite~ LibMap_map_read. rewrite~ LibMap_map_read; [| rewrite~ ED].
subst L'. rewrite read_update. case_if.
{ forwards~ (m&Hm): roots_inv_L_Root x HI. subst a. rewrite Hm. simple~. }
rewrite* LibMap_map_read. rewrite* LibMap_map_read; [| rewrite* ED].
subst L'. rewrite read_update. case_if.
{ forwards* (m&Hm): roots_inv_L_Root x HI. subst a. rewrite Hm. simple*. }
{ auto. } } } }
{ auto. }
{ subst L'. unfolds no_self_link. intros a b Ha HLa.
rewrite read_update in HLa. case_if. applys~ HL. }
rewrite read_update in HLa. case_if. applys* HL. }
Qed.
Lemma union_spec : forall D R x y,
......@@ -285,23 +284,23 @@ Lemma union_spec : forall D R x y,
Proof using.
introv Ix Iy. xcf. xapps*. xapps*. xapps. xif.
{ unfold UF. xpull. intros L HI. lets (HD&HR&HN&HL): HI.
xapps~. xapps*. xmatch.
xapps*. xapps*. xmatch.
{ xif.
{ xapps~. xrets*. applys* link_correct. }
{ xapps*. xrets*. applys* link_correct. }
{ xif.
{ xapp~. xrets*. rewrite link_sym. applys* link_correct. }
{ xapp~. sets L': (L[R x:=Root (n + 1)%I]).
{ xapp*. xrets*. rewrite link_sym. applys* link_correct. }
{ xapp*. sets L': (L[R x:=Root (n + 1)%I]).
asserts ED: (dom L = dom L').
{ unfold L'. rewrite~ dom_update_at_index.
rewrite~ index_eq_indom. rewrite~ <- HD. }
forwards~ HRy: indom_root y HI.
xapp~. xrets*. rewrite link_sym. applys~ link_correct L'.
subst L'. applys~ inv_rerank x. } } }
{ unfold L'. rewrite* dom_update_at_index.
rewrite* index_eq_indom. rewrite* <- HD. }
forwards* HRy: indom_root y HI.
xapp*. xrets*. rewrite link_sym. applys* link_correct L'.
subst L'. applys* inv_rerank x. } } }
{ xfail.
forwards* (n&En): roots_inv_L_Root x D.
forwards* (m&Em): roots_inv_L_Root y D.
(* false C0. *) } }
{ xrets. rewrite link_sym. rewrite~ link_related. }
{ xrets. rewrite link_sym. rewrite* link_related. }
Qed.
Hint Extern 1 (RegisterSpec union) => Provide union_spec.
......
......@@ -55,7 +55,7 @@ Definition UF (D:set loc) (R:loc->loc) : hprop :=
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.
intros. rewrite index_eq_indom. rewrite* LibMap_dom_map.
Qed.
Lemma indom_root : forall D R L x,
......@@ -64,8 +64,8 @@ Lemma indom_root : forall D R L x,
(R x) \in D.
Proof using.
introv (HD&HR&HN&HL) Hx. subst D.
rewrites* <- index_map_parent_eq.
applys~ index_R. rewrite~ index_map_parent_eq.
rewrites* <- index_map_parent_eq.
applys* index_R. rewrite* index_map_parent_eq.
Qed.
Hint Extern 1 (index (LibMap_map parent ?L) ?x) => rewrite index_map_parent_eq.
......@@ -88,13 +88,13 @@ Proof using.
intros y Hy.
rewrite index_eq_indom in Hy. rewrite LibMap_dom_map in Hy. rewrite dom_update in Hy.
rewrite in_union_eq in Hy. destruct Hy.
{ forwards~ Ry: HR y. rewrite LibMap_map_update. applys* repr_extends.
{ forwards* Ry: HR y. rewrite LibMap_map_update. applys* repr_extends.
{ rewrite* LibMap_dom_map. }
{ rewrite* LibMap_dom_map. } }
{ rewrite~ @in_single_eq in H. subst y. rewrite LibMap_map_update. rewrite Rx.
{ rewrite* @in_single_eq in H. subst y. rewrite LibMap_map_update. rewrite Rx.
applys repr_root.
{ rewrite index_eq_indom. rewrite LibMap.dom_update, LibMap_dom_map.
rewrite in_union_eq. right. rewrite~ @in_single_eq. typeclass. } (* TODO: simpler *)
rewrite in_union_eq. right. rewrite* @in_single_eq. typeclass. } (* TODO: simpler *)
{ rewrite* LibMap.read_update_same. }
{ typeclass. } }
Qed.
......@@ -107,9 +107,9 @@ Lemma inv_create : forall L R D x,
inv (D \u '{x}) R L[x:=Root].
Proof using.
introv (HD&HR&HN&HL) Hx. splits.
{ rewrite~ dom_update. }
{ subst D. applys~ roots_create. }
{ intros y Hy. rewrite notin_union_eq in Hy. applys~ HN. }
{ rewrite* dom_update. }
{ subst D. applys* roots_create. }
{ intros y Hy. rewrite notin_union_eq in Hy. applys* HN. }
{ intros y z Hy Hz. rewrite in_union_eq, in_single_eq in Hy.
destruct Hy.
{ rewrite read_update in Hz. case_if. applys* HL. }
......@@ -124,7 +124,7 @@ Lemma create_spec : forall D R,
POST (fun x => UF (D \u \{x}) R \* \[x \notin D]).
Proof using.
xcf. xunfold UF. xpull. intros L HI. lets (HD&HR&HN&HL): HI.
xapp. intros x. xsimpl~. applys~ inv_create.
xapp. intros x. xsimpl*. applys* inv_create.
Qed.
Hint Extern 1 (RegisterSpec create) => Provide create_spec.
......@@ -143,13 +143,13 @@ Lemma inv_compress : forall D R L L' x r,
inv D R L'.
Proof using.
introv (HD&HR&HN&HL) Hx Nx ->. splits.
{ rewrite~ dom_update_at_index. rewrite~ index_eq_indom. }
{ 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. } }
{ inverts* Hb. } { applys* HL. } }
Qed.
(** [find] is correct. *)
......@@ -169,24 +169,23 @@ Proof using.
rewrite* LibMap_map_read. rewrite* HLx. }
{ intros y Hy. sets L':(LibMap_map parent L). inverts Hx' as.
{ intros IRx E1 E2. forwards* HLx: roots_inv_L x HR.
{ subst L'. rewrite~ index_map_parent_eq. }
{ 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.
rewrite Hy in E1. simpls. unfolds in HL. false* (>> HL x y). }
{ 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. }
{ 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).
{ lets: repr_of_reprn Hy'. subst D. rewrite <- index_map_parent_eq.
xapp_spec (IH d); try solve [ subst L'; autos* ].
{ subst L'. lets: repr_of_reprn Hy'. subst D. rewrite <- index_map_parent_eq.
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. }
{ 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 HI. lets (HD&HR&HN&HL): HI.
xapp~. xrets*. applys~ inv_compress. } }
xapp*. xrets*. applys* inv_compress. } }
Qed.
Hint Extern 1 (RegisterSpec find) => Provide find_spec.
......@@ -227,12 +226,12 @@ Proof using.
introv HI ER' EL' Hx Hy Hxy. lets (HD&HR&HN&HL): HI.
forwards* HRx: indom_root x HI. forwards* HRy: indom_root y HI.
splits.
{ subst D L'. rewrite~ dom_update_at_index. }
{ subst L'. applys* roots_link R x y. rewrite~ LibMap_map_update. }
{ subst D L'. rewrite* dom_update_at_index. }
{ subst L'. applys* roots_link R x y. rewrite* LibMap_map_update. }
{ intros z Hz. subst R'. unfold link. specializes HN Hz. case_if as Cz.
{ destruct Cz. { false; congruence. } { congruence. } } { auto. } }
{ subst L'. intros a b Ha Hb. rewrite read_update in Hb. case_if.
{ inverts~ Hb. } { applys~ HL. } }
{ inverts* Hb. } { applys* HL. } }
Qed.
(** [union] is correct. *)
......@@ -246,8 +245,8 @@ Lemma union_spec : forall D R x y,
Proof using.
introv Ix Iy. xcf. xapps*. xapps*. xapps. xif.
{ unfold UF. xpull. intros L HI. lets (HD&HR&HN&HL): HI.
xapp~. xrets*. applys~ link_correct x y HI. }
{ xrets. rewrite~ link_related. }
xapp*. xrets*. applys* link_correct x y HI. }
{ 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