[Iris-Club] Change in weakest-pre

Ralf Jung jung at mpi-sws.org
Sat Nov 7 18:39:27 CET 2015

Hi all,

Janno and Dave reminded me the other day, that I recently made one
change to weakest-pre that is not documented as a closed issue

While I introduced the user-defined fork, I also changed the value case
of weakest-pre to no longer do anything interesting. It is now just

  is_value e -> n > 1 -> \phi e w n

Notice that weakest-pre is still trivially true at step index 1 (and 0),
which is important for the atomic rule of consequence and the new
lifting lemmas <https://gitlab.mpi-sws.org/FP/iris-coq/issues/5>.

The advantage of this change is that we don't need a post-rule of
consequence for weakest-pre anymore: We now define Hoare triples as

  {P} e {Q} := \box(P => wp(e, vs(Q)))

and the post-part of the rule of consequence follows by view shift
transitivity. It also means all of the weakest-pre proofs need to do
less, because the value case got much simpler. Generally, this removes
redundancy we used to have in the definitions, where weakest-pre of a
value, and a view shift, were pretty much the same thing.

Kind regards,

More information about the Iris-Club mailing list