Commit bd9cea6c authored by Dan Frumin's avatar Dan Frumin

Fix formatting

parent add06828
......@@ -11,6 +11,7 @@ Section Sets.
| [] => hd = NONEV
| x :: xs => hd', hd = SOMEV (x,hd') is_list hd' xs
end.
Definition is_set (hd : val) (X : gset val) : Prop :=
l : list val, is_list hd l NoDup l of_list l X.
......@@ -26,7 +27,6 @@ Section Sets.
let: "y" := (Snd "p") in "member" "x" "y"
end.
Definition set_add : val :=
λ: "x" "xs",
if: set_member "x" "xs"
......@@ -40,7 +40,6 @@ Section MutableSet.
Definition is_set_mut `{heapG Σ} (v : val) (X : gset val) : iProp Σ
:= ( (l : loc) hd, v = #l l hd is_set hd X )%I.
Definition mset_create : val := λ: <>, ref (newset #()).
Definition mset_member : val :=
......@@ -60,8 +59,7 @@ Section MutableSet.
End MutableSet.
Section Sets_wp.
Context `{heapG Σ}.
Context `{heapG Σ}.
Lemma set_newset_spec:
{{{ True }}} newset #() {{{ v, RET v; is_set v ∅⌝ }}}.
......@@ -102,7 +100,7 @@ Section Sets_wp.
Lemma set_add_spec (x: val) (xs: val) (X: gset val):
{{{ is_set xs X x X }}}
set_add x xs
{{{ v, RET v;
{{{ v, RET v;
(is_set v ({[x]} X) )}}}.
Proof.
iIntros (Φ) "[% %] HPost".
......@@ -126,7 +124,7 @@ End Sets_wp.
Section MutableSet_wp.
Context `{heapG Σ}.
Context `{heapG Σ}.
Lemma mset_create_spec:
{{{ True }}} mset_create #() {{{ v, RET v; is_set_mut v }}}.
......@@ -142,7 +140,7 @@ Section MutableSet_wp.
Lemma mset_member_spec (x: val) (xs: val) (X: gset val):
{{{ is_set_mut xs X }}}
mset_member x xs
{{{ v, RET v; (v = #true x X) (v = #false x X) }}}.
{{{ v, RET v; (v = #true x X) (v = #false x X) }}}.
Proof.
iIntros (Φ) "Hmut H".
iDestruct "Hmut" as (s hd) "[% [Hs Hset]]"; subst .
......@@ -153,7 +151,7 @@ Section MutableSet_wp.
Lemma mset_add_spec (x: val) (xs: val) (X: gset val):
{{{ is_set_mut xs X x X }}}
mset_add x xs
{{{ RET #() ; (is_set_mut xs ({[x]} X))}}}.
{{{ RET #() ; (is_set_mut xs ({[x]} X))}}}.
Proof.
iIntros (Φ) "[Hmut %] HPost".
iDestruct "Hmut" as (s hd) "[% [Hs Hset]]"; subst.
......@@ -168,7 +166,7 @@ Section MutableSet_wp.
Lemma mset_clear_spec (xs: val) (X: gset val):
{{{ is_set_mut xs X }}}
mset_clear xs
{{{ RET #() ; is_set_mut xs }}}.
{{{ RET #() ; is_set_mut xs }}}.
Proof.
iIntros (Φ) "Hmut HPost".
iDestruct "Hmut" as (s hd) "[% [Hs Hset]]"; subst.
......@@ -178,4 +176,4 @@ Section MutableSet_wp.
iApply "HPost". iExists s, v. by iFrame.
Qed.
End MutableSet_wp.
\ No newline at end of file
End MutableSet_wp.
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