Merge branch 'ralf/wp-bind-empty' into 'master'

fix wp_bind with empty context

See merge request !579

CHANGELOG.md

@@ -138,6 +138,8 @@ With this release, we dropped support for Coq 8.9.
 **Changes in `heap_lang`:**
 
 * `wp_pures` now turns goals of the form `WP v {{ Φ }}` into `Φ v`.
+* Fix `wp_bind` in case of a NOP (i.e., when the given expression pattern is
+  already at the top level).
 
 The following `sed` script helps adjust your code to the renaming (on macOS,
 replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).

tests/heap_lang.v

@@ -138,6 +138,14 @@ Section tests.
     by replace (S n - 1)%Z with (n:Z) by lia.
   Qed.
 
+  (* Make sure [wp_bind] works even when it changes nothing. *)
+  Lemma wp_bind_nop (e : expr) :
+    ⊢ WP e + #0 {{ _, True }}.
+  Proof. wp_bind (e + #0)%E. Abort.
+  Lemma wp_bind_nop (e : expr) :
+    ⊢ WP e + #0 [{ _, True }].
+  Proof. wp_bind (e + #0)%E. Abort.
+
   Lemma wp_apply_evar e P :
     P -∗ (∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
   Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.

theories/heap_lang/proofmode.v

@@ -56,7 +56,7 @@ Proof. rewrite envs_entails_eq=> ->. by apply twp_value. Qed.
 Ltac wp_expr_simpl := wp_expr_eval simpl.
 
 Ltac wp_value_head :=
-  first [eapply tac_wp_value || eapply tac_twp_value].
+  first [eapply tac_wp_value | eapply tac_twp_value].
 
 Ltac wp_finish :=
   wp_expr_simpl;      (* simplify occurences of subst/fill *)
@@ -167,11 +167,11 @@ Tactic Notation "wp_bind" open_constr(efoc) :=
   iStartProof;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
-    reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
-    || fail "wp_bind: cannot find" efoc "in" e
+    first [ reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
+          | fail "wp_bind: cannot find" efoc "in" e ]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
-    reshape_expr e ltac:(fun K e' => unify e' efoc; twp_bind_core K)
-    || fail "wp_bind: cannot find" efoc "in" e
+    first [ reshape_expr e ltac:(fun K e' => unify e' efoc; twp_bind_core K)
+          | fail "wp_bind: cannot find" efoc "in" e ]
   | _ => fail "wp_bind: not a 'wp'"
   end.