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

[Ralf Jung]

Hi,

> Oops, yes, sorry, I should have proof-read my mail more carefully. Thank
> you for correcting this. Here are two quick proofs (which work when
> placed sufficiently late in the uPred_logic section in uPred.v):
> 
> Lemma rvs_nn P: (|=r=> P) ⊢ ((P -★ False) -★ False).
> Proof.
>   split. unseal. intros.
>   edestruct H0; eauto.
>   eapply (H3 n' x0); eauto.
>   - rewrite comm; naive_solver.
>   - naive_solver.
> Qed.

Ah, this makes sense. :)

So, we indeed get that

> Lemma rvs_ownM_update_nn x (Φ : M → Prop) :
>   x ~~>: Φ → uPred_ownM x |- (((∃ y, ■ Φ y ∧ uPred_ownM y) -* False) -* False).

That's funny. On the other hand, we don't get adequacy, so it seems that
double negation is strictly too weak as a notion for our updates.

Kind regards,
Ralf