Commit 97c64ab2 authored by charguer's avatar charguer
Browse files

remove xapp_spec

parent ee4bdb24
......@@ -154,11 +154,6 @@ End MArray.
(* TODO rename
ref_spec_group
infix_emark_spec_group
infix_colon_eq_spec_group
*)
(* TODO: id outside domain *)
Section Map.
......@@ -205,8 +200,10 @@ End Map.
(* TODO rename
ref_spec_group
infix_emark_spec_group
infix_colon_eq_spec_group
*)
Module RefGroupSpecs.
Hint Extern 1 (RegisterSpec ref) => Provide ref_spec_group.
Hint Extern 1 (RegisterSpec infix_emark__) => Provide infix_emark_spec_group.
Hint Extern 1 (RegisterSpec infix_colon_eq__) => Provide infix_colon_eq_spec_group.
End RefGroupSpecs.
Set Implicit Arguments.
Require Import UF.
Require Import UFPointerRank_ml.
Import RefGroupSpecs.
(*******************************************************************)
......@@ -88,7 +89,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 (HD&HR&HN&HL).
xapp_spec ref_spec_group. intros x. xsimpl.
xapp. intros x. xsimpl.
{ congruence. }
{ splits.
{ rewrite~ dom_update. }
......@@ -139,7 +140,7 @@ Proof using.
{ 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*.
xapp~. xrets*. splits*.
{ rewrite~ dom_update_at_index. rewrite~ index_eq_indom. }
{ rewrite Hr,ER. applys* roots_compress.
{ rewrite* LibMap_map_update. }
......@@ -220,23 +221,17 @@ Proof using.
{ subst D. rewrites* <- index_map_parent_eq. applys~ index_R. }
asserts Ry: (R y \in D).
{ subst D. rewrites* <- index_map_parent_eq. applys~ index_R. }
xapps_spec* infix_emark_spec_group.
xapps_spec* infix_emark_spec_group.
xmatch.
xapps*. xapps*. xmatch.
{ xif.
{ xapp_spec* infix_colon_eq_spec_group.
xrets*. applys* link_correct. }
{ xapps~. xrets*. applys* link_correct. }
{ xif.
{ xapp_spec* infix_colon_eq_spec_group.
xrets*. rewrite link_sym. applys* link_correct. }
{ xapp_spec* infix_colon_eq_spec_group.
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. }
asserts EP: (LibMap_map parent L' = LibMap_map parent L).
{ unfold L'. skip. (* TODO by extensionality ... *) }
xapp_spec* infix_colon_eq_spec_group.
xret. xsimpl*. rewrite link_sym. applys~ link_correct.
xapp~. xrets*. rewrite link_sym. applys~ link_correct.
{ unfolds roots. rewrite~ EP. }
{ unfolds no_self_link. intros a b Ha HLa. unfold L' in HLa.
rewrite read_update in HLa. case_if. applys~ HL. } } } }
......
Set Implicit Arguments.
Require Import UF.
Require Import UFPointer_ml.
Import RefGroupSpecs.
(*******************************************************************)
......@@ -87,7 +88,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 (HD&HR&HN&HL).
xapp_spec ref_spec_group. intros x. xsimpl.
xapp. intros x. xsimpl.
{ congruence. }
{ splits.
{ rewrite~ dom_update. }
......@@ -137,7 +138,7 @@ Proof using.
{ 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*.
xapp~. xrets*. splits*.
{ rewrite~ dom_update_at_index. rewrite~ index_eq_indom. }
{ rewrite Hr,ER. applys* roots_compress.
{ rewrite* LibMap_map_update. }
......@@ -179,7 +180,7 @@ Proof using.
{ unfold UF. xpull. intros L (HD&HR&HN&HL).
asserts Rx: (R x \in D).
{ subst D. rewrites* <- index_map_parent_eq. applys~ index_R. }
xapp_spec* infix_colon_eq_spec_group. xrets*. splits.
xapp~. xrets*. 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.
......
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