Common tactic machinery for symbolic execution of pure reductions

The goal of this merge request is to unify some machinery used for performing pure symbolic reductions in a way that would allow for better code reuse between WP and e.g. sequential WP or WP for total program correctness.

Overview

The way that symbolic execution for the WP-calculus (for heap_lang) is implemented right now is basically as follows. For each possible reduction in the language there is a Coq tactic lemma (that can be iApplied) and a corresponding Ltac code that

• Tries to find the place where this lemma can be applied
• Applies the lemma
• Gets rid of some clutter (e.g. reduces #();; e to e).

If one wants to implement tactics for symbolic execution for WP for total program correctness or for if-convergence, then essentially all this effort has to be duplicated.

These sort of issues arose in the formalisation of logical relations that we were working on with @robbertkrebbers. There we had several layers of tactics for symbolic execution: in the weakest precondition, in the ghost threadpool, and on both sides of the logical relation. After having troubles maintaining 4*n tactics and tactic lemmas we decided to abstract it away as follows.

Implementation and advantages

For each "layer" of symbolic execution you have an "open ended" tactic/lemma that is parameterized over a typeclass:

Lemma wp_pure' `{Inhabited state} K E e1 e2 φ Φ :
  PureExec φ e1 e2 →
  φ →
  (▷ WP fill K e2 @ E {{ Φ }}) ⊢ WP fill K e1 @ E {{ Φ }}.

The typeclass PureExec φ e1 e2 says that there is a pure (and deterministic) reduction from e1 to e2 in the language under some (pure) assumption φ.

The instances for the PureExec typeclass are declared separately and can be reused for symbolic execution lemmas for constructs other than WP.

Then, there is a single Ltac tactic wp_pure for applying the said lemma. All the other tactics for pure reductions are defined in terms of it (see proofmode.v for examples).

Another advantage of having a single tactic is that you can use it to perform as much pure reductions as possible, as in this example (tests/heap_lang.v):

  Definition heap_e3 : expr :=
    let: "x" := #true in
    let: "f" := λ: "z", "z" + #1 in
    if: "x" then "f" #0 else "f" #1.

  Lemma heap_e3_spec E : WP heap_e3 @ E {{ v, ⌜v = #1⌝ }}%I.
  Proof.
    iIntros "". rewrite /heap_e3.
    by repeat (wp_pure _).
  Qed.

Issues

1. Should the pure premises for PureExec be split into those that should be solve automatically and those that should be solved manually?
2. wp_binop/wp_op does not behave as it used to be. Previously the wp_op tactic for the BinOp Eq case was specialized in such a way that it would generate two different goals. E.g. proving WP #a = #b {{ Φ }} could be reduced to proving #a = #b → Φ #true and #a ≠ #b → Φ #true. Right now, wp_op reduces the goal to Φ #(bool_decide (#a = #b)). Not sure if that's an important issue.