From f9d6ada17b1e550362e0dfb09bd9500bfae4ca69 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Mon, 15 Jun 2020 16:46:52 -0500
Subject: [PATCH] Use [fill K] in tac_wp_pure

This is more consistent with other tac_wp tactics for HeapLang and also
a tiny bit more efficient, which is good to embody in the basic tactics
so derived code follows the same patterns.
---
 theories/heap_lang/proofmode.v | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 739d78cea..f1a12ed12 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -27,21 +27,21 @@ Tactic Notation "wp_expr_eval" tactic3(t) :=
   | _ => fail "wp_expr_eval: not a 'wp'"
   end.
 
-Lemma tac_wp_pure `{!heapG Σ} Δ Δ' s E e1 e2 φ n Φ :
+Lemma tac_wp_pure `{!heapG Σ} Δ Δ' s E K e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
   φ →
   MaybeIntoLaterNEnvs n Δ Δ' →
-  envs_entails Δ' (WP e2 @ s; E {{ Φ }}) →
-  envs_entails Δ (WP e1 @ s; E {{ Φ }}).
+  envs_entails Δ' (WP (fill K e2) @ s; E {{ Φ }}) →
+  envs_entails Δ (WP (fill K e1) @ s; E {{ Φ }}).
 Proof.
   rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
   rewrite HΔ' -lifting.wp_pure_step_later //.
 Qed.
-Lemma tac_twp_pure `{!heapG Σ} Δ s E e1 e2 φ n Φ :
+Lemma tac_twp_pure `{!heapG Σ} Δ s E K e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
   φ →
-  envs_entails Δ (WP e2 @ s; E [{ Φ }]) →
-  envs_entails Δ (WP e1 @ s; E [{ Φ }]).
+  envs_entails Δ (WP (fill K e2) @ s; E [{ Φ }]) →
+  envs_entails Δ (WP (fill K e1) @ s; E [{ Φ }]).
 Proof.
   rewrite envs_entails_eq=> ?? ->. rewrite -total_lifting.twp_pure_step //.
 Qed.
@@ -84,7 +84,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
     let e := eval simpl in e in
     reshape_expr e ltac:(fun K e' =>
       unify e' efoc;
-      eapply (tac_wp_pure _ _ _ _ (fill K e'));
+      eapply (tac_wp_pure _ _ _ _ K e');
       [iSolveTC                       (* PureExec *)
       |try solve_vals_compare_safe    (* The pure condition for PureExec -- handles trivial goals, including [vals_compare_safe] *)
       |iSolveTC                       (* IntoLaters *)
@@ -95,7 +95,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
     let e := eval simpl in e in
     reshape_expr e ltac:(fun K e' =>
       unify e' efoc;
-      eapply (tac_twp_pure _ _ _ (fill K e'));
+      eapply (tac_twp_pure _ _ _ K e');
       [iSolveTC                       (* PureExec *)
       |try solve_vals_compare_safe    (* The pure condition for PureExec *)
       |wp_finish                      (* new goal *)
-- 
GitLab