[Iris-Club] Two Monoid Questions

[Gregory Malecha]

Naive question: What sort of reasoning are the bijections used for that
makes this lemma so crucial?

On Tue, Aug 13, 2019 at 6:48 AM Ralf Jung <jung at mpi-sws.org> wrote:

> 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
>


-- 
gregory malecha
gregory at bedrocksystems.com
director of formal methods
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20190813/6c9fa32d/attachment.html>