[Iris-Club] Two Monoid Questions

[Ralf Jung]

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.

Alternatively, given that we don't state ownership so terribly often, it might
be reasonable to just ask the user to give the predicate each time they use a
constructor.

> A possible alternative would be to embed the models relation into the
> authoritative piece (though I don't understand the meta-theory to know if this
> would be sound, I'm just using Prop below but it obviously needs to adhere to a
> bunch of laws). In this case the relation gets carried around in the logic but
> is only ever mentioned in one place. I guess this would look something like:
> 
> Auth(V) :=
>   { av : option { t : Type & t * (t -> V -> Prop) } * V
>   | match fst av with
>     | None => True
>     | Some (existT _ (a, M)) => M a (snd av)
>     end }.
> 
> I guess this simplifies to just making the authoritative piece a predicate over
> the view:
> 
> Auth(V) :=
>    { av : option (V -> Prop) * V
>    | match fst av with
>      | None => True
>      | Some ok => ok (snd av)
>      end }.
> 
> I imagine that in practice they would both be used in the same way.

Hm, this is an interesting thought. We do not permit composing two
authoritatives anyway, so it should not be a problem that we cannot compute with
these predicates during composition.

I am torn know, cannot decide whether explaining auth as "the views framework
embedded into Iris" or "a way to state an invariant about the composition of all
fragments out there" is the better explanation.

Kind regards,
Ralf