[Iris-Club] Two Monoid Questions
jung at mpi-sws.org
Tue Aug 13 12:48:54 CEST 2019
> However, I think the predicate won't do for another reason: it can be very
> useful to know, given ownership of some fragment, that this is a (partial) view
> for *some* authoritative element. For example, this proposal  for an
> authoritative partial bijection exploits this for a lemma like
> Lemma in_bij_agree γ L (a a' : A) (b b' : B) :
> own_bij γ L -∗
> in_bij γ a b -∗
> in_bij γ a' b' -∗
> ⌜a = a' ↔ b = b'⌝.
Correction: the lemma as given does not need this, because it takes `own_bij`.
But I think we'd want a lemma that says
Lemma in_bij_agree γ (a a' : A) (b b' : B) :
in_bij γ a b -∗
in_bij γ a' b' -∗
⌜a = a' ↔ b = b'⌝.
and then we would need to know the relation without having any clue what the
More information about the Iris-Club