wp_finish: avoid making a goal unprovable

One common problem for Iris newcomers is accidentally making their goal unprovable by "losing the fupd" in a WP proof. The underlying reason for this is that wp_finish, which is implicitly run after each wp_ tactic, applies a lemma that is not an equivalence, but a strengthening of the goal. I think we should avoid doing this, both as a matter of principle (such implicit tactics one cannot opt out of should only apply equivalences, never make the goal harder to prove) and to make Iris a bit easier to learn.

So this adjusts wp_finish to instead apply a lemma that holds in both directions when the expression turned into a value. To avoid adding too many update modalities, we special-case the situation where the postcondition is a WP or fupd with the right mask -- in that case, |={E}=> Φ is equivalent to Φ so no fupd needs to be added to ensure that the goal remains provable. Matching this, I also made wp_value_fupd a bidirectional lemma and got rid of wp_value_inv.

This requires adjusting some proofs where the extra modality got in the way. However, many proofs just don't care (IPM is pretty good at "looking through" that modality), and more importantly, these issues will not be a problem for new users: they can use iIntros "!>" or iModIntro, tactics they will learn anyway, to solve them. This is in contrast to now where new users will have a hard time figuring out that they need to go back to some earlier place in the proof and add rewrite -wp_fupd. So while there are probably fewer proofs that need the final fupd than ones that do not, having "too many fupds" is also much easier to solve than having too few of them, which is why I think we should err on the side of having too many.

Changelog entry for program_logic:

* Merge `wp_value_inv`/`wp_value_inv'` into `wp_value_fupd`/`wp_value_fupd'` by making the lemma bidirectional.

And for heap_lang:

* The `wp_` tactics now preserve the possibility of doing a fancy update when the expression reduces to a value.