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 saved_pred_own
?).
Also, I am not sure if we should do this before or after Iris 3.1. Either way, it is backwards-compatible.