[Iris-Club] Several small questions on Iris
Robbert Krebbers
mail at robbertkrebbers.nl
Thu Feb 16 10:44:42 CET 2017
On 02/16/2017 10:25 AM, Ralf Jung wrote:
> We currently do not have CMRAs of different sizes; doing so would
> require using Coq's universe polymorphism to have a CMRA structure for
> every universe that can contain CMRAs of lower universes. I guess if we
> did that we could parameterize all our proofs by the universe level that
> is used for the "big product", making all lower universes available for
> the user-supplied CMRAs. Combining different proofs would use the
> maximum universe.
> That could work, but (a) it's very different from what you suggested
> [so it doesn't help me understand your question], and (b) messing with
> Coq's universe polymorphism like that sounds very daring and asking for
> trouble. ;)
c.) What we "actually" want is to have a big product over all ofe ->
cmra functors, i.e. instantiate Iris with the functor:
F : ofeT -contractive-> cmraT
F(X) := nat -fin-> { G : ofeT -contractive-> cmraT & G X }
And solve:
iProp ~ uPred (F (▷ iProp))
However, even mathematically speaking (ignoring how to model this using
universe polymorphism in Coq) this does not make sense: iProp itself
will be big, hence the cmra in the range of G in the Sigma-type will be
big, hence F will be bigger, hence universe inconsistency.
More information about the Iris-Club
mailing list