Commit 45e74acc authored by Dan Frumin's avatar Dan Frumin

Remove an admit from flock.v

parent 062b5533
......@@ -317,9 +317,9 @@ Section flock.
own γ ( (f <$> m)) - [ map] ix m, own γ ( {[ i := f x ]}).
Proof.
simple refine (map_ind (λ m, _)%I _ _ m); simpl.
- iIntros "He". admit. (* rewrite fmap_empty big_sepM_empty. iSplit; eauto. *)
- iIntros "He". rewrite fmap_empty big_sepM_empty. iSplit; eauto.
- iIntros (i x m' Hi IH) "He".
(* rewrite fmap_insert insert_union_singleton_l.
rewrite fmap_insert insert_union_singleton_l.
assert (({[i := f x]} (f <$> m')) = {[i := f x]} (f <$> m')) as ->.
{ rewrite /op /cmra_op /= /gmap_op.
apply map_eq. intros j. destruct (decide (i = j)) as [->|?].
......@@ -340,9 +340,9 @@ Section flock.
rewrite lookup_merge lookup_singleton_ne // lookup_fmap -Heqmj //. }
rewrite auth_frag_op own_op IH big_sepM_insert; last eauto.
iSplit; iIntros "[$ Hm']"; by iApply "He".
Qed. *) Admitted.
Qed.
(* here it is crucial that we use a gmap:
(* here it is crucial that we use a gmap:
that way there is at most one flock_res associated with a prop_id *)
Lemma acquire_cancel_spec γ lk (I : gmap prop_id (iProp Σ * frac)) :
{{{ is_flock γ lk [ map] i p I, flock_res γ i p.1 p.2 }}}
......
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