[Iris-Club] Two Monoid Questions

[Gregory Malecha]

Is SProp essential? Or just useful for this?

On Thu, Aug 15, 2019, 4:40 PM Robbert Krebbers <
mailinglists at robbertkrebbers.nl> wrote:

> 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.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20190815/933482ae/attachment.html>