<div dir="auto">Is SProp essential? Or just useful for this?</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Aug 15, 2019, 4:40 PM Robbert Krebbers <<a href="mailto:mailinglists@robbertkrebbers.nl">mailinglists@robbertkrebbers.nl</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On 14/08/2019 12.49, Ralf Jung wrote:<br>
> The annoying part is generalizing this to step-indexing, where we will need a<br>
> notion of "step-indexed relations". It is clear what that means (A -> B -> nat<br>
> -> Prop, down-closed and non-expansive), but so far we managed to avoid<br>
> realizing this notion in Coq. I have long advocated for adding it, though.<br>
<br>
Although I initially believed it would not be useful to have this notion <br>
since we didn't have machinery for doing proofs in SProp---we do have <br>
such machinery now! We can instantiate MoSeL with SProp, although it's <br>
not really a separation logic, we can just define P ∗ Q := P ∧ Q and <br>
<pers> P := P. I think it's worth a short to do this and see how useful <br>
it is.<br>
</blockquote></div>