[Iris-Club] Frame-preserving update and double-negation

[Joseph Tassarotti]

Hello,

Inspired by the recent discussion about classical separation logic, I 
was wondering about the following. In Iris 3.0, there is a new modality 
called "rvs", written "|=r=>", where |=r=> P n x holds if we can do a 
frame-preserving update which changes x into a resource that satisfies P.

It is not hard to show that (P -* False) -* False implies |=r=> P. In 
addition, if (a) P is timeless, (b) the underlying CMRA is discrete, and 
(c) your meta-logic is classical, you can show that |=r=> P entails (P 
-* False) -* False.

So, now I have two questions:

(a) Does anyone know of a way to characterize |=r=> P as (P -* Q) -* Q 
for some (simple) Q in the more general case where P is not timeless and 
the CMRA is not discrete? Ideally, Q should be definable using the other 
primitive connectives.

(b) Would anything break if we replaced all uses of |=r=> P with (P -* 
False) -* False in the Iris 3.0 model?

This is purely idle curiosity.

-Joe

P.S. What is "rvs" supposed to stand for?