From 88dcbd11a10bd65726742df86f3466bea4242515 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
Date: Tue, 9 Aug 2022 02:45:04 +0000
Subject: [PATCH] final tweaks

---
 iris_heap_lang/primitive_laws.v | 12 ------------
 iris_heap_lang/proofmode.v      | 14 +++++++-------
 tests/heap_lang.ref             |  2 +-
 3 files changed, 8 insertions(+), 20 deletions(-)

diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index d3b167168..91fd17a56 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -170,18 +170,6 @@ Proof.
   iIntros "_". iPureIntro. rewrite /num_laters_per_step /=. lia.
 Qed.
 
-(** This just re-exports the lifting lemma when one wants to generate a single
-credit during a pure step. *)
-Lemma wp_pure_step_credit s E e1 e2 ϕ Φ :
-  PureExec ϕ 1 e1 e2 →
-  ϕ →
-  ▷ (£ 1 -∗ WP e2 @ s; E {{ Φ }}) -∗
-  WP e1 @ s; E {{ Φ }}.
-Proof.
-  iIntros (Hexec Hphi) "Hwp".
-  iApply wp_pure_step_later; done.
-Qed.
-
 (** Recursive functions: we do not use this lemmas as it is easier to use Löb
 induction directly, but this demonstrates that we can state the expected
 reasoning principle for recursive functions, without any visible â–·. *)
diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index f53dd4490..6a8fd1de7 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -57,16 +57,16 @@ Lemma tac_wp_pure_credit `{!heapGS_gen hlc Σ} Δ Δ' s E j K e1 e2 ϕ Φ :
   PureExec ϕ 1 e1 e2 →
   ϕ →
   MaybeIntoLaterNEnvs 1 Δ Δ' →
-  (match envs_app false (Esnoc Enil j (£ 1)) Δ' with
-    | Some Δ'' =>
-       envs_entails Δ'' (WP fill K e2 @ s; E {{ Φ }})
-    | None => False
-    end) →
+  match envs_app false (Esnoc Enil j (£ 1)) Δ' with
+  | Some Δ'' =>
+     envs_entails Δ'' (WP fill K e2 @ s; E {{ Φ }})
+  | None => False
+  end →
   envs_entails Δ (WP (fill K e1) @ s; E {{ Φ }}).
 Proof.
   rewrite envs_entails_unseal=> ??? HΔ.
   pose proof @pure_exec_fill.
-  rewrite -wp_pure_step_credit; last done.
+  rewrite -lifting.wp_pure_step_later; last done.
   rewrite into_laterN_env_sound /=. apply later_mono.
   destruct (envs_app _ _ _) as [Δ''|] eqn:HΔ'; [ | contradiction ].
   rewrite envs_app_sound //; simpl.
@@ -161,7 +161,7 @@ Tactic Notation "wp_pure" open_constr(efoc) "credit:" constr(H) :=
   let Htmp := iFresh in
   let finish _ :=
     pm_reduce;
-    (iDestructHyp Htmp as H || fail 2 "wp_pure: " H " is not fresh");
+    (iDestructHyp Htmp as H || fail 2 "wp_pure:" H "is not fresh");
     wp_finish
     in
   lazymatch goal with
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 3835c2cbe..f85b167b4 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -193,7 +193,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 "test_wp_pure_credit_fail"
      : string
 The command has indeed failed with message:
-Tactic failure: wp_pure:  "Hcred"  is not fresh.
+Tactic failure: wp_pure: "Hcred" is not fresh.
 1 goal
   
   Σ : gFunctors
-- 
GitLab