From c650b0ee6be0290e16707b9d3d57d301a539190f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 20 Apr 2018 23:36:02 +0200
Subject: [PATCH] Fix issue #181: let `wp_expr_eval` check that the goal is in
fact a WP.
Also, remove the inconsistency that `wp_expr_eval` succeeds on a goal
that is not a WP.
---
theories/heap_lang/proofmode.v | 19 ++++++++++++-------
1 file changed, 12 insertions(+), 7 deletions(-)
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 6468daddc..d291d51c8 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -15,11 +15,16 @@ Lemma tac_twp_expr_eval `{heapG Σ} Δ s E Φ e e' :
Proof. by intros ->. Qed.
Tactic Notation "wp_expr_eval" tactic(t) :=
- try (
- iStartProof;
- first [eapply tac_wp_expr_eval|eapply tac_twp_expr_eval];
- [let x := fresh in intros x; t; unfold x; reflexivity
- |]).
+ iStartProof;
+ lazymatch goal with
+ | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+ eapply tac_wp_expr_eval;
+ [let x := fresh in intros x; t; unfold x; reflexivity|]
+ | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+ eapply tac_twp_expr_eval;
+ [let x := fresh in intros x; t; unfold x; reflexivity|]
+ | _ => fail "wp_expr_eval: not a 'wp'"
+ end.
Ltac wp_expr_simpl := wp_expr_eval simpl.
Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
@@ -293,13 +298,13 @@ Tactic Notation "wp_apply" open_constr(lem) :=
lazymatch goal with
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
reshape_expr e ltac:(fun K e' =>
- wp_bind_core K; iApplyHyp H; try iNext; wp_expr_simpl) ||
+ wp_bind_core K; iApplyHyp H; try iNext; try wp_expr_simpl) ||
lazymatch iTypeOf H with
| Some (_,?P) => fail "wp_apply: cannot apply" P
end
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
reshape_expr e ltac:(fun K e' =>
- twp_bind_core K; iApplyHyp H; wp_expr_simpl) ||
+ twp_bind_core K; iApplyHyp H; try wp_expr_simpl) ||
lazymatch iTypeOf H with
| Some (_,?P) => fail "wp_apply: cannot apply" P
end
--
GitLab