From 1aae01e6d0befdefaba6a33d87febeefb1c2e088 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 28 Jun 2016 00:26:10 +0200
Subject: [PATCH] Rename type classes in proof mode.

We are now using the prefixes Into, From, and Is (the first two are
inspired by the names of some traits in the Rust stdlib), and hopefully
doing that consistenly.
---
 heap_lang/proofmode.v       |  26 +-
 proofmode/coq_tactics.v     | 479 ++++++++++++++++++------------------
 proofmode/ghost_ownership.v |  12 +-
 proofmode/invariants.v      |  12 +-
 proofmode/pviewshifts.v     |  59 +++--
 proofmode/sts.v             |   6 +-
 proofmode/tactics.v         |  56 ++---
 proofmode/weakestpre.v      |   4 +-
 8 files changed, 326 insertions(+), 328 deletions(-)

diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index aeb96f07d..7d1113a18 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -12,14 +12,14 @@ Implicit Types P Q : iPropG heap_lang Î£.
 Implicit Types Î¦ : val â†’ iPropG heap_lang Î£.
 Implicit Types Î” : envs (iResUR heap_lang (globalF Î£)).
 
-Global Instance sep_destruct_mapsto l q v :
-  SepDestruct false (l â†¦{q} v) (l â†¦{q/2} v) (l â†¦{q/2} v).
-Proof. by rewrite /SepDestruct heap_mapsto_op_split. Qed.
+Global Instance into_sep_mapsto l q v :
+  IntoSep false (l â†¦{q} v) (l â†¦{q/2} v) (l â†¦{q/2} v).
+Proof. by rewrite /IntoSep heap_mapsto_op_split. Qed.
 
 Lemma tac_wp_alloc Î” Î”' N E j e v Î¦ :
   to_val e = Some v â†’ 
   (Î” âŠ¢ heap_ctx N) â†’ nclose N âŠ† E â†’
-  StripLaterEnvs Î” Î”' â†’
+  IntoLaterEnvs Î” Î”' â†’
   (âˆ€ l, âˆƒ Î”'',
     envs_app false (Esnoc Enil j (l â†¦ v)) Î”' = Some Î”'' âˆ§
     (Î”'' âŠ¢ Î¦ (LitV (LitLoc l)))) â†’
@@ -27,60 +27,60 @@ Lemma tac_wp_alloc Î” Î”' N E j e v Î¦ :
 Proof.
   intros ???? HÎ”. rewrite -wp_alloc // -always_and_sep_l.
   apply and_intro; first done.
-  rewrite strip_later_env_sound; apply later_mono, forall_intro=> l.
+  rewrite into_later_env_sound; apply later_mono, forall_intro=> l.
   destruct (HÎ” l) as (Î”''&?&HÎ”'). rewrite envs_app_sound //; simpl.
   by rewrite right_id HÎ”'.
 Qed.
 
 Lemma tac_wp_load Î” Î”' N E i l q v Î¦ :
   (Î” âŠ¢ heap_ctx N) â†’ nclose N âŠ† E â†’
-  StripLaterEnvs Î” Î”' â†’
+  IntoLaterEnvs Î” Î”' â†’
   envs_lookup i Î”' = Some (false, l â†¦{q} v)%I â†’
   (Î”' âŠ¢ Î¦ v) â†’
   Î” âŠ¢ WP Load (Lit (LitLoc l)) @ E {{ Î¦ }}.
 Proof.
   intros. rewrite -wp_load // -always_and_sep_l. apply and_intro; first done.
-  rewrite strip_later_env_sound -later_sep envs_lookup_split //; simpl.
+  rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
 Lemma tac_wp_store Î” Î”' Î”'' N E i l v e v' Î¦ :
   to_val e = Some v' â†’
   (Î” âŠ¢ heap_ctx N) â†’ nclose N âŠ† E â†’
-  StripLaterEnvs Î” Î”' â†’
+  IntoLaterEnvs Î” Î”' â†’
   envs_lookup i Î”' = Some (false, l â†¦ v)%I â†’
   envs_simple_replace i false (Esnoc Enil i (l â†¦ v')) Î”' = Some Î”'' â†’
   (Î”'' âŠ¢ Î¦ (LitV LitUnit)) â†’ Î” âŠ¢ WP Store (Lit (LitLoc l)) e @ E {{ Î¦ }}.
 Proof.
   intros. rewrite -wp_store // -always_and_sep_l. apply and_intro; first done.
-  rewrite strip_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
+  rewrite into_later_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 Î” Î”' N E i l q v e1 v1 e2 v2 Î¦ :
   to_val e1 = Some v1 â†’ to_val e2 = Some v2 â†’
   (Î” âŠ¢ heap_ctx N) â†’ nclose N âŠ† E â†’
-  StripLaterEnvs Î” Î”' â†’
+  IntoLaterEnvs Î” Î”' â†’
   envs_lookup i Î”' = Some (false, l â†¦{q} v)%I â†’ v â‰  v1 â†’
   (Î”' âŠ¢ Î¦ (LitV (LitBool false))) â†’
   Î” âŠ¢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Î¦ }}.
 Proof.
   intros. rewrite -wp_cas_fail // -always_and_sep_l. apply and_intro; first done.
-  rewrite strip_later_env_sound -later_sep envs_lookup_split //; simpl.
+  rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
 Lemma tac_wp_cas_suc Î” Î”' Î”'' N E i l v e1 v1 e2 v2 Î¦ :
   to_val e1 = Some v1 â†’ to_val e2 = Some v2 â†’
   (Î” âŠ¢ heap_ctx N) â†’ nclose N âŠ† E â†’
-  StripLaterEnvs Î” Î”' â†’
+  IntoLaterEnvs Î” Î”' â†’
   envs_lookup i Î”' = Some (false, l â†¦ v)%I â†’ v = v1 â†’
   envs_simple_replace i false (Esnoc Enil i (l â†¦ v2)) Î”' = Some Î”'' â†’
   (Î”'' âŠ¢ Î¦ (LitV (LitBool true))) â†’ Î” âŠ¢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Î¦ }}.
 Proof.
   intros; subst.
   rewrite -wp_cas_suc // -always_and_sep_l. apply and_intro; first done.
-  rewrite strip_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
+  rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 End heap.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index fe01f3c17..9611f7dcf 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -292,19 +292,19 @@ Proof.
 Qed.
 
 (** * Basic rules *)
-Class ToAssumption (p : bool) (P Q : uPred M) := to_assumption : â–¡?p P âŠ¢ Q.
-Arguments to_assumption _ _ _ {_}.
-Global Instance to_assumption_exact p P : ToAssumption p P P.
-Proof. destruct p; by rewrite /ToAssumption /= ?always_elim. Qed.
-Global Instance to_assumption_always_l p P Q :
-  ToAssumption p P Q â†’ ToAssumption p (â–¡ P) Q.
-Proof. rewrite /ToAssumption=><-. by rewrite always_elim. Qed.
-Global Instance to_assumption_always_r P Q :
-  ToAssumption true P Q â†’ ToAssumption true P (â–¡ Q).
-Proof. rewrite /ToAssumption=><-. by rewrite always_always. Qed.
+Class FromAssumption (p : bool) (P Q : uPred M) := from_assumption : â–¡?p P âŠ¢ Q.
+Arguments from_assumption _ _ _ {_}.
+Global Instance from_assumption_exact p P : FromAssumption p P P.
+Proof. destruct p; by rewrite /FromAssumption /= ?always_elim. Qed.
+Global Instance from_assumption_always_l p P Q :
+  FromAssumption p P Q â†’ FromAssumption p (â–¡ P) Q.
+Proof. rewrite /FromAssumption=><-. by rewrite always_elim. Qed.
+Global Instance from_assumption_always_r P Q :
+  FromAssumption true P Q â†’ FromAssumption true P (â–¡ Q).
+Proof. rewrite /FromAssumption=><-. by rewrite always_always. Qed.
 
 Lemma tac_assumption Î” i p P Q :
-  envs_lookup i Î” = Some (p,P) â†’ ToAssumption p P Q â†’ Î” âŠ¢ Q.
+  envs_lookup i Î” = Some (p,P) â†’ FromAssumption p P Q â†’ Î” âŠ¢ Q.
 Proof. intros. by rewrite envs_lookup_sound // sep_elim_l. Qed.
 
 Lemma tac_rename Î” Î”' i j p P Q :
@@ -327,96 +327,96 @@ Lemma tac_ex_falso Î” Q : (Î” âŠ¢ False) â†’ Î” âŠ¢ Q.
 Proof. by rewrite -(False_elim Q). Qed.
 
 (** * Pure *)
-Class ToPure (P : uPred M) (Ï† : Prop) := to_pure : P âŠ£âŠ¢ â–  Ï†.
-Arguments to_pure : clear implicits.
-Global Instance to_pure_pure Ï† : ToPure (â–  Ï†) Ï†.
+Class IsPure (P : uPred M) (Ï† : Prop) := is_pure : P âŠ£âŠ¢ â–  Ï†.
+Arguments is_pure : clear implicits.
+Global Instance is_pure_pure Ï† : IsPure (â–  Ï†) Ï†.
 Proof. done. Qed.
-Global Instance to_pure_eq {A : cofeT} (a b : A) :
-  Timeless a â†’ ToPure (a â‰¡ b) (a â‰¡ b).
+Global Instance is_pure_eq {A : cofeT} (a b : A) :
+  Timeless a â†’ IsPure (a â‰¡ b) (a â‰¡ b).
 Proof. intros; red. by rewrite timeless_eq. Qed.
-Global Instance to_pure_valid `{CMRADiscrete A} (a : A) : ToPure (âœ“ a) (âœ“ a).
+Global Instance is_pure_valid `{CMRADiscrete A} (a : A) : IsPure (âœ“ a) (âœ“ a).
 Proof. intros; red. by rewrite discrete_valid. Qed.
 
-Lemma tac_pure_intro Î” Q (Ï† : Prop) : ToPure Q Ï† â†’ Ï† â†’ Î” âŠ¢ Q.
+Lemma tac_pure_intro Î” Q (Ï† : Prop) : IsPure Q Ï† â†’ Ï† â†’ Î” âŠ¢ Q.
 Proof. intros ->. apply pure_intro. Qed.
 
 Lemma tac_pure Î” Î”' i p P Ï† Q :
-  envs_lookup_delete i Î” = Some (p, P, Î”') â†’ ToPure P Ï† â†’
+  envs_lookup_delete i Î” = Some (p, P, Î”') â†’ IsPure P Ï† â†’
   (Ï† â†’ Î”' âŠ¢ Q) â†’ Î” âŠ¢ Q.
 Proof.
   intros ?? HQ. rewrite envs_lookup_delete_sound' //; simpl.
-  rewrite (to_pure P); by apply pure_elim_sep_l.
+  rewrite (is_pure P); by apply pure_elim_sep_l.
 Qed.
 
 Lemma tac_pure_revert Î” Ï† Q : (Î” âŠ¢ â–  Ï† â†’ Q) â†’ (Ï† â†’ Î” âŠ¢ Q).
 Proof. intros HÎ” ?. by rewrite HÎ” pure_equiv // left_id. Qed.
 
 (** * Later *)
-Class StripLaterR (P Q : uPred M) := strip_later_r : P âŠ¢ â–· Q.
-Arguments strip_later_r _ _ {_}.
-Class StripLaterL (P Q : uPred M) := strip_later_l : â–· Q âŠ¢ P.
-Arguments strip_later_l _ _ {_}.
-Class StripLaterEnv (Î“1 Î“2 : env (uPred M)) :=
-  strip_later_env : env_Forall2 StripLaterR Î“1 Î“2.
-Class StripLaterEnvs (Î”1 Î”2 : envs M) := {
-  strip_later_persistent: StripLaterEnv (env_persistent Î”1) (env_persistent Î”2);
-  strip_later_spatial: StripLaterEnv (env_spatial Î”1) (env_spatial Î”2)
+Class IntoLater (P Q : uPred M) := into_later : P âŠ¢ â–· Q.
+Arguments into_later _ _ {_}.
+Class FromLater (P Q : uPred M) := from_later : â–· Q âŠ¢ P.
+Arguments from_later _ _ {_}.
+Class IntoLaterEnv (Î“1 Î“2 : env (uPred M)) :=
+  into_later_env : env_Forall2 IntoLater Î“1 Î“2.
+Class IntoLaterEnvs (Î”1 Î”2 : envs M) := {
+  into_later_persistent: IntoLaterEnv (env_persistent Î”1) (env_persistent Î”2);
+  into_later_spatial: IntoLaterEnv (env_spatial Î”1) (env_spatial Î”2)
 }.
 
-Global Instance strip_later_r_fallthrough P : StripLaterR P P | 1000.
+Global Instance into_later_fallthrough P : IntoLater P P | 1000.
 Proof. apply later_intro. Qed.
-Global Instance strip_later_r_later P : StripLaterR (â–· P) P.
+Global Instance into_later_later P : IntoLater (â–· P) P.
 Proof. done. Qed.
-Global Instance strip_later_r_and P1 P2 Q1 Q2 :
-  StripLaterR P1 Q1 â†’ StripLaterR P2 Q2 â†’ StripLaterR (P1 âˆ§ P2) (Q1 âˆ§ Q2).
+Global Instance into_later_and P1 P2 Q1 Q2 :
+  IntoLater P1 Q1 â†’ IntoLater P2 Q2 â†’ IntoLater (P1 âˆ§ P2) (Q1 âˆ§ Q2).
 Proof. intros ??; red. by rewrite later_and; apply and_mono. Qed.
-Global Instance strip_later_r_or P1 P2 Q1 Q2 :
-  StripLaterR P1 Q1 â†’ StripLaterR P2 Q2 â†’ StripLaterR (P1 âˆ¨ P2) (Q1 âˆ¨ Q2).
+Global Instance into_later_or P1 P2 Q1 Q2 :
+  IntoLater P1 Q1 â†’ IntoLater P2 Q2 â†’ IntoLater (P1 âˆ¨ P2) (Q1 âˆ¨ Q2).
 Proof. intros ??; red. by rewrite later_or; apply or_mono. Qed.
-Global Instance strip_later_r_sep P1 P2 Q1 Q2 :
-  StripLaterR P1 Q1 â†’ StripLaterR P2 Q2 â†’ StripLaterR (P1 â˜… P2) (Q1 â˜… Q2).
+Global Instance into_later_sep P1 P2 Q1 Q2 :
+  IntoLater P1 Q1 â†’ IntoLater P2 Q2 â†’ IntoLater (P1 â˜… P2) (Q1 â˜… Q2).
 Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.
 
-Global Instance strip_later_r_big_sepM `{Countable K} {A}
+Global Instance into_later_big_sepM `{Countable K} {A}
     (Î¦ Î¨ : K â†’ A â†’ uPred M) (m : gmap K A) :
-  (âˆ€ x k, StripLaterR (Î¦ k x) (Î¨ k x)) â†’
-  StripLaterR ([â˜… map] k â†¦ x âˆˆ m, Î¦ k x) ([â˜… map] k â†¦ x âˆˆ m, Î¨ k x).
+  (âˆ€ x k, IntoLater (Î¦ k x) (Î¨ k x)) â†’
+  IntoLater ([â˜… map] k â†¦ x âˆˆ m, Î¦ k x) ([â˜… map] k â†¦ x âˆˆ m, Î¨ k x).
 Proof.
-  rewrite /StripLaterR=> ?. rewrite big_sepM_later; by apply big_sepM_mono.
+  rewrite /IntoLater=> ?. rewrite big_sepM_later; by apply big_sepM_mono.
 Qed.
-Global Instance strip_later_r_big_sepS `{Countable A}
+Global Instance into_later_big_sepS `{Countable A}
     (Î¦ Î¨ : A â†’ uPred M) (X : gset A) :
-  (âˆ€ x, StripLaterR (Î¦ x) (Î¨ x)) â†’
-  StripLaterR ([â˜… set] x âˆˆ X, Î¦ x) ([â˜… set] x âˆˆ X, Î¨ x).
+  (âˆ€ x, IntoLater (Î¦ x) (Î¨ x)) â†’
+  IntoLater ([â˜… set] x âˆˆ X, Î¦ x) ([â˜… set] x âˆˆ X, Î¨ x).
 Proof.
-  rewrite /StripLaterR=> ?. rewrite big_sepS_later; by apply big_sepS_mono.
+  rewrite /IntoLater=> ?. rewrite big_sepS_later; by apply big_sepS_mono.
 Qed.
 
-Global Instance strip_later_l_later P : StripLaterL (â–· P) P.
+Global Instance from_later_later P : FromLater (â–· P) P.
 Proof. done. Qed.
-Global Instance strip_later_l_and P1 P2 Q1 Q2 :
-  StripLaterL P1 Q1 â†’ StripLaterL P2 Q2 â†’ StripLaterL (P1 âˆ§ P2) (Q1 âˆ§ Q2).
+Global Instance from_later_and P1 P2 Q1 Q2 :
+  FromLater P1 Q1 â†’ FromLater P2 Q2 â†’ FromLater (P1 âˆ§ P2) (Q1 âˆ§ Q2).
 Proof. intros ??; red. by rewrite later_and; apply and_mono. Qed.
-Global Instance strip_later_l_or P1 P2 Q1 Q2 :
-  StripLaterL P1 Q1 â†’ StripLaterL P2 Q2 â†’ StripLaterL (P1 âˆ¨ P2) (Q1 âˆ¨ Q2).
+Global Instance from_later_or P1 P2 Q1 Q2 :
+  FromLater P1 Q1 â†’ FromLater P2 Q2 â†’ FromLater (P1 âˆ¨ P2) (Q1 âˆ¨ Q2).
 Proof. intros ??; red. by rewrite later_or; apply or_mono. Qed.
-Global Instance strip_later_l_sep P1 P2 Q1 Q2 :
-  StripLaterL P1 Q1 â†’ StripLaterL P2 Q2 â†’ StripLaterL (P1 â˜… P2) (Q1 â˜… Q2).
+Global Instance from_later_sep P1 P2 Q1 Q2 :
+  FromLater P1 Q1 â†’ FromLater P2 Q2 â†’ FromLater (P1 â˜… P2) (Q1 â˜… Q2).
 Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.
 
-Global Instance strip_later_env_nil : StripLaterEnv Enil Enil.
+Global Instance into_later_env_nil : IntoLaterEnv Enil Enil.
 Proof. constructor. Qed.
-Global Instance strip_later_env_snoc Î“1 Î“2 i P Q :
-  StripLaterEnv Î“1 Î“2 â†’ StripLaterR P Q â†’
-  StripLaterEnv (Esnoc Î“1 i P) (Esnoc Î“2 i Q).
+Global Instance into_later_env_snoc Î“1 Î“2 i P Q :
+  IntoLaterEnv Î“1 Î“2 â†’ IntoLater P Q â†’
+  IntoLaterEnv (Esnoc Î“1 i P) (Esnoc Î“2 i Q).
 Proof. by constructor. Qed.
 
-Global Instance strip_later_envs Î“p1 Î“p2 Î“s1 Î“s2 :
-  StripLaterEnv Î“p1 Î“p2 â†’ StripLaterEnv Î“s1 Î“s2 â†’
-  StripLaterEnvs (Envs Î“p1 Î“s1) (Envs Î“p2 Î“s2).
+Global Instance into_later_envs Î“p1 Î“p2 Î“s1 Î“s2 :
+  IntoLaterEnv Î“p1 Î“p2 â†’ IntoLaterEnv Î“s1 Î“s2 â†’
+  IntoLaterEnvs (Envs Î“p1 Î“s1) (Envs Î“p2 Î“s2).
 Proof. by split. Qed.
 
-Lemma strip_later_env_sound Î”1 Î”2 : StripLaterEnvs Î”1 Î”2 â†’ Î”1 âŠ¢ â–· Î”2.
+Lemma into_later_env_sound Î”1 Î”2 : IntoLaterEnvs Î”1 Î”2 â†’ Î”1 âŠ¢ â–· Î”2.
 Proof.
   intros [Hp Hs]; rewrite /of_envs /= !later_sep -always_later.
   repeat apply sep_mono; try apply always_mono.
@@ -427,8 +427,8 @@ Proof.
 Qed.
 
 Lemma tac_next Î” Î”' Q Q' :
-  StripLaterEnvs Î” Î”' â†’ StripLaterL Q Q' â†’ (Î”' âŠ¢ Q') â†’ Î” âŠ¢ Q.
-Proof. intros ?? HQ. by rewrite -(strip_later_l Q) strip_later_env_sound HQ. Qed.
+  IntoLaterEnvs Î” Î”' â†’ FromLater Q Q' â†’ (Î”' âŠ¢ Q') â†’ Î” âŠ¢ Q.
+Proof. intros ?? HQ. by rewrite -(from_later Q) into_later_env_sound HQ. Qed.
 
 Lemma tac_lÃ¶b Î” Î”' i Q :
   envs_persistent Î” = true â†’
@@ -445,24 +445,24 @@ Qed.
 Lemma tac_always_intro Î” Q : envs_persistent Î” = true â†’ (Î” âŠ¢ Q) â†’ Î” âŠ¢ â–¡ Q.
 Proof. intros. by apply: always_intro. Qed.
 
-Class ToPersistentP (P Q : uPred M) := to_persistentP : P âŠ¢ â–¡ Q.
-Arguments to_persistentP : clear implicits.
-Global Instance to_persistentP_always_trans P Q :
-  ToPersistentP P Q â†’ ToPersistentP (â–¡ P) Q | 0.
-Proof. rewrite /ToPersistentP=> ->. by rewrite always_always. Qed.
-Global Instance to_persistentP_always P : ToPersistentP (â–¡ P) P | 1.
+Class IntoPersistentP (P Q : uPred M) := into_persistentP : P âŠ¢ â–¡ Q.
+Arguments into_persistentP : clear implicits.
+Global Instance into_persistentP_always_trans P Q :
+  IntoPersistentP P Q â†’ IntoPersistentP (â–¡ P) Q | 0.
+Proof. rewrite /IntoPersistentP=> ->. by rewrite always_always. Qed.
+Global Instance into_persistentP_always P : IntoPersistentP (â–¡ P) P | 1.
 Proof. done. Qed.
-Global Instance to_persistentP_persistent P :
-  PersistentP P â†’ ToPersistentP P P | 100.
+Global Instance into_persistentP_persistent P :
+  PersistentP P â†’ IntoPersistentP P P | 100.
 Proof. done. Qed.
 
 Lemma tac_persistent Î” Î”' i p P P' Q :
-  envs_lookup i Î” = Some (p, P) â†’ ToPersistentP P P' â†’
+  envs_lookup i Î” = Some (p, P) â†’ IntoPersistentP P P' â†’
   envs_replace i p true (Esnoc Enil i P') Î” = Some Î”' â†’
   (Î”' âŠ¢ Q) â†’ Î” âŠ¢ Q.
 Proof.
   intros ??? <-. rewrite envs_replace_sound //; simpl.
-  by rewrite right_id (to_persistentP P) always_if_always wand_elim_r.
+  by rewrite right_id (into_persistentP P) always_if_always wand_elim_r.
 Qed.
 
 (** * Implication and wand *)
@@ -475,16 +475,16 @@ Proof.
   by rewrite right_id always_wand_impl always_elim HQ.
 Qed.
 Lemma tac_impl_intro_persistent Î” Î”' i P P' Q :
-  ToPersistentP P P' â†’
+  IntoPersistentP P P' â†’
   envs_app true (Esnoc Enil i P') Î” = Some Î”' â†’
   (Î”' âŠ¢ Q) â†’ Î” âŠ¢ P â†’ Q.
 Proof.
   intros ?? HQ. rewrite envs_app_sound //; simpl. apply impl_intro_l.
-  by rewrite right_id {1}(to_persistentP P) always_and_sep_l wand_elim_r.
+  by rewrite right_id {1}(into_persistentP P) always_and_sep_l wand_elim_r.
 Qed.
-Lemma tac_impl_intro_pure Î” P Ï† Q : ToPure P Ï† â†’ (Ï† â†’ Î” âŠ¢ Q) â†’ Î” âŠ¢ P â†’ Q.
+Lemma tac_impl_intro_pure Î” P Ï† Q : IsPure P Ï† â†’ (Ï† â†’ Î” âŠ¢ Q) â†’ Î” âŠ¢ P â†’ Q.
 Proof.
-  intros. by apply impl_intro_l; rewrite (to_pure P); apply pure_elim_l.
+  intros. by apply impl_intro_l; rewrite (is_pure P); apply pure_elim_l.
 Qed.
 
 Lemma tac_wand_intro Î” Î”' i P Q :
@@ -493,37 +493,37 @@ Proof.
   intros ? HQ. rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
 Qed.
 Lemma tac_wand_intro_persistent Î” Î”' i P P' Q :
-  ToPersistentP P P' â†’
+  IntoPersistentP P P' â†’
   envs_app true (Esnoc Enil i P') Î” = Some Î”' â†’
   (Î”' âŠ¢ Q) â†’ Î” âŠ¢ P -â˜… Q.
 Proof.
   intros. rewrite envs_app_sound //; simpl.
   rewrite right_id. by apply wand_mono.
 Qed.
-Lemma tac_wand_intro_pure Î” P Ï† Q : ToPure P Ï† â†’ (Ï† â†’ Î” âŠ¢ Q) â†’ Î” âŠ¢ P -â˜… Q.
+Lemma tac_wand_intro_pure Î” P Ï† Q : IsPure P Ï† â†’ (Ï† â†’ Î” âŠ¢ Q) â†’ Î” âŠ¢ P -â˜… Q.
 Proof.
-  intros. by apply wand_intro_l; rewrite (to_pure P); apply pure_elim_sep_l.
+  intros. by apply wand_intro_l; rewrite (is_pure P); apply pure_elim_sep_l.
 Qed.
 
-Class ToWand (R P Q : uPred M) := to_wand : R âŠ¢ P -â˜… Q.
-Arguments to_wand : clear implicits.
-Global Instance to_wand_wand P Q : ToWand (P -â˜… Q) P Q.
+Class IntoWand (R P Q : uPred M) := into_wand : R âŠ¢ P -â˜… Q.
+Arguments into_wand : clear implicits.
+Global Instance into_wand_wand P Q : IntoWand (P -â˜… Q) P Q.
 Proof. done. Qed.
-Global Instance to_wand_impl P Q : ToWand (P â†’ Q) P Q.
+Global Instance into_wand_impl P Q : IntoWand (P â†’ Q) P Q.
 Proof. apply impl_wand. Qed.
-Global Instance to_wand_iff_l P Q : ToWand (P â†” Q) P Q.
+Global Instance into_wand_iff_l P Q : IntoWand (P â†” Q) P Q.
 Proof. by apply and_elim_l', impl_wand. Qed.
-Global Instance to_wand_iff_r P Q : ToWand (P â†” Q) Q P.
+Global Instance into_wand_iff_r P Q : IntoWand (P â†” Q) Q P.
 Proof. apply and_elim_r', impl_wand. Qed.
-Global Instance to_wand_always R P Q : ToWand R P Q â†’ ToWand (â–¡ R) P Q.
-+Proof. rewrite /ToWand=> ->. apply always_elim. Qed.
+Global Instance into_wand_always R P Q : IntoWand R P Q â†’ IntoWand (â–¡ R) P Q.
+Proof. rewrite /IntoWand=> ->. apply always_elim. Qed.
 
 (* This is pretty much [tac_specialize_assert] with [js:=[j]] and [tac_exact],
 but it is doing some work to keep the order of hypotheses preserved. *)
 Lemma tac_specialize Î” Î”' Î”'' i p j q P1 P2 R Q :
   envs_lookup_delete i Î” = Some (p, P1, Î”') â†’
   envs_lookup j (if p then Î” else Î”') = Some (q, R) â†’
-  ToWand R P1 P2 â†’
+  IntoWand R P1 P2 â†’
   match p with
   | true  => envs_simple_replace j q (Esnoc Enil j P2) Î”
   | false => envs_replace j q false (Esnoc Enil j P2) Î”'
@@ -533,22 +533,22 @@ Lemma tac_specialize Î” Î”' Î”'' i p j q P1 P2 R Q :
 Proof.
   intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
   - rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
-    rewrite assoc (to_wand R) (always_elim_if q) -always_if_sep wand_elim_r.
+    rewrite assoc (into_wand R) (always_elim_if q) -always_if_sep wand_elim_r.
     by rewrite right_id wand_elim_r.
   - rewrite envs_lookup_sound //; simpl.
     rewrite envs_lookup_sound // (envs_replace_sound' _ Î”'') //; simpl.
-    by rewrite right_id assoc (to_wand R) always_if_elim wand_elim_r wand_elim_r.
+    by rewrite right_id assoc (into_wand R) always_if_elim wand_elim_r wand_elim_r.
 Qed.
 
-Class ToAssert (P : uPred M) (Q : uPred M) (R : uPred M) :=
-  to_assert : R â˜… (P -â˜… Q) âŠ¢ Q.
-Global Arguments to_assert _ _ _ {_}.
-Lemma to_assert_fallthrough P Q : ToAssert P Q P.
-Proof. by rewrite /ToAssert wand_elim_r. Qed.
+Class IntoAssert (P : uPred M) (Q : uPred M) (R : uPred M) :=
+  into_assert : R â˜… (P -â˜… Q) âŠ¢ Q.
+Global Arguments into_assert _ _ _ {_}.
+Lemma into_assert_fallthrough P Q : IntoAssert P Q P.
+Proof. by rewrite /IntoAssert wand_elim_r. Qed.
 
 Lemma tac_specialize_assert Î” Î”' Î”1 Î”2' j q lr js R P1 P2 P1' Q :
   envs_lookup_delete j Î” = Some (q, R, Î”') â†’
-  ToWand R P1 P2 â†’ ToAssert P1 Q P1' â†’
+  IntoWand R P1 P2 â†’ IntoAssert P1 Q P1' â†’
   ('(Î”1,Î”2) â† envs_split lr js Î”';
     Î”2' â† envs_app false (Esnoc Enil j P2) Î”2;
     Some (Î”1,Î”2')) = Some (Î”1,Î”2') â†’ (* does not preserve position of [j] *)
@@ -559,24 +559,24 @@ Proof.
     destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
   rewrite envs_lookup_sound // envs_split_sound //.
   rewrite (envs_app_sound Î”2) //; simpl.
-  rewrite right_id (to_wand R) HP1 assoc -(comm _ P1') -assoc.
-  rewrite -(to_assert P1 Q); apply sep_mono_r, wand_intro_l.
+  rewrite right_id (into_wand R) HP1 assoc -(comm _ P1') -assoc.
+  rewrite -(into_assert P1 Q); apply sep_mono_r, wand_intro_l.
   by rewrite always_if_elim assoc !wand_elim_r.
 Qed.
 
 Lemma tac_specialize_pure Î” Î”' j q R P1 P2 Ï† Q :
   envs_lookup j Î” = Some (q, R) â†’
-  ToWand R P1 P2 â†’ ToPure P1 Ï† â†’
+  IntoWand R P1 P2 â†’ IsPure P1 Ï† â†’
   envs_simple_replace j q (Esnoc Enil j P2) Î” = Some Î”' â†’
   Ï† â†’ (Î”' âŠ¢ Q) â†’ Î” âŠ¢ Q.
 Proof.
   intros. rewrite envs_simple_replace_sound //; simpl.
-  by rewrite right_id (to_wand R) (to_pure P1) pure_equiv // wand_True wand_elim_r.
+  by rewrite right_id (into_wand R) (is_pure P1) pure_equiv // wand_True wand_elim_r.
 Qed.
 
 Lemma tac_specialize_persistent Î” Î”' Î”'' j q P1 P2 R Q :
   envs_lookup_delete j Î” = Some (q, R, Î”') â†’
-  ToWand R P1 P2 â†’
+  IntoWand R P1 P2 â†’
   envs_simple_replace j q (Esnoc Enil j P2) Î” = Some Î”'' â†’
   (Î”' âŠ¢ P1) â†’ (PersistentP P1 âˆ¨ PersistentP P2) â†’
   (Î”'' âŠ¢ Q) â†’ Î” âŠ¢ Q.
@@ -586,11 +586,11 @@ Proof.
     rewrite -(idemp uPred_and (envs_delete _ _ _)).
     rewrite {1}HP1 (persistentP P1) always_and_sep_l assoc.
     rewrite envs_simple_replace_sound' //; simpl.
-    rewrite right_id (to_wand R) (always_elim_if q) -always_if_sep wand_elim_l.
+    rewrite right_id (into_wand R) (always_elim_if q) -always_if_sep wand_elim_l.
     by rewrite wand_elim_r.
   - rewrite -(idemp uPred_and Î”) {1}envs_lookup_sound //; simpl; rewrite HP1.
     rewrite envs_simple_replace_sound //; simpl.
-    rewrite (sep_elim_r _ (_ -â˜… _)) right_id (to_wand R) always_if_elim.
+    rewrite (sep_elim_r _ (_ -â˜… _)) right_id (into_wand R) always_if_elim.
     by rewrite wand_elim_l always_and_sep_l -{1}(always_if_always q P2) wand_elim_r.
 Qed.
 
@@ -610,7 +610,7 @@ Proof.
 Qed.
 
 Lemma tac_assert Î” Î”1 Î”2 Î”2' lr js j P Q R :
-  ToAssert P Q R â†’
+  IntoAssert P Q R â†’
   envs_split lr js Î” = Some (Î”1,Î”2) â†’
   envs_app false (Esnoc Enil j P) Î”2 = Some Î”2' â†’
   (Î”1 âŠ¢ R) â†’ (Î”2' âŠ¢ Q) â†’ Î” âŠ¢ Q.
@@ -630,22 +630,24 @@ Proof.
 Qed.
 
 (** Whenever posing [lem : True âŠ¢ Q] as [H] we want it to appear as [H : Q] and
-not as [H : True -â˜… Q]. The class [ToPosedProof] is used to strip off the
+not as [H : True -â˜… Q]. The class [IntoPosedProof] is used to strip off the
 [True]. Note that [to_posed_proof_True] is declared using a [Hint Extern] to
 make sure it is not used while posing [lem : ?P âŠ¢ Q] with [?P] an evar. *)
-Class ToPosedProof (P1 P2 R : uPred M) := to_pose_proof : (P1 âŠ¢ P2) â†’ True âŠ¢ R.
-Arguments to_pose_proof : clear implicits.
-Instance to_posed_proof_True P : ToPosedProof True P P.
-Proof. by rewrite /ToPosedProof. Qed.
-Global Instance to_posed_proof_wand P Q : ToPosedProof P Q (P -â˜… Q).
-Proof. rewrite /ToPosedProof. apply entails_wand. Qed.
+Class IntoPosedProof (P1 P2 R : uPred M) :=
+  into_pose_proof : (P1 âŠ¢ P2) â†’ True âŠ¢ R.
+Arguments into_pose_proof : clear implicits.
+Instance to_posed_proof_True P : IntoPosedProof True P P.
+Proof. by rewrite /IntoPosedProof. Qed.
+Global Instance to_posed_proof_wand P Q : IntoPosedProof P Q (P -â˜… Q).
+Proof. rewrite /IntoPosedProof. apply entails_wand. Qed.
 
 Lemma tac_pose_proof Î” Î”' j P1 P2 R Q :
-  (P1 âŠ¢ P2) â†’ ToPosedProof P1 P2 R â†’ envs_app true (Esnoc Enil j R) Î” = Some Î”' â†’
+  (P1 âŠ¢ P2) â†’ IntoPosedProof P1 P2 R â†’
+  envs_app true (Esnoc Enil j R) Î” = Some Î”' â†’
   (Î”' âŠ¢ Q) â†’ Î” âŠ¢ Q.
 Proof.
   intros HP ?? <-. rewrite envs_app_sound //; simpl.
-  by rewrite right_id -(to_pose_proof P1 P2 R) // always_pure wand_True.
+  by rewrite right_id -(into_pose_proof P1 P2 R) // always_pure wand_True.
 Qed.
 
 Lemma tac_pose_proof_hyp Î” Î”' Î”'' i p j P Q :
@@ -661,11 +663,11 @@ Proof.
 Qed.
 
 Lemma tac_apply Î” Î”' i p R P1 P2 :
-  envs_lookup_delete i Î” = Some (p, R, Î”') â†’ ToWand R P1 P2 â†’
+  envs_lookup_delete i Î” = Some (p, R, Î”') â†’ IntoWand R P1 P2 â†’
   (Î”' âŠ¢ P1) â†’ Î” âŠ¢ P2.
 Proof.
   intros ?? HP1. rewrite envs_lookup_delete_sound' //.
-  by rewrite (to_wand R) HP1 wand_elim_l.
+  by rewrite (into_wand R) HP1 wand_elim_l.
 Qed.
 
 (** * Rewriting *)
@@ -703,71 +705,71 @@ Proof.
 Qed.
 
 (** * Conjunction splitting *)
-Class AndSplit (P Q1 Q2 : uPred M) := and_split : Q1 âˆ§ Q2 âŠ¢ P.
-Arguments and_split : clear implicits.
+Class FromAnd (P Q1 Q2 : uPred M) := from_and : Q1 âˆ§ Q2 âŠ¢ P.
+Arguments from_and : clear implicits.
 
-Global Instance and_split_and P1 P2 : AndSplit (P1 âˆ§ P2) P1 P2.
+Global Instance from_and_and P1 P2 : FromAnd (P1 âˆ§ P2) P1 P2.
 Proof. done. Qed.
-Global Instance and_split_sep_persistent_l P1 P2 :
-  PersistentP P1 â†’ AndSplit (P1 â˜… P2) P1 P2.
-Proof. intros. by rewrite /AndSplit always_and_sep_l. Qed.
-Global Instance and_split_sep_persistent_r P1 P2 :
-  PersistentP P2 â†’ AndSplit (P1 â˜… P2) P1 P2.
-Proof. intros. by rewrite /AndSplit always_and_sep_r. Qed.
-Global Instance and_split_always P Q1 Q2 :
-  AndSplit P Q1 Q2 â†’ AndSplit (â–¡ P) (â–¡ Q1) (â–¡ Q2).
-Proof. rewrite /AndSplit=> <-. by rewrite always_and. Qed.
-Global Instance and_split_later P Q1 Q2 :
-  AndSplit P Q1 Q2 â†’ AndSplit (â–· P) (â–· Q1) (â–· Q2).
-Proof. rewrite /AndSplit=> <-. by rewrite later_and. Qed.
-
-Lemma tac_and_split Î” P Q1 Q2 : AndSplit P Q1 Q2 â†’ (Î” âŠ¢ Q1) â†’ (Î” âŠ¢ Q2) â†’ Î” âŠ¢ P.
-Proof. intros. rewrite -(and_split P). by apply and_intro. Qed.
+Global Instance from_and_sep_persistent_l P1 P2 :
+  PersistentP P1 â†’ FromAnd (P1 â˜… P2) P1 P2.
+Proof. intros. by rewrite /FromAnd always_and_sep_l. Qed.
+Global Instance from_and_sep_persistent_r P1 P2 :
+  PersistentP P2 â†’ FromAnd (P1 â˜… P2) P1 P2.
+Proof. intros. by rewrite /FromAnd always_and_sep_r. Qed.
+Global Instance from_and_always P Q1 Q2 :
+  FromAnd P Q1 Q2 â†’ FromAnd (â–¡ P) (â–¡ Q1) (â–¡ Q2).
+Proof. rewrite /FromAnd=> <-. by rewrite always_and. Qed.
+Global Instance from_and_later P Q1 Q2 :
+  FromAnd P Q1 Q2 â†’ FromAnd (â–· P) (â–· Q1) (â–· Q2).
+Proof. rewrite /FromAnd=> <-. by rewrite later_and. Qed.
+
+Lemma tac_and_split Î” P Q1 Q2 : FromAnd P Q1 Q2 â†’ (Î” âŠ¢ Q1) â†’ (Î” âŠ¢ Q2) â†’ Î” âŠ¢ P.
+Proof. intros. rewrite -(from_and P). by apply and_intro. Qed.
 
 (** * Separating conjunction splitting *)
-Class SepSplit (P Q1 Q2 : uPred M) := sep_split : Q1 â˜… Q2 âŠ¢ P.
-Arguments sep_split : clear implicits.
+Class FromSep (P Q1 Q2 : uPred M) := from_sep : Q1 â˜… Q2 âŠ¢ P.
+Arguments from_sep : clear implicits.
 
-Global Instance sep_split_sep P1 P2 : SepSplit (P1 â˜… P2) P1 P2 | 100.
+Global Instance from_sep_sep P1 P2 : FromSep (P1 â˜… P2) P1 P2 | 100.
 Proof. done. Qed.
-Global Instance sep_split_always P Q1 Q2 :
-  SepSplit P Q1 Q2 â†’ SepSplit (â–¡ P) (â–¡ Q1) (â–¡ Q2).
-Proof. rewrite /SepSplit=> <-. by rewrite always_sep. Qed.
-Global Instance sep_split_later P Q1 Q2 :
-  SepSplit P Q1 Q2 â†’ SepSplit (â–· P) (â–· Q1) (â–· Q2).
-Proof. rewrite /SepSplit=> <-. by rewrite later_sep. Qed.
-
-Global Instance sep_split_ownM (a b : M) :
-  SepSplit (uPred_ownM (a â‹… b)) (uPred_ownM a) (uPred_ownM b) | 99.
-Proof. by rewrite /SepSplit ownM_op. Qed.
-Global Instance sep_split_big_sepM
+Global Instance from_sep_always P Q1 Q2 :
+  FromSep P Q1 Q2 â†’ FromSep (â–¡ P) (â–¡ Q1) (â–¡ Q2).
+Proof. rewrite /FromSep=> <-. by rewrite always_sep. Qed.
+Global Instance from_sep_later P Q1 Q2 :
+  FromSep P Q1 Q2 â†’ FromSep (â–· P) (â–· Q1) (â–· Q2).
+Proof. rewrite /FromSep=> <-. by rewrite later_sep. Qed.
+
+Global Instance from_sep_ownM (a b : M) :
+  FromSep (uPred_ownM (a â‹… b)) (uPred_ownM a) (uPred_ownM b) | 99.
+Proof. by rewrite /FromSep ownM_op. Qed.
+Global Instance from_sep_big_sepM
     `{Countable K} {A} (Î¦ Î¨1 Î¨2 : K â†’ A â†’ uPred M) m :
-  (âˆ€ k x, SepSplit (Î¦ k x) (Î¨1 k x) (Î¨2 k x)) â†’
-  SepSplit ([â˜… map] k â†¦ x âˆˆ m, Î¦ k x)
+  (âˆ€ k x, FromSep (Î¦ k x) (Î¨1 k x) (Î¨2 k x)) â†’
+  FromSep ([â˜… map] k â†¦ x âˆˆ m, Î¦ k x)
     ([â˜… map] k â†¦ x âˆˆ m, Î¨1 k x) ([â˜… map] k â†¦ x âˆˆ m, Î¨2 k x).
 Proof.
-  rewrite /SepSplit=> ?. rewrite -big_sepM_sepM. by apply big_sepM_mono.
+  rewrite /FromSep=> ?. rewrite -big_sepM_sepM. by apply big_sepM_mono.
 Qed.
-Global Instance sep_split_big_sepS `{Countable A} (Î¦ Î¨1 Î¨2 : A â†’ uPred M) X :
-  (âˆ€ x, SepSplit (Î¦ x) (Î¨1 x) (Î¨2 x)) â†’
-  SepSplit ([â˜… set] x âˆˆ X, Î¦ x) ([â˜… set] x âˆˆ X, Î¨1 x) ([â˜… set] x âˆˆ X, Î¨2 x).
+Global Instance from_sep_big_sepS `{Countable A} (Î¦ Î¨1 Î¨2 : A â†’ uPred M) X :
+  (âˆ€ x, FromSep (Î¦ x) (Î¨1 x) (Î¨2 x)) â†’
+  FromSep ([â˜… set] x âˆˆ X, Î¦ x) ([â˜… set] x âˆˆ X, Î¨1 x) ([â˜… set] x âˆˆ X, Î¨2 x).
 Proof.
-  rewrite /SepSplit=> ?. rewrite -big_sepS_sepS. by apply big_sepS_mono.
+  rewrite /FromSep=> ?. rewrite -big_sepS_sepS. by apply big_sepS_mono.
 Qed.
 
 Lemma tac_sep_split Î” Î”1 Î”2 lr js P Q1 Q2 :
-  SepSplit P Q1 Q2 â†’
+  FromSep P Q1 Q2 â†’
   envs_split lr js Î” = Some (Î”1,Î”2) â†’
   (Î”1 âŠ¢ Q1) â†’ (Î”2 âŠ¢ Q2) â†’ Î” âŠ¢ P.
 Proof.
-  intros. rewrite envs_split_sound // -(sep_split P). by apply sep_mono.
+  intros. rewrite envs_split_sound // -(from_sep P). by apply sep_mono.
 Qed.
 
 (** * Combining *)
 Lemma tac_combine Î”1 Î”2 Î”3 Î”4 i1 p P1 i2 q P2 j P Q :
   envs_lookup_delete i1 Î”1 = Some (p,P1,Î”2) â†’
   envs_lookup_delete i2 (if p then Î”1 else Î”2) = Some (q,P2,Î”3) â†’
-  SepSplit P P1 P2 â†’
+  FromSep P P1 P2 â†’
   envs_app (p && q) (Esnoc Enil j P)
     (if q then (if p then Î”1 else Î”2) else Î”3) = Some Î”4 â†’
   (Î”4 âŠ¢ Q) â†’ Î”1 âŠ¢ Q.
@@ -776,83 +778,81 @@ Proof.
   destruct p.
   - rewrite envs_lookup_persistent_sound //. destruct q.
     + rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl.
-      by rewrite right_id assoc -always_sep (sep_split P) wand_elim_r.
+      by rewrite right_id assoc -always_sep (from_sep P) wand_elim_r.
     + rewrite envs_lookup_sound // envs_app_sound //; simpl.
-      by rewrite right_id assoc always_elim (sep_split P) wand_elim_r.
+      by rewrite right_id assoc always_elim (from_sep P) wand_elim_r.
   - rewrite envs_lookup_sound //; simpl. destruct q.
     + rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl.
-      by rewrite right_id assoc always_elim (sep_split P) wand_elim_r.
+      by rewrite right_id assoc always_elim (from_sep P) wand_elim_r.
     + rewrite envs_lookup_sound // envs_app_sound //; simpl.
-      by rewrite right_id assoc (sep_split P) wand_elim_r.
+      by rewrite right_id assoc (from_sep P) wand_elim_r.
 Qed.
 
 (** * Conjunction/separating conjunction elimination *)
-Class SepDestruct (p : bool) (P Q1 Q2 : uPred M) :=
-  sep_destruct : â–¡?p P âŠ¢ â–¡?p (Q1 â˜… Q2).
-Arguments sep_destruct : clear implicits.
-Class OpDestruct {A : cmraT} (a b1 b2 : A) :=
-  op_destruct : a â‰¡ b1 â‹… b2.
-Arguments op_destruct {_} _ _ _ {_}.
-
-Global Instance op_destruct_op {A : cmraT} (a b : A) : OpDestruct (a â‹… b) a b.
-Proof. by rewrite /OpDestruct. Qed.
-Global Instance op_destruct_persistent {A : cmraT} (a : A) :
-  Persistent a â†’ OpDestruct a a a.
+Class IntoSep (p: bool) (P Q1 Q2 : uPred M) := into_sep : â–¡?p P âŠ¢ â–¡?p (Q1 â˜… Q2).
+Arguments into_sep : clear implicits.
+Class IntoOp {A : cmraT} (a b1 b2 : A) := into_op : a â‰¡ b1 â‹… b2.
+Arguments into_op {_} _ _ _ {_}.
+
+Global Instance into_op_op {A : cmraT} (a b : A) : IntoOp (a â‹… b) a b.
+Proof. by rewrite /IntoOp. Qed.
+Global Instance into_op_persistent {A : cmraT} (a : A) :
+  Persistent a â†’ IntoOp a a a.
 Proof. intros; apply (persistent_dup a). Qed.
-Global Instance op_destruct_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
-  OpDestruct a b1 b2 â†’ OpDestruct a' b1' b2' â†’
-  OpDestruct (a,a') (b1,b1') (b2,b2').
+Global Instance into_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
+  IntoOp a b1 b2 â†’ IntoOp a' b1' b2' â†’
+  IntoOp (a,a') (b1,b1') (b2,b2').
 Proof. by constructor. Qed.
-Global Instance op_destruct_Some {A : cmraT} (a : A) b1 b2 :
-  OpDestruct a b1 b2 â†’ OpDestruct (Some a) (Some b1) (Some b2).
+Global Instance into_op_Some {A : cmraT} (a : A) b1 b2 :
+  IntoOp a b1 b2 â†’ IntoOp (Some a) (Some b1) (Some b2).
 Proof. by constructor. Qed.
 
-Global Instance sep_destruct_sep p P Q : SepDestruct p (P â˜… Q) P Q.
-Proof. rewrite /SepDestruct. by rewrite always_if_sep. Qed.
-Global Instance sep_destruct_ownM p (a b1 b2 : M) :
-  OpDestruct a b1 b2 â†’
-  SepDestruct p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Global Instance into_sep_sep p P Q : IntoSep p (P â˜… Q) P Q.
+Proof. rewrite /IntoSep. by rewrite always_if_sep. Qed.
+Global Instance into_sep_ownM p (a b1 b2 : M) :
+  IntoOp a b1 b2 â†’
+  IntoSep p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
 Proof.
-  rewrite /OpDestruct /SepDestruct=> ->. by rewrite ownM_op always_if_sep.
+  rewrite /IntoOp /IntoSep=> ->. by rewrite ownM_op always_if_sep.
 Qed.
 
-Global Instance sep_destruct_and P Q : SepDestruct true (P âˆ§ Q) P Q.
-Proof. by rewrite /SepDestruct /= always_and_sep. Qed.
-Global Instance sep_destruct_and_persistent_l P Q :
-  PersistentP P â†’ SepDestruct false (P âˆ§ Q) P Q.
-Proof. intros; by rewrite /SepDestruct /= always_and_sep_l. Qed.
-Global Instance sep_destruct_and_persistent_r P Q :
-  PersistentP Q â†’ SepDestruct false (P âˆ§ Q) P Q.
-Proof. intros; by rewrite /SepDestruct /= always_and_sep_r. Qed.
+Global Instance into_sep_and P Q : IntoSep true (P âˆ§ Q) P Q.
+Proof. by rewrite /IntoSep /= always_and_sep. Qed.
+Global Instance into_sep_and_persistent_l P Q :
+  PersistentP P â†’ IntoSep false (P âˆ§ Q) P Q.
+Proof. intros; by rewrite /IntoSep /= always_and_sep_l. Qed.
+Global Instance into_sep_and_persistent_r P Q :
+  PersistentP Q â†’ IntoSep false (P âˆ§ Q) P Q.
+Proof. intros; by rewrite /IntoSep /= always_and_sep_r. Qed.
 
-Global Instance sep_destruct_later p P Q1 Q2 :
-  SepDestruct p P Q1 Q2 â†’ SepDestruct p (â–· P) (â–· Q1) (â–· Q2).
-Proof. by rewrite /SepDestruct -later_sep !always_if_later=> ->. Qed.
+Global Instance into_sep_later p P Q1 Q2 :
+  IntoSep p P Q1 Q2 â†’ IntoSep p (â–· P) (â–· Q1) (â–· Q2).
+Proof. by rewrite /IntoSep -later_sep !always_if_later=> ->. Qed.
 
-Global Instance sep_destruct_big_sepM
+Global Instance into_sep_big_sepM
     `{Countable K} {A} (Î¦ Î¨1 Î¨2 : K â†’ A â†’ uPred M) p m :
-  (âˆ€ k x, SepDestruct p (Î¦ k x) (Î¨1 k x) (Î¨2 k x)) â†’
-  SepDestruct p ([â˜… map] k â†¦ x âˆˆ m, Î¦ k x)
+  (âˆ€ k x, IntoSep p (Î¦ k x) (Î¨1 k x) (Î¨2 k x)) â†’
+  IntoSep p ([â˜… map] k â†¦ x âˆˆ m, Î¦ k x)
     ([â˜… map] k â†¦ x âˆˆ m, Î¨1 k x) ([â˜… map] k â†¦ x âˆˆ m, Î¨2 k x).
 Proof.
-  rewrite /SepDestruct=> ?. rewrite -big_sepM_sepM !big_sepM_always_if.
+  rewrite /IntoSep=> ?. rewrite -big_sepM_sepM !big_sepM_always_if.
   by apply big_sepM_mono.
 Qed.
-Global Instance sep_destruct_big_sepS `{Countable A} (Î¦ Î¨1 Î¨2 : A â†’ uPred M) p X :
-  (âˆ€ x, SepDestruct p (Î¦ x) (Î¨1 x) (Î¨2 x)) â†’
-  SepDestruct p ([â˜… set] x âˆˆ X, Î¦ x) ([â˜… set] x âˆˆ X, Î¨1 x) ([â˜… set] x âˆˆ X, Î¨2 x).
+Global Instance into_sep_big_sepS `{Countable A} (Î¦ Î¨1 Î¨2 : A â†’ uPred M) p X :
+  (âˆ€ x, IntoSep p (Î¦ x) (Î¨1 x) (Î¨2 x)) â†’
+  IntoSep p ([â˜… set] x âˆˆ X, Î¦ x) ([â˜… set] x âˆˆ X, Î¨1 x) ([â˜… set] x âˆˆ X, Î¨2 x).
 Proof.
-  rewrite /SepDestruct=> ?. rewrite -big_sepS_sepS !big_sepS_always_if.
+  rewrite /IntoSep=> ?. rewrite -big_sepS_sepS !big_sepS_always_if.
   by apply big_sepS_mono.
 Qed.
 
 Lemma tac_sep_destruct Î” Î”' i p j1 j2 P P1 P2 Q :
-  envs_lookup i Î” = Some (p, P) â†’ SepDestruct p P P1 P2 â†’
+  envs_lookup i Î” = Some (p, P) â†’ IntoSep p 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 (sep_destruct p P) right_id (comm uPred_sep P1) wand_elim_r.
+  by rewrite (into_sep p P) right_id (comm uPred_sep P1) wand_elim_r.
 Qed.
 
 (** * Framing *)
@@ -930,32 +930,32 @@ Proof.
 Qed.
 
 (** * Disjunction *)
-Class OrSplit (P Q1 Q2 : uPred M) := or_split : Q1 âˆ¨ Q2 âŠ¢ P.
-Arguments or_split : clear implicits.
-Global Instance or_split_or P1 P2 : OrSplit (P1 âˆ¨ P2) P1 P2.
+Class FromOr (P Q1 Q2 : uPred M) := from_or : Q1 âˆ¨ Q2 âŠ¢ P.
+Arguments from_or : clear implicits.
+Global Instance from_or_or P1 P2 : FromOr (P1 âˆ¨ P2) P1 P2.
 Proof. done. Qed.
 
-Lemma tac_or_l Î” P Q1 Q2 : OrSplit P Q1 Q2 â†’ (Î” âŠ¢ Q1) â†’ Î” âŠ¢ P.
-Proof. intros. rewrite -(or_split P). by apply or_intro_l'. Qed.
-Lemma tac_or_r Î” P Q1 Q2 : OrSplit P Q1 Q2 â†’ (Î” âŠ¢ Q2) â†’ Î” âŠ¢ P.
-Proof. intros. rewrite -(or_split P). by apply or_intro_r'. Qed.
+Lemma tac_or_l Î” P Q1 Q2 : FromOr P Q1 Q2 â†’ (Î” âŠ¢ Q1) â†’ Î” âŠ¢ P.
+Proof. intros. rewrite -(from_or P). by apply or_intro_l'. Qed.
+Lemma tac_or_r Î” P Q1 Q2 : FromOr P Q1 Q2 â†’ (Î” âŠ¢ Q2) â†’ Î” âŠ¢ P.
+Proof. intros. rewrite -(from_or P). by apply or_intro_r'. Qed.
 
-Class OrDestruct P Q1 Q2 := or_destruct : P âŠ¢ Q1 âˆ¨ Q2.
-Arguments or_destruct : clear implicits.
-Global Instance or_destruct_or P Q : OrDestruct (P âˆ¨ Q) P Q.
+Class IntoOr P Q1 Q2 := into_or : P âŠ¢ Q1 âˆ¨ Q2.
+Arguments into_or : clear implicits.
+Global Instance into_or_or P Q : IntoOr (P âˆ¨ Q) P Q.
 Proof. done. Qed.
-Global Instance or_destruct_later P Q1 Q2 :
-  OrDestruct P Q1 Q2 â†’ OrDestruct (â–· P) (â–· Q1) (â–· Q2).
-Proof. rewrite /OrDestruct=>->. by rewrite later_or. Qed.
+Global Instance into_or_later P Q1 Q2 :
+  IntoOr P Q1 Q2 â†’ IntoOr (â–· P) (â–· Q1) (â–· Q2).
+Proof. rewrite /IntoOr=>->. by rewrite later_or. Qed.
 
 Lemma tac_or_destruct Î” Î”1 Î”2 i p j1 j2 P P1 P2 Q :
-  envs_lookup i Î” = Some (p, P) â†’ OrDestruct P P1 P2 â†’
+  envs_lookup i Î” = Some (p, P) â†’ IntoOr P P1 P2 â†’
   envs_simple_replace i p (Esnoc Enil j1 P1) Î” = Some Î”1 â†’
   envs_simple_replace i p (Esnoc Enil j2 P2) Î” = Some Î”2 â†’
   (Î”1 âŠ¢ Q) â†’ (Î”2 âŠ¢ Q) â†’ Î” âŠ¢ Q.
 Proof.
   intros ???? HP1 HP2. rewrite envs_lookup_sound //.
-  rewrite (or_destruct P) always_if_or sep_or_r; apply or_elim.
+  rewrite (into_or P) always_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) //.
@@ -991,41 +991,40 @@ Lemma tac_forall_revert {A} Î” (Î¦ : A â†’ uPred M) :
 Proof. intros HÎ” a. by rewrite HÎ” (forall_elim a). Qed.
 
 (** * Existential *)
-Class ExistSplit {A} (P : uPred M) (Î¦ : A â†’ uPred M) :=
-  exist_split : (âˆƒ x, Î¦ x) âŠ¢ P.
-Arguments exist_split {_} _ _ {_}.
-Global Instance exist_split_exist {A} (Î¦: A â†’ uPred M): ExistSplit (âˆƒ a, Î¦ a) Î¦.
+Class FromExist {A} (P : uPred M) (Î¦ : A â†’ uPred M) :=
+  from_exist : (âˆƒ x, Î¦ x) âŠ¢ P.
+Arguments from_exist {_} _ _ {_}.
+Global Instance from_exist_exist {A} (Î¦: A â†’ uPred M): FromExist (âˆƒ a, Î¦ a) Î¦.
 Proof. done. Qed.
 
 Lemma tac_exist {A} Î” P (Î¦ : A â†’ uPred M) :
-  ExistSplit P Î¦ â†’ (âˆƒ a, Î” âŠ¢ Î¦ a) â†’ Î” âŠ¢ P.
-Proof. intros ? [a ?]. rewrite -(exist_split P). eauto using exist_intro'. Qed.
-
-Class ExistDestruct {A} (P : uPred M) (Î¦ : A â†’ uPred M) :=
-  exist_destruct : P âŠ¢ âˆƒ x, Î¦ x.
-Arguments exist_destruct {_} _ _ {_}.
-Global Instance exist_destruct_exist {A} (Î¦ : A â†’ uPred M) :
-  ExistDestruct (âˆƒ a, Î¦ a) Î¦.
+  FromExist P Î¦ â†’ (âˆƒ a, Î” âŠ¢ Î¦ a) â†’ Î” âŠ¢ P.
+Proof. intros ? [a ?]. rewrite -(from_exist P). eauto using exist_intro'. Qed.
+
+Class IntoExist {A} (P : uPred M) (Î¦ : A â†’ uPred M) :=
+  into_exist : P âŠ¢ âˆƒ x, Î¦ x.
+Arguments into_exist {_} _ _ {_}.
+Global Instance into_exist_exist {A} (Î¦ : A â†’ uPred M) : IntoExist (âˆƒ a, Î¦ a) Î¦.
 Proof. done. Qed.
-Global Instance exist_destruct_later {A} P (Î¦ : A â†’ uPred M) :
-  ExistDestruct P Î¦ â†’ Inhabited A â†’ ExistDestruct (â–· P) (Î» a, â–· (Î¦ a))%I.
-Proof. rewrite /ExistDestruct=> HP ?. by rewrite HP later_exist. Qed.
-Global Instance exist_destruct_always {A} P (Î¦ : A â†’ uPred M) :
-  ExistDestruct P Î¦ â†’ ExistDestruct (â–¡ P) (Î» a, â–¡ (Î¦ a))%I.
-Proof. rewrite /ExistDestruct=> HP. by rewrite HP always_exist. Qed.
+Global Instance into_exist_later {A} P (Î¦ : A â†’ uPred M) :
+  IntoExist P Î¦ â†’ Inhabited A â†’ IntoExist (â–· P) (Î» a, â–· (Î¦ a))%I.
+Proof. rewrite /IntoExist=> HP ?. by rewrite HP later_exist. Qed.
+Global Instance into_exist_always {A} P (Î¦ : A â†’ uPred M) :
+  IntoExist P Î¦ â†’ IntoExist (â–¡ P) (Î» a, â–¡ (Î¦ a))%I.
+Proof. rewrite /IntoExist=> HP. by rewrite HP always_exist. Qed.
 
 Lemma tac_exist_destruct {A} Î” i p j P (Î¦ : A â†’ uPred M) Q :
-  envs_lookup i Î” = Some (p, P) â†’ ExistDestruct P Î¦ â†’
+  envs_lookup i Î” = Some (p, P) â†’ IntoExist P Î¦ â†’
   (âˆ€ a, âˆƒ Î”',
     envs_simple_replace i p (Esnoc Enil j (Î¦ a)) Î” = Some Î”' âˆ§ (Î”' âŠ¢ Q)) â†’
   Î” âŠ¢ Q.
 Proof.
   intros ?? HÎ¦. rewrite envs_lookup_sound //.
-  rewrite (exist_destruct P) always_if_exist sep_exist_r.
+  rewrite (into_exist P) always_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.
 Qed.
 End tactics.
 
-Hint Extern 0 (ToPosedProof True _ _) =>
+Hint Extern 0 (IntoPosedProof True _ _) =>
   class_apply @to_posed_proof_True : typeclass_instances.
diff --git a/proofmode/ghost_ownership.v b/proofmode/ghost_ownership.v
index 87b8e0ef3..2c557444a 100644
--- a/proofmode/ghost_ownership.v
+++ b/proofmode/ghost_ownership.v
@@ -6,10 +6,10 @@ Section ghost.
 Context `{inG Î› Î£ A}.
 Implicit Types a b : A.
 
-Global Instance sep_destruct_own p Î³ a b1 b2 :
-  OpDestruct a b1 b2 â†’ SepDestruct p (own Î³ a) (own Î³ b1) (own Î³ b2).
-Proof. rewrite /OpDestruct /SepDestruct => ->. by rewrite own_op. Qed.
-Global Instance sep_split_own Î³ a b :
-  SepSplit (own Î³ (a â‹… b)) (own Î³ a) (own Î³ b) | 90.
-Proof. by rewrite /SepSplit own_op. Qed.
+Global Instance into_sep_own p Î³ a b1 b2 :
+  IntoOp a b1 b2 â†’ IntoSep p (own Î³ a) (own Î³ b1) (own Î³ b2).
+Proof. rewrite /IntoOp /IntoSep => ->. by rewrite own_op. Qed.
+Global Instance from_sep_own Î³ a b :
+  FromSep (own Î³ (a â‹… b)) (own Î³ a) (own Î³ b) | 90.
+Proof. by rewrite /FromSep own_op. Qed.
 End ghost.
diff --git a/proofmode/invariants.v b/proofmode/invariants.v
index fbb6478ec..48277e7cf 100644
--- a/proofmode/invariants.v
+++ b/proofmode/invariants.v
@@ -9,23 +9,23 @@ Implicit Types N : namespace.
 Implicit Types P Q R : iProp Î› Î£.
 
 Lemma tac_inv_fsa {A} (fsa : FSA Î› Î£ A) fsaV Î” Î”' E N i P Q Î¦ :
-  FSASplit Q E fsa fsaV Î¦ â†’
+  IsFSA Q E fsa fsaV Î¦ â†’
   fsaV â†’ nclose N âŠ† E â†’ (of_envs Î” âŠ¢ inv N P) â†’
   envs_app false (Esnoc Enil i (â–· P)) Î” = Some Î”' â†’
   (Î”' âŠ¢ fsa (E âˆ– nclose N) (Î» a, â–· P â˜… Î¦ a)) â†’ Î” âŠ¢ Q.
 Proof.
-  intros ????? HÎ”'. rewrite -(fsa_split Q) -(inv_fsa fsa _ _ P) //.
+  intros ????? HÎ”'. rewrite (is_fsa Q) -(inv_fsa fsa _ _ P) //.
   rewrite // -always_and_sep_l. apply and_intro; first done.
   rewrite envs_app_sound //; simpl. by rewrite right_id HÎ”'.
 Qed.
 
 Lemma tac_inv_fsa_timeless {A} (fsa : FSA Î› Î£ A) fsaV Î” Î”' E N i P Q Î¦ :
-  FSASplit Q E fsa fsaV Î¦ â†’
+  IsFSA Q E fsa fsaV Î¦ â†’
   fsaV â†’ nclose N âŠ† E â†’ (of_envs Î” âŠ¢ inv N P) â†’ TimelessP P â†’
   envs_app false (Esnoc Enil i P) Î” = Some Î”' â†’
   (Î”' âŠ¢ fsa (E âˆ– nclose N) (Î» a, P â˜… Î¦ a)) â†’ Î” âŠ¢ Q.
 Proof.
-  intros ?????? HÎ”'. rewrite -(fsa_split Q) -(inv_fsa fsa _ _ P) //.
+  intros ?????? HÎ”'. rewrite (is_fsa Q) -(inv_fsa fsa _ _ P) //.
   rewrite // -always_and_sep_l. apply and_intro, wand_intro_l; first done.
   trans (|={E âˆ– N}=> P â˜… Î”)%I; first by rewrite pvs_timeless pvs_frame_r.
   apply (fsa_strip_pvs _).
@@ -36,7 +36,7 @@ End invariants.
 
 Tactic Notation "iInvCore" constr(N) "as" constr(H) :=
   eapply tac_inv_fsa with _ _ _ _ N H _ _;
-    [let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
+    [let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
      apply _ || fail "iInv: cannot viewshift in goal" P
     |try fast_done (* atomic *)
     |done || eauto with ndisj (* [eauto with ndisj] is slow *)
@@ -62,7 +62,7 @@ Tactic Notation "iInv" constr(N) "as" "{" simple_intropattern(x1)
 
 Tactic Notation "iInvCore>" constr(N) "as" constr(H) :=
   eapply tac_inv_fsa_timeless with _ _ _ _ N H _ _;
-    [let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
+    [let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
      apply _ || fail "iInv: cannot viewshift in goal" P
     |try fast_done (* atomic *)
     |done || eauto with ndisj (* [eauto with ndisj] is slow *)
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index 5085e6c50..86afa3f6b 100644
--- a/proofmode/pviewshifts.v
+++ b/proofmode/pviewshifts.v
@@ -7,45 +7,44 @@ Section pvs.
 Context {Î› : language} {Î£ : iFunctor}.
 Implicit Types P Q : iProp Î› Î£.
 
-Global Instance to_assumption_pvs E p P Q :
-  ToAssumption p P Q â†’ ToAssumption p P (|={E}=> Q)%I.
-Proof. rewrite /ToAssumption=>->. apply pvs_intro. Qed.
-Global Instance sep_split_pvs E P Q1 Q2 :
-  SepSplit P Q1 Q2 â†’ SepSplit (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
-Proof. rewrite /SepSplit=><-. apply pvs_sep. Qed.
+Global Instance from_assumption_pvs E p P Q :
+  FromAssumption p P Q â†’ FromAssumption p P (|={E}=> Q)%I.
+Proof. rewrite /FromAssumption=>->. apply pvs_intro. Qed.
+Global Instance from_sep_pvs E P Q1 Q2 :
+  FromSep P Q1 Q2 â†’ FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
+Proof. rewrite /FromSep=><-. apply pvs_sep. Qed.
 Global Instance or_split_pvs E1 E2 P Q1 Q2 :
-  OrSplit P Q1 Q2 â†’ OrSplit (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
-Proof. rewrite /OrSplit=><-. apply or_elim; apply pvs_mono; auto with I. Qed.
+  FromOr P Q1 Q2 â†’ FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
+Proof. rewrite /FromOr=><-. apply or_elim; apply pvs_mono; auto with I. Qed.
 Global Instance exists_split_pvs {A} E1 E2 P (Î¦ : A â†’ iProp Î› Î£) :
-  ExistSplit P Î¦ â†’ ExistSplit (|={E1,E2}=> P) (Î» a, |={E1,E2}=> Î¦ a)%I.
+  FromExist P Î¦ â†’ FromExist (|={E1,E2}=> P) (Î» a, |={E1,E2}=> Î¦ a)%I.
 Proof.
-  rewrite /ExistSplit=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
+  rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
 Qed.
 Global Instance frame_pvs E1 E2 R P Q :
   Frame R P Q â†’ Frame R (|={E1,E2}=> P) (|={E1,E2}=> Q).
 Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.
-Global Instance to_wand_pvs E1 E2 R P Q :
-  ToWand R P Q â†’ ToWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
-Proof. rewrite /ToWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
+Global Instance into_wand_pvs E1 E2 R P Q :
+  IntoWand R P Q â†’ IntoWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
+Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
 
-Class FSASplit {A} (P : iProp Î› Î£) (E : coPset)
+Class IsFSA {A} (P : iProp Î› Î£) (E : coPset)
     (fsa : FSA Î› Î£ A) (fsaV : Prop) (Î¦ : A â†’ iProp Î› Î£) := {
-  fsa_split : fsa E Î¦ âŠ£âŠ¢ P;
-  fsa_split_is_fsa :> FrameShiftAssertion fsaV fsa;
+  is_fsa : P âŠ£âŠ¢ fsa E Î¦;
+  is_fsa_is_fsa :> FrameShiftAssertion fsaV fsa;
 }.
-Global Arguments fsa_split {_} _ _ _ _ _ {_}.
-Global Instance fsa_split_pvs E P :
-  FSASplit (|={E}=> P)%I E pvs_fsa True (Î» _, P).
+Global Arguments is_fsa {_} _ _ _ _ _ {_}.
+Global Instance is_fsa_pvs E P :
+  IsFSA (|={E}=> P)%I E pvs_fsa True (Î» _, P).
 Proof. split. done. apply _. Qed.
-Global Instance fsa_split_fsa {A} (fsa : FSA Î› Î£ A) E Î¦ :
-  FrameShiftAssertion fsaV fsa â†’ FSASplit (fsa E Î¦) E fsa fsaV Î¦.
+Global Instance is_fsa_fsa {A} (fsa : FSA Î› Î£ A) E Î¦ :
+  FrameShiftAssertion fsaV fsa â†’ IsFSA (fsa E Î¦) E fsa fsaV Î¦.
 Proof. done. Qed.
 
 Global Instance to_assert_pvs {A} P Q E (fsa : FSA Î› Î£ A) fsaV Î¦ :
-  FSASplit Q E fsa fsaV Î¦ â†’ ToAssert P Q (|={E}=> P).
+  IsFSA Q E fsa fsaV Î¦ â†’ IntoAssert P Q (|={E}=> P).
 Proof.
-  intros.
-  by rewrite /ToAssert pvs_frame_r wand_elim_r -(fsa_split Q) fsa_pvs_fsa.
+  intros. by rewrite /IntoAssert pvs_frame_r wand_elim_r (is_fsa Q) fsa_pvs_fsa.
 Qed.
 
 Lemma tac_pvs_intro Î” E1 E2 Q : E1 = E2 â†’ (Î” âŠ¢ Q) â†’ Î” âŠ¢ |={E1,E2}=> Q.
@@ -66,11 +65,11 @@ Qed.
 
 Lemma tac_pvs_elim_fsa {A} (fsa : FSA Î› Î£ A) fsaV Î” Î”' E i p P' P Q Î¦ :
   envs_lookup i Î” = Some (p, P') â†’ P' = (|={E}=> P)%I â†’
-  FSASplit Q E fsa fsaV Î¦ â†’
+  IsFSA Q E fsa fsaV Î¦ â†’
   envs_replace i p false (Esnoc Enil i P) Î” = Some Î”' â†’
   (Î”' âŠ¢ fsa E Î¦) â†’ Î” âŠ¢ Q.
 Proof.
-  intros ? -> ??. rewrite -(fsa_split Q) -fsa_pvs_fsa.
+  intros ? -> ??. rewrite (is_fsa Q) -fsa_pvs_fsa.
   eapply tac_pvs_elim; set_solver.
 Qed.
 
@@ -85,12 +84,12 @@ Proof.
 Qed.
 
 Lemma tac_pvs_timeless_fsa {A} (fsa : FSA Î› Î£ A) fsaV Î” Î”' E i p P Q Î¦ :
-  FSASplit Q E fsa fsaV Î¦ â†’
+  IsFSA Q E fsa fsaV Î¦ â†’
   envs_lookup i Î” = Some (p, â–· P)%I â†’ TimelessP P â†’
   envs_simple_replace i p (Esnoc Enil i P) Î” = Some Î”' â†’
   (Î”' âŠ¢ fsa E Î¦) â†’ Î” âŠ¢ Q.
 Proof.
-  intros ????. rewrite -(fsa_split Q) -fsa_pvs_fsa.
+  intros ????. rewrite (is_fsa Q) -fsa_pvs_fsa.
   eauto using tac_pvs_timeless.
 Qed.
 End pvs.
@@ -114,7 +113,7 @@ Tactic Notation "iPvsCore" constr(H) :=
       [env_cbv; reflexivity || fail "iPvs:" H "not found"
       |let P := match goal with |- ?P = _ => P end in
        reflexivity || fail "iPvs:" H ":" P "not a pvs with the right mask"
-      |let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
+      |let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
        apply _ || fail "iPvs:" P "not a pvs"
       |env_cbv; reflexivity|simpl]
   end.
@@ -170,7 +169,7 @@ Tactic Notation "iTimeless" constr(H) :=
        |env_cbv; reflexivity|simpl]
   | |- _ =>
      eapply tac_pvs_timeless_fsa with _ _ _ _ H _ _ _;
-       [let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
+       [let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
         apply _ || fail "iTimeless: " P "not a pvs"
        |env_cbv; reflexivity || fail "iTimeless:" H "not found"
        |let P := match goal with |- TimelessP ?P => P end in
diff --git a/proofmode/sts.v b/proofmode/sts.v
index b4817fbac..4b535fb3c 100644
--- a/proofmode/sts.v
+++ b/proofmode/sts.v
@@ -8,7 +8,7 @@ Context `{stsG Î› Î£ sts} (Ï† : sts.state sts â†’ iPropG Î› Î£).
 Implicit Types P Q : iPropG Î› Î£.
 
 Lemma tac_sts_fsa {A} (fsa : FSA Î› _ A) fsaV Î” E N i Î³ S T Q Î¦ :
-  FSASplit Q E fsa fsaV Î¦ â†’
+  IsFSA Q E fsa fsaV Î¦ â†’
   fsaV â†’
   envs_lookup i Î” = Some (false, sts_ownS Î³ S T) â†’
   (of_envs Î” âŠ¢ sts_ctx Î³ N Ï†) â†’ nclose N âŠ† E â†’
@@ -18,7 +18,7 @@ Lemma tac_sts_fsa {A} (fsa : FSA Î› _ A) fsaV Î” E N i Î³ S T Q Î¦ :
       â–  sts.steps (s, T) (s', T') â˜… â–· Ï† s' â˜… (sts_own Î³ s' T' -â˜… Î¦ a)))) â†’
   Î” âŠ¢ Q.
 Proof.
-  intros ????? HÎ”'. rewrite -(fsa_split Q) -(sts_fsaS Ï† fsa) //.
+  intros ????? HÎ”'. rewrite (is_fsa Q) -(sts_fsaS Ï† fsa) //.
   rewrite // -always_and_sep_l. apply and_intro; first done.
   rewrite envs_lookup_sound //; simpl; apply sep_mono_r.
   apply forall_intro=>s; apply wand_intro_l.
@@ -36,7 +36,7 @@ Tactic Notation "iSts" constr(H) "as"
   | gname => eapply tac_sts_fsa with _ _ _ _ _ _ _ H _ _ _
   | _ => fail "iSts:" H "not a string or gname"
   end;
-    [let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
+    [let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
      apply _ || fail "iSts: cannot viewshift in goal" P
     |try fast_done (* atomic *)
     |iAssumptionCore || fail "iSts:" H "not found"
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 28d0300ca..ab34269ab 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -68,7 +68,7 @@ Tactic Notation "iClear" constr(Hs) :=
 Tactic Notation "iExact" constr(H) :=
   eapply tac_assumption with H _ _; (* (i:=H) *)
     [env_cbv; reflexivity || fail "iExact:" H "not found"
-    |let P := match goal with |- ToAssumption _ ?P _ => P end in
+    |let P := match goal with |- FromAssumption _ ?P _ => P end in
      apply _ || fail "iExact:" H ":" P "does not match goal"].
 
 Tactic Notation "iAssumptionCore" :=
@@ -88,7 +88,7 @@ Tactic Notation "iAssumption" :=
   let rec find p Î“ Q :=
     match Î“ with
     | Esnoc ?Î“ ?j ?P => first
-       [pose proof (_ : ToAssumption p P Q) as Hass;
+       [pose proof (_ : FromAssumption p P Q) as Hass;
         apply (tac_assumption _ j p P); [env_cbv; reflexivity|apply Hass]
        |find p Î“ Q]
     end in
@@ -105,20 +105,20 @@ Tactic Notation "iExFalso" := apply tac_ex_falso.
 Local Tactic Notation "iPersistent" constr(H) :=
   eapply tac_persistent with _ H _ _ _; (* (i:=H) *)
     [env_cbv; reflexivity || fail "iPersistent:" H "not found"
-    |let Q := match goal with |- ToPersistentP ?Q _ => Q end in
+    |let Q := match goal with |- IntoPersistentP ?Q _ => Q end in
      apply _ || fail "iPersistent:" H ":" Q "not persistent"
     |env_cbv; reflexivity|].
 
 Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
   eapply tac_pure with _ H _ _ _; (* (i:=H1) *)
     [env_cbv; reflexivity || fail "iPure:" H "not found"
-    |let P := match goal with |- ToPure ?P _ => P end in
+    |let P := match goal with |- IsPure ?P _ => P end in
      apply _ || fail "iPure:" H ":" P "not pure"
     |intros pat].
 
 Tactic Notation "iPureIntro" :=
   eapply tac_pure_intro;
-    [let P := match goal with |- ToPure ?P _ => P end in
+    [let P := match goal with |- IsPure ?P _ => P end in
      apply _ || fail "iPureIntro:" P "not pure"|].
 
 (** * Specialize *)
@@ -144,7 +144,7 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
 
 Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
   let solve_to_wand H1 :=
-    let P := match goal with |- ToWand ?P _ _ => P end in
+    let P := match goal with |- IntoWand ?P _ _ => P end in
     apply _ || fail "iSpecialize:" H1 ":" P "not an implication/wand" in
   let rec go H1 pats :=
     lazymatch pats with
@@ -154,8 +154,8 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
        eapply tac_specialize with _ _ H2 _ H1 _ _ _ _; (* (j:=H1) (i:=H2) *)
          [env_cbv; reflexivity || fail "iSpecialize:" H2 "not found"
          |env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
-         |let P := match goal with |- ToWand ?P ?Q _ => P end in
-          let Q := match goal with |- ToWand ?P ?Q _ => Q end in
+         |let P := match goal with |- IntoWand ?P ?Q _ => P end in
+          let Q := match goal with |- IntoWand ?P ?Q _ => Q end in
           apply _ || fail "iSpecialize: cannot instantiate" H1 ":" P "with" H2 ":" Q
          |env_cbv; reflexivity|go H1 pats]
     | SName true ?H2 :: ?pats =>
@@ -184,7 +184,7 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
        eapply tac_specialize_pure with _ H1 _ _ _ _ _;
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
-         |let Q := match goal with |- ToPure ?Q _ => Q end in
+         |let Q := match goal with |- IsPure ?Q _ => Q end in
           apply _ || fail "iSpecialize:" Q "not pure"
          |env_cbv; reflexivity
          |(*goal*)
@@ -194,7 +194,7 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
          |match k with
-          | GoalStd => apply to_assert_fallthrough
+          | GoalStd => apply into_assert_fallthrough
           | GoalPvs => apply _ || fail "iSpecialize: cannot generate pvs goal"
           end
          |env_cbv; reflexivity || fail "iSpecialize:" Hs "not found"
@@ -237,7 +237,7 @@ Tactic Notation "iApply" open_constr(t) :=
     [iExact H
     |eapply tac_apply with _ H _ _ _;
        [env_cbv; reflexivity || fail 1 "iApply:" H "not found"
-       |let P := match goal with |- ToWand ?P _ _ => P end in
+       |let P := match goal with |- IntoWand ?P _ _ => P end in
         apply _ || fail 1 "iApply: cannot apply" H ":" P
        |lazy beta (* reduce betas created by instantiation *)]] in
   let Htmp := iFresh in
@@ -320,17 +320,17 @@ Tactic Notation "iRevert" "{" ident(x1) ident(x2) ident(x3) ident(x4)
 (** * Disjunction *)
 Tactic Notation "iLeft" :=
   eapply tac_or_l;
-    [let P := match goal with |- OrSplit ?P _ _ => P end in
+    [let P := match goal with |- FromOr ?P _ _ => P end in
      apply _ || fail "iLeft:" P "not a disjunction"|].
 Tactic Notation "iRight" :=
   eapply tac_or_r;
-    [let P := match goal with |- OrSplit ?P _ _ => P end in
+    [let P := match goal with |- FromOr ?P _ _ => P end in
      apply _ || fail "iRight:" P "not a disjunction"|].
 
 Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
   eapply tac_or_destruct with _ _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
     [env_cbv; reflexivity || fail "iOrDestruct:" H "not found"
-    |let P := match goal with |- OrDestruct ?P _ _ => P end in
+    |let P := match goal with |- IntoOr ?P _ _ => P end in
      apply _ || fail "iOrDestruct:" H ":" P "not a disjunction"
     |env_cbv; reflexivity || fail "iOrDestruct:" H1 "not fresh"
     |env_cbv; reflexivity || fail "iOrDestruct:" H2 "not fresh"| |].
@@ -340,7 +340,7 @@ Tactic Notation "iSplit" :=
   lazymatch goal with
   | |- _ âŠ¢ _ =>
     eapply tac_and_split;
-      [let P := match goal with |- AndSplit ?P _ _ => P end in
+      [let P := match goal with |- FromAnd ?P _ _ => P end in
        apply _ || fail "iSplit:" P "not a conjunction"| |]
   | |- _ âŠ£âŠ¢ _ => apply (anti_symm (âŠ¢))
   end.
@@ -348,13 +348,13 @@ Tactic Notation "iSplit" :=
 Tactic Notation "iSplitL" constr(Hs) :=
   let Hs := words Hs in
   eapply tac_sep_split with _ _ false Hs _ _; (* (js:=Hs) *)
-    [let P := match goal with |- SepSplit ?P _ _ => P end in
+    [let P := match goal with |- FromSep ?P _ _ => P end in
      apply _ || fail "iSplitL:" P "not a separating conjunction"
     |env_cbv; reflexivity || fail "iSplitL: hypotheses" Hs "not found"| |].
 Tactic Notation "iSplitR" constr(Hs) :=
   let Hs := words Hs in
   eapply tac_sep_split with _ _ true Hs _ _; (* (js:=Hs) *)
-    [let P := match goal with |- SepSplit ?P _ _ => P end in
+    [let P := match goal with |- FromSep ?P _ _ => P end in
      apply _ || fail "iSplitR:" P "not a separating conjunction"
     |env_cbv; reflexivity || fail "iSplitR: hypotheses" Hs "not found"| |].
 
@@ -364,7 +364,7 @@ Tactic Notation "iSplitR" := iSplitL "".
 Local Tactic Notation "iSepDestruct" constr(H) "as" constr(H1) constr(H2) :=
   eapply tac_sep_destruct with _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
     [env_cbv; reflexivity || fail "iSepDestruct:" H "not found"
-    |let P := match goal with |- SepDestruct _ ?P _ _ => P end in
+    |let P := match goal with |- IntoSep _ ?P _ _ => P end in
      apply _ || fail "iSepDestruct:" H ":" P "not separating destructable"
     |env_cbv; reflexivity || fail "iSepDestruct:" H1 "or" H2 " not fresh"|].
 
@@ -395,15 +395,15 @@ Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) :=
   eapply tac_combine with _ _ _ H1 _ _ H2 _ _ H _;
     [env_cbv; reflexivity || fail "iCombine:" H1 "not found"
     |env_cbv; reflexivity || fail "iCombine:" H2 "not found"
-    |let P1 := match goal with |- SepSplit _ ?P1 _ => P1 end in
-     let P2 := match goal with |- SepSplit _ _ ?P2 => P2 end in
+    |let P1 := match goal with |- FromSep _ ?P1 _ => P1 end in
+     let P2 := match goal with |- FromSep _ _ ?P2 => P2 end in
      apply _ || fail "iCombine: cannot combine" H1 ":" P1 "and" H2 ":" P2
     |env_cbv; reflexivity || fail "iCombine:" H "not fresh"|].
 
 (** * Existential *)
 Tactic Notation "iExists" uconstr(x1) :=
   eapply tac_exist;
-    [let P := match goal with |- ExistSplit ?P _ => P end in
+    [let P := match goal with |- FromExist ?P _ => P end in
      apply _ || fail "iExists:" P "not an existential"
     |cbv beta; eexists x1].
 
@@ -432,7 +432,7 @@ Local Tactic Notation "iExistDestruct" constr(H)
     "as" simple_intropattern(x) constr(Hx) :=
   eapply tac_exist_destruct with H _ Hx _ _; (* (i:=H) (j:=Hx) *)
     [env_cbv; reflexivity || fail "iExistDestruct:" H "not found"
-    |let P := match goal with |- ExistDestruct ?P _ => P end in
+    |let P := match goal with |- IntoExist ?P _ => P end in
      apply _ || fail "iExistDestruct:" H ":" P "not an existential"|];
   let y := fresh in
   intros y; eexists; split;
@@ -498,18 +498,18 @@ Tactic Notation "iAlways":=
 Tactic Notation "iNext":=
   eapply tac_next;
     [apply _
-    |let P := match goal with |- StripLaterL ?P _ => P end in
+    |let P := match goal with |- FromLater ?P _ => P end in
      apply _ || fail "iNext:" P "does not contain laters"|].
 
 (** * Introduction tactic *)
 Local Tactic Notation "iIntro" "{" simple_intropattern(x) "}" := first
   [ (* (âˆ€ _, _) *) apply tac_forall_intro; intros x
   | (* (?P â†’ _) *) eapply tac_impl_intro_pure;
-     [let P := match goal with |- ToPure ?P _ => P end in
+     [let P := match goal with |- IsPure ?P _ => P end in
       apply _ || fail "iIntro:" P "not pure"
      |intros x]
   | (* (?P -â˜… _) *) eapply tac_wand_intro_pure;
-     [let P := match goal with |- ToPure ?P _ => P end in
+     [let P := match goal with |- IsPure ?P _ => P end in
       apply _ || fail "iIntro:" P "not pure"
      |intros x]
   |intros x].
@@ -528,12 +528,12 @@ Local Tactic Notation "iIntro" constr(H) := first
 Local Tactic Notation "iIntro" "#" constr(H) := first
   [ (* (?P â†’ _) *)
     eapply tac_impl_intro_persistent with _ H _; (* (i:=H) *)
-      [let P := match goal with |- ToPersistentP ?P _ => P end in
+      [let P := match goal with |- IntoPersistentP ?P _ => P end in
        apply _ || fail 1 "iIntro: " P " not persistent"
       |env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
   | (* (?P -â˜… _) *)
     eapply tac_wand_intro_persistent with _ H _; (* (i:=H) *)
-      [let P := match goal with |- ToPersistentP ?P _ => P end in
+      [let P := match goal with |- IntoPersistentP ?P _ => P end in
        apply _ || fail 1 "iIntro: " P " not persistent"
       |env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
   | fail 1 "iIntro: nothing to introduce" ].
@@ -746,7 +746,7 @@ Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
   | [SGoal ?k ?lr ?Hs] =>
      eapply tac_assert with _ _ _ lr Hs H Q _; (* (js:=Hs) (j:=H) (P:=Q) *)
        [match k with
-        | GoalStd => apply to_assert_fallthrough
+        | GoalStd => apply into_assert_fallthrough
         | GoalPvs => apply _ || fail "iAssert: cannot generate pvs goal"
         end
        |env_cbv; reflexivity || fail "iAssert:" Hs "not found"
diff --git a/proofmode/weakestpre.v b/proofmode/weakestpre.v
index 2e60cd40e..e7249a464 100644
--- a/proofmode/weakestpre.v
+++ b/proofmode/weakestpre.v
@@ -11,7 +11,7 @@ Implicit Types Î¦ : val Î› â†’ iProp Î› Î£.
 Global Instance frame_wp E e R Î¦ Î¨ :
   (âˆ€ v, Frame R (Î¦ v) (Î¨ v)) â†’ Frame R (WP e @ E {{ Î¦ }}) (WP e @ E {{ Î¨ }}).
 Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
-Global Instance fsa_split_wp E e Î¦ :
-  FSASplit (WP e @ E {{ Î¦ }})%I E (wp_fsa e) (language.atomic e) Î¦.
+Global Instance is_fsa_wp E e Î¦ :
+  IsFSA (WP e @ E {{ Î¦ }})%I E (wp_fsa e) (language.atomic e) Î¦.
 Proof. split. done. apply _. Qed.
 End weakestpre.
-- 
GitLab