[Iris-Club] Two Monoid Questions

[Ralf Jung]

Ah, sorry.  Yes that is a rather unfortunate clash of terminology. ;)
Our S is for "step-indexed".  I don't even know what the "s" in Coq's sprop is
for, do you?

; Ralf

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

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