[Iris-Club] Two Monoid Questions

[Robbert Krebbers]

On 14/08/2019 12.49, Ralf Jung wrote:
> 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.

Although I initially believed it would not be useful to have this notion 
since we didn't have machinery for doing proofs in SProp---we do have 
such machinery now! We can instantiate MoSeL with SProp, although it's 
not really a separation logic, we can just define P ∗ Q := P ∧ Q and 
<pers> P := P. I think it's worth a short to do this and see how useful 
it is.