Skip to content

WIP: Avoid inG when possible

Ralf Jung requested to merge ralf/const-rf into master

This is a proposal for how we might be able to avoid using inG when just dealing with constant functors, which is the common case. The approach here is preferable because when defining your resources like

Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].

you have no way to accidentally write down a recursive functor, and when you then later use subG one_shotΣ Σ you are also not silently introducing any extra assumptions. (Cases of accidentally introduced assumptions include authG assuming something is a discrete CMRA, or savedAnythingG assuming something is a contractive functor.)

I ported just a few users to see if the approach is viable, and it seems it is. I added a closed proof for some code that actually uses resources, because it seems so far the only test case for that situation is in iris-examples. This also shows that the change is backwards-compatible, we don't have to port everything as once. To find places where we are still using the old pattern, just grep for inG. Before I go on porting more things, I'd like to get some feedback.

Fixes #227

Edited by Ralf Jung

Merge request reports