Skip to content

Step fupd commutes with for all for plain predicates in Iris.

Joseph Tassarotti requested to merge joe/fupd_extra into master

@robbertkrebbers needed a result showing that forall commutes with step taking fancy updates when the predicate under the modality is plain in order to adapt total_weakestpre.v to the style of !171 (merged). It holds for how Iris defines fancy updates, as this commit shows, but I don't know how to prove it from the interface axioms. Robbert proposed possibly adding this to the interface. A similar result also holds for |==> and |={E}=>, I believe, but I'm not sure they can be deduced from the respective interfaces either.

This is relevant to #164 (closed). I don't think the axiom proposed by @amintimany there would let you deduce this, either.

Edited by Joseph Tassarotti

Merge request reports