<div dir="ltr">Ah, that makes more sense. When you said SProp, I thought you meant the new sprop Coq feature, not step-indexed propositions.<br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Aug 16, 2019 at 9:58 AM Robbert Krebbers <<a href="mailto:mailinglists@robbertkrebbers.nl">mailinglists@robbertkrebbers.nl</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">I realized I defined the type sProp in Coq a long time ago already, but <br>
never created a merge request for it. I have done that now:<br>
<br>
   <a href="https://gitlab.mpi-sws.org/iris/iris/merge_requests/304/diffs" rel="noreferrer" target="_blank">https://gitlab.mpi-sws.org/iris/iris/merge_requests/304/diffs</a><br>
<br>
I propose we continue this discussion there.<br>
<br>
On 16/08/2019 14.30, Ralf Jung wrote:<br>
>> By defining SProp, I suppose you would also define the logical operators and<br>
>> prove that it's an step-indexed intuitionistic logic?<br>
> <br>
> No, I'd just define the notion of down-closed predicates, and show that they<br>
> form a COFE.  I'd show that `dist` can be written as one (and maybe validity<br>
> too, for fun's sake).  And that's about all I need to get started.<br>
> <br>
> Even independent of a proof mode instance this opens all sorts of questions:<br>
> should `dist` be define as one of these? Should `UPred` use this? Should there<br>
> be embeddings to/from the Iris Base Logic?<br>
> For now, I am only interested in what is needed to generalize auth.<br>
> <br>
> ; Ralf<br>
> <br>
</blockquote></div><br clear="all"><br>-- <br><div dir="ltr" class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div>gregory malecha</div><div><a href="mailto:gregory@bedrocksystems.com" target="_blank">gregory@bedrocksystems.com</a></div><div><span>director of formal methods</span></div></div></div></div></div>