[Iris-Club] Two Monoid Questions

[Ralf Jung]

Hi again,

> 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 [1] 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'⌝.
> 
> [1]:
> https://gitlab.mpi-sws.org/iris/iris/merge_requests/91/diffs#61cdf7eb214f1f82c632a3363846a4add084219c_0_121

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
authoritative is.

; Ralf