Commit e805705f authored by Léon Gondelman's avatar Léon Gondelman

fix mset_member_spec

parent bd9cea6c
......@@ -140,12 +140,16 @@ 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; is_set_mut xs X
((v = #true x X) (v = #false x X)) }}}.
Proof.
iIntros (Φ) "Hmut H".
iDestruct "Hmut" as (s hd) "[% [Hs Hset]]"; subst .
iDestruct "Hmut" as (s hd) "[% [Hs #Hset]]"; subst .
wp_lam. wp_let. wp_load. wp_let.
by iApply (set_member_spec with "[$Hset//]").
iApply (set_member_spec with "[$Hset //]").
iNext. iIntros (v) "%".
iApply ("H" $! _). iSplit; last done.
iExists s, hd. eauto.
Qed.
Lemma mset_add_spec (x: val) (xs: val) (X: gset val):
......
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