Instead of writing a separate tactic lemma for each pure reduction,
there is a single tactic lemma for performing all of them.

The instances of PureExec can be shared between WP tactics and, e.g.
symbolic execution in the ghost  threadpool

That caused some problems, e.g.:

  From iris.base_logic Require Export fix.

Gave:

  Syntax error: [constr:global] expected after
  [export_token] (in [vernac:gallina_ext]).

Implementation is by Robbert <FP/iris-atomic!5 (comment 19496)>

Instead, I have introduced a type class `Monoid` that is used by the big operators:

    Class Monoid {M : ofeT} (o : M → M → M) := {
      monoid_unit : M;
      monoid_ne : NonExpansive2 o;
      monoid_assoc : Assoc (≡) o;
      monoid_comm : Comm (≡) o;
      monoid_left_id : LeftId (≡) monoid_unit o;
      monoid_right_id : RightId (≡) monoid_unit o;
    }.

Note that the operation is an argument because we want to have multiple monoids over
the same type (for example, on `uPred`s we have monoids for `∗`, `∧`, and `∨`). However,
we do bundle the unit because:

- If we would not, the unit would appear explicitly in an implicit argument of the
  big operators, which confuses rewrite. By bundling the unit in the `Monoid` class
  it is hidden, and hence rewrite won't even see it.
- The unit is unique.

We could in principle have big ops over setoids instead of OFEs. However, since we do
not have a canonical structure for bundled setoids, I did not go that way.

Also:

- Remove the wp_strip_later hack.
- Let wp_lam, wp_rec, wp_... initiate the proof mode.

Really, *all* of our files contain proof rules

Thanks to Robbert for fixing gen_heap

Use COFEs only for the recursive domain equation solver

This way we avoid the env_cbv tactic unfolding string related stuff
that appears in the goal and hypotheses of the proof mode.

And also rename the corresponding proof mode tactics.

rename program_logic.{ownership -> wsat}. It really is about world satisfaction and invariants more than about ownership.