From 228f3a2edc7d57dfe641a2095413ed29e0fbf8d0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 29 Nov 2017 16:45:10 +0100
Subject: [PATCH] =?UTF-8?q?A=20tactic=20`wp=5Fsimpl=5Fsubst`=20that=20only?=
 =?UTF-8?q?=20simplifies=20in=20the=20`e`=20of=20`WP=20e=20@=20E=20{{=20?=
 =?UTF-8?q?=CE=A6=20}}`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/heap_lang/proofmode.v | 14 +++++++++++++-
 theories/tests/tree_sum.v      |  2 +-
 2 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index cfdd88652..26ddb58af 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -12,6 +12,18 @@ Ltac wp_simpl :=
       let e' := eval simpl in e in change (envs_entails Δ (wp E e' Q))
   end.
 
+Lemma tac_wp_simpl_subst `{heapG Σ} Δ E Φ e e' :
+  e = e' →
+  envs_entails Δ (WP e' @ E {{ Φ }}) → envs_entails Δ (WP e @ E {{ Φ }}).
+Proof. by intros ->. Qed.
+
+Ltac wp_simpl_subst :=
+  try iStartProof;
+  try lazymatch goal with
+  | |- envs_entails ?Δ (wp ?E ?e ?Q) =>
+      eapply tac_wp_simpl_subst; [simpl_subst; reflexivity|]
+  end.
+
 Lemma tac_wp_pure `{heapG Σ} Δ Δ' E e1 e2 φ Φ :
   PureExec φ e1 e2 →
   φ →
@@ -41,7 +53,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
       [apply _                        (* PureExec *)
       |try fast_done                  (* The pure condition for PureExec *)
       |apply _                        (* IntoLaters *)
-      |simpl_subst; try wp_value_head (* new goal *)
+      |wp_simpl_subst; try wp_value_head (* new goal *)
       ])
    || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
   | _ => fail "wp_pure: not a 'wp'"
diff --git a/theories/tests/tree_sum.v b/theories/tests/tree_sum.v
index 28f75f6c8..01441c800 100644
--- a/theories/tests/tree_sum.v
+++ b/theories/tests/tree_sum.v
@@ -40,7 +40,7 @@ Lemma sum_loop_wp `{!heapG Σ} v t l (n : Z) :
   {{{ RET #(); l ↦ #(sum t + n) ∗ is_tree v t }}}.
 Proof.
   iIntros (Φ) "[Hl Ht] HΦ".
-  iInduction t as [n'|tl ? tr] "IH" forall (v l n Φ); wp_rec; wp_let.
+  iInduction t as [n'|tl ? tr] "IH" forall (v l n Φ); simpl; wp_rec; wp_let.
   - iDestruct "Ht" as "%"; subst.
     wp_match. wp_load. wp_op. wp_store.
     by iApply ("HΦ" with "[$Hl]").
-- 
GitLab