Porting iProp to typeclasses

Stream: iris-lean

[Markus de Medeiros]

@Mario Carneiro I'm getting kind of stuck on some Lean details for porting iProp and I'm wondering if you might have any ideas on how to proceed.

Basically, iProp in Rocq does equational reasoning about a global list of RFunctors, using a typeclass to specify that the ith entry in the list gives a specific CMRA when applied to the fixpoint iProp. This is straightforward to specify in Rocq since they are using bundled structures. Remy tried porting it the same way (bundling RFunctor instances in the list of GFunctors), but this leads to a bunch of CMRA transports I was not sure how to deal with.

The central issue is that if we need to be able to relate lemmas about a particular CMRA, say ConstOF Unit (IProp FF) (IProp FF), to the iProp constructions where the typeclass instances come from an IsGFunctors instance. I tried another approach here where I used a typeclass to specify what the ith entry in the list of OFunctorPre's is, though this also leads to CMRA's not being defeq that I would expect to be so.

Do you have any ideas about the right way to mechanize this? I can't think of a good way which allows us to describe the global list of OFunctors using equations.

[Mario Carneiro]

I've been wanting to refactor the RFunctors thing to avoid needing an explicit finite list of functors and instead do something more abstract like a type (which will ultimately be instantiated as a finite product of CMRAs) from which individual CMRAs can be projected, with each projection being its own typeclass (or maybe one typeclass parameterized by the CMRA to project out). This should eliminate the equational reasoning

[Mario Carneiro]

I'm looking at the file now and I am not sure how much of this is your work vs what is in iris

[Mario Carneiro]

I assume you want to fix the sorries in that file?

[Markus de Medeiros]

My file is mostly my work. Remy's fork is closer to Iris (bundled structures, etc)

[Markus de Medeiros]

The sorry's are one thing but I think the problem I'm describing is exemplified by the example on line 55 (the rfl fails)

[Markus de Medeiros]

I'm not sure I understand how your idea allows us to have impredicative resources, the construction is not abstract specifically for that purpose?

[Mario Carneiro]

I might be missing a design constraint, can you explain more about that?

[Markus de Medeiros]

Like, the Iris construction uses RFunctors for UPred and gmap so that the fixpoint is a UPred resource, whose UCMRA is a map, and where each projection of this map is a particular RFunctor applied to the fixpoint. Solving the fixpoint and is integrated with how the map of resources are represented.

[Mario Carneiro]

Markus de Medeiros said:

The sorry's are one thing but I think the problem I'm describing is exemplified by the example on line 55 (the rfl fails)

I thought a bit about this, and I think it's expected behavior. GFunctors is essentially a map keyed by type, which means when you have a type which is not unique or in this case overlaps a general purpose type then you get overlapping instances. These aren't even equal, not just not defeq

[Markus de Medeiros]

Agreed

[Mario Carneiro]

The solution is to ensure that any functor you use in a GFunctors is specifically intended for use in one

[Mario Carneiro]

i.e. don't put ConstOF Unit in a GFunctors directly, put MyFunctor (ConstOF Unit) instead

[Mario Carneiro]

Markus de Medeiros said:

Like, the Iris construction uses RFunctors for UPred and gmap so that the fixpoint is a UPred resource, whose UCMRA is a map, and where each projection of this map is a particular RFunctor applied to the fixpoint. Solving the fixpoint and is integrated with how the map of resources are represented.

This is fine I think, the ultimate implementation can still be a finite list of functors as before. You just abstract that in the API so that this is only visible in the construction and at the end when you "tie the knot" to prove that there exists some GFunctors which contains four specific functors corresponding to various modalities you wanted to use in your heaplang etc

[Mario Carneiro]

and we can provide a macro to do the latter part

[Mario Carneiro]

For the in between stuff we just have a typeclass saying that you can somehow extract a MyFunctor from FF which is used in the myModality theory file

[Markus de Medeiros]

What is MyFunctor supposed to mean?

[Mario Carneiro]

That's ultimately FF 2 : MyFunctor extracted from FF : GFunctors

[Mario Carneiro]

but we hide all the details about the fact that we are applying a function or what index it is

[Mario Carneiro]

I believe MyFunctor is the F in ElemG FF τ F in your code

[Mario Carneiro]

instantiated in the particular case for some specific F

[Markus de Medeiros]

Mario Carneiro said:

i.e. don't put ConstOF Unit in a GFunctors directly, put MyFunctor (ConstOF Unit) instead

I'm not sure how to reconcile that with this

[Mario Carneiro]

Let's say you want to have a GFunctors containing functors MyF1, MyF2, MyF3 which each give you some kind of capability. There will be a file talking about MyF1 and the operations associated with having one; this will have a typeclass assumption [ElemG FF MyF1] (I don't think it is necessary to expose the τ parameter in the typeclass). Most of the work will therefore have assumptions [ElemG FF MyF1] [ElemG FF MyF2] [ElemG FF MyF3], and then there is a macro which constructs some MyFF definition with instances ElemG MyFF MyF1, ElemG MyFF MyF2, ElemG MyFF MyF3

[Mario Carneiro]

you would never write [ElemG FF (ConstOF Unit)] because this would cause a diamond problem with the pre-existing ConstOF Unit instance

[Markus de Medeiros]

How do we specify that we have access to ConstOF Unit resources in this system?

[Mario Carneiro]

maybe I misunderstood, but I think the Inst1 instance says that ConstOF Unit resources exist in every system?

[Mario Carneiro]

aha, I did misunderstand

[Mario Carneiro]

instCMRAElemG is a bad instance, you should always have an alternative route to prove that

[Markus de Medeiros]

I agree that it is a problematic instance I just don't really see a way around it...

[Mario Carneiro]

Why are GFunctors and IsGFunctors separate?

[Mario Carneiro]

the name is not great

[Mario Carneiro]

because it's not obvious what it means to assert that a GFunctors IsGFunctors, it sounds like it should always be the case

[Markus de Medeiros]

Definitely agreed

[Mario Carneiro]

moreover it seems IsGFunctors is additional dependent data

[Markus de Medeiros]

Right. So should we use bundled structures for this then?

[Mario Carneiro]

I guess it's the actual instance and stuff, more than just the type

[Mario Carneiro]

yeah, I think it would make sense to bundle GFunctors

[Mario Carneiro]

we don't want to use its projections directly as discussed anyway

[Mario Carneiro]

we instead want to use separate variables which already have instances of their own (like F := ConstOF Unit), with a typeclass saying that they can be extracted from FF

[Mario Carneiro]

which is where we hide the equality assumption

[Mario Carneiro]

OH I get it now, ElemG is taking a lawless GFunctors so it's actually wrong

[Mario Carneiro]

it should take both the GFunctors and IsGFunctors because it needs to assert that the cmra part is also equal to the pre-existing cmra on F

[Mario Carneiro]

(or alternatively bundle everything)

[Markus de Medeiros]

Yeah, right. This is the tricky part though. I tried adding a CMRA equality constraint to the ElemG typeclass at one point and having to rewrite by equations for both the CMRA and the type on that CMRA was difficult. I also couldn't figure out how to relate lemmas about the base CMRA (for example, validN unit) to the versions specified by ElemG.

I will revisit the bundling idea then.

[Mario Carneiro]

bundling will definitely make it easier to write that equality

[Markus de Medeiros]

OK. To give concrete code, Remy was working on that here.

[Mario Carneiro]

Markus de Medeiros said:

I also couldn't figure out how to relate lemmas about the base CMRA (for example, validN unit) to the versions specified by ElemG.

You shouldn't need to do this, you should only ever be using the CMRA structure coming from F and not the one you can obtain by transport out of GF i

[Markus de Medeiros]

But the lemmas in the algebra library are (rightly) are written in terms of the regular CMRA's

[Mario Carneiro]

exactly, that's why you use F which is a regular CMRA

[Mario Carneiro]

we might need a bit of automation to make it easy to declare newtype CMRAs

[Mario Carneiro]

if all of the GFunctor types are different (and I don't see why you would want to have the same type twice since the GMap already lets you make as many instances of a given type as you want) then it should be fine even to not use newtypes and just use the types you actually want

[Markus de Medeiros]

I think I'm starting to get on the same page as you, though at some level the own primitive will need to be written in terms of the projected-out CMRA GF i

[Mario Carneiro]

if you have some relevant half written code I can try to be more concrete

[Mario Carneiro]

I don't like this argument v : FF τ (IProp FF) (IProp FF)

[Mario Carneiro]

it's exposing FF τ

[Mario Carneiro]

I think it should look like

def iOwn {GF F} [OFunctor F] [ElemG GF F] (γ : GName) (v : F.ap (IProp GF)) : IProp GF

[Markus de Medeiros]

I get it now (though here we would also need a [IsGFunctors GF] instance, or to be bundled, but I believe that either of those are possible).

[Mario Carneiro]

using this definition of ElemG

def BundledGFunctors := GType → Σ F : COFE.OFunctorPre, OFunctor F

class ElemG (FF : BundledGFunctors) (F : OFunctorPre) [OFunctor F] where
  τ : GType
  transp : FF τ = ⟨F, ‹_›⟩

[Markus de Medeiros]

Yes. So then under the hood iOwn will be the singleton map where the γth entry of theτth entry of the ghost map is the transported version of v.

[Mario Carneiro]

(you might need F explicit in iOwn, not sure if that will always be inferred correctly)

[Mario Carneiro]

yeah, I'm not sure which side of the ElemG abstraction results in shorter code for iSingleton

[Mario Carneiro]

but I think the approach you are taking there basically makes sense

[Mario Carneiro]

at some point you obviously do need to do something with that equality argument

[Mario Carneiro]

there is already a cast in iSingleton so maybe it would be better to have the cmra cast there too

[Markus de Medeiros]

Yeah okay, this makes sense to me. Thanks for hashing it out!

[Markus de Medeiros]

One last thing, do you have any tricks for working with cast? It is difficult to work with, my best attempts have relied on using the subst tactic basically whenever I could though this is a little inelegant.

[Mario Carneiro]

that's the universal technique for this

[Mario Carneiro]

make sure one side of your equality is a variable, then subst it until the equality is refl and the casts will go away. This is how you prove anything about a cast

[Mario Carneiro]

if you are very lucky you might have some other kind of compositional abstraction which can push casts around like eqToHom. I don't think we are lucky in this case

[Markus de Medeiros]

Understood, thanks!

[Markus de Medeiros]

I still have quite a few sorry's to work through on my branch but now I think we are getting close to something that looks a lot like iProp :)

Screenshot 2025-10-10 at 3.54.40 PM.png