[Iris-Club] Two Monoid Questions

[Ralf Jung]

Hi Gregory,

> This makes sense to me. Is there a pre-packaged way to express the views concept
> in Iris?

No, the closest we have is the general auth construction.

> You were mentioning that it can be annoying to have fractional permissions and
> such hanging out in the authoritative piece, so I was thinking that perhaps if
> you had a way to generalize equality to a predicate, then you wouldn't need to
> separate out the bijection.

I don't follow.  The authoritative piece needs a fractional (or exclusive)
permission, that is crucial for realizing its "authoritativeness".

But indeed, my thinking is that we can generalize auth the way you suggested
with a "models" relationship -- or rather, introduce a new "view" CMRA like
that, and then define auth as an instance of it, and the "bijection-auth" would
be another instance.

The annoying part is generalizing this to step-indexing, where we will need a
notion of "step-indexed relations". It is clear what that means (A -> B -> nat
-> Prop, down-closed and non-expansive), but so far we managed to avoid
realizing this notion in Coq. I have long advocated for adding it, though.

; Ralf