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

[Ralf Jung]

Hi,

> 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) (■ φ)) → φ.

Yeah, I remembered adequacy as we were walking up to Mensa, and that
would definitely at least need excluded middle.

> It is not to difficult to prove that the following is vacuously true:
> 
>   (▷ P -★ False) -★ False

Wait, what?^^
Oh, you went into the model for this proof.  Yeah, this makes sense.

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

I suggest we add this to the derived rules about \later ? (Not doing it
myself in order to avoid merge conflicts with your rename branch.)

Kind regards,
Ralf