GitLab

So, only use the type class for contractive functors.

Add both non-expansive and contractive functors, and bundle them for the general Iris instance as well as the global functor construction

This allows us to move the \later in the user-defined functor to any place we want.
In particular, we can now have "\later (iProp -> iProp)" in the ghost CMRA.

Since functor instances are just used as combinators, there is really
no need for functors that are not contractive.

This cleans up some ad-hoc stuff and prepares for a generalization
of saved propositions.

This replaces f_equiv and solve_proper with our own, hopefully better, versions

* Use sig instead of sigT: the proof is a Prop after all
* Tweak implicit arguments
* Shorten proof of sigma

barrier: strive for consistency between barrierGF and the inGF assumptions; also change some instance names

And now the part that I forgot to commit.

Also, give all these global functors the suffix GF to avoid shadowing
such as we had with authF.

And add some type annotations for clarity.

I added a new typeclass "inGF" to witness that a particular *functor* is part of \Sigma. inG, in contrast, witnesses a particular *CMRA* to be in there, after applying the functor to "\later iProp".
inGF can be inferred if that functor is consed to the head of \Sigma, and it is preserved by consing a new functor to \Sigma. This is not the case for inG since the recursive occurence of \Sigma also changes.
For evry construction (auth, sts, saved_prop), there is an instance infering the respective authG, stsG, savedPropG from an inGF. There is also a global inG_inGF, but Coq is unable to use it.

I tried to instead have *only* inGF, since having both typeclasses seemed weird. However, then the actual type that e.g. "own" is about is the result of applying a functor, and Coq entirely fails to infer anything.

I had to add a few type annotations in heap.v, because Coq tried to use the "authG_inGF" instance before the A got fixed, and ended up looping and expanding endlessly on that proof of timelessness.
This does not seem entirely unreasonable, I was honestly surprised Coq was able to infer the types previously.

* These type classes bundle an identifier into the global CMRA with a proof
  that the identifier points to the correct CMRA. Bundling allows us to get
  rid of many arguments everywhere.

* I have setup the type classes so that we no longer have to keep track of the
  global CMRA identifiers. These are implicit and resolved automatically.

* For heap I am also bundling the name of the heap RA instance. There always
  should be at most one heap instance so this does not introduce ambiguities.

* We now have a "maps to" notation!