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

[Ralf Jung]

Hi,

> 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.

Right, this is the core of the new view shift (after stripping away the
invariants and the funny bit that lets us view shift away laters from
timeless stuff).

> 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.

Eh, is it?  I have to admit I don't find the proofs obvious, could you
spell out some details?  In any case, this is certainly not an
observation that occurred to me before.

It kind of makes sense though; |=r=> P means that you could own P any
time (by executing that view shift), so if you also had "P -* False",
you would have a contradiction.

> 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?

Well, most crucially, we need the following property

> Lemma rvs_ownM_updateP x (Φ : M → Prop) :
>   x ~~>: Φ → uPred_ownM x =r=> ∃ y, ■ Φ y ∧ uPred_ownM y.

and then also the following easier ones

> Lemma rvs_intro P : P =r=> P.
> Lemma rvs_mono P Q : (P ⊢ Q) → (|=r=> P) =r=> Q.
> Lemma rvs_trans P : (|=r=> |=r=> P) =r=> P.
> Lemma rvs_frame_r P R : (|=r=> P) ★ R =r=> P ★ R.
> Lemma now_True_rvs P : ◇ (|=r=> P) ⊢ (|=r=> ◇ P).

Anything satisfying those 6 laws will do, we shouldn't be using any
other property of rvs.

> This is purely idle curiosity.

It is a pretty interesting observation in any case.

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

"raw view shift"... don't remember the name, it's going to change.  We
agreed on calling it the "update modality" until we find a better name.

Kind regards,
Ralf