[Iris-Club] Frame-preserving update and double-negation
mail at robbertkrebbers.nl
Wed Aug 24 12:21:11 CEST 2016
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