OFunctor definition

Stream: iris-lean

[Markus de Medeiros]

@Mario Carneiro I'm making some progress towards finishing iProp, but I'm a little stuck on one part and wondering what you think. Your definition of OFunctor is a typeclass on top of functions (Type _ -> Type _ -> Type _) rather than the bundled Iris version (COFE -> COFE -> OFE). I'm not sure how to write an OFunctor in the case that the result type is only defined when the input types are COFE's.

The particular difficulty here comes when defining uPred, which in Rocq is parameterized by a UCMRA. If I define a bundled version of uPred (like how it is in my branch right now), then the OFunctor is only defined when the input types are COFE's. On the other hand, when I define an unbundled version (ie. moving the uPred_mono field to a separate typeclass so I can remove the UCMRA requirement from uPred) the type is no longer complete, and I cannot prove that uPred is a COFE.

Have you (or anyone) seen an issue like this before? I couldn't figure this issue out when I was working in Eileen either. The code at the bottom of my branch illustrates the issue concretely.

[Mario Carneiro]

hm, I was rather hoping that such functions would not come up

[Markus de Medeiros]

Yeah. FWIW the unbundled version seems to work fine with the other oFunctors I've tried (though I'm not finished with those yet either).

[Mario Carneiro]

I pushed a fix, allowing the functor to depend on OFE structure

[Mario Carneiro]

I can add COFE structure too if needed, but I prefer to keep it as loose as reasonably possible

[Markus de Medeiros]

Nice! Thanks for doing that, I'm a little surprised it was fixable!!

I believe that dependence on COFE is necessary. The reason why is because the uPred OFunctor looks like

def uPredOF F [URFunctor F] (A : Type _) (B : Type _) : Type _ :=
  @uPred (F B A) (@URFunctor.cmra F _ B A sorry sorry)

so we need F B A to be a UCMRA. We get that from the URFunctor field

class URFunctor (F : Type _ → Type _ → Type _) where
  cmra [COFE α] [COFE β] : UCMRA (F α β)
   -- ...

which requires the arguments to be COFEs.

[Mario Carneiro]

why is that there though?

[Markus de Medeiros]

Are you asking why URFunctors require COFEs rather than OFE's?

[Mario Carneiro]

yes

[Markus de Medeiros]

Every URFunctor is an OFunctor which has the same restriction. I do not know why OFunctors have this requirement off the top of my head.

[Mario Carneiro]

indeed, one can just replace COFE by OFE everywhere in OFunctor and it still works

[Mario Carneiro]

I suspect we just don't have enough examples to see the rationale

[Mario Carneiro]

maybe we should just downgrade everything to OFE now and that way we'll notice when something gets stuck later

[Mario Carneiro]

intuitively, COFE "shouldn't" matter since it's just a proposition and not data

[Markus de Medeiros]

I agree that we should try with just OFE. If you're confident that it's easy to change after the fact then yeah, we might as well do some destructive testing on Iris (lol)

[Mario Carneiro]

yeah, upgrading/downgrading these typeclasses has very little impact on most proofs

[Mario Carneiro]

Mario Carneiro said:

intuitively, COFE "shouldn't" matter since it's just a proposition and not data

oh wait, that's a lie. COFE's have a compl field which is data (although I suspect it won't be computable in most cases)

[Markus de Medeiros]

A relevant snippet from Iris From the Ground Up: Screenshot 2025-04-05 at 5.02.57 PM.png

[Mario Carneiro]

sounds like it is the right idea to start with OFEs and upgrade as needed then