Make invariants and slices closed under equivalence
This has come up several times before. I think @jjourdan has proposed this previously and I have argued against it, but by now I feel like it may be worth a try. We could slightly change the definition of invariants so that the following holds:
Lemma inv_iff P Q : later persistently (P <-> Q) -> inv P -> inv Q.
I think this may be worth it, if it means we can simplify the definition of the lifetime logic a little bit. However, that will only be the case if we manage to also get this law for
slice, which requires either a separate closure in
slice (so the one in
inv does not help), or doing the same kind of closure in
saved_prop_own (but then, do we also want the equivalent law for
Also, I am not sure if we should do this before or after Iris 3.1. Either way, it is backwards-compatible.