[Iris-Club] Change in weakest-pre

[Ralf Jung]

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
<https://gitlab.mpi-sws.org/FP/iris-coq/issues?assignee_id=&author_id=&label_name=&milestone_id=&scope=all&sort=created_desc&state=closed>.

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,
Ralf