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

Robbert Krebbers mail at robbertkrebbers.nl
Wed Aug 24 12:21:11 CEST 2016

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.




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

More information about the Iris-Club mailing list