[Iris-Club] Two Monoid Questions
jung at mpi-sws.org
Tue Aug 13 12:46:49 CEST 2019
> I'm not sure that it even makes sense to use a canonical structure or a type
> class to infer the "models" relation. I would suppose it's possible that on the
> same types you may want to use a different "models" relations depending on the
> As such, I would suppose that the first option (namely, having the types +
> relation unbundled) makes most sense. Most of the time, you would do something
> Definition myR := authR ...
> And if you use myR, Coq can infer the "models" relation from that.
> The thing that I'm a bit more worried about is that in the general setting, the
> types A and V will be OFEs, the "models" relation will be a step-indexed
> relation, and should be non-expansive.
> Without the type sProp of step-indexed propositions this will all be very
> annoying to use. Maybe we should add that type someday.
Yeah, we would likely need that type for the step-indexed version of this.
>> Hm, this is an interesting thought. We do not permit composing two
>> authoritatives anyway,
> We actually do: https://gitlab.mpi-sws.org/iris/iris/merge_requests/215
Good point, I forgot about that. But we can just use agreement for the predicate.
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'⌝.
So, I think we want the predicate/relation encoded in the type, not just the
authoritative element. And that will mean making it a relation so that the
"full view" can change.
More information about the Iris-Club