[Iris-Club] Several small questions on Iris

[Ralf Jung]

Hi,

> On ξ and ξ^{−1}: I agree that it is not worth an issue to examine
> further.  I realized that what I wanted to ask is: how it is done in Coq?

In Coq, we have a shallow embedding.  The key difference to the deep
embedding is that we don't have to say in advance which are the terms of
our logic.  Hence we can just use every OFE and every non-expansive
function in any way we like.  This also applies to ξ and its inverse.

The file that "ties the recursive knot" is iprod.v
<https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/base_logic/lib/iprop.v>.
 To see how the isomorphism is actually used, have a look at
saved_prop.v
<https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/base_logic/lib/saved_prop.v>.
 One of the key lemmas here is the little innocent-looking lemma
characterizing the equality of "type-level later" inside the logic
<https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/base_logic/primitive.v#L562>:

Lemma later_equivI {A : ofeT} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y).

>     Indeed, if you do that in Coq, you get a universe conflict.  And I think
>     that's not just superficial; if you do the same in set theory, you would
>     get the same problem -- the "CMRA of all CMRAs" can't contain itself, or
>     else Russel comes and hits you with his paradox.
> 
> 
> But you anyway need to provide the list of CMRAs, right?  Then the list
> of CMRAs can also be interpreted as a CMRA, while it does not incur
> universe size problem.

Wait, wasn't the entire point of your proposal that no list of CMRAs
needs to be given?  You wrote "why don't you just product over all
possible bifunctor \Sigma?"
If by that you mean "all bifunctor \Sigma given in a list", then I don't
understand the question.  That's pretty much what we are doing, isn't it?

>  I would like to ask if we could do the same
> technique here: just define the logic with the product of all CMRAs
> (whose size is less than something), and let users to use only those
> CMRAs that are small enough.
> 
> I am quite sure my explanation is bad :-\  maybe it would be better for
> me to contribute to Iris in this respect (or learn why it is difficult
> to do that by actually doing some proofs in Coq).  I will return to this
> subject as soon as I am used to iris-coq.
> 
> 
> 
> On composability: what about "compositionality" as said in the
> parametric (bi)simulation works?

Kind regards,
Ralf