Commit 823bfcad authored by Dan Frumin's avatar Dan Frumin

Implement `own_frag_emp`

parent 00c5460f
......@@ -587,6 +587,15 @@ Section flock.
iSplit; iIntros "[$ Hm']"; by iApply "He".
Qed.
Lemma own_frag_empty γ X :
own (flock_props_name γ) ( X) ==
own (flock_props_name γ) ( X) own (flock_props_name γ) ( ).
Proof.
iIntros "H". rewrite -own_op.
iApply (own_update with "H").
by apply auth_update_alloc.
Qed.
Lemma acquire_flock_spec γ lk (I : gmap prop_id lock_res) :
{{{ is_flock γ lk [ map] i X I, flock_res γ i X }}}
acquire lk
......@@ -638,11 +647,8 @@ Section flock.
(* show that I ⊆ fp, or, better fp = fp' ∪ I *)
(* first obtain the empty fragment for big_sepM_own_frag *)
iAssert (own (flock_props_name γ) ( to_props_map fp)
own (flock_props_name γ) ( ))%I
with "[Haprops]"
as "[Haprops Hemp]".
{ admit. }
iMod (own_frag_empty with "Haprops") as "[Haprops #Hemp]".
pose (I' := (fmap (λ X, (res_frac X, to_agree (res_name X))) I)).
iAssert (own (flock_props_name γ) ( I'))
with "[HI Hemp]" as "HI".
......@@ -685,8 +691,7 @@ Section flock.
apply map_eq=> k. by rewrite lookup_fmap. }
iFrame. iSplit; eauto.
rewrite big_sepM_fmap.
iApply (big_sepM_own_frag with "[] HI").
admit.
iApply (big_sepM_own_frag with "Hemp HI").
Abort.
Lemma release_cancel_spec' γ lk I :
......
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