[Iris-Club] Two Monoid Questions

[Robbert Krebbers]

On 8/13/19 11:20 AM, Ralf Jung wrote:
> Hi Gregory,
> 
>> I'm probably showing my ignorance and naivity with the following thoughts
>> but....On the engineering Coq inference point, would it make sense to set up
>> parameters like?
>>
>> Definition Auth {A V : Type} (R : A -> V -> Prop) : RA :=
>>
>> This would allow you to write `Auth R` where `R` is the models relation as the
>> type. While the type is easy to write, this doesn't really solve the problem
>> with the constructors. I guess a canonical structure would address this:
>>
>> Record AuthS : Type :=
>> { a_auth : Type
>> ; a_view : Type
>> ; a_models : a_auth -> a_view -> Prop }. (* subject to the appropriate constraints.
>> Definition auth (A : AuthS) (m : A.(a_auth)) : Auth A := (Some m, id).
>> Definition view (A : AuthS) (m : A.(a_view)) : Auth A := (None, m).
>>
>> If `m` have appropriate types, then you could probably just write `auth m` and
>> `view m`, but getting the right annotations might be annoying when values arise
>> in the middle of your proofs.
> 
> Yeah, something like this is probably what we should do -- using either
> typeclasses or canonical structures to infer the "models" relation.  With
> canonical structures, knowing either the "auth" or "view" type would have to
> uniquely determine the relation, but OTOH when stating ownership one often will
> give only one type.

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 use-case.

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

   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.

> 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