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

[Robbert Krebbers]

Hi Joe,

Fun observation! I think Ralf answered most of your questions, but let 
me remark that another property will break when using your definition, 
namely adequacy (which is crucial to prove adequacy of weakest pre):

   Lemma adequacy φ n : (True ⊢ Nat.iter n (λ P, |=r=> ▷ P) (■ φ)) → φ.

It is not to difficult to prove that the following is vacuously true:

   (▷ P -★ False) -★ False

This means that the above adequacy statement is not going to hold for 
any n apart from 0.

Best,

Robbert

----------

Goal ∀ P : uPred M, True ⊢ (▷ P -★ False) -★ False.
Proof.
   unseal=> P; split=> n x /= ? _ n' x' ?? H.
   eapply (H 0 x); auto. rewrite comm. eauto using cmra_validN_le.
Qed.