Merge remote-tracking branch 'origin/master' into gen_proofmode

CHANGELOG.md

@@ -18,6 +18,7 @@ Changes in Coq:
 
 * Rename some things and change notation:
   - The unit of a camera: `empty` -> `unit`, `∅` -> `ε`
+  - Disjointness: `⊥` -> `##`
   - A proof mode type class `IntoOp` -> `IsOp`
   - OFEs with all elements being discrete: `Discrete` -> `OfeDiscrete`
   - OFE elements whose equality is discrete: `Timeless` -> `Discrete`
@@ -85,6 +86,8 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
   of evars, which often led to divergence. There are a few places where type
   annotations are now needed.
 * Move the `prelude` folder to its own project: std++
+* The rules `internal_eq_rewrite` and `internal_eq_rewrite_contractive` are now
+  stated in the logic, i.e. they are `iApply` friendly.
 
 ## Iris 3.0.0 (released 2017-01-11)
 
@@ -113,7 +116,7 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
 * Slightly weaker notion of atomicity: an expression is atomic if it reduces in
   one step to something that does not reduce further.
 * Changed notation for embedding Coq assertions into Iris.  The new notation is
-  ⌜φ⌝.  Also removed `=` and `##` from the Iris scope.  (The old notations are
+  ⌜φ⌝.  Also removed `=` and `⊥` from the Iris scope.  (The old notations are
   provided in `base_logic.deprecated`.)
 * Up-closure of namespaces is now a notation (↑) instead of a coercion.
 * With invariants and the physical state being handled in the logic, there is no

build/opam-ci.sh

@@ -55,7 +55,7 @@ done
 # Upgrade cached things.
 echo
 echo "[opam-ci] Upgrading opam"
-opam upgrade -y --fixup
+opam upgrade -y --fixup && opam upgrade -y
 
 # Install build-dependencies.
 echo

theories/base_logic/base_logic.v

@@ -9,7 +9,7 @@ Module Import uPred.
 End uPred.
 
 (* Hint DB for the logic *)
-Hint Resolve pure_intro.
+Hint Resolve pure_intro : I.
 Hint Resolve or_elim or_intro_l' or_intro_r' : I.
 Hint Resolve and_intro and_elim_l' and_elim_r' : I.
 Hint Resolve persistently_mono : I.

theories/base_logic/lib/boxes.v

@@ -272,7 +272,7 @@ Proof.
     iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
     { by eapply lookup_insert_None. }
     { by apply (lookup_insert_None (delete γ f) γ1 γ2 true). }
-    iNext. eapply internal_eq_rewrite_contractive'; [by apply _| |by eauto].
+    iNext. iApply (internal_eq_rewrite_contractive with "[Heq] Hbox").
     iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
   - iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; try done.
     iMod (slice_insert_empty with "Hbox") as (γ1 ?) "[#Hslice1 Hbox]".
@@ -280,7 +280,7 @@ Proof.
     iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
     { by eapply lookup_insert_None. }
     { by apply (lookup_insert_None (delete γ f) γ1 γ2 false). }
-    iNext. eapply internal_eq_rewrite_contractive'; [by apply _| |by eauto].
+    iNext. iApply (internal_eq_rewrite_contractive with "[Heq] Hbox").
     iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
 Qed.
 
@@ -297,14 +297,14 @@ Proof.
     iMod (slice_insert_full _ _ _ _ (Q1 ∗ Q2)%I with "[$HQ1 $HQ2] Hbox")
       as (γ ?) "[#Hslice Hbox]"; first done.
     iExists γ. iIntros "{$% $#} !>". iNext.
-    eapply internal_eq_rewrite_contractive'; [by apply _| |by eauto].
+    iApply (internal_eq_rewrite_contractive with "[Heq1 Heq2] Hbox").
     iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
   - iMod (slice_delete_empty with "Hslice1 Hbox") as (P1) "(Heq1 & Hbox)"; try done.
     iMod (slice_delete_empty with "Hslice2 Hbox") as (P2) "(Heq2 & Hbox)"; first done.
     { by simplify_map_eq. }
     iMod (slice_insert_empty with "Hbox") as (γ ?) "[#Hslice Hbox]".
     iExists γ. iIntros "{$% $#} !>". iNext.
-    eapply internal_eq_rewrite_contractive'; [by apply _| |by eauto].
+    iApply (internal_eq_rewrite_contractive with "[Heq1 Heq2] Hbox").
     iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
 Qed.
 End box.

theories/base_logic/lib/fancy_updates.v

@@ -80,6 +80,25 @@ Qed.
 Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) ∗ Q ={E1,E2}=∗ P ∗ Q.
 Proof. rewrite fupd_eq /fupd_def. by iIntros "[HwP $]". Qed.
 
+Lemma fupd_plain' E1 E2 E2' P Q `{!Plain P} :
+  E1 ⊆ E2 →
+  (Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P.
+Proof.
+  iIntros ((E3&->&HE)%subseteq_disjoint_union_L) "HQP HQ".
+  rewrite fupd_eq /fupd_def ownE_op //. iIntros "H".
+  iMod ("HQ" with "H") as ">(Hws & [HE1 HE3] & HQ)"; iModIntro.
+  iAssert (◇ P)%I as "#HP".
+  { by iMod ("HQP" with "HQ [$]") as "(_ & _ & HP)". }
+  iMod "HP". iFrame. auto.
+Qed.
+
+Lemma later_fupd_plain E P `{!Plain P} : (▷ |={E}=> P) ={E}=∗ ▷ ◇ P.
+Proof.
+  rewrite fupd_eq /fupd_def. iIntros "HP [Hw HE]".
+  iAssert (▷ ◇ P)%I with "[-]" as "#$"; last by iFrame.
+  iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)".
+Qed.
+
 (** * Derived rules *)
 Global Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (@fupd Σ _ E1 E2).
 Proof. intros P Q; apply fupd_mono. Qed.
@@ -139,6 +158,13 @@ Proof.
   apply (big_opS_forall (λ P Q, P ={E}=∗ Q)); auto using fupd_intro.
   intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
 Qed.
+
+Lemma fupd_plain E1 E2 P Q `{!Plain P} :
+  E1 ⊆ E2 → (Q -∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P.
+Proof.
+  iIntros (HE) "HQP HQ". iApply (fupd_plain' _ _ E1 with "[HQP] HQ"); first done.
+  iIntros "?". iApply fupd_intro. by iApply "HQP".
+Qed.
 End fupd.
 
 (** Proofmode class instances *)
@@ -212,7 +238,7 @@ Section proofmode_classes.
   Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
 End proofmode_classes.
 
-Hint Extern 2 (coq_tactics.of_envs _ ⊢ |={_}=> _) => iModIntro.
+Hint Extern 2 (coq_tactics.envs_entails _ (|={_}=> _)) => iModIntro.
 
 (** Fancy updates that take a step. *)
 

theories/base_logic/lib/iprop.v

@@ -151,6 +151,5 @@ End iProp_solution.
 Lemma iProp_unfold_equivI {Σ} (P Q : iProp Σ) :
   iProp_unfold P ≡ iProp_unfold Q ⊢ (P ≡ Q : iProp Σ).
 Proof.
-  rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q).
-  apply: bi.f_equiv.
+  rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q). apply: bi.f_equiv.
 Qed.

theories/base_logic/lib/saved_prop.v

@@ -44,7 +44,6 @@ Section saved_prop.
     assert (∀ z, G2 (G1 z) ≡ z) as help.
     { intros z. rewrite /G1 /G2 -cFunctor_compose -{2}[z]cFunctor_id.
       apply (ne_proper (cFunctor_map F)); split=>?; apply iProp_fold_unfold. }
-    rewrite -{2}[x]help -{2}[y]help. apply later_mono.
-    apply f_equiv. solve_proper.
+    rewrite -{2}[x]help -{2}[y]help. apply later_mono, f_equiv, _.
   Qed.
 End saved_prop.

theories/base_logic/proofmode.v

@@ -4,7 +4,7 @@ From iris.algebra Require Import proofmode_classes.
 Import uPred.
 Import bi.
 
-Hint Extern 1 (coq_tactics.of_envs _ ⊢ |==> _) => iModIntro.
+Hint Extern 1 (coq_tactics.envs_entails _ (|==> _)) => iModIntro.
 
 Section class_instances.
 Context {M : ucmraT}.

theories/bi/big_op.v

@@ -842,6 +842,3 @@ Section gmultiset.
 End gmultiset.
 End sbi_big_op.
 End bi.
-
-Hint Resolve bi.big_sepL_nil' bi.big_sepM_empty'
-  bi.big_sepS_empty' bi.big_sepMS_empty' | 0.

theories/bi/derived.v

@@ -1741,9 +1741,9 @@ Global Instance from_option_persistent {A} P (Ψ : A → PROP) (mx : option A) :
   (∀ x, Persistent (Ψ x)) → Persistent P → Persistent (from_option Ψ P mx).
 Proof. destruct mx; apply _. Qed.
 
+(* Not an instance, see the bottom of this file *)
 Lemma plain_persistent P : Plain P → Persistent P.
 Proof. intros. by rewrite /Persistent -plainly_elim_persistently. Qed.
-Hint Immediate plain_persistent.
 
 (* Properties of persistent propositions *)
 Lemma persistent_persistently_2 P `{!Persistent P} : P ⊢ bi_persistently P.
@@ -1925,6 +1925,12 @@ Global Instance later_proper' :
   Proper ((⊣⊢) ==> (⊣⊢)) (@bi_later PROP) := ne_proper _.
 
 (* Equality *)
+Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A → PROP)
+  {HΨ : Contractive Ψ} : ▷ (a ≡ b) ⊢ Ψ a → Ψ b.
+Proof.
+  rewrite later_eq_2. move: HΨ=>/contractive_alt [g [? HΨ]]. rewrite !HΨ.
+  by apply internal_eq_rewrite.
+Qed.
 Lemma internal_eq_rewrite_contractive' {A : ofeT} a b (Ψ : A → PROP) P
   {HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
 Proof.
@@ -2113,8 +2119,18 @@ Proof.
   - rewrite sep_or_r !sep_or_l {1}(later_intro P) {1}(later_intro Q).
     rewrite -!later_sep !left_absorb right_absorb. auto.
 Qed.
-Lemma except_0_forall_1 {A} (Φ : A → PROP) : ◇ (∀ a, Φ a) ⊢ ∀ a, ◇ Φ a.
-Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
+Lemma except_0_forall {A} (Φ : A → PROP) : ◇ (∀ a, Φ a) ⊣⊢ ∀ a, ◇ Φ a.
+Proof.
+  apply (anti_symm _).
+  { apply forall_intro=> a. by rewrite (forall_elim a). }
+  trans (▷ (∀ a : A, Φ a) ∧ (∀ a : A, ◇ Φ a))%I.
+  { apply and_intro, reflexivity. rewrite later_forall. apply forall_mono=> a.
+    apply or_elim; auto using later_intro. }
+  rewrite later_false_em and_or_r. apply or_elim.
+  { rewrite and_elim_l. apply or_intro_l. }
+  apply or_intro_r', forall_intro=> a. rewrite !(forall_elim a).
+  by rewrite and_or_l impl_elim_l and_elim_r idemp.
+Qed.
 Lemma except_0_exist_2 {A} (Φ : A → PROP) : (∃ a, ◇ Φ a) ⊢ ◇ ∃ a, Φ a.
 Proof. apply exist_elim=> a. by rewrite (exist_intro a). Qed.
 Lemma except_0_exist `{Inhabited A} (Φ : A → PROP) :
@@ -2157,6 +2173,13 @@ Proof.
   by apply and_mono, except_0_intro.
 Qed.
 
+Global Instance except_0_plain P : Plain P → Plain (◇ P).
+Proof. rewrite /bi_except_0; apply _. Qed.
+Global Instance except_0_persistent P : Persistent P → Persistent (◇ P).
+Proof. rewrite /bi_except_0; apply _. Qed.
+Global Instance except_0_absorbing P : Absorbing P → Absorbing (◇ P).
+Proof. rewrite /bi_except_0; apply _. Qed.
+
 (* Timeless instances *)
 Global Instance Timeless_proper : Proper ((≡) ==> iff) (@Timeless PROP).
 Proof. solve_proper. Qed.
@@ -2198,11 +2221,8 @@ Qed.
 Global Instance forall_timeless {A} (Ψ : A → PROP) :
   (∀ x, Timeless (Ψ x)) → Timeless (∀ x, Ψ x).
 Proof.
-  rewrite /Timeless=> HQ. rewrite later_false_em.
-  apply or_mono; first done. apply forall_intro=> x.
-  rewrite -(löb (Ψ x)); apply impl_intro_l.
-  rewrite HQ /bi_except_0 !and_or_r. apply or_elim; last auto.
-  by rewrite impl_elim_r (forall_elim x).
+  rewrite /Timeless=> HQ. rewrite except_0_forall later_forall.
+  apply forall_mono; auto.
 Qed.
 Global Instance exist_timeless {A} (Ψ : A → PROP) :
   (∀ x, Timeless (Ψ x)) → Timeless (∃ x, Ψ x).
@@ -2297,3 +2317,12 @@ Global Instance bi_except_0_sep_entails_homomorphism :
 Proof. split; try apply _. apply except_0_intro. Qed.
 End sbi_derived.
 End bi.
+
+(* When declared as an actual instance, [plain_persistent] will cause
+failing proof searches to take exponential time, as Coq will try to
+apply it the instance at any node in the proof search tree.
+
+To avoid that, we declare it using a [Hint Immediate], so that it will
+only be used at the leaves of the proof search tree, i.e. when the
+premise of the hint can be derived from just the current context. *)
+Hint Immediate bi.plain_persistent : typeclass_instances.

theories/heap_lang/lang.v

@@ -109,14 +109,6 @@ Fixpoint to_val (e : expr) : option val :=
   | _ => None
   end.
 
-Class AsRec (e : expr) (f x : binder) (erec : expr) :=
-  as_rec : e = Rec f x erec.
-
-Instance AsRec_rec f x e : AsRec (Rec f x e) f x e := eq_refl.
-Instance AsRec_rec_locked_val v f x e :
-  AsRec (of_val v) f x e → AsRec (of_val (locked v)) f x e.
-Proof. by unlock. Qed.
-
 (** The state: heaps of vals. *)
 Definition state := gmap loc val.
 
@@ -420,7 +412,7 @@ Lemma is_closed_of_val X v : is_closed X (of_val v).
 Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.
 
 Lemma is_closed_to_val X e v : to_val e = Some v → is_closed X e.
-Proof. intros Hev; rewrite -(of_to_val e v Hev); apply is_closed_of_val. Qed.
+Proof. intros <-%of_to_val. apply is_closed_of_val. Qed.
 
 Lemma is_closed_subst X e x es :
   is_closed [] es → is_closed (x :: X) e → is_closed X (subst x es e).

theories/heap_lang/lifting.v

@@ -83,16 +83,21 @@ Qed.
 Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
 Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
 Local Ltac solve_pure_exec :=
-  repeat lazymatch goal with
-  | H: IntoVal ?e _ |- _ => rewrite -(of_to_val e _ into_val); clear H
-  | H: AsRec _ _ _ _ |- _ => rewrite H; clear H
-  end;
+  unfold IntoVal, AsVal in *; subst;
+  repeat match goal with H : is_Some _ |- _ => destruct H as [??] end;
   apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ].
 
-Global Instance pure_rec f x (erec e1 e2 : expr) (v2 : val)
-    `{!IntoVal e2 v2, AsRec e1 f x erec, Closed (f :b: x :b: []) erec} :
+Class AsRec (e : expr) (f x : binder) (erec : expr) :=
+  as_rec : e = Rec f x erec.
+Global Instance AsRec_rec f x e : AsRec (Rec f x e) f x e := eq_refl.
+Global Instance AsRec_rec_locked_val v f x e :
+  AsRec (of_val v) f x e → AsRec (of_val (locked v)) f x e.
+Proof. by unlock. Qed.
+
+Global Instance pure_rec f x (erec e1 e2 : expr)
+    `{!AsVal e2, AsRec e1 f x erec, Closed (f :b: x :b: []) erec} :
   PureExec True (App e1 e2) (subst' x e2 (subst' f e1 erec)).
-Proof. solve_pure_exec. Qed.
+Proof. unfold AsRec in *; solve_pure_exec. Qed.
 
 Global Instance pure_unop op e v v' `{!IntoVal e v} :
   PureExec (un_op_eval op v = Some v') (UnOp op e) (of_val v').
@@ -110,11 +115,11 @@ Global Instance pure_if_false e1 e2 :
   PureExec True (If (Lit (LitBool false)) e1 e2) e2.
 Proof. solve_pure_exec. Qed.
 
-Global Instance pure_fst e1 e2 v1 v2 `{!IntoVal e1 v1, !IntoVal e2 v2} :
+Global Instance pure_fst e1 e2 v1 `{!IntoVal e1 v1, !AsVal e2} :
   PureExec True (Fst (Pair e1 e2)) e1.
 Proof. solve_pure_exec. Qed.
 
-Global Instance pure_snd e1 e2 v1 v2 `{!IntoVal e1 v1, !IntoVal e2 v2} :
+Global Instance pure_snd e1 e2 v2 `{!AsVal e1, !IntoVal e2 v2} :
   PureExec True (Snd (Pair e1 e2)) e2.
 Proof. solve_pure_exec. Qed.
 
@@ -128,7 +133,7 @@ Proof. solve_pure_exec. Qed.
 
 (** Heap *)
 Lemma wp_alloc E e v :
-  to_val e = Some v →
+  IntoVal e v →
   {{{ True }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
 Proof.
   iIntros (<-%of_to_val Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
@@ -149,7 +154,7 @@ Proof.
 Qed.
 
 Lemma wp_store E l v' e v :
-  to_val e = Some v →
+  IntoVal e v →
   {{{ ▷ l ↦ v' }}} Store (Lit (LitLoc l)) e @ E {{{ RET LitV LitUnit; l ↦ v }}}.
 Proof.
   iIntros (<-%of_to_val Φ) ">Hl HΦ".
@@ -160,12 +165,12 @@ Proof.
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
 
-Lemma wp_cas_fail E l q v' e1 v1 e2 v2 :
-  to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 →
+Lemma wp_cas_fail E l q v' e1 v1 e2 :
+  IntoVal e1 v1 → AsVal e2 → v' ≠ v1 →
   {{{ ▷ l ↦{q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E
   {{{ RET LitV (LitBool false); l ↦{q} v' }}}.
 Proof.
-  iIntros (<-%of_to_val <-%of_to_val ? Φ) ">Hl HΦ".
+  iIntros (<-%of_to_val [v2 <-%of_to_val] ? Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
@@ -173,7 +178,7 @@ Proof.
 Qed.
 
 Lemma wp_cas_suc E l e1 v1 e2 v2 :
-  to_val e1 = Some v1 → to_val e2 = Some v2 →
+  IntoVal e1 v1 → IntoVal e2 v2 →
   {{{ ▷ l ↦ v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E
   {{{ RET LitV (LitBool true); l ↦ v2 }}}.
 Proof.
@@ -184,23 +189,4 @@ Proof.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
-
-(** Proof rules for derived constructs *)
-Lemma wp_seq E e1 e2 Φ :
-  is_Some (to_val e1) → Closed [] e2 →
-  ▷ WP e2 @ E {{ Φ }} ⊢ WP Seq e1 e2 @ E {{ Φ }}.
-Proof. iIntros ([? ?] ?). rewrite -wp_pure_step_later; by eauto. Qed.
-
-Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊢ WP Skip @ E {{ Φ }}.
-Proof. rewrite -wp_seq; last eauto. by rewrite -wp_value. Qed.
-
-Lemma wp_match_inl E e0 x1 e1 x2 e2 Φ :
-  is_Some (to_val e0) → Closed (x1 :b: []) e1 →
-  ▷ WP subst' x1 e0 e1 @ E {{ Φ }} ⊢ WP Match (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
-Proof. iIntros ([? ?] ?) "?". rewrite -!wp_pure_step_later; by eauto. Qed.
-
-Lemma wp_match_inr E e0 x1 e1 x2 e2 Φ :
-  is_Some (to_val e0) → Closed (x2 :b: []) e2 →
-  ▷ WP subst' x2 e0 e2 @ E {{ Φ }} ⊢ WP Match (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
-Proof. iIntros ([? ?] ?) "?". rewrite -!wp_pure_step_later; by eauto. Qed.
 End lifting.

theories/heap_lang/proofmode.v

@@ -9,20 +9,25 @@ Lemma tac_wp_pure `{heapG Σ} K Δ Δ' E e1 e2 φ Φ :
   PureExec φ e1 e2 →
   φ →
   IntoLaterNEnvs 1 Δ Δ' →
-  (Δ' ⊢ WP fill K e2 @ E {{ Φ }}) →
-  (Δ ⊢ WP fill K e1 @ E {{ Φ }}).
+  envs_entails Δ' (WP fill K e2 @ E {{ Φ }}) →
+  envs_entails Δ (WP fill K e1 @ E {{ Φ }}).
 Proof.
-  intros ??? HΔ'. rewrite into_laterN_env_sound /=.
+  rewrite /envs_entails=> ??? HΔ'. rewrite into_laterN_env_sound /=.
   rewrite -lifting.wp_bind HΔ' -wp_pure_step_later //.
   by rewrite -ectx_lifting.wp_ectx_bind_inv.
 Qed.
 
-Ltac wp_value_head := etrans; [|eapply wp_value; apply _]; simpl.
+Lemma tac_wp_value `{heapG Σ} Δ E Φ e v :
+  IntoVal e v →
+  envs_entails Δ (Φ v) → envs_entails Δ (WP e @ E {{ Φ }}).
+Proof. rewrite /envs_entails=> ? ->. by apply wp_value. Qed.
+
+Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
 
 Tactic Notation "wp_pure" open_constr(efoc) :=
   iStartProof;
   lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+  | |- envs_entails _ (wp ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
     unify e' efoc;
     eapply (tac_wp_pure K);
     [simpl; apply _                 (* PureExec *)
@@ -47,19 +52,23 @@ Tactic Notation "wp_proj" := wp_pure (Fst _) || wp_pure (Snd _).
 Tactic Notation "wp_case" := wp_pure (Case _ _ _).
 Tactic Notation "wp_match" := wp_case; wp_let.
 
+Lemma tac_wp_bind `{heapG Σ} K Δ E Φ e :
+  envs_entails Δ (WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }})%I →
+  envs_entails Δ (WP fill K e @ E {{ Φ }}).
+Proof. rewrite /envs_entails=> ->. by apply wp_bind. Qed.
+
 Ltac wp_bind_core K :=
   lazymatch eval hnf in K with
   | [] => idtac
-  | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
+  | _ => apply (tac_wp_bind K); simpl
   end.
 
 Tactic Notation "wp_bind" open_constr(efoc) :=
   iStartProof;
   lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match e' with
-    | efoc => unify e' efoc; wp_bind_core K
-    end) || fail "wp_bind: cannot find" efoc "in" e
+  | |- envs_entails _ (wp ?E ?e ?Q) =>
+    reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
+    || fail "wp_bind: cannot find" efoc "in" e
   | _ => fail "wp_bind: not a 'wp'"
   end.
 
@@ -75,10 +84,11 @@ Lemma tac_wp_alloc Δ Δ' E j K e v Φ :
   IntoLaterNEnvs 1 Δ Δ' →
   (∀ l, ∃ Δ'',
     envs_app false (Esnoc Enil j (l ↦ v)) Δ' = Some Δ'' ∧
-    (Δ'' ⊢ WP fill K (Lit (LitLoc l)) @ E {{ Φ }})) →
-  Δ ⊢ WP fill K (Alloc e) @ E {{ Φ }}.
+    envs_entails Δ'' (WP fill K (Lit (LitLoc l)) @ E {{ Φ }})) →
+  envs_entails Δ (WP fill K (Alloc e) @ E {{ Φ }}).
 Proof.
-  intros ?? HΔ. rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
+  rewrite /envs_entails=> ?? HΔ.
+  rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
   rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
   destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
   by rewrite right_id HΔ'.
@@ -87,10 +97,11 @@ Qed.
 Lemma tac_wp_load Δ Δ' E i K l q v Φ :
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
-  (Δ' ⊢ WP fill K (of_val v) @ E {{ Φ }}) →
-  Δ ⊢ WP fill K (Load (Lit (LitLoc l))) @ E {{ Φ }}.
+  envs_entails Δ' (WP fill K (of_val v) @ E {{ Φ }}) →
+  envs_entails Δ (WP fill K (Load (Lit (LitLoc l))) @ E {{ Φ }}).
 Proof.
-  intros. rewrite -wp_bind. eapply wand_apply; first exact: wp_load.
+  rewrite /envs_entails=> ???.
+  rewrite -wp_bind. eapply wand_apply; first exact: wp_load.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
@@ -100,22 +111,24 @@ Lemma tac_wp_store Δ Δ' Δ'' E i K l v e v' Φ :
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
-  (Δ'' ⊢ WP fill K (Lit LitUnit) @ E {{ Φ }}) →
-  Δ ⊢ WP fill K (Store (Lit (LitLoc l)) e) @ E {{ Φ }}.
+  envs_entails Δ'' (WP fill K (Lit LitUnit) @ E {{ Φ }}) →
+  envs_entails Δ (WP fill K (Store (Lit (LitLoc l)) e) @ E {{ Φ }}).
 Proof.
-  intros. rewrite -wp_bind. eapply wand_apply; first by eapply wp_store.
+  rewrite /envs_entails=> ?????.
+  rewrite -wp_bind. eapply wand_apply; first by eapply wp_store.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
-Lemma tac_wp_cas_fail Δ Δ' E i K l q v e1 v1 e2 v2 Φ :
-  IntoVal e1 v1 → IntoVal e2 v2 →
+Lemma tac_wp_cas_fail Δ Δ' E i K l q v e1 v1 e2 Φ :
+  IntoVal e1 v1 → AsVal e2 →
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I → v ≠ v1 →
-  (Δ' ⊢ WP fill K (Lit (LitBool false)) @ E {{ Φ }}) →
-  Δ ⊢ WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ E {{ Φ }}.
+  envs_entails Δ' (WP fill K (Lit (LitBool false)) @ E {{ Φ }}) →
+  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ E {{ Φ }}).
 Proof.
-  intros. rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_fail.
+  rewrite /envs_entails=> ??????.
+  rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_fail.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
@@ -125,10 +138,11 @@ Lemma tac_wp_cas_suc Δ Δ' Δ'' E i K l v e1 v1 e2 v2 Φ :
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I → v = v1 →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
-  (Δ'' ⊢ WP fill K (Lit (LitBool true)) @ E {{ Φ }}) →
-  Δ ⊢ WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ E {{ Φ }}.
+  envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ E {{ Φ }}) →
+  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ E {{ Φ }}).
 Proof.
-  intros; subst. rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
+  rewrite /envs_entails=> ???????; subst.
+  rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
@@ -137,7 +151,7 @@ End heap.
 Tactic Notation "wp_apply" open_constr(lem) :=
   iPoseProofCore lem as false true (fun H =>
     lazymatch goal with
-    | |- _ ⊢ wp ?E ?e ?Q =>
+    | |- envs_entails _ (wp ?E ?e ?Q) =>
       reshape_expr e ltac:(fun K e' =>
         wp_bind_core K; iApplyHyp H; try iNext; simpl) ||
       lazymatch iTypeOf H with
@@ -149,7 +163,7 @@ Tactic Notation "wp_apply" open_constr(lem) :=
 Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
   iStartProof;
   lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
+  | |- envs_entails _ (wp ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
          eapply (tac_wp_alloc _ _ _ H K); [apply _|..])
@@ -168,7 +182,7 @@ Tactic Notation "wp_alloc" ident(l) :=
 Tactic Notation "wp_load" :=
   iStartProof;
   lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
+  | |- envs_entails _ (wp ?E ?e ?Q) =>
     first