[Iris-Club] Two Monoid Questions

[Ralf Jung]

Probably just useful, and I think we could get a decent generalization of auth
without a lot of SProp infrastructure.  That infrastructure will be nice if we
want to have more fancy relations, but I think we can leave that to future work.
I might give this a try on the train to ICFP and see how it goes. ;)

; Ralf

On 16.08.19 00:23, Gregory Malecha wrote:
> Is SProp essential? Or just useful for this?
> 
> On Thu, Aug 15, 2019, 4:40 PM Robbert Krebbers <mailinglists at robbertkrebbers.nl
> <mailto: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.
> 

-- 
Website: https://people.mpi-sws.org/~jung/