From 2a92f2659d05f5ea4d51226d865b02be143e4e1b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 24 Oct 2017 17:42:07 +0200
Subject: [PATCH] Replace/remove some occurences of `persistently` into
 `persistent` where the property instead of the modality is used.

---
 theories/base_logic/big_op.v         | 12 ++--
 theories/base_logic/derived.v        | 84 ++++++++++++++--------------
 theories/base_logic/lib/fractional.v |  2 +-
 theories/base_logic/lib/own.v        |  2 +-
 theories/base_logic/lib/viewshifts.v |  2 +-
 theories/proofmode/class_instances.v | 42 +++++++-------
 theories/proofmode/classes.v         |  4 +-
 theories/proofmode/coq_tactics.v     | 20 +++----
 8 files changed, 82 insertions(+), 86 deletions(-)

diff --git a/theories/base_logic/big_op.v b/theories/base_logic/big_op.v
index 65b9f2391..6079c922a 100644
--- a/theories/base_logic/big_op.v
+++ b/theories/base_logic/big_op.v
@@ -134,7 +134,7 @@ Section list.
       apply impl_intro_l, pure_elim_l=> ?; by apply big_sepL_lookup. }
     revert Φ HΦ. induction l as [|x l IH]=> Φ HΦ.
     { rewrite big_sepL_nil; auto with I. }
-    rewrite big_sepL_cons. rewrite -persistently_and_sep_l; apply and_intro.
+    rewrite big_sepL_cons. rewrite -and_sep_l; apply and_intro.
     - by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
     - rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)).
   Qed.
@@ -146,7 +146,7 @@ Section list.
     rewrite persistently_and_sep_l. do 2 setoid_rewrite persistently_forall.
     setoid_rewrite persistently_impl; setoid_rewrite persistently_pure.
     rewrite -big_sepL_forall -big_sepL_sepL. apply big_sepL_mono; auto=> k x ?.
-    by rewrite -persistently_wand_impl persistently_elim wand_elim_l.
+    by rewrite persistently_impl_wand persistently_elim wand_elim_l.
   Qed.
 
   Global Instance big_sepL_nil_persistent Φ :
@@ -323,7 +323,7 @@ Section gmap.
     { apply forall_intro=> k; apply forall_intro=> x.
       apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
     induction m as [|i x m ? IH] using map_ind; [rewrite ?big_sepM_empty; auto|].
-    rewrite big_sepM_insert // -persistently_and_sep_l. apply and_intro.
+    rewrite big_sepM_insert // -and_sep_l. apply and_intro.
     - rewrite (forall_elim i) (forall_elim x) lookup_insert.
       by rewrite pure_True // True_impl.
     - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
@@ -339,7 +339,7 @@ Section gmap.
     rewrite persistently_and_sep_l. do 2 setoid_rewrite persistently_forall.
     setoid_rewrite persistently_impl; setoid_rewrite persistently_pure.
     rewrite -big_sepM_forall -big_sepM_sepM. apply big_sepM_mono; auto=> k x ?.
-    by rewrite -persistently_wand_impl persistently_elim wand_elim_l.
+    by rewrite persistently_impl_wand persistently_elim wand_elim_l.
   Qed.
 
   Global Instance big_sepM_empty_persistent Φ :
@@ -475,7 +475,7 @@ Section gset.
       apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
     induction X as [|x X ? IH] using collection_ind_L.
     { rewrite big_sepS_empty; auto. }
-    rewrite big_sepS_insert // -persistently_and_sep_l. apply and_intro.
+    rewrite big_sepS_insert // -and_sep_l. apply and_intro.
     - by rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
     - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
       by rewrite pure_True ?True_impl; last set_solver.
@@ -487,7 +487,7 @@ Section gset.
     rewrite persistently_and_sep_l persistently_forall.
     setoid_rewrite persistently_impl; setoid_rewrite persistently_pure.
     rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?.
-    by rewrite -persistently_wand_impl persistently_elim wand_elim_l.
+    by rewrite persistently_impl_wand persistently_elim wand_elim_l.
   Qed.
 
   Global Instance big_sepS_empty_persistent Φ : Persistent ([∗ set] x ∈ ∅, Φ x).
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 1839c214e..0875fde43 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -432,7 +432,7 @@ Qed.
 
 Lemma sep_and P Q : (P ∗ Q) ⊢ (P ∧ Q).
 Proof. auto. Qed.
-Lemma impl_wand P Q : (P → Q) ⊢ P -∗ Q.
+Lemma impl_wand_1 P Q : (P → Q) ⊢ P -∗ Q.
 Proof. apply wand_intro_r, impl_elim with P; auto. Qed.
 Lemma pure_elim_sep_l φ Q R : (φ → Q ⊢ R) → ⌜φ⌝ ∗ Q ⊢ R.
 Proof. intros; apply pure_elim with φ; eauto. Qed.
@@ -518,38 +518,38 @@ Proof.
   rewrite -(internal_eq_refl a) persistently_pure; auto.
 Qed.
 
-Lemma persistently_and_sep_l' P Q : □ P ∧ Q ⊣⊢ □ P ∗ Q.
+Lemma persistently_and_sep_l P Q : □ P ∧ Q ⊣⊢ □ P ∗ Q.
 Proof. apply (anti_symm (⊢)); auto using persistently_and_sep_l_1. Qed.
-Lemma persistently_and_sep_r' P Q : P ∧ □ Q ⊣⊢ P ∗ □ Q.
-Proof. by rewrite !(comm _ P) persistently_and_sep_l'. Qed.
-Lemma persistently_sep_dup' P : □ P ⊣⊢ □ P ∗ □ P.
-Proof. by rewrite -persistently_and_sep_l' idemp. Qed.
+Lemma persistently_and_sep_r P Q : P ∧ □ Q ⊣⊢ P ∗ □ Q.
+Proof. by rewrite !(comm _ P) persistently_and_sep_l. Qed.
+Lemma persistently_sep_dup P : □ P ⊣⊢ □ P ∗ □ P.
+Proof. by rewrite -persistently_and_sep_l idemp. Qed.
 
 Lemma persistently_and_sep P Q : □ (P ∧ Q) ⊣⊢ □ (P ∗ Q).
 Proof.
   apply (anti_symm (⊢)); auto.
-  rewrite -{1}persistently_idemp persistently_and persistently_and_sep_l'; auto.
+  rewrite -{1}persistently_idemp persistently_and persistently_and_sep_l; auto.
 Qed.
 Lemma persistently_sep P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
-Proof. by rewrite -persistently_and_sep -persistently_and_sep_l' persistently_and. Qed.
+Proof. by rewrite -persistently_and_sep -persistently_and_sep_l persistently_and. Qed.
 
 Lemma persistently_wand P Q : □ (P -∗ Q) ⊢ □ P -∗ □ Q.
 Proof. by apply wand_intro_r; rewrite -persistently_sep wand_elim_l. Qed.
-Lemma persistently_wand_impl P Q : □ (P -∗ Q) ⊣⊢ □ (P → Q).
+Lemma persistently_impl_wand P Q : □ (P → Q) ⊣⊢ □ (P -∗ Q).
 Proof.
-  apply (anti_symm (⊢)); [|by rewrite -impl_wand].
+  apply (anti_symm (⊢)); [by rewrite -impl_wand_1|].
   apply persistently_intro', impl_intro_r.
-  by rewrite persistently_and_sep_l' persistently_elim wand_elim_l.
+  by rewrite persistently_and_sep_l persistently_elim wand_elim_l.
 Qed.
-Lemma wand_impl_persistently P Q : ((□ P) -∗ Q) ⊣⊢ ((□ P) → Q).
+Lemma impl_wand_persistently P Q : (□ P → Q) ⊣⊢ (□ P -∗ Q).
 Proof.
-  apply (anti_symm (⊢)); [|by rewrite -impl_wand].
-  apply impl_intro_l. by rewrite persistently_and_sep_l' wand_elim_r.
+  apply (anti_symm (⊢)); [by rewrite -impl_wand_1|].
+  apply impl_intro_l. by rewrite persistently_and_sep_l wand_elim_r.
 Qed.
-Lemma persistently_entails_l' P Q : (P ⊢ □ Q) → P ⊢ □ Q ∗ P.
-Proof. intros; rewrite -persistently_and_sep_l'; auto. Qed.
-Lemma persistently_entails_r' P Q : (P ⊢ □ Q) → P ⊢ P ∗ □ Q.
-Proof. intros; rewrite -persistently_and_sep_r'; auto. Qed.
+Lemma persistently_entails_l P Q : (P ⊢ □ Q) → P ⊢ □ Q ∗ P.
+Proof. intros; rewrite -persistently_and_sep_l; auto. Qed.
+Lemma persistently_entails_r P Q : (P ⊢ □ Q) → P ⊢ P ∗ □ Q.
+Proof. intros; rewrite -persistently_and_sep_r; auto. Qed.
 
 Lemma persistently_laterN n P : □ ▷^n P ⊣⊢ ▷^n □ P.
 Proof. induction n as [|n IH]; simpl; auto. by rewrite persistently_later IH. Qed.
@@ -560,7 +560,7 @@ Proof.
   - rewrite -(right_id True%I uPred_sep (P -∗ Q)%I) -(exist_intro (P -∗ Q)%I).
     apply sep_mono_r. rewrite -persistently_pure. apply persistently_mono, impl_intro_l.
     by rewrite wand_elim_r 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).
@@ -569,7 +569,7 @@ Proof.
   - rewrite -(right_id True%I uPred_and (P → Q)%I) -(exist_intro (P → Q)%I).
     apply and_mono_r. rewrite -persistently_pure. apply persistently_mono, wand_intro_l.
     by rewrite impl_elim_r right_id.
-  - apply exist_elim=> R. apply impl_intro_l. rewrite assoc persistently_and_sep_r'.
+  - apply exist_elim=> R. apply impl_intro_l. rewrite assoc persistently_and_sep_r.
     by rewrite persistently_elim wand_elim_r.
 Qed.
 
@@ -727,7 +727,7 @@ Lemma except_0_sep P Q : ◇ (P ∗ Q) ⊣⊢ ◇ P ∗ ◇ Q.
 Proof.
   rewrite /uPred_except_0. apply (anti_symm _).
   - apply or_elim; last by auto.
-    by rewrite -!or_intro_l -persistently_pure -persistently_later -persistently_sep_dup'.
+    by rewrite -!or_intro_l -persistently_pure -persistently_later -persistently_sep_dup.
   - rewrite sep_or_r sep_elim_l sep_or_l; auto.
 Qed.
 Lemma except_0_forall {A} (Φ : A → uPred M) : ◇ (∀ a, Φ a) ⊢ ∀ a, ◇ Φ a.
@@ -823,8 +823,8 @@ Proof.
   apply or_mono, wand_intro_l; first done.
   rewrite -{2}(löb Q); apply impl_intro_l.
   rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto.
-  rewrite -(persistently_pure) -persistently_later persistently_and_sep_l'.
-  by rewrite assoc (comm _ _ P) -assoc -persistently_and_sep_l' impl_elim_r wand_elim_r.
+  rewrite -(persistently_pure) -persistently_later persistently_and_sep_l.
+  by rewrite assoc (comm _ _ P) -assoc -persistently_and_sep_l impl_elim_r wand_elim_r.
 Qed.
 Global Instance forall_timeless {A} (Ψ : A → uPred M) :
   (∀ x, Timeless (Ψ x)) → Timeless (∀ x, Ψ x).
@@ -867,26 +867,26 @@ Global Instance limit_preserving_Persistent {A:ofeT} `{Cofe A} (Φ : A → uPred
   NonExpansive Φ → LimitPreserving (λ x, Persistent (Φ x)).
 Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
 
-Lemma persistently_persistently P `{!Persistent P} : □ P ⊣⊢ P.
+Lemma persistent_persistently P `{!Persistent P} : □ P ⊣⊢ P.
 Proof. apply (anti_symm (⊢)); auto using persistently_elim. Qed.
-Lemma persistently_if_persistently p P `{!Persistent P} : □?p P ⊣⊢ P.
-Proof. destruct p; simpl; auto using persistently_persistently. Qed.
+Lemma persistent_persistently_if p P `{!Persistent P} : □?p P ⊣⊢ P.
+Proof. destruct p; simpl; auto using persistent_persistently. Qed.
 Lemma persistently_intro P Q `{!Persistent P} : (P ⊢ Q) → P ⊢ □ Q.
-Proof. rewrite -(persistently_persistently P); apply persistently_intro'. Qed.
-Lemma persistently_and_sep_l P Q `{!Persistent P} : P ∧ Q ⊣⊢ P ∗ Q.
-Proof. by rewrite -(persistently_persistently P) persistently_and_sep_l'. Qed.
-Lemma persistently_and_sep_r P Q `{!Persistent Q} : P ∧ Q ⊣⊢ P ∗ Q.
-Proof. by rewrite -(persistently_persistently Q) persistently_and_sep_r'. Qed.
-Lemma persistently_sep_dup P `{!Persistent P} : P ⊣⊢ P ∗ P.
-Proof. by rewrite -(persistently_persistently P) -persistently_sep_dup'. Qed.
-Lemma persistently_entails_l P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ Q ∗ P.
-Proof. by rewrite -(persistently_persistently Q); apply persistently_entails_l'. Qed.
-Lemma persistently_entails_r P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
-Proof. by rewrite -(persistently_persistently Q); apply persistently_entails_r'. Qed.
-Lemma persistently_impl_wand P `{!Persistent P} Q : (P → Q) ⊣⊢ (P -∗ Q).
-Proof.
-  apply (anti_symm _); auto using impl_wand.
-  apply impl_intro_l. by rewrite persistently_and_sep_l wand_elim_r.
+Proof. rewrite -(persistent_persistently P); apply persistently_intro'. Qed.
+Lemma and_sep_l P Q `{!Persistent P} : P ∧ Q ⊣⊢ P ∗ Q.
+Proof. by rewrite -(persistent_persistently P) persistently_and_sep_l. Qed.
+Lemma and_sep_r P Q `{!Persistent Q} : P ∧ Q ⊣⊢ P ∗ Q.
+Proof. by rewrite -(persistent_persistently Q) persistently_and_sep_r. Qed.
+Lemma sep_dup P `{!Persistent P} : P ⊣⊢ P ∗ P.
+Proof. by rewrite -(persistent_persistently P) -persistently_sep_dup. Qed.
+Lemma sep_entails_l P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ Q ∗ P.
+Proof. by rewrite -(persistent_persistently Q); apply persistently_entails_l. Qed.
+Lemma sep_entails_r P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
+Proof. by rewrite -(persistent_persistently Q); apply persistently_entails_r. Qed.
+Lemma impl_wand P `{!Persistent P} Q : (P → Q) ⊣⊢ (P -∗ Q).
+Proof.
+  apply (anti_symm _); auto using impl_wand_1.
+  apply impl_intro_l. by rewrite and_sep_l wand_elim_r.
 Qed.
 
 (* Persistence *)
@@ -900,7 +900,7 @@ Qed.
 Global Instance pure_wand_persistent φ Q :
   Persistent Q → Persistent (⌜φ⌝ -∗ Q)%I.
 Proof.
-  rewrite /Persistent -persistently_impl_wand pure_impl_forall persistently_forall.
+  rewrite /Persistent -impl_wand pure_impl_forall persistently_forall.
   auto using forall_mono.
 Qed.
 Global Instance persistently_persistent P : Persistent (â–¡ P).
diff --git a/theories/base_logic/lib/fractional.v b/theories/base_logic/lib/fractional.v
index c1c2b0d97..179eac0fc 100644
--- a/theories/base_logic/lib/fractional.v
+++ b/theories/base_logic/lib/fractional.v
@@ -51,7 +51,7 @@ Section fractional.
   (** Fractional and logical connectives *)
   Global Instance persistent_fractional P :
     Persistent P → Fractional (λ _, P).
-  Proof. intros HP q q'. by apply uPred.persistently_sep_dup. Qed.
+  Proof. intros HP q q'. by apply uPred.sep_dup. Qed.
 
   Global Instance fractional_sep Φ Ψ :
     Fractional Φ → Fractional Ψ → Fractional (λ q, Φ q ∗ Ψ q)%I.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index d3d71f8d9..9381789f3 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -102,7 +102,7 @@ Proof. apply wand_intro_r. by rewrite -own_op own_valid. Qed.
 Lemma own_valid_3 γ a1 a2 a3 : own γ a1 -∗ own γ a2 -∗ own γ a3 -∗ ✓ (a1 ⋅ a2 ⋅ a3).
 Proof. do 2 apply wand_intro_r. by rewrite -!own_op own_valid. Qed.
 Lemma own_valid_r γ a : own γ a ⊢ own γ a ∗ ✓ a.
-Proof. apply: uPred.persistently_entails_r. apply own_valid. Qed.
+Proof. apply: uPred.sep_entails_r. apply own_valid. Qed.
 Lemma own_valid_l γ a : own γ a ⊢ ✓ a ∗ own γ a.
 Proof. by rewrite comm -own_valid_r. Qed.
 
diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index cdefcc3f3..e1b5bafc2 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -81,5 +81,5 @@ Lemma vs_alloc N P : ▷ P ={↑N}=> inv N P.
 Proof. iIntros "!# HP". by iApply inv_alloc. Qed.
 
 Lemma wand_fupd_alt E1 E2 P Q : (P ={E1,E2}=∗ Q) ⊣⊢ ∃ R, R ∗ (P ∗ R ={E1,E2}=> Q).
-Proof. rewrite uPred.wand_alt. by setoid_rewrite <-uPred.persistently_wand_impl. Qed.
+Proof. rewrite uPred.wand_alt. by setoid_rewrite uPred.persistently_impl_wand. Qed.
 End vs.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index e4f814b10..234053f12 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -17,7 +17,7 @@ Proof. destruct p; rewrite /FromAssumption /= ?persistently_pure; apply False_el
 
 Global Instance from_assumption_persistently_r P Q :
   FromAssumption true P Q → FromAssumption true P (□ Q).
-Proof. rewrite /FromAssumption=><-. by rewrite persistently_persistently. Qed.
+Proof. rewrite /FromAssumption=><-. by rewrite persistent_persistently. Qed.
 
 Global Instance from_assumption_persistently_l p P Q :
   FromAssumption p P Q → FromAssumption p (□ P) Q.
@@ -65,9 +65,7 @@ Global Instance into_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
 Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
 Global Instance into_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
   FromPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 -∗ P2) (φ1 → φ2).
-Proof.
-  rewrite /FromPure /IntoPure pure_impl persistently_impl_wand. by intros -> ->.
-Qed.
+Proof. rewrite /FromPure /IntoPure pure_impl impl_wand. by intros -> ->. Qed.
 
 Global Instance into_pure_exist {X : Type} (Φ : X → uPred M) (φ : X → Prop) :
   (∀ x, @IntoPure M (Φ x) (φ x)) → @IntoPure M (∃ x, Φ x) (∃ x, φ x).
@@ -113,7 +111,7 @@ Global Instance from_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
 Proof. rewrite /FromPure pure_and. by intros -> ->. Qed.
 Global Instance from_pure_pure_sep (φ1 φ2 : Prop) P1 P2 :
   FromPure P1 φ1 → FromPure P2 φ2 → FromPure (P1 ∗ P2) (φ1 ∧ φ2).
-Proof. rewrite /FromPure pure_and persistently_and_sep_l. by intros -> ->. Qed.
+Proof. rewrite /FromPure pure_and and_sep_l. by intros -> ->. Qed.
 Global Instance from_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
   FromPure P1 φ1 → FromPure P2 φ2 → FromPure (P1 ∨ P2) (φ1 ∨ φ2).
 Proof. rewrite /FromPure pure_or. by intros -> ->. Qed.
@@ -122,9 +120,7 @@ Global Instance from_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
 Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
 Global Instance from_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
   IntoPure P1 φ1 → FromPure P2 φ2 → FromPure (P1 -∗ P2) (φ1 → φ2).
-Proof.
-  rewrite /FromPure /IntoPure pure_impl persistently_impl_wand. by intros -> ->.
-Qed.
+Proof. rewrite /FromPure /IntoPure pure_impl impl_wand. by intros -> ->. Qed.
 
 Global Instance from_pure_exist {X : Type} (Φ : X → uPred M) (φ : X → Prop) :
   (∀ x, @FromPure M (Φ x) (φ x)) → @FromPure M (∃ x, Φ x) (∃ x, φ x).
@@ -142,7 +138,7 @@ Qed.
 (* IntoPersistent *)
 Global Instance into_persistent_persistently_trans p P Q :
   IntoPersistent true P Q → IntoPersistent p (□ P) Q | 0.
-Proof. rewrite /IntoPersistent /==> ->. by rewrite persistently_if_persistently. Qed.
+Proof. rewrite /IntoPersistent /==> ->. by rewrite persistent_persistently_if. Qed.
 Global Instance into_persistent_persistently P : IntoPersistent true P P | 1.
 Proof. done. Qed.
 Global Instance into_persistent_persistent P :
@@ -298,14 +294,14 @@ Global Instance into_wand_wand p P P' Q Q' :
 Proof. done. Qed.
 Global Instance into_wand_impl p P P' Q Q' :
   WandWeaken p P Q P' Q' → IntoWand p (P → Q) P' Q'.
-Proof. rewrite /WandWeaken /IntoWand /= => <-. apply impl_wand. Qed.
+Proof. rewrite /WandWeaken /IntoWand /= => <-. apply impl_wand_1. Qed.
 
 Global Instance into_wand_iff_l p P P' Q Q' :
   WandWeaken p P Q P' Q' → IntoWand p (P ↔ Q) P' Q'.
-Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_l', impl_wand. Qed.
+Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_l', impl_wand_1. Qed.
 Global Instance into_wand_iff_r p P P' Q Q' :
   WandWeaken p Q P Q' P' → IntoWand p (P ↔ Q) Q' P'.
-Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_r', impl_wand. Qed.
+Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_r', impl_wand_1. Qed.
 
 Global Instance into_wand_forall {A} p (Φ : A → uPred M) P Q x :
   IntoWand p (Φ x) P Q → IntoWand p (∀ x, Φ x) P Q.
@@ -340,10 +336,10 @@ Global Instance from_and_sep P1 P2 : FromAnd false (P1 ∗ P2) P1 P2 | 100.
 Proof. done. Qed.
 Global Instance from_and_sep_persistent_l P1 P2 :
   Persistent P1 → FromAnd true (P1 ∗ P2) P1 P2 | 9.
-Proof. intros. by rewrite /FromAnd persistently_and_sep_l. Qed.
+Proof. intros. by rewrite /FromAnd and_sep_l. Qed.
 Global Instance from_and_sep_persistent_r P1 P2 :
   Persistent P2 → FromAnd true (P1 ∗ P2) P1 P2 | 10.
-Proof. intros. by rewrite /FromAnd persistently_and_sep_r. Qed.
+Proof. intros. by rewrite /FromAnd and_sep_r. Qed.
 
 Global Instance from_and_pure p φ ψ : @FromAnd M p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. apply mk_from_and_and. by rewrite pure_and. Qed.
@@ -351,7 +347,7 @@ Global Instance from_and_persistently p P Q1 Q2 :
   FromAnd false P Q1 Q2 → FromAnd p (□ P) (□ Q1) (□ Q2).
 Proof.
   intros. apply mk_from_and_and.
-  by rewrite persistently_and_sep_l' -persistently_sep -(from_and _ P).
+  by rewrite persistently_and_sep_l -persistently_sep -(from_and _ P).
 Qed.
 Global Instance from_and_later p P Q1 Q2 :
   FromAnd p P Q1 Q2 → FromAnd p (▷ P) (▷ Q1) (▷ Q2).
@@ -387,7 +383,7 @@ Proof. by rewrite /FromAnd big_sepL_cons. Qed.
 Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat → A → uPred M) x l :
   Persistent (Φ 0 x) →
   FromAnd true ([∗ list] k ↦ y ∈ x :: l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l, Φ (S k) y).
-Proof. intros. by rewrite /FromAnd big_opL_cons persistently_and_sep_l. Qed.
+Proof. intros. by rewrite /FromAnd big_opL_cons and_sep_l. Qed.
 
 Global Instance from_and_big_sepL_app {A} (Φ : nat → A → uPred M) l1 l2 :
   FromAnd false ([∗ list] k ↦ y ∈ l1 ++ l2, Φ k y)
@@ -397,7 +393,7 @@ Global Instance from_sep_big_sepL_app_persistent {A} (Φ : nat → A → uPred M
   (∀ k y, Persistent (Φ k y)) →
   FromAnd true ([∗ list] k ↦ y ∈ l1 ++ l2, Φ k y)
     ([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y).
-Proof. intros. by rewrite /FromAnd big_opL_app persistently_and_sep_l. Qed.
+Proof. intros. by rewrite /FromAnd big_opL_app and_sep_l. Qed.
 
 (* FromOp *)
 (* TODO: Worst case there could be a lot of backtracking on these instances,
@@ -431,13 +427,13 @@ Global Instance into_and_and P Q : IntoAnd true (P ∧ Q) P Q.
 Proof. done. Qed.
 Global Instance into_and_and_persistent_l P Q :
   Persistent P → IntoAnd false (P ∧ Q) P Q.
-Proof. intros; by rewrite /IntoAnd /= persistently_and_sep_l. Qed.
+Proof. intros; by rewrite /IntoAnd /= and_sep_l. Qed.
 Global Instance into_and_and_persistent_r P Q :
   Persistent Q → IntoAnd false (P ∧ Q) P Q.
-Proof. intros; by rewrite /IntoAnd /= persistently_and_sep_r. Qed.
+Proof. intros; by rewrite /IntoAnd /= and_sep_r. Qed.
 
 Global Instance into_and_pure p φ ψ : @IntoAnd M p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
-Proof. apply mk_into_and_sep. by rewrite pure_and persistently_and_sep_r. Qed.
+Proof. apply mk_into_and_sep. by rewrite pure_and and_sep_r. Qed.
 Global Instance into_and_persistently p P Q1 Q2 :
   IntoAnd true P Q1 Q2 → IntoAnd p (□ P) (□ Q1) (□ Q2).
 Proof.
@@ -488,7 +484,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)). solve_sep_entails.
+  rewrite {1}(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.
@@ -589,7 +585,7 @@ 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_sep /= persistently_persistently.
+  by rewrite persistently_sep /= persistent_persistently.
 Qed.
 
 Class MakeExcept0 (P Q : uPred M) := make_except_0 : ◇ P ⊣⊢ Q.
@@ -741,7 +737,7 @@ Global Instance from_forall_wand_pure P Q φ :
   IntoPureT P φ → FromForall (P -∗ Q) (λ _ : φ, Q)%I.
 Proof.
   intros (φ'&->&?). rewrite /FromForall -pure_impl_forall.
-  by rewrite persistently_impl_wand (into_pure P).
+  by rewrite impl_wand (into_pure P).
 Qed.
 
 Global Instance from_forall_persistently {A} P (Φ : A → uPred M) :
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index fe35f90c2..028fe9441 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -125,8 +125,8 @@ Lemma mk_from_and_persistent {M} (P Q1 Q2 : uPred M) :
   Or (Persistent Q1) (Persistent Q2) → (Q1 ∗ Q2 ⊢ P) → FromAnd true P Q1 Q2.
 Proof.
   intros [?|?] ?; rewrite /FromAnd.
-  - by rewrite persistently_and_sep_l.
-  - by rewrite persistently_and_sep_r.
+  - by rewrite and_sep_l.
+  - by rewrite and_sep_r.
 Qed.
 
 Class IntoAnd {M} (p : bool) (P Q1 Q2 : uPred M) :=
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 1d69bf60b..923cb4fd3 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -345,7 +345,7 @@ Lemma envs_split_sound Δ lr js Δ1 Δ2 :
   envs_split lr js Δ = Some (Δ1,Δ2) → Δ ⊢ Δ1 ∗ Δ2.
 Proof.
   rewrite /envs_split=> ?. rewrite -(idemp uPred_and Δ).
-  rewrite {2}envs_clear_spatial_sound sep_elim_l persistently_and_sep_r.
+  rewrite {2}envs_clear_spatial_sound sep_elim_l and_sep_r.
   destruct (envs_split_go _ _) as [[Δ1' Δ2']|] eqn:HΔ; [|done].
   apply envs_split_go_sound in HΔ as ->; last first.
   { intros j P. by rewrite envs_lookup_envs_clear_spatial=> ->. }
@@ -470,7 +470,7 @@ Proof.
   intros ?? HQ. rewrite -(persistently_elim Q) -(löb (□ Q)) -persistently_later.
   apply impl_intro_l, (persistently_intro _ _).
   rewrite envs_app_sound //; simpl.
-  by rewrite right_id persistently_and_sep_l' wand_elim_r HQ.
+  by rewrite right_id persistently_and_sep_l wand_elim_r HQ.
 Qed.
 
 (** * Always *)
@@ -499,9 +499,9 @@ Lemma tac_impl_intro Δ Δ' i P Q :
 Proof.
   intros ?? <-. destruct (env_spatial_is_nil Δ) eqn:?.
   - rewrite (persistent Δ) envs_app_sound //; simpl.
-    by rewrite right_id persistently_wand_impl persistently_elim.
+    by rewrite right_id -persistently_impl_wand persistently_elim.
   - apply impl_intro_l. rewrite envs_app_sound //; simpl.
-    by rewrite persistently_and_sep_l right_id wand_elim_r.
+    by rewrite and_sep_l right_id wand_elim_r.
 Qed.
 Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
   IntoPersistent false P P' →
@@ -552,7 +552,7 @@ Proof.
   intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
   - rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
     rewrite right_id assoc (into_wand _ R) /=. destruct q; simpl.
-    + by rewrite persistently_wand persistently_persistently !wand_elim_r.
+    + by rewrite persistently_wand persistent_persistently !wand_elim_r.
     + by rewrite !wand_elim_r.
   - rewrite envs_lookup_sound //; simpl.
     rewrite envs_lookup_sound // (envs_replace_sound' _ Δ'') //; simpl.
@@ -628,9 +628,9 @@ Lemma tac_specialize_persistent_helper Δ Δ' j q P R Q :
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ? HR ?? <-.
-  rewrite -(idemp uPred_and Δ) {1}HR persistently_and_sep_l.
+  rewrite -(idemp uPred_and Δ) {1}HR and_sep_l.
   rewrite envs_replace_sound //; simpl.
-  by rewrite right_id assoc (sep_elim_l R) persistently_persistently wand_elim_r.
+  by rewrite right_id assoc (sep_elim_l R) persistent_persistently wand_elim_r.
 Qed.
 
 Lemma tac_revert Δ Δ' i p P Q :
@@ -680,7 +680,7 @@ Lemma tac_assert_persistent Δ Δ1 Δ2 Δ' lr js j P Q :
   (Δ1 ⊢ P) → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ??? HP <-. rewrite -(idemp uPred_and Δ) {1}envs_split_sound //.
-  rewrite HP sep_elim_l (persistently_and_sep_l P) envs_app_sound //; simpl.
+  rewrite HP sep_elim_l (and_sep_l P) envs_app_sound //; simpl.
   by rewrite right_id wand_elim_r.
 Qed.
 
@@ -690,7 +690,7 @@ Lemma tac_assert_pure Δ Δ' j P φ Q :
   φ → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ??? <-. rewrite envs_app_sound //; simpl.
-  by rewrite right_id -(from_pure P) pure_True // -persistently_impl_wand True_impl.
+  by rewrite right_id -(from_pure P) pure_True // -impl_wand True_impl.
 Qed.
 
 Lemma tac_pose_proof Δ Δ' j P Q :
@@ -748,7 +748,7 @@ Lemma tac_rewrite_in Δ i p Pxy j q P (lr : bool) Q :
 Proof.
   intros ?? A Δ' x y Φ HPxy HP ?? <-.
   rewrite -(idemp uPred_and Δ) {2}(envs_lookup_sound' _ i) //.
-  rewrite sep_elim_l HPxy persistently_and_sep_r.
+  rewrite sep_elim_l HPxy and_sep_r.
   rewrite (envs_simple_replace_sound _ _ j) //; simpl.
   rewrite HP right_id -assoc; apply wand_elim_r'. destruct lr.
   - apply (internal_eq_rewrite x y (λ y, □?q Φ y -∗ Δ')%I);
-- 
GitLab