From 7791266ac7258d29d5a53abb74e831550f3134c6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 9 Nov 2020 16:55:23 +0100
Subject: [PATCH] fix wp_bind with empty context
---
tests/heap_lang.v | 5 +++++
theories/heap_lang/proofmode.v | 8 ++++----
2 files changed, 9 insertions(+), 4 deletions(-)
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 019a1c8af..de474eb48 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -138,6 +138,11 @@ 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_apply_evar e P :
P -∗ (∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index b5a5f78cc..48448b358 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -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.
--
GitLab