From cd509c3fbe9f019ad61f461e8e1f8a23516e0325 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 16 Feb 2016 10:31:55 +0100
Subject: [PATCH] Tweak use of wp_value in wp_tactics.
We only use wp_value in the end if the resulting goal is yet
another wp. Otherwise we may not be able to do a final view
shift (as observed by Ralf).
---
heap_lang/tests.v | 2 +-
heap_lang/wp_tactics.v | 7 +++++--
2 files changed, 6 insertions(+), 3 deletions(-)
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index d3c948d43..8d98a5ee0 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -67,7 +67,7 @@ Section LiftingTests.
wp_rec. wp_bin_op. wp_rec. wp_bin_op=> ?; wp_if.
- rewrite (forall_elim (n1 + 1)) const_equiv; last omega.
by rewrite left_id impl_elim_l.
- - assert (n1 = n2 - 1) as -> by omega; auto with I.
+ - wp_value. assert (n1 = n2 - 1) as -> by omega; auto with I.
Qed.
Lemma Pred_spec n E Q : ▷ Q (LitV (n - 1)) ⊑ wp E (Pred 'n)%L Q.
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 164bb9b48..1ec6d231a 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -16,7 +16,11 @@ Ltac wp_finish :=
match goal with
| |- ∀ _, _ => let H := fresh in intro H; go; revert H
| |- _ ⊑ ▷ _ => etransitivity; [|apply later_mono; go; reflexivity]
- | |- _ ⊑ wp _ _ _ => etransitivity; [|eapply wp_value; reflexivity]; simpl
+ | |- _ ⊑ wp _ _ _ =>
+ etransitivity; [|eapply wp_value; reflexivity];
+ (* sometimes, we will have to do a final view shift, so only apply
+ wp_value if we obtain a consecutive wp *)
+ match goal with |- _ ⊑ wp _ _ _ => simpl | _ => fail end
| _ => idtac
end in simpl; go.
@@ -55,7 +59,6 @@ Tactic Notation "wp_un_op" ">" :=
end.
Tactic Notation "wp_un_op" := wp_un_op>; wp_strip_later.
Tactic Notation "wp_if" ">" :=
- try wp_value;
match goal with
| |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval cbv in e' with
--
GitLab