From f2eaf912c34743d32c23545efa52108b0cf31753 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 29 Aug 2017 13:28:55 +0200
Subject: [PATCH] Drop positivity axiom of the BI canonical structure.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The absence of this axiom has two consequences:

- We no longer have `■ (P ∗ Q) ⊢ ■ P ∗ ■ Q` and `□ (P ∗ Q) ⊢ □ P ∗ □ Q`,
  and as a result, separating conjunctions in the unrestricted/persistent
  context cannot be eliminated.
- When having `(P -∗ ⬕ Q) ∗ P`, we do not get `⬕ Q ∗ P`. In the proof
  mode this means when having:

    H1 : P -∗ ⬕ Q
    H2 : P

  We cannot say `iDestruct ("H1" with "H2") as "#H1"` and keep `H2`.

However, there is now a type class `PositiveBI PROP`, and when there is an
instance of this type class, one gets the above reasoning principle back.

TODO: Can we describe positivity of individual propositions instead of the
whole BI? That way, we would get the above reasoning principles even when
the BI is not positive, but the propositions involved are.
---
 theories/base_logic/lib/own.v        |   4 +-
 theories/base_logic/proofmode.v      |   4 +-
 theories/base_logic/upred.v          |   3 -
 theories/bi/derived.v                | 149 +++++++++--------
 theories/bi/fractional.v             |   8 +-
 theories/bi/interface.v              |   5 -
 theories/proofmode/class_instances.v | 100 +++++-------
 theories/proofmode/classes.v         |  10 +-
 theories/proofmode/coq_tactics.v     | 232 +++++++++++++++++----------
 theories/proofmode/tactics.v         |   5 +-
 theories/tests/proofmode.v           |   4 +-
 11 files changed, 280 insertions(+), 244 deletions(-)

diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index a051d2cb0..308331a04 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -185,8 +185,8 @@ Section proofmode_classes.
   Context `{inG Σ A}.
   Implicit Types a b : A.
 
-  Global Instance into_sep_own p γ a b1 b2 :
-    IsOp a b1 b2 → IntoSep p (own γ a) (own γ b1) (own γ b2).
+  Global Instance into_sep_own γ a b1 b2 :
+    IsOp a b1 b2 → IntoSep (own γ a) (own γ b1) (own γ b2).
   Proof. intros. by rewrite /IntoSep (is_op a) own_op. Qed.
   Global Instance into_and_own p γ a b1 b2 :
     IsOp a b1 b2 → IntoAnd p (own γ a) (own γ b1) (own γ b2).
diff --git a/theories/base_logic/proofmode.v b/theories/base_logic/proofmode.v
index f252ffe10..ac7c11bef 100644
--- a/theories/base_logic/proofmode.v
+++ b/theories/base_logic/proofmode.v
@@ -88,8 +88,8 @@ Proof.
   intros. apply bare_persistently_if_mono. by rewrite (is_op a) ownM_op sep_and.
 Qed.
 
-Global Instance into_sep_ownM p (a b1 b2 : M) :
-  IsOp a b1 b2 → IntoSep p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Global Instance into_sep_ownM (a b1 b2 : M) :
+  IsOp a b1 b2 → IntoSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
 Proof. intros. by rewrite /IntoSep (is_op a) ownM_op. Qed.
 
 Global Instance from_sep_bupd P Q1 Q2 :
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index eaa3fe780..29695fe35 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -438,9 +438,6 @@ Proof.
   - (* (P ⊢ Q -∗ R) → P ∗ Q ⊢ R *)
     intros P Q R. unseal=> HPQR. split; intros n x ? (?&?&?&?&?). ofe_subst.
     eapply HPQR; eauto using cmra_validN_op_l.
-  - (* emp ∧ (Q ∗ R) ⊢ (emp ∧ Q) ∗ R (ADMISSIBLE) *)
-    intros Q R. unfold uPred_emp; unseal; split; intros n x ? [_ (x1&x2&?&?&?)].
-    exists x1, x2; simpl; auto. 
   - (* (P ⊢ Q) → □ P ⊢ □ Q *)
     intros P QR HP. unseal; split=> n x ? /=. by apply HP, cmra_core_validN.
   - (* □ P ⊢ □ □ P *)
diff --git a/theories/bi/derived.v b/theories/bi/derived.v
index c76973060..d08f72e30 100644
--- a/theories/bi/derived.v
+++ b/theories/bi/derived.v
@@ -34,6 +34,9 @@ Hint Mode Affine + ! : typeclass_instances.
 Class AffineBI (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
 Existing Instance absorbing_bi | 0.
 
+Class PositiveBI (PROP : bi) :=
+  positive_bi (P Q : PROP) : ■ (P ∗ Q) ⊢ ■ P ∗ Q.
+
 Class Absorbing {PROP : bi} (P : PROP) := absorbing Q : P ∗ Q ⊢ P.
 Arguments Absorbing {_} _%I : simpl never.
 Arguments absorbing {_} _%I _%I.
@@ -705,28 +708,22 @@ Proof.
   rewrite /bi_bare -(comm _ P) (assoc _ (_ ∧ _)%I) -!(assoc _ P).
   by rewrite idemp !assoc (comm _ P).
 Qed.
-Lemma bare_sep P Q : ■ (P ∗ Q) ⊣⊢ ■ P ∗ ■ Q.
+Lemma bare_sep_2 P Q : ■ P ∗ ■ Q ⊢ ■ (P ∗ Q).
 Proof.
-  rewrite /bi_bare. apply (anti_symm _).
-  - rewrite -{1}(idemp bi_and emp%I) -assoc emp_and_sep_assoc_1.
-    by rewrite (comm bi_sep) emp_and_sep_assoc_1 comm.
-  - apply and_intro.
-    + by rewrite !and_elim_l right_id.
-    + by rewrite !and_elim_r.
+  rewrite /bi_bare. apply and_intro.
+  - by rewrite !and_elim_l right_id.
+  - by rewrite !and_elim_r.
+Qed.
+Lemma bare_sep `{PositiveBI PROP} P Q : ■ (P ∗ Q) ⊣⊢ ■ P ∗ ■ Q.
+Proof.
+  apply (anti_symm _), bare_sep_2.
+  by rewrite -{1}bare_idemp positive_bi !(comm _ (â–  P)%I) positive_bi.
 Qed.
 Lemma bare_forall {A} (Φ : A → PROP) : ■ (∀ a, Φ a) ⊢ ∀ a, ■ Φ a.
 Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
 Lemma bare_exist {A} (Φ : A → PROP) : ■ (∃ a, Φ a) ⊣⊢ ∃ a, ■ Φ a.
 Proof. by rewrite /bi_bare and_exist_l. Qed.
 
-Lemma bare_sep_l P Q : ■ (P ∗ Q) ⊢ ■ P.
-Proof.
-  rewrite /bi_bare. apply and_intro; auto.
-  by rewrite (comm _ P) emp_and_sep_assoc_1 {1}and_elim_l left_id.
-Qed.
-Lemma bare_sep_r P Q : ■ (P ∗ Q) ⊢ ■ Q.
-Proof. by rewrite (comm _ P) bare_sep_l. Qed.
-
 Lemma bare_True_emp : ■ True ⊣⊢ ■ emp.
 Proof. apply (anti_symm _); rewrite /bi_bare; auto. Qed.
 
@@ -838,8 +835,10 @@ Proof. apply (anti_symm _); auto using sep_True_2. Qed.
 Section affine_bi.
   Context `{AffineBI PROP}.
 
-  Global Instance affine_bi P : Absorbing P | 0.
+  Global Instance affine_bi_absorbing P : Absorbing P | 0.
   Proof. intros Q. by rewrite (affine Q) right_id. Qed.
+  Global Instance affine_bi_positive : PositiveBI PROP.
+  Proof. intros P Q. by rewrite !affine_bare. Qed.
 
   Lemma True_emp : True ⊣⊢ emp.
   Proof. apply (anti_symm _); auto using affine. Qed.
@@ -876,19 +875,23 @@ Proof. intros P Q; apply persistently_mono. Qed.
 Global Instance persistently_absorbing P : Absorbing (â–¡ P).
 Proof. rewrite /Absorbing=> R. apply persistently_absorbing. Qed.
 
-Lemma persistently_and_sep_assoc_1 P Q R : □ P ∧ (Q ∗ R) ⊢ (□ P ∧ Q) ∗ R.
+Lemma persistently_and_sep_assoc P Q R : □ P ∧ (Q ∗ R) ⊣⊢ (□ P ∧ Q) ∗ R.
 Proof.
-  rewrite {1}persistently_idemp_2 persistently_and_sep_elim assoc.
-  apply sep_mono_l, and_intro.
-  - by rewrite and_elim_r absorbing.
-  - by rewrite and_elim_l left_id.
+  apply (anti_symm (⊢)).
+  - rewrite {1}persistently_idemp_2 persistently_and_sep_elim assoc.
+    apply sep_mono_l, and_intro.
+    + by rewrite and_elim_r absorbing.
+    + by rewrite and_elim_l left_id.
+  - apply and_intro.
+    + by rewrite and_elim_l sep_elim_l.
+    + by rewrite and_elim_r.
 Qed.
 Lemma persistently_and_emp_elim P : emp ∧ □ P ⊢ P.
 Proof. by rewrite comm persistently_and_sep_elim right_id and_elim_r. Qed.
 Lemma persistently_elim_True P : □ P ⊢ P ∗ True.
 Proof.
   rewrite -(right_id True%I _ (â–¡ _)%I) -{1}(left_id emp%I _ True%I).
-  by rewrite persistently_and_sep_assoc_1 (comm bi_and) persistently_and_emp_elim.
+  by rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim.
 Qed.
 Lemma persistently_elim P `{!Absorbing P} : □ P ⊢ P.
 Proof. by rewrite persistently_elim_True sep_elim_l. Qed.
@@ -939,24 +942,9 @@ Lemma persistently_sep_dup P : □ P ⊣⊢ □ P ∗ □ P.
 Proof.
   apply (anti_symm _); last by eauto using sep_elim_l with typeclass_instances.
   rewrite -{1}(idemp bi_and (â–¡ _)%I) -{2}(left_id emp%I _ (â–¡ _)%I).
-  by rewrite persistently_and_sep_assoc_1 and_elim_l.
+  by rewrite persistently_and_sep_assoc and_elim_l.
 Qed.
 
-Lemma persistently_and_sep_assoc P Q R : □ P ∧ (Q ∗ R) ⊣⊢ (□ P ∧ Q) ∗ R.
-Proof.
-  apply (anti_symm (⊢)); auto using persistently_and_sep_assoc_1.
-  apply and_intro.
-  - by rewrite and_elim_l sep_elim_l.
-  - by rewrite and_elim_r.
-Qed.
-Lemma persistently_sep_elim_l P Q : □ (P ∗ Q) ⊢ □ P.
-Proof.
-  rewrite -(left_id True%I bi_and (â–¡ _)%I) (persistently_emp_intro True%I).
-  by rewrite -persistently_and (comm bi_sep) emp_and_sep_assoc_1 and_elim_l left_id.
-Qed.
-Lemma persistently_sep_elim_r P Q : □ (P ∗ Q) ⊢ □ Q.
-Proof. by rewrite comm persistently_sep_elim_l. Qed.
-
 Lemma persistently_and_sep_l_1 P Q : □ P ∧ Q ⊢ □ P ∗ Q.
 Proof.
   by rewrite -{1}(left_id emp%I _ Q%I) persistently_and_sep_assoc and_elim_l.
@@ -966,12 +954,17 @@ Proof. by rewrite !(comm _ P) persistently_and_sep_l_1. Qed.
 
 Lemma persistently_True_emp : □ True ⊣⊢ □ emp.
 Proof. apply (anti_symm _); auto using persistently_emp_intro. Qed.
-Lemma persistently_and_sep P Q : □ (P ∧ Q) ⊣⊢ □ (P ∗ Q).
+Lemma persistently_and_sep P Q : □ (P ∧ Q) ⊢ □ (P ∗ Q).
 Proof.
-  rewrite persistently_and. apply (anti_symm (⊢)).
-  - rewrite -{1}persistently_idemp -persistently_and -{1}(left_id emp%I _ Q%I).
-    by rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim.
-  - auto using persistently_sep_elim_l, persistently_sep_elim_r.
+  rewrite persistently_and.
+  rewrite -{1}persistently_idemp -persistently_and -{1}(left_id emp%I _ Q%I).
+  by rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim.
+Qed.
+
+Lemma persistently_bare P : □ ■ P ⊣⊢ □ P.
+Proof.
+  by rewrite /bi_bare persistently_and -persistently_True_emp
+             persistently_pure left_id.
 Qed.
 
 Lemma and_sep_persistently P Q : □ P ∧ □ Q ⊣⊢ □ P ∗ □ Q.
@@ -980,11 +973,17 @@ Proof.
   - auto using persistently_and_sep_l_1.
   - eauto 10 using sep_elim_l, sep_elim_r with typeclass_instances.
 Qed.
-Lemma persistently_sep P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
+Lemma persistently_sep_2 P Q : □ P ∗ □ Q ⊢ □ (P ∗ Q).
 Proof. by rewrite -persistently_and_sep persistently_and -and_sep_persistently. Qed.
+Lemma persistently_sep `{PositiveBI PROP} P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
+Proof.
+  apply (anti_symm _); auto using persistently_sep_2.
+  by rewrite -persistently_bare bare_sep sep_and !bare_elim persistently_and
+             and_sep_persistently.
+Qed.
 
 Lemma persistently_wand P Q : □ (P -∗ Q) ⊢ □ P -∗ □ Q.
-Proof. by apply wand_intro_r; rewrite -persistently_sep wand_elim_l. Qed.
+Proof. apply wand_intro_r. by rewrite persistently_sep_2 wand_elim_l. Qed.
 
 Lemma persistently_entails_l P Q : (P ⊢ □ Q) → P ⊢ □ Q ∗ P.
 Proof. intros; rewrite -persistently_and_sep_l_1; auto. Qed.
@@ -1023,53 +1022,48 @@ Section persistently_bare_bi.
   Proof.
     apply (anti_symm (⊢)).
     - rewrite -(right_id True%I bi_sep (P -∗ Q)%I) -(exist_intro (P -∗ Q)%I).
-      apply sep_mono_r. rewrite -persistently_pure. apply persistently_intro', impl_intro_l.
+      apply sep_mono_r. rewrite -persistently_pure.
+      apply persistently_intro', impl_intro_l.
       by rewrite wand_elim_r persistently_pure right_id.
-    - apply exist_elim=> R. apply wand_intro_l. rewrite assoc -persistently_and_sep_r.
+    - apply exist_elim=> R. apply wand_intro_l.
+      rewrite assoc -persistently_and_sep_r.
       by rewrite persistently_elim impl_elim_r.
   Qed.
   Lemma impl_alt P Q : (P → Q) ⊣⊢ ∃ R, R ∧ □ (P ∧ R -∗ Q).
   Proof.
     apply (anti_symm (⊢)).
     - rewrite -(right_id True%I bi_and (P → Q)%I) -(exist_intro (P → Q)%I).
-      apply and_mono_r. rewrite -persistently_pure. apply persistently_intro', wand_intro_l.
+      apply and_mono_r. rewrite -persistently_pure.
+      apply persistently_intro', wand_intro_l.
       by rewrite impl_elim_r persistently_pure right_id.
     - apply exist_elim=> R. apply impl_intro_l. rewrite assoc persistently_and_sep_r.
       by rewrite persistently_elim wand_elim_r.
   Qed.
 End persistently_bare_bi.
 
-(* The combined bare persistently modality *)
-Lemma persistently_bare P : □ ■ P ⊣⊢ □ P.
-Proof.
-  by rewrite /bi_bare persistently_and -persistently_True_emp
-             persistently_pure left_id.
-Qed.
 
+(* The combined bare persistently modality *)
 Lemma bare_persistently_elim P : ⬕ P ⊢ P.
 Proof. apply persistently_and_emp_elim. Qed.
 Lemma bare_persistently_intro' P Q : (⬕ P ⊢ Q) → ⬕ P ⊢ ⬕ Q.
 Proof. intros <-. by rewrite persistently_bare persistently_idemp. Qed.
 
 Lemma bare_persistently_emp : ⬕ emp ⊣⊢ emp.
-Proof.
-  by rewrite -persistently_True_emp persistently_pure bare_True_emp bare_emp.
-Qed.
+Proof. by rewrite -persistently_True_emp persistently_pure bare_True_emp bare_emp. Qed.
 Lemma bare_persistently_and P Q : ⬕ (P ∧ Q) ⊣⊢ ⬕ P ∧ ⬕ Q.
 Proof. by rewrite persistently_and bare_and. Qed.
 Lemma bare_persistently_or P Q : ⬕ (P ∨ Q) ⊣⊢ ⬕ P ∨ ⬕ Q.
 Proof. by rewrite persistently_or bare_or. Qed.
 Lemma bare_persistently_exist {A} (Φ : A → PROP) : ⬕ (∃ x, Φ x) ⊣⊢ ∃ x, ⬕ Φ x.
 Proof. by rewrite persistently_exist bare_exist. Qed.
-Lemma bare_persistently_sep P Q : ⬕ (P ∗ Q) ⊣⊢ ⬕ P ∗ ⬕ Q.
-Proof. by rewrite persistently_sep bare_sep. Qed.
+Lemma bare_persistently_sep_2 P Q : ⬕ P ∗ ⬕ Q ⊢ ⬕ (P ∗ Q).
+Proof. by rewrite bare_sep_2 persistently_sep_2. Qed.
+Lemma bare_persistently_sep `{PositiveBI PROP} P Q : ⬕ (P ∗ Q) ⊣⊢ ⬕ P ∗ ⬕ Q.
+Proof. by rewrite -bare_sep -persistently_sep. Qed.
 
 Lemma bare_persistently_idemp P : ⬕ ⬕ P ⊣⊢ ⬕ P.
 Proof. by rewrite persistently_bare persistently_idemp. Qed.
 
-Lemma bare_persistently_sep_dup P : ⬕ P ⊣⊢ ⬕ P ∗ ⬕ P.
-Proof. by rewrite {1}persistently_sep_dup bare_sep. Qed.
-
 Lemma persistently_and_bare_sep_l P Q : □ P ∧ Q ⊣⊢ ⬕ P ∗ Q.
 Proof.
   apply (anti_symm _).
@@ -1078,6 +1072,11 @@ Proof.
 Qed.
 Lemma persistently_and_bare_sep_r P Q : P ∧ □ Q ⊣⊢ P ∗ ⬕ Q.
 Proof. by rewrite !(comm _ P) persistently_and_bare_sep_l. Qed.
+Lemma and_sep_bare_persistently P Q : ⬕ P ∧ ⬕ Q ⊣⊢ ⬕ P ∗ ⬕ Q.
+Proof. by rewrite -persistently_and_bare_sep_l -bare_and bare_and_l. Qed.
+
+Lemma bare_persistently_sep_dup P : ⬕ P ⊣⊢ ⬕ P ∗ ⬕ P.
+Proof. by rewrite -persistently_and_bare_sep_l bare_and_l bare_and idemp. Qed.
 
 (* Conditional bare modality *)
 Global Instance bare_if_ne p : NonExpansive (@bi_bare_if PROP p).
@@ -1108,7 +1107,9 @@ Lemma bare_if_or p P Q : ■?p (P ∨ Q) ⊣⊢ ■?p P ∨ ■?p Q.
 Proof. destruct p; simpl; auto using bare_or. Qed.
 Lemma bare_if_exist {A} p (Ψ : A → PROP) : (■?p ∃ a, Ψ a) ⊣⊢ ∃ a, ■?p Ψ a.
 Proof. destruct p; simpl; auto using bare_exist. Qed.
-Lemma bare_if_sep p P Q : ■?p (P ∗ Q) ⊣⊢ ■?p P ∗ ■?p Q.
+Lemma bare_if_sep_2 p P Q : ■?p P ∗ ■?p Q ⊢ ■?p (P ∗ Q).
+Proof. destruct p; simpl; auto using bare_sep_2. Qed.
+Lemma bare_if_sep `{PositiveBI PROP} p P Q : ■?p (P ∗ Q) ⊣⊢ ■?p P ∗ ■?p Q.
 Proof. destruct p; simpl; auto using bare_sep. Qed.
 
 Lemma bare_if_idemp p P : ■?p ■?p P ⊣⊢ ■?p P.
@@ -1138,7 +1139,9 @@ Lemma persistently_if_or p P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q.
 Proof. destruct p; simpl; auto using persistently_or. Qed.
 Lemma persistently_if_exist {A} p (Ψ : A → PROP) : (□?p ∃ a, Ψ a) ⊣⊢ ∃ a, □?p Ψ a.
 Proof. destruct p; simpl; auto using persistently_exist. Qed.
-Lemma persistently_if_sep p P Q : □?p (P ∗ Q) ⊣⊢ □?p P ∗ □?p Q.
+Lemma persistently_if_sep_2 p P Q : □?p P ∗ □?p Q ⊢ □?p (P ∗ Q).
+Proof. destruct p; simpl; auto using persistently_sep_2. Qed.
+Lemma persistently_if_sep `{PositiveBI PROP} p P Q : □?p (P ∗ Q) ⊣⊢ □?p P ∗ □?p Q.
 Proof. destruct p; simpl; auto using persistently_sep. Qed.
 
 Lemma persistently_if_idemp p P : □?p □?p P ⊣⊢ □?p P.
@@ -1161,10 +1164,11 @@ Lemma bare_persistently_if_and p P Q : ⬕?p (P ∧ Q) ⊣⊢ ⬕?p P ∧ ⬕?p
 Proof. destruct p; simpl; auto using bare_persistently_and. Qed.
 Lemma bare_persistently_if_or p P Q : ⬕?p (P ∨ Q) ⊣⊢ ⬕?p P ∨ ⬕?p Q.
 Proof. destruct p; simpl; auto using bare_persistently_or. Qed.
-Lemma bare_persistently_if_exist {A} p (Ψ : A → PROP) :
-  (⬕?p ∃ a, Ψ a) ⊣⊢ ∃ a, ⬕?p Ψ a.
+Lemma bare_persistently_if_exist {A} p (Ψ : A → PROP) : (⬕?p ∃ a, Ψ a) ⊣⊢ ∃ a, ⬕?p Ψ a.
 Proof. destruct p; simpl; auto using bare_persistently_exist. Qed.
-Lemma bare_persistently_if_sep p P Q : ⬕?p (P ∗ Q) ⊣⊢ ⬕?p P ∗ ⬕?p Q.
+Lemma bare_persistently_if_sep_2 p P Q : ⬕?p P ∗ ⬕?p Q ⊢ ⬕?p (P ∗ Q).
+Proof. destruct p; simpl; auto using bare_persistently_sep_2. Qed.
+Lemma bare_persistently_if_sep `{PositiveBI PROP} p P Q : ⬕?p (P ∗ Q) ⊣⊢ ⬕?p P ∗ ⬕?p Q.
 Proof. destruct p; simpl; auto using bare_persistently_sep. Qed.
 
 Lemma bare_persistently_if_idemp p P : ⬕?p ⬕?p P ⊣⊢ ⬕?p P.
@@ -1211,7 +1215,7 @@ Proof. intros. rewrite pure_wand_forall. apply _. Qed.
 
 Global Instance sep_persistent P Q :
   Persistent P → Persistent Q → Persistent (P ∗ Q).
-Proof. intros. by rewrite /Persistent persistently_sep -!persistent. Qed.
+Proof. intros. by rewrite /Persistent -persistently_sep_2 -!persistent. Qed.
 
 Global Instance from_option_persistent {A} P (Ψ : A → PROP) (mx : option A) :
   (∀ x, Persistent (Ψ x)) → Persistent P → Persistent (from_option Ψ P mx).
@@ -1294,7 +1298,7 @@ Global Instance bi_persistently_or_homomorphism :
   MonoidHomomorphism bi_or bi_or (≡) (@bi_persistently PROP).
 Proof. split; [split|]; try apply _. apply persistently_or. apply persistently_pure. Qed.
 
-Global Instance bi_persistently_sep_weak_homomorphism :
+Global Instance bi_persistently_sep_weak_homomorphism `{PositiveBI PROP} :
   WeakMonoidHomomorphism bi_sep bi_sep (≡) (@bi_persistently PROP).
 Proof. split; try apply _. apply persistently_sep. Qed.
 
@@ -1304,7 +1308,7 @@ Proof. split. apply _. apply persistently_emp. Qed.
 
 Global Instance bi_persistently_sep_entails_weak_homomorphism :
   WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_persistently PROP).
-Proof. split; try apply _. intros P Q; by rewrite persistently_sep. Qed.
+Proof. split; try apply _. intros P Q; by rewrite persistently_sep_2. Qed.
 
 Global Instance bi_persistently_sep_entails_homomorphism :
   MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_persistently PROP).
@@ -1421,7 +1425,10 @@ Lemma bare_persistently_if_later p P : ⬕?p ▷ P ⊢ ▷ ⬕?p P.
 Proof. destruct p; simpl; auto using bare_persistently_later. Qed.
 
 Global Instance later_persistent P : Persistent P → Persistent (▷ P).
-Proof. intros. by rewrite /Persistent {1}(persistent_persistently_2 P) later_persistently. Qed.
+Proof.
+  intros. by rewrite /Persistent {1}(persistent_persistently_2 P)
+                     later_persistently.
+Qed.
 Global Instance later_absorbing P : Absorbing P → Absorbing (▷ P).
 Proof. intros ? Q. by rewrite {1}(later_intro Q) -later_sep absorbing. Qed.
 
diff --git a/theories/bi/fractional.v b/theories/bi/fractional.v
index 615d996ab..38dc36fd0 100644
--- a/theories/bi/fractional.v
+++ b/theories/bi/fractional.v
@@ -131,14 +131,14 @@ Section fractional.
     FromSep Q P P.
   Proof. rewrite /FromSep=>-[-> <-] [-> _]. by rewrite Qp_div_2. Qed.
 
-  Global Instance into_sep_fractional p P P1 P2 Φ q1 q2 :
+  Global Instance into_sep_fractional P P1 P2 Φ q1 q2 :
     AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
-    IntoSep p P P1 P2.
+    IntoSep P P1 P2.
   Proof. intros. rewrite /IntoSep [P]fractional_split //. Qed.
 
-  Global Instance into_sep_fractional_half p P Q Φ q :
+  Global Instance into_sep_fractional_half P Q Φ q :
     AsFractional P Φ q → AsFractional Q Φ (q/2) →
-    IntoSep p P Q Q | 100.
+    IntoSep P Q Q | 100.
   Proof. intros. rewrite /IntoSep [P]fractional_half //. Qed.
 
   (* The instance [frame_fractional] can be tried at all the nodes of
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 3e59b2983..982881c76 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -99,8 +99,6 @@ Section bi_mixin.
     bi_mixin_wand_intro_r P Q R : (P ∗ Q ⊢ R) → P ⊢ Q -∗ R;
     bi_mixin_wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R;
 
-    bi_mixin_emp_and_sep_assoc_1 Q R : emp ∧ (Q ∗ R) ⊢ (emp ∧ Q) ∗ R;
-
     (* Persistently *)
     bi_mixin_persistently_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q;
     bi_mixin_persistently_idemp_2 P : □ P ⊢ □ □ P;
@@ -401,9 +399,6 @@ Proof. eapply bi_mixin_wand_intro_r, bi_bi_mixin. Qed.
 Lemma wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R.
 Proof. eapply bi_mixin_wand_elim_l', bi_bi_mixin. Qed.
 
-Lemma emp_and_sep_assoc_1 Q R : emp ∧ (Q ∗ R) ⊢ (emp ∧ Q) ∗ R.
-Proof. eapply bi_mixin_emp_and_sep_assoc_1, bi_bi_mixin. Qed.
-
 (* Persistently *)
 Lemma persistently_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q.
 Proof. eapply bi_mixin_persistently_mono, bi_bi_mixin. Qed.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index d1bcf824d..03dffe73a 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -185,8 +185,8 @@ Global Instance into_wand_impl_true_true P Q P' :
   FromAssumption true P P' → IntoWand true true (P' → Q) P Q.
 Proof.
   rewrite /FromAssumption /IntoWand /= => <-. apply wand_intro_l.
-  rewrite -{1}(bare_persistently_idemp P) -bare_persistently_sep -persistently_and_sep.
-  by rewrite impl_elim_r bare_persistently_elim.
+  rewrite -{1}(bare_persistently_idemp P) -and_sep_bare_persistently.
+  by rewrite -bare_persistently_and impl_elim_r bare_persistently_elim.
 Qed.
 
 Global Instance into_wand_and_l p q R1 R2 P' Q' :
@@ -266,10 +266,10 @@ Proof. by rewrite /FromSep pure_and sep_and. Qed.
 
 Global Instance from_sep_bare P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (■ P) (■ Q1) (■ Q2).
-Proof. rewrite /FromSep=> <-. by rewrite bare_sep. Qed.
+Proof. rewrite /FromSep=> <-. by rewrite bare_sep_2. Qed.
 Global Instance from_sep_persistently P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (□ P) (□ Q1) (□ Q2).
-Proof. rewrite /FromSep=> <-. by rewrite persistently_sep. Qed.
+Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
 
 Global Instance from_sep_big_sepL_cons {A} (Φ : nat → A → PROP) x l :
   FromSep ([∗ list] k ↦ y ∈ x :: l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l, Φ (S k) y).
@@ -282,11 +282,8 @@ Proof. by rewrite /FromSep big_opL_app. Qed.
 (* IntoAnd *)
 Global Instance into_and_and p P Q : IntoAnd p (P ∧ Q) P Q.
 Proof. by rewrite /IntoAnd bare_persistently_if_and. Qed.
-Global Instance into_and_sep P Q : IntoAnd true (P ∗ Q) P Q.
-Proof.
-    by rewrite /IntoAnd /= bare_persistently_sep -bare_persistently_sep
-               persistently_and_sep.
-Qed.
+Global Instance into_and_sep `{PositiveBI PROP} P Q : IntoAnd true (P ∗ Q) P Q.
+Proof. by rewrite /IntoAnd /= persistently_sep -and_sep_persistently persistently_and. Qed.
 
 Global Instance into_and_pure p φ ψ : @IntoAnd PROP p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. by rewrite /IntoAnd pure_and bare_persistently_if_and. Qed.
@@ -307,55 +304,44 @@ Proof.
 Qed.
 
 (* IntoSep *)
-Global Instance into_sep_sep p P Q : IntoSep p (P ∗ Q) P Q.
-Proof. by rewrite /IntoSep bare_persistently_if_sep. Qed.
-Global Instance into_sep_and P Q : IntoSep true (P ∧ Q) P Q.
-Proof. by rewrite /IntoSep /= persistently_and_sep. Qed.
+Global Instance into_sep_sep P Q : IntoSep (P ∗ Q) P Q.
+Proof. by rewrite /IntoSep. Qed.
 
 Global Instance into_sep_and_persistent_l P P' Q :
-  Persistent P → FromBare P' P → IntoSep false (P ∧ Q) P' Q.
+  Persistent P → FromBare P' P → IntoSep (P ∧ Q) P' Q.
 Proof.
   rewrite /FromBare /IntoSep /=. intros ? <-.
   by rewrite persistent_and_bare_sep_l_1.
 Qed.
 Global Instance into_sep_and_persistent_r P Q Q' :
-  Persistent Q → FromBare Q' Q → IntoSep false (P ∧ Q) P Q'.
+  Persistent Q → FromBare Q' Q → IntoSep (P ∧ Q) P Q'.
 Proof.
   rewrite /FromBare /IntoSep /=. intros ? <-.
   by rewrite persistent_and_bare_sep_r_1.
 Qed.
 
-Global Instance into_sep_pure p φ ψ : @IntoSep PROP p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
-Proof.
-  by rewrite /IntoSep pure_and persistent_and_sep_1 bare_persistently_if_sep.
-Qed.
 
-Global Instance into_sep_bare p P Q1 Q2 :
-  IntoSep p P Q1 Q2 → IntoSep p (■ P) (■ Q1) (■ Q2).
-Proof.
-  rewrite /IntoSep /=. destruct p; simpl.
-  - by rewrite -bare_sep !persistently_bare.
-  - intros ->. by rewrite bare_sep.
-Qed.
-Global Instance into_sep_persistently p P Q1 Q2 :
-  IntoSep p P Q1 Q2 → IntoSep p (□ P) (□ Q1) (□ Q2).
-Proof.
-  rewrite /IntoSep /=. destruct p; simpl.
-  - by rewrite -persistently_sep !persistently_idemp.
-  - intros ->. by rewrite persistently_sep.
-Qed.
+Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
+Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.
+
+Global Instance into_sep_bare `{PositiveBI PROP} P Q1 Q2 :
+  IntoSep P Q1 Q2 → IntoSep (■ P) (■ Q1) (■ Q2).
+Proof. rewrite /IntoSep /= => ->. by rewrite bare_sep. Qed.
+Global Instance into_sep_persistently `{PositiveBI PROP} P Q1 Q2 :
+  IntoSep P Q1 Q2 → IntoSep (□ P) (□ Q1) (□ Q2).
+Proof. rewrite /IntoSep /= => ->. by rewrite persistently_sep. Qed.
 
 (* We use [IsCons] and [IsApp] to make sure that [frame_big_sepL_cons] and
 [frame_big_sepL_app] cannot be applied repeatedly often when having
 [ [∗ list] k ↦ x ∈ ?e, Φ k x] with [?e] an evar. *)
-Global Instance into_sep_big_sepL_cons {A} p (Φ : nat → A → PROP) l x l' :
+Global Instance into_sep_big_sepL_cons {A} (Φ : nat → A → PROP) l x l' :
   IsCons l x l' →
-  IntoSep p ([∗ list] k ↦ y ∈ l, Φ k y)
+  IntoSep ([∗ list] k ↦ y ∈ l, Φ k y)
     (Φ 0 x) ([∗ list] k ↦ y ∈ l', Φ (S k) y).
 Proof. rewrite /IsCons=>->. by rewrite /IntoSep big_sepL_cons. Qed.
-Global Instance into_sep_big_sepL_app {A} p (Φ : nat → A → PROP) l l1 l2 :
+Global Instance into_sep_big_sepL_app {A} (Φ : nat → A → PROP) l l1 l2 :
   IsApp l l1 l2 →
-  IntoSep p ([∗ list] k ↦ y ∈ l, Φ k y)
+  IntoSep ([∗ list] k ↦ y ∈ l, Φ k y)
     ([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y).
 Proof. rewrite /IsApp=>->. by rewrite /IntoSep big_sepL_app. Qed.
 
@@ -499,7 +485,7 @@ Global Instance frame_sep_persistent_l R P1 P2 Q1 Q2 Q' :
   Frame true R (P1 ∗ P2) Q' | 9.
 Proof.
   rewrite /Frame /MaybeFrame /MakeSep /= => <- <- <-.
-  rewrite {1}(persistently_sep_dup R) bare_sep. solve_sep_entails.
+  rewrite {1}(bare_persistently_sep_dup R). solve_sep_entails.
 Qed.
 Global Instance frame_sep_l R P1 P2 Q Q' :
   Frame false R P1 Q → MakeSep Q P2 Q' → Frame false R (P1 ∗ P2) Q' | 9.
@@ -602,7 +588,10 @@ Proof. by rewrite /MakeBare. Qed.
 
 Global Instance frame_bare R P Q Q' :
   Frame true R P Q → MakeBare Q Q' → Frame true R (■ P) Q'.
-Proof. rewrite /Frame /MakeBare=> <- <- /=. by rewrite bare_sep bare_idemp. Qed.
+Proof.
+  rewrite /Frame /MakeBare=> <- <- /=.
+  by rewrite -{1}bare_idemp bare_sep_2.
+Qed.
 
 Class MakePersistently (P Q : PROP) := make_persistently : □ P ⊣⊢ Q.
 Arguments MakePersistently _%I _%I.
@@ -616,9 +605,9 @@ Proof. by rewrite /MakePersistently. Qed.
 Global Instance frame_persistently R P Q Q' :
   Frame true R P Q → MakePersistently Q Q' → Frame true R (□ P) Q'.
 Proof.
-  rewrite /Frame /MakePersistently=> <- <- /=.
-  by rewrite -persistently_and_bare_sep_l persistently_sep persistently_bare
-             persistently_idemp -persistently_and_sep_l_1.
+  rewrite /Frame /MakePersistently=> <- <- /=. rewrite -persistently_and_bare_sep_l.
+  by rewrite -persistently_sep_2 -persistently_and_sep_l_1 persistently_bare
+              persistently_idemp.
 Qed.
 
 Global Instance frame_exist {A} p R (Φ Ψ : A → PROP) :
@@ -722,24 +711,15 @@ Proof.
 Qed.
 
 (* IntoSep *)
-Global Instance into_sep_later p P Q1 Q2 :
-  IntoSep p P Q1 Q2 → IntoSep p (▷ P) (▷ Q1) (▷ Q2).
-Proof.
-  rewrite /IntoSep=> HP. apply bare_persistently_if_intro'.
-  by rewrite bare_persistently_if_later HP bare_persistently_if_elim later_sep.
-Qed.
-Global Instance into_sep_laterN n p P Q1 Q2 :
-  IntoSep p P Q1 Q2 → IntoSep p (▷^n P) (▷^n Q1) (▷^n Q2).
-Proof.
-  rewrite /IntoSep=> HP. apply bare_persistently_if_intro'.
-  by rewrite bare_persistently_if_laterN HP bare_persistently_if_elim laterN_sep.
-Qed.
-Global Instance into_sep_except_0 p P Q1 Q2 :
-  IntoSep p P Q1 Q2 → IntoSep p (◇ P) (◇ Q1) (◇ Q2).
-Proof.
-  rewrite /IntoSep=> HP. apply bare_persistently_if_intro'.
-  by rewrite bare_persistently_if_except_0 HP bare_persistently_if_elim except_0_sep.
-Qed.
+Global Instance into_sep_later P Q1 Q2 :
+  IntoSep P Q1 Q2 → IntoSep (▷ P) (▷ Q1) (▷ Q2).
+Proof. rewrite /IntoSep=> ->. by rewrite later_sep. Qed.
+Global Instance into_sep_laterN n P Q1 Q2 :
+  IntoSep P Q1 Q2 → IntoSep (▷^n P) (▷^n Q1) (▷^n Q2).
+Proof. rewrite /IntoSep=> ->. by rewrite laterN_sep. Qed.
+Global Instance into_sep_except_0 P Q1 Q2 :
+  IntoSep P Q1 Q2 → IntoSep (◇ P) (◇ Q1) (◇ Q2).
+Proof. rewrite /IntoSep=> ->. by rewrite except_0_sep. Qed.
 
 (* FromOr *)
 Global Instance from_or_later P Q1 Q2 :
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 1f620fb70..d44d6d5f4 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -121,11 +121,11 @@ Arguments IntoAnd {_} _ _%I _%I _%I : simpl never.
 Arguments into_and {_} _ _%I _%I _%I {_}.
 Hint Mode IntoAnd + + ! - - : typeclass_instances.
 
-Class IntoSep {PROP : bi} (p : bool) (P Q1 Q2 : PROP) :=
-  into_sep : ⬕?p P ⊢ ⬕?p (Q1 ∗ Q2).
-Arguments IntoSep {_} _ _%I _%I _%I : simpl never.
-Arguments into_sep {_} _ _%I _%I _%I {_}.
-Hint Mode IntoAnd + + ! - - : typeclass_instances.
+Class IntoSep {PROP : bi} (P Q1 Q2 : PROP) :=
+  into_sep : P ⊢ Q1 ∗ Q2.
+Arguments IntoSep {_} _%I _%I _%I : simpl never.
+Arguments into_sep {_} _%I _%I _%I {_}.
+Hint Mode IntoSep + ! - - : typeclass_instances.
 
 Class FromOr {PROP : bi} (P Q1 Q2 : PROP) := from_or : Q1 ∨ Q2 ⊢ P.
 Arguments FromOr {_} _%I _%I _%I : simpl never.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 428cda55c..817edd512 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -22,7 +22,7 @@ Record envs_wf {PROP} (Δ : envs PROP) := {
 }.
 
 Coercion of_envs {PROP} (Δ : envs PROP) : PROP :=
-  (⌜envs_wf Δ⌝ ∧ ⬕ [∗] env_persistent Δ ∗ [∗] env_spatial Δ)%I.
+  (⌜envs_wf Δ⌝ ∧ ⬕ [∧] env_persistent Δ ∗ [∗] env_spatial Δ)%I.
 Instance: Params (@of_envs) 1.
 Arguments of_envs : simpl never.
 
@@ -126,7 +126,7 @@ Implicit Types Δ : envs PROP.
 Implicit Types P Q : PROP.
 
 Lemma of_envs_eq Δ :
-  of_envs Δ = (⌜envs_wf Δ⌝ ∧ ⬕ [∗] env_persistent Δ ∗ [∗] env_spatial Δ)%I.
+  of_envs Δ = (⌜envs_wf Δ⌝ ∧ ⬕ [∧] env_persistent Δ ∗ [∗] env_spatial Δ)%I.
 Proof. done. Qed.
 
 Lemma envs_lookup_delete_Some Δ Δ' i p P :
@@ -145,7 +145,8 @@ Proof.
   destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
   - rewrite pure_True ?left_id; last (destruct Hwf; constructor;
       naive_solver eauto using env_delete_wf, env_delete_fresh).
-    by rewrite (env_lookup_perm Γp) //= bare_persistently_sep -assoc.
+    rewrite (env_lookup_perm Γp) //= bare_persistently_and.
+    by rewrite and_sep_bare_persistently -assoc.
   - destruct (Γs !! i) eqn:?; simplify_eq/=.
     rewrite pure_True ?left_id; last (destruct Hwf; constructor;
       naive_solver eauto using env_delete_wf, env_delete_fresh).
@@ -165,7 +166,7 @@ Proof.
   rewrite /envs_lookup /of_envs=>?. apply pure_elim_l=> Hwf.
   destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
   - rewrite pure_True // left_id.
-    rewrite (env_lookup_perm Γp) //= bare_persistently_sep.
+    rewrite (env_lookup_perm Γp) //= bare_persistently_and and_sep_bare_persistently.
     cancel [⬕ P]%I. apply wand_intro_l. solve_sep_entails.
   - destruct (Γs !! i) eqn:?; simplify_eq/=.
     rewrite (env_lookup_perm Γs) //=. rewrite pure_True // left_id.
@@ -177,14 +178,15 @@ Lemma envs_lookup_delete_sound Δ Δ' i p P :
 Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound. Qed.
 
 Lemma envs_lookup_delete_list_sound Δ Δ' js rp p Ps :
-  envs_lookup_delete_list js rp Δ = Some (p,Ps,Δ') → Δ ⊢ ⬕?p [∗] Ps ∗ Δ'.
+  envs_lookup_delete_list js rp Δ = Some (p,Ps,Δ') →
+  Δ ⊢ ⬕?p [∗] Ps ∗ Δ'.
 Proof.
   revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=.
   { by rewrite bare_persistently_emp left_id. }
   destruct (envs_lookup_delete j Δ) as [[[q1 P] Δ']|] eqn:Hj; simplify_eq/=.
   apply envs_lookup_delete_Some in Hj as [Hj ->].
   destruct (envs_lookup_delete_list js rp _) as [[[q2 Ps'] ?]|] eqn:?; simplify_eq/=.
-  rewrite bare_persistently_if_sep -assoc. destruct q1; simpl.
+  rewrite -bare_persistently_if_sep_2 -assoc. destruct q1; simpl.
   - destruct rp.
     + rewrite envs_lookup_sound //; simpl.
       by rewrite IH // (bare_persistently_bare_persistently_if q2).
@@ -215,14 +217,15 @@ Proof.
   - apply and_intro; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
       intros j; destruct (strings.string_beq_reflect j i); naive_solver.
-    + by rewrite bare_persistently_sep assoc.
+    + by rewrite bare_persistently_and and_sep_bare_persistently assoc.
   - apply and_intro; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
       intros j; destruct (strings.string_beq_reflect j i); naive_solver.
     + solve_sep_entails.
 Qed.
 
-Lemma envs_app_sound Δ Δ' p Γ : envs_app p Γ Δ = Some Δ' → Δ ⊢ ⬕?p [∗] Γ -∗ Δ'.
+Lemma envs_app_sound Δ Δ' p Γ :
+  envs_app p Γ Δ = Some Δ' → Δ ⊢ (if p then ⬕ [∧] Γ else [∗] Γ) -∗ Δ'.
 Proof.
   rewrite /of_envs /envs_app=> ?; apply pure_elim_l=> Hwf.
   destruct Δ as [Γp Γs], p; simplify_eq/=.
@@ -233,7 +236,8 @@ Proof.
       intros j. apply (env_app_disjoint _ _ _ j) in Happ.
       naive_solver eauto using env_app_fresh.
     + rewrite (env_app_perm _ _ Γp') //.
-      rewrite big_opL_app bare_persistently_sep. solve_sep_entails.
+      rewrite big_opL_app bare_persistently_and and_sep_bare_persistently.
+      solve_sep_entails.
   - destruct (env_app Γ Γp) eqn:Happ,
       (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
     apply wand_intro_l, and_intro; [apply pure_intro|].
@@ -243,9 +247,13 @@ Proof.
     + rewrite (env_app_perm _ _ Γs') // big_opL_app. solve_sep_entails.
 Qed.
 
+Lemma envs_app_singleton_sound Δ Δ' p j Q :
+  envs_app p (Esnoc Enil j Q) Δ = Some Δ' → Δ ⊢ ⬕?p Q -∗ Δ'.
+Proof. move=> /envs_app_sound. destruct p; by rewrite /= right_id. Qed.
+
 Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
   envs_simple_replace i p Γ Δ = Some Δ' →
-  envs_delete i p Δ ⊢ ⬕?p [∗] Γ -∗ Δ'.
+  envs_delete i p Δ ⊢ (if p then ⬕ [∧] Γ else [∗] Γ) -∗ Δ'.
 Proof.
   rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
   apply pure_elim_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
@@ -256,7 +264,8 @@ Proof.
       intros j. apply (env_app_disjoint _ _ _ j) in Happ.
       destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
     + rewrite (env_replace_perm _ _ Γp') //.
-      rewrite big_opL_app bare_persistently_sep. solve_sep_entails.
+      rewrite big_opL_app bare_persistently_and and_sep_bare_persistently.
+      solve_sep_entails.
   - destruct (env_app Γ Γp) eqn:Happ,
       (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
     apply wand_intro_l, and_intro; [apply pure_intro|].
@@ -266,24 +275,49 @@ Proof.
     + rewrite (env_replace_perm _ _ Γs') // big_opL_app. solve_sep_entails.
 Qed.
 
+Lemma envs_simple_replace_singleton_sound' Δ Δ' i p j Q :
+  envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' →
+  envs_delete i p Δ ⊢ ⬕?p Q -∗ Δ'.
+Proof. move=> /envs_simple_replace_sound'. destruct p; by rewrite /= right_id. Qed.
+
 Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
   envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' →
-  Δ ⊢ ⬕?p P ∗ (⬕?p [∗] Γ -∗ Δ').
+  Δ ⊢ ⬕?p P ∗ ((if p then ⬕ [∧] Γ else [∗] Γ) -∗ Δ').
 Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.
 
+Lemma envs_simple_replace_singleton_sound Δ Δ' i p P j Q :
+  envs_lookup i Δ = Some (p,P) →
+  envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' →
+  Δ ⊢ ⬕?p P ∗ (⬕?p Q -∗ Δ').
+Proof.
+  intros. by rewrite envs_lookup_sound// envs_simple_replace_singleton_sound'//.
+Qed.
+
 Lemma envs_replace_sound' Δ Δ' i p q Γ :
-  envs_replace i p q Γ Δ = Some Δ' → envs_delete i p Δ ⊢ ⬕?q [∗] Γ -∗ Δ'.
+  envs_replace i p q Γ Δ = Some Δ' →
+  envs_delete i p Δ ⊢ (if q then ⬕ [∧] Γ else [∗] Γ) -∗ Δ'.
 Proof.
   rewrite /envs_replace; destruct (eqb _ _) eqn:Hpq.
   - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
   - apply envs_app_sound.
 Qed.
 
+Lemma envs_replace_singleton_sound' Δ Δ' i p q j Q :
+  envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' →
+  envs_delete i p Δ ⊢ ⬕?q Q -∗ Δ'.
+Proof. move=> /envs_replace_sound'. destruct q; by rewrite /= ?right_id. Qed.
+
 Lemma envs_replace_sound Δ Δ' i p q P Γ :
   envs_lookup i Δ = Some (p,P) → envs_replace i p q Γ Δ = Some Δ' →
-  Δ ⊢ ⬕?p P ∗ (⬕?q [∗] Γ -∗ Δ').
+  Δ ⊢ ⬕?p P ∗ ((if q then ⬕ [∧] Γ else [∗] Γ) -∗ Δ').
 Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.
 
+Lemma envs_replace_singleton_sound Δ Δ' i p q P j Q :
+  envs_lookup i Δ = Some (p,P) →
+  envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' →
+  Δ ⊢ ⬕?p P ∗ (⬕?q Q -∗ Δ').
+Proof. intros. by rewrite envs_lookup_sound// envs_replace_singleton_sound'//. Qed.
+
 Lemma envs_lookup_envs_clear_spatial Δ j :
   envs_lookup j (envs_clear_spatial Δ)
   = '(p,P) ← envs_lookup j Δ; if p then Some (p,P) else None.
@@ -396,7 +430,7 @@ Proof. by constructor. Qed.
 (** * Adequacy *)
 Lemma tac_adequate P : (Envs Enil Enil ⊢ P) → P.
 Proof.
-  intros <-. rewrite /of_envs /= bare_persistently_emp left_id.
+  intros <-. rewrite /of_envs /= persistently_True_emp bare_persistently_emp left_id.
   apply and_intro=> //. apply pure_intro; repeat constructor.
 Qed.
 
@@ -437,8 +471,8 @@ Lemma tac_rename Δ Δ' i j p P Q :
   envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros. rewrite envs_simple_replace_sound //.
-  destruct p; simpl; by rewrite right_id wand_elim_r.
+  intros. rewrite envs_simple_replace_singleton_sound //.
+  by rewrite wand_elim_r.
 Qed.
 
 Lemma tac_clear Δ Δ' i p P Q :
@@ -501,33 +535,44 @@ Lemma tac_persistent Δ Δ' i p P P' Q :
   envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros ???? <-. rewrite envs_replace_sound //; simpl.
-  rewrite right_id. apply wand_elim_r', wand_mono=> //. destruct p; simpl.
+  intros ???? <-. rewrite envs_replace_singleton_sound //; simpl.
+  apply wand_elim_r', wand_mono=> //. destruct p; simpl.
   - by rewrite -(into_persistent _ P).
   - by rewrite -(into_persistent _ P) /= affine_bare.
 Qed.
 
 (** * Implication and wand *)
+Lemma envs_app_singleton_sound_foo Δ Δ' p j Q :
+  envs_app p (Esnoc Enil j Q) Δ = Some Δ' → Δ ∗ ⬕?p Q ⊢ Δ'.
+Proof. intros. apply wand_elim_l'. eapply envs_app_singleton_sound. eauto. Qed.
+
 Lemma tac_impl_intro Δ Δ' i P Q :
   (if env_spatial_is_nil Δ then TCTrue else Persistent P) →
   envs_app false (Esnoc Enil i P) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ P → Q.
 Proof.
   intros ?? <-. destruct (env_spatial_is_nil Δ) eqn:?.
-  - rewrite (env_spatial_is_nil_bare_persistently Δ) // envs_app_sound //; simpl.
-    rewrite right_id. apply impl_intro_l. rewrite bare_and_l persistently_and_sep_r_1.
-    by rewrite bare_sep bare_persistently_elim bare_elim wand_elim_r.
-  - apply impl_intro_l. rewrite envs_app_sound //; simpl.
-    by rewrite persistent_and_sep_1 right_id wand_elim_r.
+  - rewrite (env_spatial_is_nil_bare_persistently Δ) //; simpl. apply impl_intro_l.
+    rewrite envs_app_singleton_sound //; simpl.
+    by rewrite bare_elim persistently_and_bare_sep_r bare_persistently_elim wand_elim_r.
+  - apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl.
+    by rewrite persistent_and_sep_1 wand_elim_r.
 Qed.
 Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
   IntoPersistent false P P' →
   envs_app true (Esnoc Enil i P') Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ P → Q.
 Proof.
-  intros ?? <-. rewrite envs_app_sound //; simpl. apply impl_intro_l.
+  intros ?? <-. rewrite envs_app_singleton_sound //; simpl. apply impl_intro_l.
   rewrite (_ : P = â–¡?false P)%I // (into_persistent false P).
-  by rewrite right_id persistently_and_bare_sep_l wand_elim_r.
+  by rewrite persistently_and_bare_sep_l wand_elim_r.
+Qed.
+Lemma tac_pure_impl_intro Δ (φ ψ : Prop) :
+  (φ → Δ ⊢ ⌜ψ⌝) → Δ ⊢ ⌜φ → ψ⌝.
+Proof. intros. rewrite pure_impl. by apply impl_intro_l, pure_elim_l. Qed.
+Lemma tac_impl_intro_pure Δ P φ Q : IntoPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ P → Q.
+Proof.
+  intros. apply impl_intro_l. rewrite (into_pure P). by apply pure_elim_l.
 Qed.
 
 Lemma tac_impl_intro_drop Δ P Q : (Δ ⊢ Q) → Δ ⊢ P → Q.
@@ -544,9 +589,16 @@ Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
   envs_app true (Esnoc Enil i P') Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ P -∗ Q.
 Proof.
-  intros ??? <-. rewrite envs_app_sound //; simpl.
-  rewrite right_id. apply wand_mono=>//.
-  by rewrite -(into_persistent _ P) /= affine_bare.
+  intros ??? <-. rewrite envs_app_singleton_sound //; simpl.
+  apply wand_mono=>//. by rewrite -(into_persistent _ P) /= affine_bare.
+Qed.
+Lemma tac_wand_intro_pure Δ P φ Q :
+  IntoPure P φ →
+  Affine P →
+  (φ → Δ ⊢ Q) → Δ ⊢ P -∗ Q.
+Proof.
+  intros. apply wand_intro_l. rewrite -(affine_bare P) (into_pure P).
+  rewrite -persistent_and_bare_sep_l. by apply pure_elim_l.
 Qed.
 Lemma tac_wand_intro_drop Δ P Q :
   TCOr (Affine P) (Absorbing Q) →
@@ -568,13 +620,14 @@ Lemma tac_specialize Δ Δ' Δ'' i p j q P1 P2 R Q :
   (Δ'' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
-  - rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
+  - rewrite envs_lookup_persistent_sound //.
+    rewrite envs_simple_replace_singleton_sound //; simpl.
     rewrite -bare_persistently_if_idemp -bare_persistently_idemp into_wand /=.
-    rewrite assoc (bare_persistently_bare_persistently_if q) -bare_persistently_if_sep wand_elim_r.
-    by rewrite right_id wand_elim_r.
+    rewrite assoc (bare_persistently_bare_persistently_if q).
+    by rewrite bare_persistently_if_sep_2 wand_elim_r wand_elim_r.
   - rewrite envs_lookup_sound //; simpl.
-    rewrite envs_lookup_sound // (envs_replace_sound' _ Δ'') //; simpl.
-    by rewrite into_wand /= assoc wand_elim_r right_id wand_elim_r.
+    rewrite envs_lookup_sound // (envs_replace_singleton_sound' _ Δ'') //; simpl.
+    by rewrite into_wand /= assoc wand_elim_r wand_elim_r.
 Qed.
 
 Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
@@ -590,9 +643,9 @@ Proof.
   destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
     destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
   rewrite envs_lookup_sound // envs_split_sound //.
-  rewrite (envs_app_sound Δ2) //; simpl.
+  rewrite (envs_app_singleton_sound Δ2) //; simpl.
   rewrite HP1 into_wand /= -(elim_modal P1' P1 Q Q). cancel [P1'].
-  apply wand_intro_l. by rewrite assoc right_id !wand_elim_r.
+  apply wand_intro_l. by rewrite assoc !wand_elim_r.
 Qed.
 
 Lemma tac_unlock P Q : (P ⊢ Q) → P ⊢ locked Q.
@@ -619,10 +672,10 @@ Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
   envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' →
   φ → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros. rewrite envs_simple_replace_sound //; simpl.
+  intros. rewrite envs_simple_replace_singleton_sound //; simpl.
   rewrite -bare_persistently_if_idemp into_wand /= -(from_pure P1).
   rewrite pure_True // persistently_pure bare_True_emp bare_emp.
-  by rewrite emp_wand right_id wand_elim_r.
+  by rewrite emp_wand wand_elim_r.
 Qed.
 
 Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P2 R Q :
@@ -635,10 +688,10 @@ Proof.
   intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
   rewrite envs_lookup_sound //.
   rewrite -(idemp bi_and (envs_delete _ _ _)).
-  rewrite {2}envs_simple_replace_sound' //; rewrite /= right_id.
+  rewrite {2}envs_simple_replace_singleton_sound' //; simpl.
   rewrite {1}HP1 (persistent_persistently_2 P1) persistently_and_bare_sep_l assoc.
   rewrite -bare_persistently_if_idemp -bare_persistently_idemp.
-  rewrite (bare_persistently_bare_persistently_if q) -bare_persistently_if_sep.
+  rewrite (bare_persistently_bare_persistently_if q) bare_persistently_if_sep_2.
   by rewrite into_wand wand_elim_l wand_elim_r.
 Qed.
 
@@ -646,15 +699,16 @@ Lemma tac_specialize_persistent_helper Δ Δ'' j q P R R' Q :
   envs_lookup j Δ = Some (q,P) →
   (Δ ⊢ R) →
   IntoPersistent false R R' →
-  (if q then TCTrue else Affine R) →
+  (if q then TCTrue else TCAnd (PositiveBI PROP) (Affine R)) →
   envs_replace j q true (Esnoc Enil j R') Δ = Some Δ'' →
   (Δ'' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros ? HR ??? <-. rewrite -(idemp bi_and Δ) {1}HR.
-  rewrite envs_replace_sound //; rewrite /= right_id. destruct q; simpl.
+  intros ? HR ? Hpos ? <-. rewrite -(idemp bi_and Δ) {1}HR.
+  rewrite envs_replace_singleton_sound //; destruct q; simpl.
   - rewrite (_ : R = â–¡?false R)%I // (into_persistent _ R).
     by rewrite sep_elim_r persistently_and_bare_sep_l wand_elim_r.
-  - rewrite -(affine_bare R) (_ : R = â–¡?false R)%I // (into_persistent _ R).
+  - destruct Hpos.
+    rewrite -(affine_bare R) (_ : R = â–¡?false R)%I // (into_persistent _ R).
     rewrite bare_and_r -bare_and_l bare_sep sep_elim_r bare_elim.
     by rewrite persistently_and_bare_sep_l wand_elim_r.
 Qed.
@@ -697,8 +751,7 @@ Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P P' Q :
   (Δ1 ⊢ P') → (Δ2' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ??? HP HQ. rewrite envs_split_sound //.
-  rewrite (envs_app_sound Δ2) //; simpl.
-  by rewrite right_id HP HQ.
+  rewrite (envs_app_singleton_sound Δ2) //; simpl. by rewrite HP HQ.
 Qed.
 
 Lemma tac_assert_persistent Δ Δ1 Δ2 Δ' lr js j P P' Q :
@@ -711,8 +764,7 @@ Proof.
   intros ???? HP <-. rewrite -(idemp bi_and Δ) {1}envs_split_sound //.
   rewrite HP. rewrite (persistent_persistently_2 P) sep_elim_l.
   rewrite persistently_and_bare_sep_l -bare_idemp bare_persistently_elim from_bare.
-  rewrite envs_app_sound //; simpl.
-  by rewrite right_id wand_elim_r.
+  rewrite envs_app_singleton_sound //; simpl. by rewrite wand_elim_r.
 Qed.
 
 Lemma tac_assert_pure Δ Δ' j P P' φ Q :
@@ -721,8 +773,8 @@ Lemma tac_assert_pure Δ Δ' j P P' φ Q :
   envs_app false (Esnoc Enil j P') Δ = Some Δ' →
   φ → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros ???? <-. rewrite envs_app_sound //; simpl.
-  rewrite right_id -(from_bare P') -(from_pure P) pure_True //.
+  intros ???? <-. rewrite envs_app_singleton_sound //; simpl.
+  rewrite -(from_bare P') -(from_pure P) pure_True //.
   by rewrite bare_True_emp bare_emp emp_wand.
 Qed.
 
@@ -731,8 +783,8 @@ Lemma tac_pose_proof Δ Δ' j P Q :
   envs_app true (Esnoc Enil j P) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros HP ? <-. rewrite envs_app_sound //; simpl.
-  by rewrite right_id -HP bare_persistently_emp emp_wand.
+  intros HP ? <-. rewrite envs_app_singleton_sound //; simpl.
+  by rewrite -HP bare_persistently_emp emp_wand.
 Qed.
 
 Lemma tac_pose_proof_hyp Δ Δ' Δ'' i p j P Q :
@@ -741,10 +793,10 @@ Lemma tac_pose_proof_hyp Δ Δ' Δ'' i p j P Q :
   (Δ'' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros [? ->]%envs_lookup_delete_Some ? <-. destruct p.
-  - rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl.
-    by rewrite right_id wand_elim_r.
-  - rewrite envs_lookup_sound // envs_app_sound //; simpl.
-    by rewrite right_id wand_elim_r.
+  - rewrite envs_lookup_persistent_sound // envs_app_singleton_sound //; simpl.
+    by rewrite wand_elim_r.
+  - rewrite envs_lookup_sound // envs_app_singleton_sound //; simpl.
+    by rewrite wand_elim_r.
 Qed.
 
 Lemma tac_apply Δ Δ' i p R P1 P2 :
@@ -783,8 +835,8 @@ Lemma tac_rewrite_in Δ i p Pxy j q P (lr : bool) Q :
 Proof.
   intros ?? A Δ' x y Φ HPxy HP ?? <-.
   rewrite -(idemp bi_and Δ) {2}(envs_lookup_sound _ i) //.
-  rewrite (envs_simple_replace_sound _ _ j) //; simpl.
-  rewrite HP right_id HPxy (bare_persistently_if_elim _ (_ ≡ _)%I) sep_elim_l.
+  rewrite (envs_simple_replace_singleton_sound _ _ j) //; simpl.
+  rewrite HP HPxy (bare_persistently_if_elim _ (_ ≡ _)%I) sep_elim_l.
   rewrite persistent_and_bare_sep_r -assoc. apply wand_elim_r'.
   rewrite -persistent_and_bare_sep_r. apply impl_elim_r'. destruct lr.
   - apply (internal_eq_rewrite x y (λ y, ⬕?q Φ y -∗ Δ')%I). solve_proper.
@@ -825,18 +877,20 @@ Lemma tac_combine Δ1 Δ2 Δ3 js p Ps j P Q :
   (Δ3 ⊢ Q) → Δ1 ⊢ Q.
 Proof.
   intros ??? <-. rewrite envs_lookup_delete_list_sound //.
-  rewrite from_seps. rewrite envs_app_sound //; simpl.
-  by rewrite right_id wand_elim_r.
+  rewrite from_seps. rewrite envs_app_singleton_sound //; simpl.
+  by rewrite wand_elim_r.
 Qed.
 
 (** * Conjunction/separating conjunction elimination *)
 Lemma tac_and_destruct Δ Δ' i p j1 j2 P P1 P2 Q :
-  envs_lookup i Δ = Some (p, P) → IntoSep p P P1 P2 →
+  envs_lookup i Δ = Some (p, P) →
+  (if p then IntoAnd true P P1 P2 else IntoSep P P1 P2) →
   envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros. rewrite envs_simple_replace_sound //; simpl.
-  by rewrite (into_sep _ P) right_id -(comm _ P1) wand_elim_r.
+  intros. rewrite envs_simple_replace_sound //; simpl. destruct p.
+  - by rewrite (into_and _ P) /= right_id -(comm _ P1) wand_elim_r.
+  - by rewrite (into_sep P) right_id -(comm _ P1) wand_elim_r.
 Qed.
 
 (* Using this tactic, one can destruct a (non-separating) conjunction in the
@@ -844,23 +898,25 @@ spatial context as long as one of the conjuncts is thrown away. It corresponds
 to the principle of "external choice" in linear logic. *)
 Lemma tac_and_destruct_choice Δ Δ' i p (lr : bool) j P P1 P2 Q :
   envs_lookup i Δ = Some (p, P) →
-  TCOr (IntoAnd p P P1 P2) (TCAnd (IntoSep p P P1 P2)
-    (if p then TCTrue
-     else if lr then TCOr (Affine P2) (Absorbing Q)
-     else TCOr (Affine P1) (Absorbing Q))) →
+  (if p then IntoAnd p P P1 P2 : Type else
+    TCOr (IntoAnd p P P1 P2) (TCAnd (IntoSep P P1 P2)
+      (if lr then TCOr (Affine P2) (Absorbing Q)
+       else TCOr (Affine P1) (Absorbing Q)))) →
   envs_simple_replace i p (Esnoc Enil j (if lr then P1 else P2)) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros ? HP ? HQ. rewrite envs_simple_replace_sound //; simpl.
+  intros ? HP ? HQ. rewrite envs_simple_replace_singleton_sound //; simpl.
+  destruct p.
+  { rewrite (into_and _ P) HQ. destruct lr; simpl.
+    - by rewrite and_elim_l wand_elim_r.
+    - by rewrite and_elim_r wand_elim_r. }
   destruct HP as [?|[??]].
-  - rewrite (into_and _ P) right_id  HQ. destruct lr.
-    + by rewrite and_elim_l wand_elim_r.
-    + by rewrite and_elim_r wand_elim_r.
-  - rewrite (into_sep _ P) right_id HQ bare_persistently_if_sep. destruct p, lr; simpl.
-    + by rewrite (sep_elim_l (⬕ P1)%I) wand_elim_r.
-    + by rewrite (sep_elim_r (⬕ P1)%I) wand_elim_r.
-    + by rewrite (comm _ P1) -assoc wand_elim_r sep_elim_r.
-    + by rewrite -assoc wand_elim_r sep_elim_r.
+  { rewrite (into_and _ P) HQ. destruct lr; simpl.
+    - by rewrite and_elim_l wand_elim_r.
+    - by rewrite and_elim_r wand_elim_r. }
+  rewrite (into_sep P) HQ. destruct lr; simpl.
+  - by rewrite (comm _ P1) -assoc wand_elim_r sep_elim_r.
+  - by rewrite -assoc wand_elim_r sep_elim_r.
 Qed.
 
 (** * Framing *)
@@ -895,10 +951,10 @@ Lemma tac_or_destruct Δ Δ1 Δ2 i p j1 j2 P P1 P2 Q :
 Proof.
   intros ???? HP1 HP2. rewrite envs_lookup_sound //.
   rewrite (into_or P) bare_persistently_if_or sep_or_r; apply or_elim.
-  - rewrite (envs_simple_replace_sound' _ Δ1) //.
-    by rewrite /= right_id wand_elim_r.
-  - rewrite (envs_simple_replace_sound' _ Δ2) //.
-    by rewrite /= right_id wand_elim_r.
+  - rewrite (envs_simple_replace_singleton_sound' _ Δ1) //.
+    by rewrite wand_elim_r.
+  - rewrite (envs_simple_replace_singleton_sound' _ Δ2) //.
+    by rewrite wand_elim_r.
 Qed.
 
 (** * Forall *)
@@ -915,8 +971,8 @@ Lemma tac_forall_specialize {A} Δ Δ' i p P (Φ : A → PROP) Q :
     (Δ' ⊢ Q)) →
   Δ ⊢ Q.
 Proof.
-  intros ?? (x&?&?). rewrite envs_simple_replace_sound //; simpl.
-  by rewrite right_id (into_forall P) (forall_elim x) wand_elim_r.
+  intros ?? (x&?&?). rewrite envs_simple_replace_singleton_sound //; simpl.
+  by rewrite (into_forall P) (forall_elim x) wand_elim_r.
 Qed.
 
 Lemma tac_forall_revert {A} Δ (Φ : A → PROP) :
@@ -937,7 +993,7 @@ Proof.
   intros ?? HΦ. rewrite envs_lookup_sound //.
   rewrite (into_exist P) bare_persistently_if_exist sep_exist_r.
   apply exist_elim=> a; destruct (HΦ a) as (Δ'&?&?).
-  rewrite envs_simple_replace_sound' //; simpl. by rewrite right_id wand_elim_r.
+  rewrite envs_simple_replace_singleton_sound' //; simpl. by rewrite wand_elim_r.
 Qed.
 
 (** * Modalities *)
@@ -950,8 +1006,8 @@ Lemma tac_modal_elim Δ Δ' i p P' P Q Q' :
   envs_replace i p false (Esnoc Enil i P') Δ = Some Δ' →
   (Δ' ⊢ Q') → Δ ⊢ Q.
 Proof.
-  intros ??? HΔ. rewrite envs_replace_sound //; simpl.
-  rewrite right_id HΔ bare_persistently_if_elim. by apply elim_modal.
+  intros ??? HΔ. rewrite envs_replace_singleton_sound //; simpl.
+  rewrite HΔ bare_persistently_if_elim. by apply elim_modal.
 Qed.
 End bi_tactics.
 
@@ -990,7 +1046,7 @@ Proof.
   - apply pure_mono; destruct 1; constructor;
       naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
   - apply bare_mono, persistently_mono.
-    induction Hp; rewrite /= ?laterN_sep. apply laterN_intro. by apply sep_mono.
+    induction Hp; rewrite /= ?laterN_and. apply laterN_intro. by apply and_mono.
   - induction Hs; rewrite /= ?laterN_sep. apply laterN_intro. by apply sep_mono.
 Qed.
 
@@ -1006,8 +1062,8 @@ Proof.
   intros ?? HQ. rewrite (env_spatial_is_nil_bare_persistently Δ) //.
   rewrite -(persistently_and_emp_elim Q). apply and_intro; first apply: affine.
   rewrite -(löb (□ Q)%I) later_persistently. apply impl_intro_l.
-  rewrite envs_app_sound //; simpl; rewrite HQ right_id.
-  rewrite persistently_and_bare_sep_l -{1}bare_persistently_idemp -bare_persistently_sep.
+  rewrite envs_app_singleton_sound //; simpl; rewrite HQ.
+  rewrite persistently_and_bare_sep_l -{1}bare_persistently_idemp bare_persistently_sep_2.
   by rewrite wand_elim_r bare_elim.
 Qed.
 End sbi_tactics.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 03f23388f..51eb5eabd 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -531,8 +531,9 @@ Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) :=
       quantifiers are instantiated. *)
       let pat := spec_pat.parse pat in
       lazymatch eval compute in
-        (bool_decide (pat ≠ []) && p && negb (existsb spec_pat_modal pat)) with
+        (p && bool_decide (pat ≠ []) && negb (existsb spec_pat_modal pat)) with
       | true =>
+         (* FIXME: do something reasonable when the BI is not positive *)
          eapply tac_specialize_persistent_helper with _ H _ _ _ _;
            [env_reflexivity || fail "iSpecialize:" H "not found"
            |iSpecializePat H pat; last (iExact H)
@@ -540,7 +541,7 @@ Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) :=
             let Q := match goal with |- IntoPersistent _ ?Q _ => Q end in
             fail "iSpecialize:" Q "not persistent"
            |env_cbv; apply _ ||
-            let Q := match goal with |- Affine ?Q => Q end in
+            let Q := match goal with |- TCAnd _ (Affine ?Q) => Q end in
             fail "iSpecialize:" Q "not affine"
            |env_reflexivity
            |(* goal *)]
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index d2b31fd4c..7aaec057b 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -44,9 +44,9 @@ Lemma test_unfold_constants : bar.
 Proof. iIntros (P) "HP //". Qed.
 
 Lemma test_iRewrite {A : ofeT} (x y : A) P :
-  (∀ z, P -∗ ■ (z ≡ y)) -∗ (P -∗ P ∧ (x,x) ≡ (y,x)).
+  ⬕ (∀ z, P -∗ ■ (z ≡ y)) -∗ (P -∗ P ∧ (x,x) ≡ (y,x)).
 Proof.
-  iIntros "H1 H2".
+  iIntros "#H1 H2".
   iRewrite (bi.internal_eq_sym x x with "[# //]").
   iRewrite -("H1" $! _ with "[- //]").
   auto.
-- 
GitLab