<div dir="ltr">Naive question: What sort of reasoning are the bijections used for that makes this lemma so crucial?<br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Aug 13, 2019 at 6:48 AM Ralf Jung <<a href="mailto:jung@mpi-sws.org">jung@mpi-sws.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi again,<br>
<br>
> However, I think the predicate won't do for another reason: it can be very<br>
> useful to know, given ownership of some fragment, that this is a (partial) view<br>
> for *some* authoritative element.  For example, this proposal [1] for an<br>
> authoritative partial bijection exploits this for a lemma like<br>
> <br>
>   Lemma in_bij_agree γ L (a a' : A) (b b' : B) :<br>
>     own_bij γ L -∗<br>
>     in_bij γ a b -∗<br>
>     in_bij γ a' b' -∗<br>
>     ⌜a = a' ↔ b = b'⌝.<br>
> <br>
> [1]:<br>
> <a href="https://gitlab.mpi-sws.org/iris/iris/merge_requests/91/diffs#61cdf7eb214f1f82c632a3363846a4add084219c_0_121" rel="noreferrer" target="_blank">https://gitlab.mpi-sws.org/iris/iris/merge_requests/91/diffs#61cdf7eb214f1f82c632a3363846a4add084219c_0_121</a><br>
<br>
Correction: the lemma as given does not need this, because it takes `own_bij`.<br>
But I think we'd want a lemma that says<br>
<br>
  Lemma in_bij_agree γ (a a' : A) (b b' : B) :<br>
    in_bij γ a b -∗<br>
    in_bij γ a' b' -∗<br>
    ⌜a = a' ↔ b = b'⌝.<br>
<br>
and then we would need to know the relation without having any clue what the<br>
authoritative is.<br>
<br>
; Ralf<br>
</blockquote></div><br clear="all"><br>-- <br><div dir="ltr" class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div>gregory malecha</div><div><a href="mailto:gregory@bedrocksystems.com" target="_blank">gregory@bedrocksystems.com</a></div><div><span>director of formal methods</span></div></div></div></div></div>