diff --git a/_CoqProject b/_CoqProject
index c2280582e58b18bb26178cd774d51cf98434e018..378e477576eafc1859e8d78d6a349fd9abd6a816 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -79,7 +79,6 @@ program_logic/saved_one_shot.v
 program_logic/auth.v
 program_logic/sts.v
 program_logic/namespaces.v
-program_logic/tactics.v
 heap_lang/lang.v
 heap_lang/tactics.v
 heap_lang/wp_tactics.v
@@ -96,7 +95,20 @@ heap_lang/lib/barrier/specification.v
 heap_lang/lib/barrier/protocol.v
 heap_lang/lib/barrier/proof.v
 heap_lang/lib/barrier/client.v
+heap_lang/proofmode.v
 tests/heap_lang.v
 tests/program_logic.v
 tests/one_shot.v
 tests/joining_existentials.v
+tests/proofmode.v
+proofmode/coq_tactics.v
+proofmode/pviewshifts.v
+proofmode/environments.v
+proofmode/intro_patterns.v
+proofmode/spec_patterns.v
+proofmode/tactics.v
+proofmode/notation.v
+proofmode/invariants.v
+proofmode/weakestpre.v
+proofmode/ghost_ownership.v
+proofmode/sts.v
diff --git a/algebra/upred.v b/algebra/upred.v
index 733893578dc19340532c6109618586d51da612bc..9beba4c28df29f1704661cfb3ae8ef7453370245 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -974,19 +974,6 @@ Lemma later_wand P Q : ▷ (P -★ Q) ⊢ (▷ P -★ ▷ Q).
 Proof. apply wand_intro_r;rewrite -later_sep; apply later_mono,wand_elim_l. Qed.
 Lemma later_iff P Q : ▷ (P ↔ Q) ⊢ (▷ P ↔ ▷ Q).
 Proof. by rewrite /uPred_iff later_and !later_impl. Qed.
-Lemma löb_strong P Q : (P ∧ ▷ Q) ⊢ Q → P ⊢ Q.
-Proof.
-  intros Hlöb. apply impl_entails. rewrite -(löb (P → Q)).
-  apply entails_impl, impl_intro_l. rewrite -{2}Hlöb.
-  apply and_intro; first by eauto.
-  by rewrite {1}(later_intro P) later_impl impl_elim_r.
-Qed.
-Lemma löb_strong_sep P Q : (P ★ ▷ (P -★ Q)) ⊢ Q → P ⊢ Q.
-Proof.
-  move/wand_intro_l=>Hlöb. apply impl_entails.
-  rewrite -[(_ → _)%I]always_elim. apply löb_strong.
-  by rewrite left_id -always_wand_impl -always_later Hlöb.
-Qed.
 
 (* Own *)
 Lemma ownM_op (a1 a2 : M) :
diff --git a/algebra/upred_tactics.v b/algebra/upred_tactics.v
index 76cf90b2871fdcc1f2a621ee883b0e9c73289496..3d8757115c3bf6ba14147d2dc9241b707bea5e97 100644
--- a/algebra/upred_tactics.v
+++ b/algebra/upred_tactics.v
@@ -248,50 +248,3 @@ Ltac strip_later :=
   intros_revert ltac:(
     etrans; [apply: strip_later_r|];
     etrans; [|apply: strip_later_l]; apply later_mono).
-
-(** Transforms a goal of the form ∀ ..., ?0... → ?1 ⊢ ?2
-    into True ⊢ ∀..., ■?0... → ?1 → ?2, applies tac, and
-    the moves all the assumptions back. *)
-(* TODO: this name may be a big too general *)
-Ltac revert_all :=
-  lazymatch goal with
-  | |- ∀ _, _ =>
-    let H := fresh in intro H; revert_all;
-    (* TODO: Really, we should distinguish based on whether this is a
-    dependent function type or not. Right now, we distinguish based
-    on the sort of the argument, which is suboptimal. *)
-    first [ apply (const_intro_impl _ _ _ H); clear H
-          | revert H; apply forall_elim']
-  | |- _ ⊢ _ => apply impl_entails
-  end.
-
-(** This starts on a goal of the form ∀ ..., ?0... → ?1 ⊢ ?2.
-   It applies löb where all the Coq assumptions have been turned into logical
-   assumptions, then moves all the Coq assumptions back out to the context,
-   applies [tac] on the goal (now of the form _ ⊢ _), and then reverts the
-   Coq assumption so that we end up with the same shape as where we started,
-   but with an additional assumption ★-ed to the context *)
-Ltac löb tac :=
-  revert_all;
-  (* Add a box *)
-  etrans; last (eapply always_elim; reflexivity);
-  (* We now have a goal for the form True ⊢ P, with the "original" conclusion
-     being locked. *)
-  apply löb_strong; etransitivity;
-    first (apply equiv_entails, left_id, _; reflexivity);
-  apply: always_intro;
-  (* Now introduce again all the things that we reverted, and at the bottom,
-     do the work *)
-  let rec go :=
-    lazymatch goal with
-    | |- _ ⊢ (∀ _, _) =>
-      apply forall_intro; let H := fresh in intro H; go; revert H
-    | |- _ ⊢ (■ _ → _) =>
-      apply impl_intro_l, const_elim_l; let H := fresh in intro H; go; revert H
-    (* This is the "bottom" of the goal, where we see the impl introduced
-       by uPred_revert_all as well as the ▷ from löb_strong and the □ we added. *)
-    | |- ▷ □ ?R ⊢ (?L → _) => apply impl_intro_l;
-      trans (L ★ ▷ □ R)%I;
-        [eapply equiv_entails, always_and_sep_r, _; reflexivity | tac]
-    end
-  in go.
diff --git a/heap_lang/lib/barrier/client.v b/heap_lang/lib/barrier/client.v
index cf2bd60a38b8c7b067bf6a1f40f4c6cccc0c96ca..d8d302b35cbac9690c8105dd4f7e63fbdd8080d7 100644
--- a/heap_lang/lib/barrier/client.v
+++ b/heap_lang/lib/barrier/client.v
@@ -1,6 +1,7 @@
 From iris.heap_lang.lib.barrier Require Import proof.
 From iris.heap_lang Require Import par.
 From iris.program_logic Require Import auth sts saved_prop hoare ownership.
+From iris.heap_lang Require Import proofmode.
 Import uPred.
 
 Definition worker (n : Z) : val :=
@@ -15,63 +16,44 @@ Section client.
   Context {Σ : gFunctors} `{!heapG Σ, !barrierG Σ, !spawnG Σ} (heapN N : namespace).
   Local Notation iProp := (iPropG heap_lang Σ).
 
-  Definition y_inv q y : iProp :=
-    (∃ f : val, y ↦{q} f ★ □ ∀ n : Z, WP f #n {{ λ v, v = #(n + 42) }})%I.
+  Definition y_inv (q : Qp) (l : loc) : iProp :=
+    (∃ f : val, l ↦{q} f ★ □ ∀ n : Z, WP f #n {{ λ v, v = #(n + 42) }})%I.
 
-  Lemma y_inv_split q y :
-    y_inv q y ⊢ (y_inv (q/2) y ★ y_inv (q/2) y).
+  Lemma y_inv_split q l : y_inv q l ⊢ (y_inv (q/2) l ★ y_inv (q/2) l).
   Proof.
-    rewrite /y_inv. apply exist_elim=>f.
-    rewrite -!(exist_intro f). rewrite heap_mapsto_op_split.
-    ecancel [y ↦{_} _; y ↦{_} _]%I. by rewrite [X in X ⊢ _]always_sep_dup.
+    iIntros "Hl"; iDestruct "Hl" as {f} "[[Hl1 Hl2] #Hf]".
+    iSplitL "Hl1"; iExists f; by iSplitL; try iAlways.
   Qed.
 
   Lemma worker_safe q (n : Z) (b y : loc) :
     (heap_ctx heapN ★ recv heapN N b (y_inv q y))
-      ⊢ WP worker n (%b) (%y) {{ λ _, True }}.
+    ⊢ WP worker n (%b) (%y) {{ λ _, True }}.
   Proof.
-    rewrite /worker. wp_lam. wp_let. ewp apply wait_spec.
-    rewrite comm. apply sep_mono_r. apply wand_intro_l.
-    rewrite sep_exist_r. apply exist_elim=>f. wp_seq.
-    (* TODO these parenthesis are rather surprising. *)
-    (ewp apply: (wp_load heapN _ _ q f)); eauto with I.
-    strip_later. (* hu, shouldn't it do that? *)
-    rewrite -assoc. apply sep_mono_r. apply wand_intro_l.
-    rewrite always_elim (forall_elim n) sep_elim_r sep_elim_l.
-    apply wp_mono=>?. eauto with I.
+    iIntros "[#Hh Hrecv]". wp_lam. wp_let.
+    wp_apply wait_spec; iFrame "Hrecv".
+    iIntros "Hy"; iDestruct "Hy" as {f} "[Hy #Hf]".
+    wp_seq. wp_load.
+    iApply wp_wand_r; iSplitR; [iApply "Hf"|by iIntros {v} "_"].
   Qed.
 
-  Lemma client_safe :
-    heapN ⊥ N → heap_ctx heapN ⊢ WP client {{ λ _, True }}.
+  Lemma client_safe : heapN ⊥ N → heap_ctx heapN ⊢ WP client {{ λ _, True }}.
   Proof.
-    intros ?. rewrite /client.
-    (ewp eapply wp_alloc); eauto with I. strip_later. apply forall_intro=>y.
-    apply wand_intro_l. wp_let.
-    ewp eapply (newbarrier_spec heapN N (y_inv 1 y)); last done.
-    rewrite comm. rewrite {1}[heap_ctx _]always_sep_dup -!assoc.
-    apply sep_mono_r. apply forall_intro=>b. apply wand_intro_l. 
-    wp_let. (ewp eapply (wp_par heapN N (λ _, True%I) (λ _, True%I))); eauto.
-    rewrite 2!{1}[heap_ctx _]always_sep_dup !assoc [(_ ★ heap_ctx _)%I]comm.
-    ecancel [heap_ctx _]. sep_split right: []; last first.
-    { do 2 apply forall_intro=>_. apply wand_intro_l.
-      eauto using later_intro with I. }
-    sep_split left: [send heapN _ _ _; heap_ctx _; y ↦ _]%I.
+    iIntros {?} "#Hh"; rewrite /client. wp_alloc y as "Hy". wp_let.
+    wp_apply (newbarrier_spec heapN N (y_inv 1 y)); first done.
+    iFrame "Hh". iIntros {l} "[Hr Hs]". wp_let.
+    iApply (wp_par heapN N (λ _, True%I) (λ _, True%I)); first done.
+    iFrame "Hh". iSplitL "Hy Hs".
     - (* The original thread, the sender. *)
-      (ewp eapply wp_store); eauto with I. strip_later.
-      ecancel [y ↦ _]%I. apply wand_intro_l.
-      wp_seq. rewrite -signal_spec right_id assoc sep_elim_l comm.
-      apply sep_mono_r. rewrite /y_inv -(exist_intro (λ: "z", '"z" + #42)%V).
-      apply sep_intro_True_r; first done. apply: always_intro.
-      apply forall_intro=>n. wp_let. wp_op. by apply const_intro.
+      wp_store. wp_seq. iApply signal_spec; iFrame "Hs"; iSplit; [|done].
+      iExists _; iSplitL; [done|]. iAlways; iIntros {n}. wp_let. by wp_op.
     - (* The two spawned threads, the waiters. *)
-      rewrite recv_mono; last exact: y_inv_split.
-      rewrite (recv_split _ _ ⊤) // pvs_frame_r. apply wp_strip_pvs.
-      (ewp eapply (wp_par heapN N (λ _, True%I) (λ _, True%I))); eauto.
-      do 2 rewrite {1}[heap_ctx _]always_sep_dup.
-      ecancel [heap_ctx _]. rewrite !assoc. sep_split right: []; last first.
-      { do 2 apply forall_intro=>_. apply wand_intro_l.
-        eauto using later_intro with I. }
-      sep_split left: [recv heapN _ _ _; heap_ctx _]%I; by rewrite -worker_safe comm.
+      iSplitL; [|iIntros {_ _} "_"; by iNext].
+      iDestruct recv_weaken "[] Hr" as "Hr".
+      { iIntros "?". by iApply y_inv_split "-". }
+      iPvs recv_split "Hr" as "[H1 H2]"; first done.
+      iApply (wp_par heapN N (λ _, True%I) (λ _, True%I)); eauto.
+      iFrame "Hh"; iSplitL "H1"; [|iSplitL "H2"; [|iIntros {_ _} "_"; by iNext]];
+        iApply worker_safe; by iSplit.
 Qed.
 End client.
 
@@ -81,11 +63,9 @@ Section ClosedProofs.
 
   Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
   Proof.
-    apply ht_alt. rewrite (heap_alloc (nroot .@ "Barrier")); last done.
-    apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
-    rewrite -(client_safe (nroot .@ "Barrier") (nroot .@ "Heap")) //.
-    (* This, too, should be automated. *)
-    by apply ndot_ne_disjoint.
+    iIntros "! Hσ".
+    iPvs (heap_alloc (nroot .@ "Barrier")) "Hσ" as {h} "[#Hh _]"; first done.
+    iApply (client_safe (nroot .@ "Barrier") (nroot .@ "Heap")); auto with ndisj.
   Qed.
 
   Print Assumptions client_safe_closed.
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 89f3f4bbb787109afd186e05b74f3b72f85f16cc..b7166cb3c9c3c3feafdbcd1d94f693413d99f548 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -1,7 +1,8 @@
 From iris.prelude Require Import functions.
 From iris.algebra Require Import upred_big_op.
-From iris.program_logic Require Import sts saved_prop tactics.
-From iris.heap_lang Require Export heap wp_tactics.
+From iris.program_logic Require Import saved_prop.
+From iris.heap_lang Require Import proofmode.
+From iris.proofmode Require Import sts.
 From iris.heap_lang.lib.barrier Require Export barrier.
 From iris.heap_lang.lib.barrier Require Import protocol.
 Import uPred.
@@ -22,6 +23,7 @@ Proof. destruct H as (?&?&?). split; apply _. Qed.
 Section proof.
 Context {Σ : gFunctors} `{!heapG Σ, !barrierG Σ}.
 Context (heapN N : namespace).
+Implicit Types I : gset gname.
 Local Notation iProp := (iPropG heap_lang Σ).
 
 Definition ress (P : iProp) (I : gset gname) : iProp :=
@@ -30,11 +32,11 @@ Definition ress (P : iProp) (I : gset gname) : iProp :=
 
 Coercion state_to_val (s : state) : val :=
   match s with State Low _ => #0 | State High _ => #1 end.
-Arguments state_to_val !_ /.
+Arguments state_to_val !_ / : simpl nomatch.
 
 Definition state_to_prop (s : state) (P : iProp) : iProp :=
   match s with State Low _ => P | State High _ => True%I end.
-Arguments state_to_val !_ /.
+Arguments state_to_prop !_ _ / : simpl nomatch.
 
 Definition barrier_inv (l : loc) (P : iProp) (s : state) : iProp :=
   (l ↦ s ★ ress (state_to_prop s P) (state_I s))%I.
@@ -54,12 +56,8 @@ Global Instance barrier_ctx_persistent (γ : gname) (l : loc) (P : iProp) :
   PersistentP (barrier_ctx γ l P).
 Proof. apply _. Qed.
 
-(* TODO: Figure out if this has a "Global" or "Local" effect.
-   We want it to be Global. *)
 Typeclasses Opaque barrier_ctx send recv.
 
-Implicit Types I : gset gname.
-
 (** Setoids *)
 Global Instance ress_ne n : Proper (dist n ==> (=) ==> dist n) ress.
 Proof. solve_proper. Qed.
@@ -79,33 +77,19 @@ Proof. solve_proper. Qed.
 (** Helper lemmas *)
 Lemma ress_split i i1 i2 Q R1 R2 P I :
   i ∈ I → i1 ∉ I → i2 ∉ I → i1 ≠ i2 →
-  (saved_prop_own i2 R2 ★
-    saved_prop_own i1 R1 ★ saved_prop_own i Q ★
+  (saved_prop_own i Q ★ saved_prop_own i1 R1 ★ saved_prop_own i2 R2 ★
     (Q -★ R1 ★ R2) ★ ress P I)
   ⊢ ress P ({[i1]} ∪ ({[i2]} ∪ (I ∖ {[i]}))).
 Proof.
-  intros. rewrite /ress !sep_exist_l. apply exist_elim=>Ψ.
-  rewrite -(exist_intro (<[i1:=R1]> (<[i2:=R2]> Ψ))).
-  rewrite [(Π★{set _} (λ _, saved_prop_own _ _))%I](big_sepS_delete _ I i) //.
-  do 4 (rewrite big_sepS_insert; last set_solver).
-  rewrite !fn_lookup_insert fn_lookup_insert_ne // !fn_lookup_insert.
-  set savedQ := _ i Q. set savedΨ := _ i (Ψ _).
-  sep_split left: [savedQ; savedΨ; Q -★ _; ▷ (_ -★ Π★{set I} _)]%I.
-  - rewrite !assoc saved_prop_agree /=. strip_later.
-    apply wand_intro_l. to_front [P; P -★ _]%I. rewrite wand_elim_r.
-    rewrite (big_sepS_delete _ I i) //.
-    sep_split right: [Π★{set _} _]%I.
-    + rewrite !assoc.
-      eapply wand_apply_r'; first done.
-      apply: (eq_rewrite (Ψ i) Q (λ x, x)%I); last by eauto with I.
-      rewrite eq_sym. eauto with I.
-    + apply big_sepS_mono; [done|] => j.
-      rewrite elem_of_difference not_elem_of_singleton=> -[??].
-      by do 2 (rewrite fn_lookup_insert_ne; last naive_solver).
-  - rewrite !assoc [(saved_prop_own i2 _ ★ _)%I]comm; apply sep_mono_r.
-    apply big_sepS_mono; [done|]=> j.
-    rewrite elem_of_difference not_elem_of_singleton=> -[??].
-    by do 2 (rewrite fn_lookup_insert_ne; last naive_solver).
+  iIntros {????} "(#HQ&#H1&#H2&HQR&H)"; iDestruct "H" as {Ψ} "[HPΨ HΨ]".
+  iDestruct (big_sepS_delete _ _ i) "HΨ" as "[#HΨi HΨ]"; first done.
+  iExists (<[i1:=R1]> (<[i2:=R2]> Ψ)). iSplitL "HQR HPΨ".
+  - iPoseProof (saved_prop_agree i Q (Ψ i)) "#" as "Heq"; first by iSplit.
+    iNext. iRewrite "Heq" in "HQR". iIntros "HP". iSpecialize "HPΨ" "HP". 
+    iDestruct (big_sepS_delete _ _ i) "HPΨ" as "[HΨ HPΨ]"; first done.
+    iDestruct "HQR" "HΨ" as "[HR1 HR2]".
+    rewrite !big_sepS_insert''; [|set_solver ..]. by iFrame "HR1 HR2".
+  - rewrite !big_sepS_insert'; [|set_solver ..]. by repeat iSplit.
 Qed.
 
 (** Actual proofs *)
@@ -114,176 +98,110 @@ Lemma newbarrier_spec (P : iProp) (Φ : val → iProp) :
   (heap_ctx heapN ★ ∀ l, recv l P ★ send l P -★ Φ (%l))
   ⊢ WP newbarrier #() {{ Φ }}.
 Proof.
-  intros HN. rewrite /newbarrier. wp_seq.
-  rewrite -wp_pvs. wp eapply wp_alloc; eauto with I ndisj.
-  apply forall_intro=>l. rewrite (forall_elim l). apply wand_intro_l.
-  rewrite !assoc. rewrite- pvs_wand_r; apply sep_mono_l.
-  (* The core of this proof: Allocating the STS and the saved prop. *)
-  eapply sep_elim_True_r; first by eapply (saved_prop_alloc (F:=idCF) _ P).
-  rewrite pvs_frame_l. apply pvs_strip_pvs. rewrite sep_exist_l.
-  apply exist_elim=>i.
-  trans (pvs ⊤ ⊤ (heap_ctx heapN ★
-    ▷ (barrier_inv l P (State Low {[ i ]})) ★ saved_prop_own i P)).
-  - rewrite -pvs_intro. cancel [heap_ctx heapN].
-    rewrite {1}[saved_prop_own _ _]always_sep_dup. cancel [saved_prop_own i P].
-    rewrite /barrier_inv /ress -later_intro. cancel [l ↦ #0]%I.
-    rewrite -(exist_intro (const P)) /=. rewrite -[saved_prop_own _ _](left_id True%I (★)%I).
-    by rewrite !big_sepS_singleton /= wand_diag -later_intro.
-  - rewrite (sts_alloc (barrier_inv l P) ⊤ N); last by eauto.
-    rewrite !pvs_frame_r !pvs_frame_l. 
-    rewrite pvs_trans'. apply pvs_strip_pvs. rewrite sep_exist_r sep_exist_l.
-    apply exist_elim=>γ.
-    rewrite /recv /send. rewrite -(exist_intro γ) -(exist_intro P).
-    rewrite -(exist_intro P) -(exist_intro i) -(exist_intro γ).
-    rewrite always_and_sep_l wand_diag later_True right_id.
-    rewrite [heap_ctx _]always_sep_dup [sts_ctx _ _ _]always_sep_dup.
-    rewrite /barrier_ctx const_equiv // left_id.
-    ecancel_pvs [saved_prop_own i _; heap_ctx _; heap_ctx _;
-                 sts_ctx _ _ _; sts_ctx _ _ _].
-    rewrite (sts_own_weaken ⊤ _ _ (i_states i ∩ low_states) _ 
-                            ({[ Change i ]} ∪ {[ Send ]})).
-    + apply pvs_mono.
-      rewrite -sts_ownS_op; eauto using i_states_closed, low_states_closed.
-      set_solver.
-    + intros []; set_solver.
+  iIntros {HN} "[#? HΦ]".
+  rewrite /newbarrier. wp_seq. iApply wp_pvs. wp_alloc l as "Hl".
+  iApply "HΦ".
+  iPvs (saved_prop_alloc (F:=idCF) _ P) as {γ} "#?".
+  iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}))
+    "-" as {γ'} "[#? Hγ']"; eauto.
+  { iNext. iFrame "Hl". iExists (const P). rewrite !big_sepS_singleton /=.
+    iSplit; [|done]. by iNext; iIntros "?". }
+  iAssert (barrier_ctx γ' l P)%I as "#?".
+  { rewrite /barrier_ctx. by repeat iSplit. }
+  iPvsAssert (sts_ownS γ' (i_states γ) {[Change γ]}
+    ★ sts_ownS γ' low_states {[Send]})%I as "[Hr Hs]" with "-".
+  { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
     + set_solver.
-    + auto using sts.closed_op, i_states_closed, low_states_closed.
+    + iApply sts_own_weaken "Hγ'";
+        auto using sts.closed_op, i_states_closed, low_states_closed;
+        set_solver. }
+  iPvsIntro. rewrite /recv /send. iSplitL "Hr".
+  - iExists γ', P, P, γ. iFrame "Hr". repeat iSplit; auto. iNext; by iIntros "?".
+  - iExists γ'. by iSplit.
 Qed.
 
 Lemma signal_spec l P (Φ : val → iProp) :
   (send l P ★ P ★ Φ #()) ⊢ WP signal (%l) {{ Φ }}.
 Proof.
-  rewrite /signal /send /barrier_ctx. rewrite sep_exist_r.
-  apply exist_elim=>γ. rewrite -!assoc. apply const_elim_sep_l=>?. wp_let.
-  (* I think some evars here are better than repeating *everything* *)
-  eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ); simpl;
-    eauto with I ndisj.
-  ecancel [sts_ownS γ _ _]. 
-  apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc.
-  apply const_elim_sep_l=>Hs. destruct p; last done.
-  rewrite {1}/barrier_inv =>/={Hs}. rewrite later_sep.
-  eapply wp_store with (v' := #0); eauto with I ndisj. 
-  strip_later. cancel [l ↦ #0]%I.
-  apply wand_intro_l. rewrite -(exist_intro (State High I)).
-  rewrite -(exist_intro ∅). rewrite const_equiv /=; last by eauto using signal_step.
-  rewrite left_id -later_intro {2}/barrier_inv -!assoc. apply sep_mono_r.
-  sep_split right: [Φ _]; last first.
-  { apply wand_intro_l. eauto with I. }
-  (* Now we come to the core of the proof: Updating from waiting to ress. *)
-  rewrite /ress sep_exist_r. apply exist_mono=>{Φ} Φ.
-  ecancel [Π★{set I} (λ _, saved_prop_own _ _)]%I. strip_later.
-  rewrite wand_True. eapply wand_apply_l'; eauto with I.
+  rewrite /signal /send /barrier_ctx.
+  iIntros "(Hs&HP&HΦ)"; iDestruct "Hs" as {γ} "[#(%&Hh&Hsts) Hγ]". wp_let.
+  iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
+  wp_store. destruct p; [|done].
+  iExists (State High I), (∅ : set token).
+  iSplit; [iPureIntro; by eauto using signal_step|].
+  iSplitR "HΦ"; [iNext|by iIntros "?"].
+  rewrite {2}/barrier_inv /ress /=; iFrame "Hl".
+  iDestruct "Hr" as {Ψ} "[? Hsp]"; iExists Ψ; iFrame "Hsp".
+  iNext; iIntros "_"; by iApply "Hr".
 Qed.
 
 Lemma wait_spec l P (Φ : val → iProp) :
   (recv l P ★ (P -★ Φ #())) ⊢ WP wait (%l) {{ Φ }}.
 Proof.
-  rename P into R. wp_rec.
-  rewrite {1}/recv /barrier_ctx. rewrite !sep_exist_r.
-  apply exist_elim=>γ. rewrite !sep_exist_r. apply exist_elim=>P.
-  rewrite !sep_exist_r. apply exist_elim=>Q. rewrite !sep_exist_r.
-  apply exist_elim=>i. rewrite -!(assoc (★)%I). apply const_elim_sep_l=>?.
-  wp_focus (! _)%E.
-  (* I think some evars here are better than repeating *everything* *)
-  eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ); simpl;
-    eauto with I ndisj.
-  ecancel [sts_ownS γ _ _].
-  apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc.
-  apply const_elim_sep_l=>Hs.
-  rewrite {1}/barrier_inv =>/=. rewrite later_sep.
-  eapply wp_load; eauto with I ndisj.
-  ecancel [▷ l ↦{_} _]%I. strip_later.
-  apply wand_intro_l. destruct p.
-  { (* a Low state. The comparison fails, and we recurse. *)
-    rewrite -(exist_intro (State Low I)) -(exist_intro {[ Change i ]}).
-    rewrite [(â–  sts.steps _ _ )%I]const_equiv /=; last by apply rtc_refl.
-    rewrite left_id -[(â–· barrier_inv _ _ _)%I]later_intro {3}/barrier_inv.
-    rewrite -!assoc. apply sep_mono_r, sep_mono_r, wand_intro_l.
-    wp_op; first done. intros _. wp_if. rewrite !assoc.
-    rewrite -always_wand_impl always_elim.
-    rewrite -{2}pvs_wp. rewrite -pvs_wand_r; apply sep_mono_l.
-    rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro Q) -(exist_intro i).
-    rewrite const_equiv // left_id -later_intro.
-    ecancel_pvs [heap_ctx _; saved_prop_own _ _; Q -★ _; R -★ _; sts_ctx _ _ _]%I.
-    apply sts_own_weaken; eauto using i_states_closed. }
-  (* a High state: the comparison succeeds, and we perform a transition and
-     return to the client *)
-  rewrite [(_ ★ □ (_ → _ ))%I]sep_elim_l.
-  rewrite -(exist_intro (State High (I ∖ {[ i ]}))) -(exist_intro ∅).
-  change (i ∈ I) in Hs.
-  rewrite const_equiv /=; last by eauto using wait_step.
-  rewrite left_id -[(â–· barrier_inv _ _ _)%I]later_intro {2}/barrier_inv.
-  rewrite -!assoc. apply sep_mono_r. rewrite /ress.
-  rewrite !sep_exist_r. apply exist_mono=>Ψ.
-  rewrite !(big_sepS_delete _ I i) //= !wand_True later_sep.
-  ecancel [▷ Π★{set _} Ψ; Π★{set _} (λ _, saved_prop_own _ _)]%I.
-  apply wand_intro_l.  set savedΨ := _ i (Ψ _). set savedQ := _ i Q.
-  to_front [savedΨ; savedQ]. rewrite saved_prop_agree /=.
-  wp_op; [|done]=> _. wp_if. rewrite -pvs_intro. rewrite !assoc. eapply wand_apply_r'; first done.
-  eapply wand_apply_r'; first done.
-  apply: (eq_rewrite (Ψ i) Q (λ x, x)%I); by eauto with I.
+  rename P into R; rewrite /recv /barrier_ctx.
+  iIntros "[Hr HΦ]"; iDestruct "Hr" as {γ P Q i} "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
+  iLöb "Hγ HQR HΦ" as "IH". wp_rec. wp_focus (! _)%E.
+  iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
+  wp_load. destruct p.
+  - (* a Low state. The comparison fails, and we recurse. *)
+    iExists (State Low I), {[ Change i ]}; iSplit; [done|iSplitL "Hl Hr"].
+    { iNext. rewrite {2}/barrier_inv /=. by iFrame "Hl". }
+    iIntros "Hγ".
+    iPvsAssert (sts_ownS γ (i_states i) {[Change i]})%I as "Hγ" with "[Hγ]".
+    { iApply sts_own_weaken "Hγ"; eauto using i_states_closed. }
+    wp_op=> ?; simplify_eq; wp_if. iApply "IH" "Hγ [HQR] HΦ". by iNext.
+  - (* a High state: the comparison succeeds, and we perform a transition and
+    return to the client *)
+    iExists (State High (I ∖ {[ i ]})), (∅ : set token).
+    iSplit; [iPureIntro; by eauto using wait_step|].
+    iDestruct "Hr" as {Ψ} "[HΨ Hsp]".
+    iDestruct (big_sepS_delete _ _ i) "Hsp" as "[#HΨi Hsp]"; first done.
+    iAssert (▷ Ψ i ★ ▷ Π★{set (I ∖ {[i]})} Ψ)%I as "[HΨ HΨ']" with "[HΨ]".
+    { iNext. iApply (big_sepS_delete _ _ i); first done. by iApply "HΨ". }
+    iSplitL "HΨ' Hl Hsp"; [iNext|].
+    + rewrite {2}/barrier_inv /=; iFrame "Hl".
+      iExists Ψ; iFrame "Hsp". iNext; by iIntros "_".
+    + iPoseProof (saved_prop_agree i Q (Ψ i)) "#" as "Heq"; first by iSplit.
+      iIntros "_". wp_op=> ?; simplify_eq/=; wp_if.
+      iPvsIntro. iApply "HΦ". iApply "HQR". by iRewrite "Heq".
 Qed.
 
 Lemma recv_split E l P1 P2 :
-  nclose N ⊆ E → 
-  recv l (P1 ★ P2) ⊢ |={E}=> recv l P1 ★ recv l P2.
+  nclose N ⊆ E → recv l (P1 ★ P2) ⊢ |={E}=> recv l P1 ★ recv l P2.
 Proof.
-  rename P1 into R1. rename P2 into R2. intros HN.
-  rewrite {1}/recv /barrier_ctx. 
-  apply exist_elim=>γ. rewrite sep_exist_r.  apply exist_elim=>P. 
-  apply exist_elim=>Q. apply exist_elim=>i. rewrite -!(assoc (★)%I).
-  apply const_elim_sep_l=>?. rewrite -pvs_trans'.
-  (* I think some evars here are better than repeating *everything* *)
-  eapply pvs_mk_fsa, (sts_fsaS _ pvs_fsa) with (N0:=N) (γ0:=γ); simpl;
-    eauto with I ndisj.
-  ecancel [sts_ownS γ _ _].
-  apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc.
-  apply const_elim_sep_l=>Hs. rewrite /pvs_fsa.
-  eapply sep_elim_True_l.
-  { eapply saved_prop_alloc_strong with (x := R1) (G := I). }
-  rewrite pvs_frame_r. apply pvs_strip_pvs. rewrite sep_exist_r.
-  apply exist_elim=>i1. rewrite always_and_sep_l. rewrite -assoc.
-  apply const_elim_sep_l=>Hi1. eapply sep_elim_True_l.
-  { eapply saved_prop_alloc_strong with (x := R2) (G := I ∪ {[ i1 ]}). }
-  rewrite pvs_frame_r. apply pvs_mono. rewrite sep_exist_r.
-  apply exist_elim=>i2. rewrite always_and_sep_l. rewrite -assoc.
-  apply const_elim_sep_l=>Hi2.
-  rewrite ->not_elem_of_union, elem_of_singleton in Hi2.
-  destruct Hi2 as [Hi2 Hi12]. change (i ∈ I) in Hs.
-  (* Update to new state. *)
-  rewrite -(exist_intro (State p ({[i1]} ∪ ({[i2]} ∪ (I ∖ {[i]}))))).
-  rewrite -(exist_intro ({[Change i1 ]} ∪ {[ Change i2 ]})).
-  rewrite [(â–  sts.steps _ _)%I]const_equiv; last by eauto using split_step.
-  rewrite left_id {1 3}/barrier_inv.
-  (* FIXME ssreflect rewrite fails if there are evars around. Also, this is very slow because we don't have a proof mode. *)
-  rewrite -(ress_split _ _ _ Q R1 R2); [|done..].
-  rewrite {1}[saved_prop_own i1 _]always_sep_dup.
-  rewrite {1}[saved_prop_own i2 _]always_sep_dup !later_sep.
-  rewrite -![(â–· saved_prop_own _ _)%I]later_intro.
-  ecancel [▷ l ↦ _; saved_prop_own i1 _; saved_prop_own i2 _ ;
-           ▷ ress _ _ ; ▷ (Q -★ _) ; saved_prop_own i _]%I. 
-  apply wand_intro_l. rewrite !assoc. rewrite /recv.
-  rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro R1) -(exist_intro i1).
-  rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro R2) -(exist_intro i2).
-  rewrite [heap_ctx _]always_sep_dup [sts_ctx _ _ _]always_sep_dup.
-  rewrite /barrier_ctx const_equiv // left_id.
-  ecancel_pvs [saved_prop_own i1 _; saved_prop_own i2 _; heap_ctx _; heap_ctx _;
-               sts_ctx _ _ _; sts_ctx _ _ _].
-  rewrite !wand_diag later_True !right_id.
-  rewrite -sts_ownS_op; eauto using i_states_closed.
-  - apply sts_own_weaken;
-      eauto using sts.closed_op, i_states_closed. set_solver.
-  - set_solver.
+  rename P1 into R1; rename P2 into R2. rewrite {1}/recv /barrier_ctx.
+  iIntros {?} "Hr"; iDestruct "Hr" as {γ P Q i} "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
+  iApply pvs_trans'.
+  iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
+  iPvs (saved_prop_alloc_strong _ (R1: ∙%CF iProp) I) as {i1} "[% #Hi1]".
+  iPvs (saved_prop_alloc_strong _ (R2: ∙%CF iProp) (I ∪ {[i1]}))
+    as {i2} "[Hi2' #Hi2]"; iPure "Hi2'" as Hi2; iPvsIntro.
+  rewrite ->not_elem_of_union, elem_of_singleton in Hi2; destruct Hi2.
+  iExists (State p ({[i1]} ∪ ({[i2]} ∪ (I ∖ {[i]})))).
+  iExists ({[Change i1 ]} ∪ {[ Change i2 ]}).
+  iSplit; [by eauto using split_step|iSplitL].
+  - iNext. rewrite {2}/barrier_inv /=. iFrame "Hl".
+    iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame "Hr HQR". by repeat iSplit.
+  - iIntros "Hγ".
+    iPvsAssert (sts_ownS γ (i_states i1) {[Change i1]}
+      ★ sts_ownS γ (i_states i2) {[Change i2]})%I as "[Hγ1 Hγ2]" with "-".
+    { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
+      + set_solver.
+      + iApply sts_own_weaken "Hγ"; eauto using sts.closed_op, i_states_closed.
+        set_solver. }
+    iPvsIntro; iSplitL "Hγ1"; rewrite /recv /barrier_ctx.
+    + iExists γ, P, R1, i1. iFrame "Hγ1 Hi1". repeat iSplit; auto.
+      by iNext; iIntros "?".
+    + iExists γ, P, R2, i2. iFrame "Hγ2 Hi2". repeat iSplit; auto.
+      by iNext; iIntros "?".
 Qed.
 
-Lemma recv_weaken l P1 P2 :
-  (P1 -★ P2) ⊢ (recv l P1 -★ recv l P2).
+Lemma recv_weaken l P1 P2 : (P1 -★ P2) ⊢ (recv l P1 -★ recv l P2).
 Proof.
-  apply wand_intro_l. rewrite /recv. rewrite sep_exist_r. apply exist_mono=>γ.
-  rewrite sep_exist_r. apply exist_mono=>P. rewrite sep_exist_r.
-  apply exist_mono=>Q. rewrite sep_exist_r. apply exist_mono=>i.
-  ecancel [barrier_ctx _ _ _; sts_ownS _ _ _; saved_prop_own _ _].
-  strip_later. apply wand_intro_l. by rewrite !assoc wand_elim_r wand_elim_r.
+  rewrite /recv.
+  iIntros "HP HP1"; iDestruct "HP1" as {γ P Q i} "(#Hctx&Hγ&Hi&HP1)".
+  iExists γ, P, Q, i; iFrame "Hctx Hγ Hi".
+  iNext; iIntros "HQ". by iApply "HP"; iApply "HP1".
 Qed.
 
 Lemma recv_mono l P1 P2 :
@@ -291,5 +209,6 @@ Lemma recv_mono l P1 P2 :
 Proof.
   intros HP%entails_wand. apply wand_entails. rewrite HP. apply recv_weaken.
 Qed.
-
 End proof.
+
+Typeclasses Opaque barrier_ctx send recv.
diff --git a/heap_lang/lib/barrier/specification.v b/heap_lang/lib/barrier/specification.v
index bfe830080583677713e8d554158ff7ec04550887..cdb18b49523507a842b4ea1534628afb853fd9a3 100644
--- a/heap_lang/lib/barrier/specification.v
+++ b/heap_lang/lib/barrier/specification.v
@@ -1,6 +1,7 @@
 From iris.program_logic Require Export hoare.
 From iris.heap_lang.lib.barrier Require Export barrier.
 From iris.heap_lang.lib.barrier Require Import proof.
+From iris.heap_lang Require Import proofmode.
 Import uPred.
 
 Section spec.
@@ -22,14 +23,11 @@ Proof.
   intros HN.
   exists (λ l, CofeMor (recv heapN N l)), (λ l, CofeMor (send heapN N l)).
   split_and?; simpl.
-  - intros P. apply: always_intro. apply impl_intro_r.
-    rewrite -(newbarrier_spec heapN N P) // always_and_sep_r.
-    apply sep_mono_r, forall_intro=>l; apply wand_intro_l.
-    by rewrite right_id -(exist_intro l) const_equiv // left_id.
-  - intros l P. apply ht_alt. by rewrite -signal_spec right_id.
-  - intros l P. apply ht_alt.
-    by rewrite -(wait_spec heapN N l P) wand_diag right_id.
-  - intros l P Q. apply vs_alt. rewrite -(recv_split heapN N N l P Q) //.
-  - intros l P Q. apply recv_weaken.
+  - iIntros {P} "#? ! _". iApply (newbarrier_spec _ _ P); first done.
+    iSplit; [done|]; iIntros {l} "?"; iExists l; by iSplit.
+  - iIntros {l P} "! [Hl HP]". by iApply signal_spec; iFrame "Hl HP".
+  - iIntros {l P} "! Hl". iApply wait_spec; iFrame "Hl". by iIntros "?".
+  - iIntros {l P Q} "! Hl". by iApply recv_split.
+  - apply recv_weaken.
 Qed.
 End spec.
diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v
index 219cb74e8377c75adf5663d5e2275ca4ba91fa1f..d65343ef02f2c6c18de63073272c73ff0a6f8d10 100644
--- a/heap_lang/lib/par.v
+++ b/heap_lang/lib/par.v
@@ -1,5 +1,5 @@
 From iris.heap_lang Require Export heap spawn.
-From iris.heap_lang Require Import wp_tactics notation.
+From iris.heap_lang Require Import proofmode notation.
 Import uPred.
 
 Definition par : val :=
@@ -25,15 +25,12 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp) e (f1 f2 : val) (Φ : val → iProp) :
    ∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ ▷ Φ (v1,v2)%V)
   ⊢ WP par e {{ Φ }}.
 Proof.
-  intros. rewrite /par. ewp (by eapply wp_value). wp_let. wp_proj.
-  ewp (eapply spawn_spec; wp_done).
-  apply sep_mono_r, sep_mono_r.
-  apply forall_intro=>h. apply wand_intro_l. wp_let. wp_proj.
-  wp_focus (f2 _). rewrite wp_frame_r wp_frame_l. apply wp_mono=>v2. wp_let.
-  ewp (by eapply join_spec).
-  apply sep_mono_r, forall_intro=>v1; apply wand_intro_l.
-  rewrite (forall_elim v1) (forall_elim v2). rewrite assoc wand_elim_r.
-  wp_let. apply wp_value; wp_done.
+  iIntros {??} "(#Hh&Hf1&Hf2&HΦ)". wp_value. wp_let. wp_proj.
+  wp_apply spawn_spec; try wp_done. iFrame "Hf1 Hh".
+  iIntros {l} "Hl". wp_let. wp_proj. wp_focus (f2 _).
+  iApply wp_wand_l; iFrame "Hf2"; iIntros {v} "H2". wp_let.
+  wp_apply join_spec; iFrame "Hl". iIntros {w} "H1".
+  iSpecialize "HΦ" "-"; first by iSplitL "H1". wp_let. by iPvsIntro.
 Qed.
 
 Lemma wp_par (Ψ1 Ψ2 : val → iProp) (e1 e2 : expr []) (Φ : val → iProp) :
@@ -42,6 +39,7 @@ Lemma wp_par (Ψ1 Ψ2 : val → iProp) (e1 e2 : expr []) (Φ : val → iProp) :
    ∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ ▷ Φ (v1,v2)%V)
   ⊢ WP ParV e1 e2 {{ Φ }}.
 Proof.
-  intros. rewrite -par_spec //. repeat apply sep_mono; done || by wp_seq.
+  iIntros {?} "(#Hh&H1&H2&H)". iApply par_spec; auto.
+  iFrame "Hh H". iSplitL "H1"; by wp_let.
 Qed.
 End proof.
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index c20c28bf6b035b45f50199d5c706b91998afde99..ba31510d9f5c49c10be684a0675a6a440fd323fb 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -1,6 +1,7 @@
 From iris.program_logic Require Export global_functor.
 From iris.heap_lang Require Export heap.
-From iris.heap_lang Require Import wp_tactics notation.
+From iris.proofmode Require Import invariants ghost_ownership.
+From iris.heap_lang Require Import proofmode notation.
 Import uPred.
 
 Definition spawn : val :=
@@ -33,12 +34,15 @@ Context (heapN N : namespace).
 Local Notation iProp := (iPropG heap_lang Σ).
 
 Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp) : iProp :=
-  (∃ lv, l ↦ lv ★ (lv = InjLV #0 ∨ ∃ v, lv = InjRV v ★ (Ψ v ∨ own γ (Excl ()))))%I.
+  (∃ lv, l ↦ lv ★ (lv = InjLV #0 ∨
+                   ∃ v, lv = InjRV v ★ (Ψ v ∨ own γ (Excl ()))))%I.
 
 Definition join_handle (l : loc) (Ψ : val → iProp) : iProp :=
   (■ (heapN ⊥ N) ★ ∃ γ, heap_ctx heapN ★ own γ (Excl ()) ★
                         inv N (spawn_inv γ l Ψ))%I.
 
+Typeclasses Opaque join_handle.
+
 Global Instance spawn_inv_ne n γ l :
   Proper (pointwise_relation val (dist n) ==> dist n) (spawn_inv γ l).
 Proof. solve_proper. Qed.
@@ -53,65 +57,36 @@ Lemma spawn_spec (Ψ : val → iProp) e (f : val) (Φ : val → iProp) :
   (heap_ctx heapN ★ WP f #() {{ Ψ }} ★ ∀ l, join_handle l Ψ -★ Φ (%l))
   ⊢ WP spawn e {{ Φ }}.
 Proof.
-  intros Hval Hdisj. rewrite /spawn. ewp (by eapply wp_value). wp_let.
-  wp eapply wp_alloc; eauto with I.
-  apply forall_intro=>l. apply wand_intro_l. wp_let.
-  rewrite (forall_elim l). eapply sep_elim_True_l.
-  { by eapply (own_alloc (Excl ())). }
-  rewrite !pvs_frame_r. eapply wp_strip_pvs. rewrite !sep_exist_r.
-  apply exist_elim=>γ.
-  (* TODO: Figure out a better way to say "I want to establish â–· spawn_inv". *)
-  trans (heap_ctx heapN ★ WP f #() {{ Ψ }} ★ (join_handle l Ψ -★ Φ (%l)%V) ★
-         own γ (Excl ()) ★ ▷ (spawn_inv γ l Ψ))%I.
-  { ecancel [ WP _ {{ _ }}; _ -★ _; heap_ctx _; own _ _]%I.
-    rewrite -later_intro /spawn_inv -(exist_intro (InjLV #0)).
-    cancel [l ↦ InjLV #0]%I. by apply or_intro_l', const_intro. }
-  rewrite (inv_alloc N) // !pvs_frame_l. eapply wp_strip_pvs.
-  ewp eapply wp_fork. rewrite [heap_ctx _]always_sep_dup [inv _ _]always_sep_dup.
-  sep_split left: [_ -★ _; inv _ _; own _ _; heap_ctx _]%I.
-  - wp_seq. rewrite -pvs_intro. eapply wand_apply_l; [done..|].
-    rewrite /join_handle. rewrite const_equiv // left_id -(exist_intro γ).
-    solve_sep_entails.
-  - wp_focus (f _). rewrite wp_frame_r wp_frame_l.
-    rewrite (of_to_val e) //. apply wp_mono=>v.
-    eapply (inv_fsa (wp_fsa _)) with (N0:=N);
-      rewrite /= ?to_of_val; eauto with I ndisj.
-    apply wand_intro_l. rewrite /spawn_inv {1}later_exist !sep_exist_r.
-    apply exist_elim=>lv. rewrite later_sep.
-    eapply wp_store; rewrite /= ?to_of_val; eauto with I ndisj.
-    cancel [▷ (l ↦ lv)]%I. strip_later. apply wand_intro_l.
-    rewrite right_id -later_intro -{2}[(∃ _, _ ↦ _ ★ _)%I](exist_intro (InjRV v)).
-    ecancel [l ↦ _]%I. apply or_intro_r'. rewrite sep_elim_r sep_elim_r sep_elim_l.
-    rewrite -(exist_intro v). rewrite const_equiv // left_id. apply or_intro_l.
+  iIntros {<-%of_to_val ?} "(#Hh&Hf&HΦ)". rewrite /spawn.
+  wp_let; wp_alloc l as "Hl"; wp_let.
+  iPvs (own_alloc (Excl ())) as {γ} "Hγ"; first done.
+  iPvs (inv_alloc N _ (spawn_inv γ l Ψ)) "[Hl]" as "#?"; first done.
+  { iNext. iExists (InjLV #0). iFrame "Hl". by iLeft. }
+  wp_apply wp_fork. iSplitR "Hf".
+  - wp_seq. iPvsIntro. iApply "HΦ"; rewrite /join_handle. iSplit; first done.
+    iExists γ. iFrame "Hγ"; by iSplit.
+  - wp_focus (f _). iApply wp_wand_l; iFrame "Hf"; iIntros {v} "Hv".
+    iInv N as "Hinv"; first wp_done; iDestruct "Hinv" as {v'} "[Hl _]".
+    wp_store. iSplit; [iNext|done].
+    iExists (InjRV v); iFrame "Hl"; iRight; iExists v; iSplit; [done|by iLeft].
 Qed.
 
 Lemma join_spec (Ψ : val → iProp) l (Φ : val → iProp) :
-  (join_handle l Ψ ★ ∀ v, Ψ v -★ Φ v)
-  ⊢ WP join (%l) {{ Φ }}.
+  (join_handle l Ψ ★ ∀ v, Ψ v -★ Φ v) ⊢ WP join (%l) {{ Φ }}.
 Proof.
-  wp_rec. wp_focus (! _)%E.
-  rewrite {1}/join_handle sep_exist_l !sep_exist_r. apply exist_elim=>γ.
-  rewrite -!assoc. apply const_elim_sep_l=>Hdisj.
-  eapply (inv_fsa (wp_fsa _)) with (N0:=N); simpl; eauto with I ndisj.
-  apply wand_intro_l. rewrite /spawn_inv {1}later_exist !sep_exist_r.
-  apply exist_elim=>lv.
-  wp eapply wp_load; eauto with I ndisj. cancel [l ↦ lv]%I.
-  apply wand_intro_l. rewrite -later_intro -[X in _ ⊢ (X ★ _)](exist_intro lv).
-  cancel [l ↦ lv]%I. rewrite sep_or_r. apply or_elim.
-  - (* Case 1 : nothing sent yet, we wait. *)
-    rewrite -or_intro_l. apply const_elim_sep_l=>-> {lv}.
-    rewrite (const_equiv (_ = _)) // left_id. wp_case.
-    wp_seq. rewrite -always_wand_impl always_elim.
-    rewrite !assoc. eapply wand_apply_r'; first done.
-    rewrite -(exist_intro γ) const_equiv //. solve_sep_entails.
-  - rewrite [(_ ★ □ _)%I]sep_elim_l -or_intro_r !sep_exist_r. apply exist_mono=>v.
-    rewrite -!assoc. apply const_elim_sep_l=>->{lv}. rewrite const_equiv // left_id.
-    rewrite sep_or_r. apply or_elim; last first.
-    { (* contradiction: we have the token twice. *)
-      rewrite [(heap_ctx _ ★ _)%I]sep_elim_r !assoc. rewrite -own_op own_valid_l.
-      rewrite -!assoc discrete_valid. apply const_elim_sep_l=>-[]. }
-    rewrite -or_intro_r. ecancel [own _ _].
-    wp_case. wp_let. ewp (eapply wp_value; wp_done).
-    rewrite (forall_elim v). rewrite !assoc. eapply wand_apply_r'; eauto with I.
+  rewrite /join_handle; iIntros "[[% H] Hv]"; iDestruct "H" as {γ} "(#?&Hγ&#?)".
+  iLöb "Hγ Hv" as "IH". wp_rec. wp_focus (! _)%E.
+  iInv N as "Hinv"; iDestruct "Hinv" as {v} "[Hl Hinv]".
+  wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
+  - iSplitL "Hl"; [iNext; iExists _; iFrame "Hl"; by iLeft|].
+    wp_case. wp_seq. iApply "IH" "Hγ Hv".
+  - iDestruct "Hinv" as {v'} "[% [HΨ|Hγ']]"; subst.
+    + iSplitL "Hl Hγ".
+      { iNext. iExists _; iFrame "Hl"; iRight.
+        iExists _; iSplit; [done|by iRight]. }
+      wp_case. wp_let. iPvsIntro. by iApply "Hv".
+    + iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct own_valid "Hγ" as "%".
 Qed.
 End proof.
+
+Typeclasses Opaque join_handle.
diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
new file mode 100644
index 0000000000000000000000000000000000000000..ff8c242c77726e6c6826d24b4fbdb5b06347b2c7
--- /dev/null
+++ b/heap_lang/proofmode.v
@@ -0,0 +1,176 @@
+From iris.proofmode Require Import coq_tactics.
+From iris.proofmode Require Export weakestpre.
+From iris.heap_lang Require Export wp_tactics heap.
+Import uPred.
+
+Ltac strip_later ::= iNext.
+
+Section heap.
+Context {Σ : gFunctors} `{heapG Σ}.
+Implicit Types N : namespace.
+Implicit Types P Q : iPropG heap_lang Σ.
+Implicit Types Φ : val → iPropG heap_lang Σ.
+Implicit Types Δ : envs (iResR 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.
+
+Lemma tac_wp_alloc Δ Δ' N E j e v Φ :
+  to_val e = Some v → 
+  Δ ⊢ heap_ctx N → nclose N ⊆ E →
+  StripLaterEnvs Δ Δ' →
+  (∀ l, ∃ Δ'',
+    envs_app false (Esnoc Enil j (l ↦ v)) Δ' = Some Δ'' ∧ Δ'' ⊢ Φ (LocV l)) →
+  Δ ⊢ WP Alloc e @ E {{ Φ }}.
+Proof.
+  intros ???? HΔ; eapply wp_alloc; eauto.
+  rewrite strip_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 Δ Δ' →
+  envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
+  Δ' ⊢ Φ v →
+  Δ ⊢ WP Load (Loc l) @ E {{ Φ }}.
+Proof.
+  intros. eapply wp_load; eauto.
+  rewrite strip_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 Δ Δ' →
+  envs_lookup i Δ' = Some (false, l ↦ v)%I →
+  envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
+  Δ'' ⊢ Φ (LitV LitUnit) → Δ ⊢ WP Store (Loc l) e @ E {{ Φ }}.
+Proof.
+  intros. eapply wp_store; eauto.
+  rewrite strip_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 Δ Δ' →
+  envs_lookup i Δ' = Some (false, l ↦{q} v)%I → v ≠ v1 →
+  Δ' ⊢ Φ (LitV (LitBool false)) →
+  Δ ⊢ WP CAS (Loc l) e1 e2 @ E {{ Φ }}.
+Proof.
+  intros. eapply wp_cas_fail; eauto.
+  rewrite strip_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 e1 v1 e2 v2 Φ :
+  to_val e1 = Some v1 → to_val e2 = Some v2 →
+  Δ ⊢ heap_ctx N → nclose N ⊆ E →
+  StripLaterEnvs Δ Δ' →
+  envs_lookup i Δ' = Some (false, l ↦ v1)%I →
+  envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
+  Δ'' ⊢ Φ (LitV (LitBool true)) → Δ ⊢ WP CAS (Loc l) e1 e2 @ E {{ Φ }}.
+Proof.
+  intros. eapply wp_cas_suc; eauto.
+  rewrite strip_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.
+
+Tactic Notation "wp_apply" open_constr(lem) :=
+  match goal with
+  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+    wp_bind K; iApply lem; try iNext)
+  end.
+
+Tactic Notation "wp_apply" open_constr(lem) constr(Hs) :=
+  match goal with
+  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+    wp_bind K; iApply lem Hs; try iNext)
+  end.
+
+Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
+  match goal with
+  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+    match eval hnf in e' with
+    | Alloc ?e =>
+       wp_bind K; eapply tac_wp_alloc with _ _ H _;
+         [wp_done || fail 2 "wp_alloc:" e "not a value"
+         |iAssumption || fail 2 "wp_alloc: cannot find heap_ctx"
+         |done || eauto with ndisj
+         |apply _
+         |intros l; eexists; split;
+           [env_cbv; reflexivity || fail 2 "wp_alloc:" H "not fresh"
+           |wp_finish]]
+    end)
+  end.
+Tactic Notation "wp_alloc" ident(l) := let H := iFresh in wp_alloc l as H.
+
+Tactic Notation "wp_load" :=
+  match goal with
+  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+    match eval hnf in e' with
+    | Load (Loc ?l) =>
+       wp_bind K; eapply tac_wp_load;
+         [iAssumption || fail 2 "wp_load: cannot find heap_ctx"
+         |done || eauto with ndisj
+         |apply _
+         |iAssumptionCore || fail 2 "wp_cas_fail: cannot find" l "↦ ?"
+         |wp_finish]
+    end)
+  end.
+
+Tactic Notation "wp_store" :=
+  match goal with
+  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+    match eval hnf in e' with
+    | Store ?l ?e =>
+       wp_bind K; eapply tac_wp_store;
+         [wp_done || fail 2 "wp_store:" e "not a value"
+         |iAssumption || fail 2 "wp_store: cannot find heap_ctx"
+         |done || eauto with ndisj
+         |apply _
+         |iAssumptionCore || fail 2 "wp_store: cannot find" l "↦ ?"
+         |env_cbv; reflexivity
+         |wp_finish]
+    end)
+  end.
+
+Tactic Notation "wp_cas_fail" :=
+  match goal with
+  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+    match eval hnf in e' with
+    | CAS (Loc ?l) ?e1 ?e2 =>
+       wp_bind K; eapply tac_wp_cas_fail;
+         [wp_done || fail 2 "wp_cas_fail:" e1 "not a value"
+         |wp_done || fail 2 "wp_cas_fail:" e2 "not a value"
+         |iAssumption || fail 2 "wp_cas_fail: cannot find heap_ctx"
+         |done || eauto with ndisj
+         |apply _
+         |iAssumptionCore || fail 2 "wp_cas_fail: cannot find" l "↦ ?"
+         |try discriminate
+         |wp_finish]
+    end)
+  end.
+
+Tactic Notation "wp_cas_suc" :=
+  match goal with
+  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+    match eval hnf in e' with
+    | CAS (Loc ?l) ?e1 ?e2 =>
+       wp_bind K; eapply tac_wp_cas_suc;
+         [wp_done || fail 2 "wp_cas_suc:" e1 "not a value"
+         |wp_done || fail 2 "wp_cas_suc:" e1 "not a value"
+         |iAssumption || fail 2 "wp_cas_suc: cannot find heap_ctx"
+         |done || eauto with ndisj
+         |apply _
+         |iAssumptionCore || fail 2 "wp_cas_suc: cannot find" l "↦ ?"
+         |env_cbv; reflexivity
+         |wp_finish]
+    end)
+  end.
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index a354151382324089c91b55f6257d24dbfe47feac..dc73a065f7a6f92a26a79c7b16718e1f674abd8f 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -9,33 +9,37 @@ Ltac wp_bind K :=
   | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
   end.
 
-Ltac wp_finish :=
-  intros_revert ltac:(
-    try strip_later;
-    match goal with
-    | |- _ ⊢ wp _ _ _ =>
-      etrans; [|eapply wp_value_pvs; fast_done]; lazy beta;
-      (* sometimes, we will have to do a final view shift, so only apply
-      pvs_intro if we obtain a consecutive wp *)
-      try (etrans; [|apply pvs_intro];
-           match goal with |- _ ⊢ wp _ _ _ => simpl | _ => fail end)
-    | _ => idtac
-    end).
-
 Ltac wp_done := rewrite -/of_val /= ?to_of_val; fast_done.
 
+Ltac wp_value_head :=
+  match goal with
+  | |- _ ⊢ wp _ _ _ =>
+    etrans; [|eapply wp_value_pvs; wp_done]; lazy beta;
+    (* sometimes, we will have to do a final view shift, so only apply
+    pvs_intro if we obtain a consecutive wp *)
+    try (
+      etrans; [|apply pvs_intro];
+      match goal with |- _ ⊢ wp _ _ _ => simpl | _ => fail end)
+  end.
+
+Ltac wp_finish := intros_revert ltac:(
+  rewrite -/of_val /= ?to_of_val; try strip_later; try wp_value_head).
+
+Tactic Notation "wp_value" :=
+  match goal with
+  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+    wp_bind K; wp_value_head)
+  end.
+
 Tactic Notation "wp_rec" :=
-  löb ltac:(
-    (* Find the redex and apply wp_rec *)
-    idtac; (* <https://coq.inria.fr/bugs/show_bug.cgi?id=4584> *)
-    lazymatch goal with
-    | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-      match eval hnf in e' with App ?e1 _ =>
+  lazymatch goal with
+  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+    match eval hnf in e' with App ?e1 _ =>
 (* hnf does not reduce through an of_val *)
 (*      match eval hnf in e1 with Rec _ _ _ => *)
-      wp_bind K; etrans; [|eapply wp_rec'; wp_done]; simpl_subst; wp_finish
+    wp_bind K; etrans; [|eapply wp_rec'; wp_done]; simpl_subst; wp_finish
 (*      end *) end)
-     end).
+   end.
 
 Tactic Notation "wp_lam" :=
   match goal with
@@ -96,13 +100,3 @@ Tactic Notation "wp_focus" open_constr(efoc) :=
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match e' with efoc => unify e' efoc; wp_bind K end)
   end.
-
-Tactic Notation "wp" tactic(tac) :=
-  match goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    wp_bind K; tac; [try strip_later|..])
-  end.
-
-(* In case the precondition does not match.
-   TODO: Have one tactic unifying wp and ewp. *)
-Tactic Notation "ewp" tactic(tac) := wp (etrans; [|tac]).
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index a136bdbae4ff5947e7af1bf4018b89c15acae05c..6aaff9f75faea8b24bd8f105080c260b44c56eba 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -69,8 +69,8 @@ Proof.
 Qed.
 Lemma own_alloc a E : ✓ a → True ⊢ (|={E}=> ∃ γ, own γ a).
 Proof.
-  intros Ha. rewrite (own_alloc_strong a E ∅) //; []. apply pvs_mono.
-  apply exist_mono=>?. eauto with I.
+  intros Ha. rewrite (own_alloc_strong a E ∅) //; [].
+  apply pvs_mono, exist_mono=>?. eauto with I.
 Qed.
 
 Lemma own_updateP P γ a E :
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index fe7966622089e8d2c26f024d757d0e55e4674f70..90c3a6ae613a121d1893c253af77b4398b8503b6 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -1,4 +1,5 @@
 From iris.program_logic Require Export weakestpre viewshifts.
+From iris.proofmode Require Import weakestpre.
 
 Definition ht {Λ Σ} (E : coPset) (P : iProp Λ Σ)
     (e : expr Λ) (Φ : val Λ → iProp Λ Σ) : iProp Λ Σ :=
@@ -39,24 +40,19 @@ Global Instance ht_mono' E :
 Proof. solve_proper. Qed.
 
 Lemma ht_alt E P Φ e : (P ⊢ WP e @ E {{ Φ }}) → {{ P }} e @ E {{ Φ }}.
-Proof.
-  intros; rewrite -{1}always_const. apply: always_intro. apply impl_intro_l.
-  by rewrite always_const right_id.
-Qed.
+Proof. iIntros {Hwp} "! HP". by iApply Hwp. Qed.
 
 Lemma ht_val E v :
   {{ True : iProp Λ Σ }} of_val v @ E {{ λ v', v = v' }}.
-Proof. apply ht_alt. by rewrite -wp_value'; apply const_intro. Qed.
+Proof. iIntros "! _". by iApply wp_value'. Qed.
 
 Lemma ht_vs E P P' Φ Φ' e :
   ((P ={E}=> P') ∧ {{ P' }} e @ E {{ Φ' }} ∧ ∀ v, Φ' v ={E}=> Φ v)
   ⊢ {{ P }} e @ E {{ Φ }}.
 Proof.
-  apply: always_intro. apply impl_intro_l.
-  rewrite (assoc _ P) {1}/vs always_elim impl_elim_r.
-  rewrite assoc pvs_impl_r pvs_always_r wp_always_r.
-  rewrite -(pvs_wp E e Φ) -(wp_pvs E e Φ); apply pvs_mono, wp_mono=> v.
-  by rewrite (forall_elim v) {1}/vs always_elim impl_elim_r.
+  iIntros "(#Hvs&#Hwp&#HΦ) ! HP". iPvs "Hvs" "HP" as "HP".
+  iApply wp_pvs; iApply wp_wand_r; iSplitL; [by iApply "Hwp"|].
+  iIntros {v} "Hv". by iApply "HΦ" "!".
 Qed.
 
 Lemma ht_atomic E1 E2 P P' Φ Φ' e :
@@ -64,33 +60,32 @@ Lemma ht_atomic E1 E2 P P' Φ Φ' e :
   ((P ={E1,E2}=> P') ∧ {{ P' }} e @ E2 {{ Φ' }} ∧ ∀ v, Φ' v ={E2,E1}=> Φ v)
   ⊢ {{ P }} e @ E1 {{ Φ }}.
 Proof.
-  intros ??; apply: always_intro. apply impl_intro_l.
-  rewrite (assoc _ P) {1}/vs always_elim impl_elim_r.
-  rewrite assoc pvs_impl_r pvs_always_r wp_always_r.
-  rewrite -(wp_atomic E1 E2) //; apply pvs_mono, wp_mono=> v.
-  by rewrite (forall_elim v) {1}/vs always_elim impl_elim_r.
+  iIntros {??} "(#Hvs&#Hwp&#HΦ) ! HP". iApply (wp_atomic _ E2); auto.
+  iPvs "Hvs" "HP" as "HP"; first set_solver. iPvsIntro.
+  iApply wp_wand_r; iSplitL; [by iApply "Hwp"|].
+  iIntros {v} "Hv". by iApply "HΦ" "!".
 Qed.
 
 Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e :
   ({{ P }} e @ E {{ Φ }} ∧ ∀ v, {{ Φ v }} K (of_val v) @ E {{ Φ' }})
   ⊢ {{ P }} K e @ E {{ Φ' }}.
 Proof.
-  intros; apply: always_intro. apply impl_intro_l.
-  rewrite (assoc _ P) {1}/ht always_elim impl_elim_r.
-  rewrite wp_always_r -wp_bind //; apply wp_mono=> v.
-  by rewrite (forall_elim v) /ht always_elim impl_elim_r.
+  iIntros "(#Hwpe&#HwpK) ! HP". iApply wp_bind.
+  iApply wp_wand_r; iSplitL; [by iApply "Hwpe"|].
+  iIntros {v} "Hv". by iApply "HwpK" "!".
 Qed.
 
 Lemma ht_mask_weaken E1 E2 P Φ e :
   E1 ⊆ E2 → {{ P }} e @ E1 {{ Φ }} ⊢ {{ P }} e @ E2 {{ Φ }}.
-Proof. intros. by apply always_mono, impl_mono, wp_mask_frame_mono. Qed.
+Proof.
+  iIntros {?} "#Hwp ! HP". iApply (wp_mask_frame_mono E1 E2); try done.
+  by iApply "Hwp".
+Qed.
 
 Lemma ht_frame_l E P Φ R e :
   {{ P }} e @ E {{ Φ }} ⊢ {{ R ★ P }} e @ E {{ λ v, R ★ Φ v }}.
 Proof.
-  apply always_intro', impl_intro_l.
-  rewrite always_and_sep_r -assoc (sep_and P) always_elim impl_elim_r.
-  by rewrite wp_frame_l.
+  iIntros "#Hwp ! [HR HP]". iApply wp_frame_l; iFrame "HR". by iApply "Hwp".
 Qed.
 
 Lemma ht_frame_r E P Φ R e :
@@ -101,17 +96,16 @@ Lemma ht_frame_step_l E P R e Φ :
   to_val e = None →
   {{ P }} e @ E {{ Φ }} ⊢ {{ ▷ R ★ P }} e @ E {{ λ v, R ★ Φ v }}.
 Proof.
-  intros; apply always_intro', impl_intro_l.
-  rewrite always_and_sep_r -assoc (sep_and P) always_elim impl_elim_r.
-  by rewrite wp_frame_step_l //; apply wp_mono=>v; rewrite pvs_frame_l.
+  iIntros {?} "#Hwp ! [HR HP]".
+  iApply wp_frame_step_l; try done. iFrame "HR". by iApply "Hwp".
 Qed.
 
 Lemma ht_frame_step_r E P Φ R e :
   to_val e = None →
   {{ P }} e @ E {{ Φ }} ⊢ {{ P ★ ▷ R }} e @ E {{ λ v, Φ v ★ R }}.
 Proof.
-  rewrite (comm _ _ (â–· R)%I); setoid_rewrite (comm _ _ R).
-  apply ht_frame_step_l.
+  iIntros {?} "#Hwp ! [HP HR]".
+  iApply wp_frame_step_r; try done. iFrame "HR". by iApply "Hwp".
 Qed.
 
 Lemma ht_inv N E P Φ R e :
@@ -119,13 +113,7 @@ Lemma ht_inv N E P Φ R e :
   (inv N R ★ {{ ▷ R ★ P }} e @ E ∖ nclose N {{ λ v, ▷ R ★ Φ v }})
     ⊢ {{ P }} e @ E {{ Φ }}.
 Proof.
-  intros; apply: always_intro. apply impl_intro_l.
-  rewrite always_and_sep_r assoc [(P ★ _)%I]comm -assoc.
-  eapply wp_inv; [by eauto with I..|].
-  rewrite sep_elim_r. apply wand_intro_l.
-  (* Oh wow, this is annyoing... *)
-  rewrite assoc -always_and_sep_r'.
-  by rewrite /ht always_elim impl_elim_r.
+  iIntros {??} "[#? #Hwp] ! HP". eapply wp_inv; eauto.
+  iIntros "HR". iApply "Hwp". by iSplitL "HR".
 Qed.
-
 End hoare.
diff --git a/program_logic/hoare_lifting.v b/program_logic/hoare_lifting.v
index c9dfcfed8faba1eac5e09a44f67cfa9b97effee9..c9db56c66e71e31e573a2dced978a963845a0a34 100644
--- a/program_logic/hoare_lifting.v
+++ b/program_logic/hoare_lifting.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Import upred_tactics.
 From iris.program_logic Require Export hoare lifting.
 From iris.program_logic Require Import ownership.
-Import uPred.
+From iris.proofmode Require Import tactics pviewshifts.
 
 Local Notation "{{ P } } ef ?@ E {{ Φ } }" :=
   (default True%I ef (λ e, ht E P e Φ))
@@ -29,23 +29,15 @@ Lemma ht_lift_step E1 E2
    (∀ e2 σ2 ef, {{ Φ2 e2 σ2 ef }} ef ?@ ⊤ {{ λ _, True }}))
   ⊢ {{ P }} e1 @ E1 {{ Ψ }}.
 Proof.
-  intros ?? Hsafe Hstep; apply: always_intro. apply impl_intro_l.
-  rewrite (assoc _ P) {1}/vs always_elim impl_elim_r pvs_always_r.
-  rewrite -(wp_lift_step E1 E2 φ _ e1 σ1) //; apply pvs_mono.
-  rewrite always_and_sep_r -assoc; apply sep_mono_r.
-  rewrite [(_ ∧ _)%I]later_intro -later_sep; apply later_mono.
-  apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
-  do 3 rewrite (forall_elim e2) (forall_elim σ2) (forall_elim ef).
-  apply wand_intro_l; rewrite !always_and_sep_l.
-  (* Apply the view shift. *)
-  rewrite (assoc _ _ P') -(assoc _ _ _ P') assoc.
-  rewrite {1}/vs -always_wand_impl always_elim wand_elim_r.
-  rewrite pvs_frame_r; apply pvs_mono.
-  (* Now we're almost done. *)
-  sep_split left: [Φ1 _ _ _; {{ Φ1 _ _ _ }} e2 @ E1 {{ Ψ }}]%I.
-  - rewrite {1}/ht -always_wand_impl always_elim wand_elim_r //.
-  - destruct ef as [e'|]; simpl; [|by apply const_intro].
-    rewrite {1}/ht -always_wand_impl always_elim wand_elim_r //.
+  iIntros {?? Hsafe Hstep} "#(#Hvs&HΦ&He2&Hef) ! HP".
+  iApply (wp_lift_step E1 E2 φ _ e1 σ1); auto.
+  iPvs "Hvs" "HP" as "[Hσ HP]"; first set_solver.
+  iPvsIntro. iNext. iSplitL "Hσ"; [done|iIntros {e2 σ2 ef} "[#Hφ Hown]"].
+  iSpecialize "HΦ" {e2 σ2 ef} "! -". by iFrame "Hφ HP Hown".
+  iPvs "HΦ" as "[H1 H2]"; first by set_solver.
+  iPvsIntro. iSplitL "H1".
+  - by iApply "He2" "!".
+  - destruct ef as [e|]; last done. by iApply "Hef" {_ _ (Some e)} "!".
 Qed.
 
 Lemma ht_lift_atomic_step
@@ -56,24 +48,19 @@ Lemma ht_lift_atomic_step
   (∀ e2 σ2 ef, {{ ■ φ e2 σ2 ef ★ P }} ef ?@ ⊤ {{ λ _, True }}) ⊢
   {{ ▷ ownP σ1 ★ ▷ P }} e1 @ E {{ λ v, ∃ σ2 ef, ownP σ2 ★ ■ φ (of_val v) σ2 ef }}.
 Proof.
-  intros ? Hsafe Hstep; set (φ' e σ ef := is_Some (to_val e) ∧ φ e σ ef).
-  rewrite -(ht_lift_step E E φ'  _ P
+  iIntros {? Hsafe Hstep} "#Hef".
+  set (φ' e σ ef := is_Some (to_val e) ∧ φ e σ ef).
+  iApply (ht_lift_step E E φ'  _ P
     (λ e2 σ2 ef, ownP σ2 ★ ■ (φ' e2 σ2 ef))%I
     (λ e2 σ2 ef, ■ φ e2 σ2 ef ★ P)%I);
     try by (rewrite /φ'; eauto using atomic_not_val, atomic_step).
-  apply and_intro; [by rewrite -vs_reflexive; apply const_intro|].
-  apply and_intro; [|apply and_intro; [|done]].
-  - apply forall_mono=>e2; apply forall_mono=>σ2; apply forall_mono=>ef.
-    rewrite -vs_impl; apply: always_intro. apply impl_intro_l.
-    rewrite and_elim_l !assoc; apply sep_mono; last done.
-    rewrite -!always_and_sep_l -!always_and_sep_r; apply const_elim_l=>-[??].
-    by repeat apply and_intro; try apply const_intro.
-  - apply forall_mono=>e2; apply forall_mono=>σ2; apply forall_mono=>ef.
-    apply (always_intro _ _), impl_intro_l; rewrite and_elim_l.
-    rewrite -always_and_sep_r; apply const_elim_r=>-[[v Hv] ?].
-    rewrite -(of_to_val e2 v) // -wp_value'; [].
-    rewrite -(exist_intro σ2) -(exist_intro ef) (of_to_val e2) //.
-    by rewrite -always_and_sep_r; apply and_intro; try apply const_intro.
+  repeat iSplit.
+  - by iApply vs_reflexive.
+  - iIntros {e2 σ2 ef} "! (#Hφ&Hown&HP)"; iPvsIntro.
+    iSplitL "Hown". by iSplit. iSplit. by iPure "Hφ" as [_ ?]. done.
+  - iIntros {e2 σ2 ef} "! [Hown #Hφ]"; iPure "Hφ" as [[v2 <-%of_to_val] ?].
+    iApply wp_value'. iExists σ2, ef. by iSplit.
+  - done.
 Qed.
 
 Lemma ht_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) P P' Ψ e1 :
@@ -84,16 +71,11 @@ Lemma ht_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) P P' Ψ e
    (∀ e2 ef, {{ ■ φ e2 ef ★ P' }} ef ?@ ⊤ {{ λ _, True }}))
   ⊢ {{ ▷(P ★ P') }} e1 @ E {{ Ψ }}.
 Proof.
-  intros ? Hsafe Hstep; apply: always_intro. apply impl_intro_l.
-  rewrite -(wp_lift_pure_step E φ _ e1) //.
-  rewrite [(_ ∧ ∀ _, _)%I]later_intro -later_and; apply later_mono.
-  apply forall_intro=>e2; apply forall_intro=>ef; apply impl_intro_l.
-  do 2 rewrite (forall_elim e2) (forall_elim ef).
-  rewrite always_and_sep_l !always_and_sep_r {1}(always_sep_dup (â–  _)).
-  sep_split left: [■ φ _ _; P; {{ ■ φ _ _ ★ P }} e2 @ E {{ Ψ }}]%I.
-  - rewrite assoc {1}/ht -always_wand_impl always_elim wand_elim_r //.
-  - destruct ef as [e'|]; simpl; [|by apply const_intro].
-    rewrite assoc {1}/ht -always_wand_impl always_elim wand_elim_r //.
+  iIntros {? Hsafe Hstep} "[#He2 #Hef] ! HP".
+  iApply (wp_lift_pure_step E φ _ e1); auto.
+  iNext; iIntros {e2 ef Hφ}. iDestruct "HP" as "[HP HP']"; iSplitL "HP".
+  - iApply "He2" "!"; by iSplit.
+  - destruct ef as [e|]; last done. iApply "Hef" {_ (Some e)} "!"; by iSplit.
 Qed.
 
 Lemma ht_lift_pure_det_step
@@ -104,18 +86,11 @@ Lemma ht_lift_pure_det_step
   ({{ P }} e2 @ E {{ Ψ }} ∧ {{ P' }} ef ?@ ⊤ {{ λ _, True }})
   ⊢ {{ ▷(P ★ P') }} e1 @ E {{ Ψ }}.
 Proof.
-  intros ? Hsafe Hdet.
-  rewrite -(ht_lift_pure_step _ (λ e2' ef', e2 = e2' ∧ ef = ef')); eauto.
-  apply and_mono.
-  - apply forall_intro=>e2'; apply forall_intro=>ef'.
-    apply: always_intro. apply impl_intro_l.
-    rewrite -always_and_sep_l -assoc; apply const_elim_l=>-[??]; subst.
-    by rewrite /ht always_elim impl_elim_r.
-  - apply forall_intro=>e2'; apply forall_intro=>ef'.
-    destruct ef' as [e'|]; simpl; [|by apply const_intro].
-    apply: always_intro. apply impl_intro_l.
-    rewrite -always_and_sep_l -assoc; apply const_elim_l=>-[??]; subst.
-    by rewrite /= /ht always_elim impl_elim_r.
+  iIntros {? Hsafe Hdet} "[#He2 #Hef]".
+  iApply (ht_lift_pure_step _ (λ e2' ef', e2 = e2' ∧ ef = ef')); eauto.
+  iSplit; iIntros {e2' ef'}.
+  - iIntros "! [#He ?]"; iPure "He" as [-> ->]. by iApply "He2".
+  - destruct ef' as [e'|]; last done.
+    iIntros "! [#He ?]"; iPure "He" as [-> ->]. by iApply "Hef" "!".
 Qed.
-
 End lifting.
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index b2dfb0eefcd40baa2558be5cedfecffd88fde8d5..490ca8baf844209bfb4bb5e426d8459f2aa718a7 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -26,7 +26,7 @@ Proof. intros n ???. apply exist_ne=>i. by apply and_ne, ownI_contractive. Qed.
 Global Instance inv_persistent N P : PersistentP (inv N P).
 Proof. rewrite /inv; apply _. Qed.
 
-Lemma always_inv N P : (□ inv N P) ⊣⊢ inv N P.
+Lemma always_inv N P : □ inv N P ⊣⊢ inv N P.
 Proof. by rewrite always_always. Qed.
 
 (** Invariants can be opened around any frame-shifting assertion. *)
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index e723026188cdb460e52ac7a67ca5cee2af0835ae..51c23f4769d970ed9bbe064baf413456aa754799 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -70,7 +70,7 @@ Proof.
   destruct (HP rf k Ef σ) as (r2&?&?); eauto.
   exists r2; eauto using uPred_in_entails.
 Qed.
-Lemma pvs_timeless E P : TimelessP P → (▷ P) ⊢ (|={E}=> P).
+Lemma pvs_timeless E P : TimelessP P → ▷ P ⊢ (|={E}=> P).
 Proof.
   rewrite pvs_eq uPred.timelessP_spec=> HP.
   uPred.unseal; split=>-[|n] r ? HP' rf k Ef σ ???; first lia.
@@ -163,8 +163,7 @@ Lemma pvs_wand_l E1 E2 P Q : ((P -★ Q) ★ (|={E1,E2}=> P)) ⊢ (|={E1,E2}=> Q
 Proof. by rewrite pvs_frame_l wand_elim_l. Qed.
 Lemma pvs_wand_r E1 E2 P Q : ((|={E1,E2}=> P) ★ (P -★ Q)) ⊢ (|={E1,E2}=> Q).
 Proof. by rewrite pvs_frame_r wand_elim_r. Qed.
-Lemma pvs_sep E P Q:
-  ((|={E}=> P) ★ (|={E}=> Q)) ⊢ (|={E}=> P ★ Q).
+Lemma pvs_sep E P Q : ((|={E}=> P) ★ (|={E}=> Q)) ⊢ (|={E}=> P ★ Q).
 Proof. rewrite pvs_frame_r pvs_frame_l pvs_trans //. set_solver. Qed.
 
 Lemma pvs_mask_frame' E1 E1' E2 E2' P :
@@ -230,17 +229,17 @@ Proof.
   move=>->. rewrite -{2}fsa_trans3.
   apply pvs_mono, fsa_mono=>a; apply pvs_intro.
 Qed.
+Lemma fsa_pvs_fsa E Φ : (|={E}=> fsa E Φ) ⊣⊢ fsa E Φ.
+Proof. apply (anti_symm (⊢)); [by apply fsa_strip_pvs|apply pvs_intro]. Qed.
 Lemma fsa_mono_pvs E Φ Ψ : (∀ a, Φ a ⊢ (|={E}=> Ψ a)) → fsa E Φ ⊢ fsa E Ψ.
 Proof. intros. rewrite -[fsa E Ψ]fsa_trans3 -pvs_intro. by apply fsa_mono. Qed.
 End fsa.
 
 Definition pvs_fsa {Λ Σ} : FSA Λ Σ () := λ E Φ, (|={E}=> Φ ())%I.
+Arguments pvs_fsa _ _ _ _/.
+
 Instance pvs_fsa_prf {Λ Σ} : FrameShiftAssertion True (@pvs_fsa Λ Σ).
 Proof.
   rewrite /pvs_fsa.
   split; auto using pvs_mask_frame_mono, pvs_trans3, pvs_frame_r.
 Qed.
-
-Lemma pvs_mk_fsa {Λ Σ} E (P Q : iProp Λ Σ) :
-  P ⊢ pvs_fsa E (λ _, Q) → P ⊢ |={E}=> Q.
-Proof. by intros ?. Qed.
diff --git a/program_logic/tactics.v b/program_logic/tactics.v
deleted file mode 100644
index d155bdc349eb43b342723aa4c518f9519e9591d7..0000000000000000000000000000000000000000
--- a/program_logic/tactics.v
+++ /dev/null
@@ -1,42 +0,0 @@
-From iris.algebra Require Export upred_tactics.
-From iris.program_logic Require Export pviewshifts.
-Import uPred.
-
-Module uPred_reflection_pvs.
-  Import uPred_reflection.
-  Section uPred_reflection_pvs.
-  
-  Context {Λ : language} {Σ : iFunctor}.
-  Local Notation iProp := (iProp Λ Σ).
-
-  Lemma cancel_entails_pvs Σ' E1 E2 e1 e2 e1' e2' ns :
-    cancel ns e1 = Some e1' → cancel ns e2 = Some e2' →
-    eval Σ' e1' ⊢ pvs E1 E2 (eval Σ' e2' : iProp) → eval Σ' e1 ⊢ pvs E1 E2 (eval Σ' e2).
-  Proof.
-    intros ??. rewrite !eval_flatten.
-    rewrite (flatten_cancel e1 e1' ns) // (flatten_cancel e2 e2' ns) //; csimpl.
-    rewrite !fmap_app !big_sep_app. rewrite -pvs_frame_l. apply sep_mono_r.
-  Qed.
-
-  End uPred_reflection_pvs.
-  
-  Ltac quote_pvs :=
-    match goal with
-    | |- ?P1 ⊢ pvs ?E1 ?E2 ?P2 =>
-      lazymatch type of (_ : Quote [] _ P1 _) with Quote _ ?Σ2 _ ?e1 =>
-      lazymatch type of (_ : Quote Σ2 _ P2 _) with Quote _ ?Σ3 _ ?e2 =>
-        change (eval Σ3 e1 ⊢ pvs E1 E2 (eval Σ3 e2)) end end
-    end.
-End uPred_reflection_pvs.
-
-Tactic Notation "cancel_pvs" constr(Ps) :=
-  uPred_reflection_pvs.quote_pvs;
-  let Σ := match goal with |- uPred_reflection.eval ?Σ _ ⊢ _ => Σ end in
-  let ns' := lazymatch type of (_ : uPred_reflection.QuoteArgs Σ Ps _) with
-             | uPred_reflection.QuoteArgs _ _ ?ns' => ns'
-             end in
-  eapply uPred_reflection_pvs.cancel_entails_pvs with (ns:=ns');
-    [cbv; reflexivity|cbv; reflexivity|simpl]. 
-
-Tactic Notation "ecancel_pvs" open_constr(Ps) :=
-  close_uPreds Ps ltac:(fun Qs => cancel_pvs Qs).
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index 2824a6ce85a5996770f4088b62fbe6c6056c3f0b..eb1c9154394b614dd9723081110ec01e79ddfcb0 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -1,5 +1,6 @@
 From iris.program_logic Require Import ownership.
 From iris.program_logic Require Export pviewshifts invariants ghost_ownership.
+From iris.proofmode Require Import pviewshifts.
 Import uPred.
 
 Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
@@ -23,10 +24,7 @@ Implicit Types P Q R : iProp Λ Σ.
 Implicit Types N : namespace.
 
 Lemma vs_alt E1 E2 P Q : P ⊢ (|={E1,E2}=> Q) → P ={E1,E2}=> Q.
-Proof.
-  intros; rewrite -{1}always_const. apply: always_intro. apply impl_intro_l.
-  by rewrite always_const right_id.
-Qed.
+Proof. iIntros {Hvs} "! ?". by iApply Hvs. Qed.
 
 Global Instance vs_ne E1 E2 n :
   Proper (dist n ==> dist n ==> dist n) (@vs Λ Σ E1 E2).
@@ -44,44 +42,35 @@ Global Instance vs_mono' E1 E2 :
 Proof. solve_proper. Qed.
 
 Lemma vs_false_elim E1 E2 P : False ={E1,E2}=> P.
-Proof. apply vs_alt, False_elim. Qed.
+Proof. iIntros "! []". Qed.
 Lemma vs_timeless E P : TimelessP P → ▷ P ={E}=> P.
-Proof. by intros ?; apply vs_alt, pvs_timeless. Qed.
+Proof. iIntros {?} "! HP". by iApply pvs_timeless. Qed.
 
 Lemma vs_transitive E1 E2 E3 P Q R :
   E2 ⊆ E1 ∪ E3 → ((P ={E1,E2}=> Q) ∧ (Q ={E2,E3}=> R)) ⊢ (P ={E1,E3}=> R).
 Proof.
-  intros; rewrite -always_and; apply: always_intro. apply impl_intro_l.
-  rewrite always_and assoc (always_elim (P → _)) impl_elim_r.
-  by rewrite pvs_impl_r; apply pvs_trans.
+  iIntros {?} "#[HvsP HvsQ] ! HP".
+  iPvs "HvsP" "! HP" as "HQ"; first done. by iApply "HvsQ" "!".
 Qed.
 
 Lemma vs_transitive' E P Q R : ((P ={E}=> Q) ∧ (Q ={E}=> R)) ⊢ (P ={E}=> R).
 Proof. apply vs_transitive; set_solver. Qed.
 Lemma vs_reflexive E P : P ={E}=> P.
-Proof. apply vs_alt, pvs_intro. Qed.
+Proof. iIntros "! HP"; by iPvsIntro. Qed.
 
 Lemma vs_impl E P Q : □ (P → Q) ⊢ (P ={E}=> Q).
-Proof.
-  apply always_intro', impl_intro_l.
-  by rewrite always_elim impl_elim_r -pvs_intro.
-Qed.
+Proof. iIntros "#HPQ ! HP". iPvsIntro. by iApply "HPQ". Qed.
 
 Lemma vs_frame_l E1 E2 P Q R : (P ={E1,E2}=> Q) ⊢ (R ★ P ={E1,E2}=> R ★ Q).
-Proof.
-  apply always_intro', impl_intro_l.
-  rewrite -pvs_frame_l always_and_sep_r -always_wand_impl -assoc.
-  by rewrite always_elim wand_elim_r.
-Qed.
+Proof. iIntros "#Hvs ! [HR HP]". iFrame "HR". by iApply "Hvs". Qed.
 
 Lemma vs_frame_r E1 E2 P Q R : (P ={E1,E2}=> Q) ⊢ (P ★ R ={E1,E2}=> Q ★ R).
-Proof. rewrite !(comm _ _ R); apply vs_frame_l. Qed.
+Proof. iIntros "#Hvs ! [HP HR]". iFrame "HR". by iApply "Hvs". Qed.
 
 Lemma vs_mask_frame E1 E2 Ef P Q :
   Ef ⊥ E1 ∪ E2 → (P ={E1,E2}=> Q) ⊢ (P ={E1 ∪ Ef,E2 ∪ Ef}=> Q).
 Proof.
-  intros ?; apply always_intro', impl_intro_l; rewrite (pvs_mask_frame _ _ Ef)//.
-  by rewrite always_elim impl_elim_r.
+  iIntros {?} "#Hvs ! HP". iApply pvs_mask_frame; auto. by iApply "Hvs".
 Qed.
 
 Lemma vs_mask_frame' E Ef P Q : Ef ⊥ E → (P ={E}=> Q) ⊢ (P ={E ∪ Ef}=> Q).
@@ -90,18 +79,12 @@ Proof. intros; apply vs_mask_frame; set_solver. Qed.
 Lemma vs_inv N E P Q R :
   nclose N ⊆ E → (inv N R ★ (▷ R ★ P ={E ∖ nclose N}=> ▷ R ★ Q)) ⊢ (P ={E}=> Q).
 Proof.
-  intros; apply: always_intro. apply impl_intro_l.
-  rewrite always_and_sep_r assoc [(P ★ _)%I]comm -assoc.
-  eapply pvs_inv; [by eauto with I..|].
-  rewrite sep_elim_r. apply wand_intro_l.
-  (* Oh wow, this is annyoing... *)
-  rewrite assoc -always_and_sep_r'.
-  by rewrite /vs always_elim impl_elim_r.
+  iIntros {?} "#[? Hvs] ! HP". eapply pvs_inv; eauto.
+  iIntros "HR". iApply "Hvs" "!". by iSplitL "HR".
 Qed.
 
 Lemma vs_alloc N P : â–· P ={N}=> inv N P.
-Proof. by intros; apply vs_alt, inv_alloc. Qed.
-
+Proof. iIntros "! HP". by iApply inv_alloc. Qed.
 End vs.
 
 Section vs_ghost.
@@ -116,8 +99,6 @@ Proof. by intros; apply vs_alt, own_updateP. Qed.
 Lemma vs_update E γ a a' : a ~~> a' → own γ a ={E}=> own γ a'.
 Proof. by intros; apply vs_alt, own_update. Qed.
 
-Lemma vs_own_empty `{Empty A, !CMRAUnit A} E γ :
-  True ={E}=> own γ ∅.
+Lemma vs_own_empty `{Empty A, !CMRAUnit A} E γ : True ={E}=> own γ ∅.
 Proof. by intros; eapply vs_alt, own_empty. Qed.
-
 End vs_ghost.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
new file mode 100644
index 0000000000000000000000000000000000000000..ec440499f13d3208546276cceb8f51b3c1a803a3
--- /dev/null
+++ b/proofmode/coq_tactics.v
@@ -0,0 +1,808 @@
+From iris.algebra Require Export upred.
+From iris.algebra Require Import upred_big_op upred_tactics.
+From iris.proofmode Require Export environments.
+From iris.prelude Require Import stringmap.
+Import uPred.
+
+Local Notation "Γ !! j" := (env_lookup j Γ).
+Local Notation "x ← y ; z" := (match y with Some x => z | None => None end).
+Local Notation "' ( x1 , x2 ) ← y ; z" :=
+  (match y with Some (x1,x2) => z | None => None end).
+Local Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
+  (match y with Some (x1,x2,x3) => z | None => None end).
+
+Record envs (M : cmraT) :=
+  Envs { env_persistent : env (uPred M); env_spatial : env (uPred M) }.
+Add Printing Constructor envs.
+Arguments Envs {_} _ _.
+Arguments env_persistent {_} _.
+Arguments env_spatial {_} _.
+
+Record envs_wf {M} (Δ : envs M) := {
+  env_persistent_valid : env_wf (env_persistent Δ);
+  env_spatial_valid : env_wf (env_spatial Δ);
+  envs_disjoint i : env_persistent Δ !! i = None ∨ env_spatial Δ !! i = None
+}.
+
+Coercion of_envs {M} (Δ : envs M) : uPred M :=
+  (■ envs_wf Δ ★ □ Π∧ env_persistent Δ ★ Π★ env_spatial Δ)%I.
+
+Instance envs_dom {M} : Dom (envs M) stringset := λ Δ,
+  dom stringset (env_persistent Δ) ∪ dom stringset (env_spatial Δ).
+
+Definition envs_lookup {M} (i : string) (Δ : envs M) : option (bool * uPred M) :=
+  let (Γp,Γs) := Δ in
+  match env_lookup i Γp with
+  | Some P => Some (true, P) | None => P ← env_lookup i Γs; Some (false, P)
+  end.
+
+Definition envs_delete {M} (i : string) (p : bool) (Δ : envs M) : envs M :=
+  let (Γp,Γs) := Δ in
+  match p with
+  | true => Envs (env_delete i Γp) Γs | false => Envs Γp (env_delete i Γs)
+  end.
+
+Definition envs_lookup_delete {M} (i : string)
+    (Δ : envs M) : option (bool * uPred M * envs M) :=
+  let (Γp,Γs) := Δ in
+  match env_lookup_delete i Γp with
+  | Some (P,Γp') => Some (true, P, Envs Γp' Γs)
+  | None => '(P,Γs') ← env_lookup_delete i Γs; Some (false, P, Envs Γp Γs')
+  end.
+
+Definition envs_app {M} (p : bool)
+    (Γ : env (uPred M)) (Δ : envs M) : option (envs M) :=
+  let (Γp,Γs) := Δ in
+  match p with
+  | true => _ ← env_app Γ Γs; Γp' ← env_app Γ Γp; Some (Envs Γp' Γs)
+  | false => _ ← env_app Γ Γp; Γs' ← env_app Γ Γs; Some (Envs Γp Γs')
+  end.
+
+Definition envs_simple_replace {M} (i : string) (p : bool) (Γ : env (uPred M))
+    (Δ : envs M) : option (envs M) :=
+  let (Γp,Γs) := Δ in
+  match p with
+  | true => _ ← env_app Γ Γs; Γp' ← env_replace i Γ Γp; Some (Envs Γp' Γs)
+  | false => _ ← env_app Γ Γp; Γs' ← env_replace i Γ Γs; Some (Envs Γp Γs')
+  end.
+
+Definition envs_replace {M} (i : string) (p q : bool) (Γ : env (uPred M))
+    (Δ : envs M) : option (envs M) :=
+  if eqb p q then envs_simple_replace i p Γ Δ
+  else envs_app q Γ (envs_delete i p Δ).
+
+(* if [lr = false] then [result = (hyps named js,remainding hyps)],
+   if [lr = true] then [result = (remainding hyps,hyps named js)] *)
+Definition envs_split {M}
+    (lr : bool) (js : list string) (Δ : envs M) : option (envs M * envs M) :=
+  let (Γp,Γs) := Δ in
+  '(Γs1,Γs2) ← env_split js Γs;
+  match lr with
+  | false  => Some (Envs Γp Γs1, Envs Γp Γs2)
+  | true => Some (Envs Γp Γs2, Envs Γp Γs1)
+  end.
+
+Definition envs_persistent {M} (Δ : envs M) :=
+  if env_spatial Δ is Enil then true else false.
+
+(* Coq versions of the tactics *)
+Section tactics.
+Context {M : cmraT}.
+Implicit Types Γ : env (uPred M).
+Implicit Types Δ : envs M.
+Implicit Types P Q : uPred M.
+
+Lemma envs_lookup_delete_Some Δ Δ' i p P :
+  envs_lookup_delete i Δ = Some (p,P,Δ')
+  ↔ envs_lookup i Δ = Some (p,P) ∧ Δ' = envs_delete i p Δ.
+Proof.
+  rewrite /envs_lookup /envs_delete /envs_lookup_delete.
+  destruct Δ as [Γp Γs]; rewrite /= !env_lookup_delete_correct.
+  destruct (Γp !! i), (Γs !! i); naive_solver.
+Qed.
+
+Lemma envs_lookup_sound Δ i p P :
+  envs_lookup i Δ = Some (p,P) →
+  Δ ⊢ ((if p then □ P else P) ★ envs_delete i p Δ).
+Proof.
+  rewrite /envs_lookup /envs_delete /of_envs=>?; apply const_elim_sep_l=> Hwf.
+  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
+  - rewrite (env_lookup_perm Γp) //= always_and_sep always_sep.
+    ecancel [□ Π∧ _; □ P; Π★ _]%I; apply const_intro.
+    destruct Hwf; constructor;
+      naive_solver eauto using env_delete_wf, env_delete_fresh.
+  - destruct (Γs !! i) eqn:?; simplify_eq/=.
+    rewrite (env_lookup_perm Γs) //=.
+    ecancel [□ Π∧ _; P; Π★ _]%I; apply const_intro.
+    destruct Hwf; constructor;
+      naive_solver eauto using env_delete_wf, env_delete_fresh.
+Qed.
+Lemma envs_lookup_sound' Δ i p P :
+  envs_lookup i Δ = Some (p,P) → Δ ⊢ (P ★ envs_delete i p Δ).
+Proof.
+  intros. rewrite envs_lookup_sound //. by destruct p; rewrite ?always_elim.
+Qed.
+Lemma envs_lookup_persistent_sound Δ i P :
+  envs_lookup i Δ = Some (true,P) → Δ ⊢ (□ P ★ Δ).
+Proof.
+  intros. apply: always_entails_l. by rewrite envs_lookup_sound // sep_elim_l.
+Qed.
+
+Lemma envs_lookup_split Δ i p P :
+  envs_lookup i Δ = Some (p,P) →
+  Δ ⊢ ((if p then □ P else P) ★ ((if p then □ P else P) -★ Δ)).
+Proof.
+  rewrite /envs_lookup /of_envs=>?; apply const_elim_sep_l=> Hwf.
+  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
+  - rewrite (env_lookup_perm Γp) //= always_and_sep always_sep.
+    rewrite const_equiv // left_id.
+    cancel [â–¡ P]%I. apply wand_intro_l. solve_sep_entails.
+  - destruct (Γs !! i) eqn:?; simplify_eq/=.
+    rewrite (env_lookup_perm Γs) //=. rewrite const_equiv // left_id.
+    cancel [P]. apply wand_intro_l. solve_sep_entails.
+Qed.
+
+Lemma envs_lookup_delete_sound Δ Δ' i p P :
+  envs_lookup_delete i Δ = Some (p,P,Δ') → Δ ⊢ ((if p then □ P else P) ★ Δ')%I.
+Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound. Qed.
+Lemma envs_lookup_delete_sound' Δ Δ' i p P :
+  envs_lookup_delete i Δ = Some (p,P,Δ') → Δ ⊢ (P ★ Δ')%I.
+Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound'. Qed.
+
+Lemma envs_app_sound Δ Δ' p Γ :
+  envs_app p Γ Δ = Some Δ' → Δ ⊢ ((if p then □ Π∧ Γ else Π★ Γ) -★ Δ').
+Proof.
+  rewrite /of_envs /envs_app=> ?; apply const_elim_sep_l=> Hwf.
+  destruct Δ as [Γp Γs], p; simplify_eq/=.
+  - destruct (env_app Γ Γs) eqn:Happ,
+      (env_app Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
+    apply wand_intro_l, sep_intro_True_l; [apply const_intro|].
+    + destruct Hwf; constructor; simpl; eauto using env_app_wf.
+      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
+      naive_solver eauto using env_app_fresh.
+    + rewrite (env_app_perm _ _ Γp') //.
+      rewrite big_and_app always_and_sep always_sep; solve_sep_entails.
+  - destruct (env_app Γ Γp) eqn:Happ,
+      (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
+    apply wand_intro_l, sep_intro_True_l; [apply const_intro|].
+    + destruct Hwf; constructor; simpl; eauto using env_app_wf.
+      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
+      naive_solver eauto using env_app_fresh.
+    + rewrite (env_app_perm _ _ Γs') // big_sep_app. solve_sep_entails.
+Qed.
+
+Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
+  envs_simple_replace i p Γ Δ = Some Δ' →
+  envs_delete i p Δ ⊢ ((if p then □ Π∧ Γ else Π★ Γ) -★ Δ')%I.
+Proof.
+  rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
+  apply const_elim_sep_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
+  - destruct (env_app Γ Γs) eqn:Happ,
+      (env_replace i Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
+    apply wand_intro_l, sep_intro_True_l; [apply const_intro|].
+    + destruct Hwf; constructor; simpl; eauto using env_replace_wf.
+      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_and_app always_and_sep always_sep; solve_sep_entails.
+  - destruct (env_app Γ Γp) eqn:Happ,
+      (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
+    apply wand_intro_l, sep_intro_True_l; [apply const_intro|].
+    + destruct Hwf; constructor; simpl; eauto using env_replace_wf.
+      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 _ _ Γs') // big_sep_app. solve_sep_entails.
+Qed.
+
+Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
+  envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' →
+  Δ ⊢ ((if p then □ P else P) ★
+       ((if p then □ Π∧ Γ else Π★ Γ) -★ Δ'))%I.
+Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.
+
+Lemma envs_replace_sound' Δ Δ' i p q Γ :
+  envs_replace i p q Γ Δ = Some Δ' →
+  envs_delete i p Δ ⊢ ((if q then □ Π∧ Γ else Π★ Γ) -★ Δ')%I.
+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_sound Δ Δ' i p q P Γ :
+  envs_lookup i Δ = Some (p,P) → envs_replace i p q Γ Δ = Some Δ' →
+  Δ ⊢ ((if p then □ P else P) ★
+       ((if q then □ Π∧ Γ else Π★ Γ) -★ Δ'))%I.
+Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.
+
+Lemma envs_split_sound Δ lr js Δ1 Δ2 :
+  envs_split lr js Δ = Some (Δ1,Δ2) → Δ ⊢ (Δ1 ★ Δ2).
+Proof.
+  rewrite /envs_split /of_envs=> ?; apply const_elim_sep_l=> Hwf.
+  destruct Δ as [Γp Γs], (env_split js _) as [[Γs1 Γs2]|] eqn:?; simplify_eq/=.
+  rewrite (env_split_perm Γs) // big_sep_app {1}always_sep_dup'.
+  destruct lr; simplify_eq/=; cancel [□ Π∧ Γp; □ Π∧ Γp; Π★ Γs1; Π★ Γs2]%I;
+    destruct Hwf; apply sep_intro_True_l; apply const_intro; constructor;
+      naive_solver eauto using env_split_wf_1, env_split_wf_2,
+      env_split_fresh_1, env_split_fresh_2.
+Qed.
+
+Lemma env_special_nil_persistent Δ : envs_persistent Δ = true → PersistentP Δ.
+Proof. intros; destruct Δ as [? []]; simplify_eq/=; apply _. Qed.
+Hint Immediate env_special_nil_persistent : typeclass_instances.
+
+(** * Adequacy *)
+Lemma tac_adequate P : Envs Enil Enil ⊢ P → True ⊢ P.
+Proof.
+  intros <-. rewrite /of_envs /= always_const !right_id.
+  apply const_intro; repeat constructor.
+Qed.
+
+(** * Basic rules *)
+Lemma tac_exact Δ i p P : envs_lookup i Δ = Some (p,P) → Δ ⊢ P.
+Proof. intros. by rewrite envs_lookup_sound' // sep_elim_l. Qed.
+
+Lemma tac_rename Δ Δ' i j p P Q :
+  envs_lookup i Δ = Some (p,P) →
+  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.
+Qed.
+Lemma tac_clear Δ Δ' i p P Q :
+  envs_lookup_delete i Δ = Some (p,P,Δ') → Δ' ⊢ Q → Δ ⊢ Q.
+Proof. intros. by rewrite envs_lookup_delete_sound // sep_elim_r. Qed.
+Lemma tac_clear_spatial Δ Δ1 Δ2 Q :
+  envs_split true [] Δ = Some (Δ1,Δ2) → Δ1 ⊢ Q → Δ ⊢ Q.
+Proof. intros. by rewrite envs_split_sound // sep_elim_l. Qed.
+
+Lemma tac_duplicate Δ Δ' i p j P Q :
+  envs_lookup i Δ = Some (p, P) →
+  p = true →
+  envs_simple_replace i true (Esnoc (Esnoc Enil i P) j P) Δ = Some Δ' →
+  Δ' ⊢ Q → Δ ⊢ Q.
+Proof.
+  intros ? -> ??. rewrite envs_simple_replace_sound //; simpl.
+  by rewrite right_id idemp wand_elim_r.
+Qed.
+
+(** * False *)
+Lemma tac_ex_falso Δ Q : Δ ⊢ False → Δ ⊢ Q.
+Proof. by rewrite -(False_elim Q). Qed.
+
+(** * Pure *)
+Lemma tac_pure_intro Δ (φ : Prop) : φ → Δ ⊢ ■ φ.
+Proof. apply const_intro. Qed.
+
+Class ToPure (P : uPred M) (φ : Prop) := to_pure : P ⊢ ■ φ.
+Arguments to_pure : clear implicits.
+Global Instance to_pure_const φ : ToPure (■ φ) φ.
+Proof. done. Qed.
+Global Instance to_pure_eq {A : cofeT} (a b : A) :
+  Timeless a → ToPure (a ≡ b) (a ≡ b).
+Proof. intros; red. by rewrite timeless_eq. Qed.
+Global Instance to_pure_valid `{CMRADiscrete A} (a : A) : ToPure (✓ a) (✓ a).
+Proof. intros; red. by rewrite discrete_valid. Qed.
+
+Lemma tac_pure Δ Δ' i p P φ Q :
+  envs_lookup_delete i Δ = Some (p, P, Δ') → ToPure P φ →
+  (φ → Δ' ⊢ Q) → Δ ⊢ Q.
+Proof.
+  intros ?? HQ. rewrite envs_lookup_delete_sound' //; simpl.
+  rewrite (to_pure P); by apply const_elim_sep_l.
+Qed.
+
+Lemma tac_pure_revert Δ φ Q : Δ ⊢ (■ φ → Q) → (φ → Δ ⊢ Q).
+Proof. intros HΔ ?. by rewrite HΔ const_equiv // left_id. Qed.
+
+(** * Later *)
+Class StripLaterEnv (Γ1 Γ2 : env (uPred M)) :=
+  strip_later_env : env_Forall2 StripLaterR Γ1 Γ2.
+Global Instance strip_later_env_nil : StripLaterEnv 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).
+Proof. by constructor. Qed.
+
+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)
+}.
+Global Instance strip_later_envs Γp1 Γp2 Γs1 Γs2 :
+  StripLaterEnv Γp1 Γp2 → StripLaterEnv Γs1 Γs2 →
+  StripLaterEnvs (Envs Γp1 Γs1) (Envs Γp2 Γs2).
+Proof. by split. Qed.
+Lemma strip_later_env_sound Δ1 Δ2 : StripLaterEnvs Δ1 Δ2 → Δ1 ⊢ ▷ Δ2.
+Proof.
+  intros [Hp Hs]; rewrite /of_envs /= !later_sep -always_later.
+  repeat apply sep_mono; try apply always_mono.
+  - rewrite -later_intro; apply const_mono; destruct 1; constructor;
+      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
+  - induction Hp; rewrite /= ?later_and; auto using and_mono, later_intro.
+  - induction Hs; rewrite /= ?later_sep; auto using sep_mono, later_intro.
+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.
+
+Lemma tac_löb Δ Δ' i Q :
+  envs_persistent Δ = true →
+  envs_app true (Esnoc Enil i (▷ Q)%I) Δ = Some Δ' →
+  Δ' ⊢ Q → Δ ⊢ Q.
+Proof.
+  intros ?? HQ. rewrite (persistentP Δ) envs_app_sound //; simpl.
+  rewrite right_id -{2}(always_elim Q) -(löb (□ Q)); apply impl_intro_l.
+  rewrite -always_later -{1}(always_always (â–¡ (â–· Q))) always_and_sep_l'.
+  by rewrite -always_sep wand_elim_r HQ.
+Qed.
+
+(** * Always *)
+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.
+Proof. done. Qed.
+Global Instance to_persistentP_persistent P :
+  PersistentP P → ToPersistentP P P | 100.
+Proof. done. Qed.
+
+Lemma tac_persistent Δ Δ' i p P P' Q :
+  envs_lookup i Δ = Some (p, P)%I → ToPersistentP P P' →
+  envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' →
+  Δ' ⊢ Q → Δ ⊢ Q.
+Proof.
+  intros ??? <-. rewrite envs_replace_sound //; simpl. destruct p.
+  - by rewrite right_id (to_persistentP P) always_always wand_elim_r.
+  - by rewrite right_id (to_persistentP P) wand_elim_r.
+Qed.
+
+(** * Implication and wand *)
+Lemma tac_impl_intro Δ Δ' i P Q :
+  envs_persistent Δ = true →
+  envs_app false (Esnoc Enil i P) Δ = Some Δ' →
+  Δ' ⊢ Q → Δ ⊢ (P → Q).
+Proof.
+  intros ?? HQ. rewrite (persistentP Δ) envs_app_sound //; simpl.
+  by rewrite right_id always_wand_impl always_elim HQ.
+Qed.
+Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
+  ToPersistentP 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.
+Qed.
+Lemma tac_impl_intro_pure Δ P φ Q : ToPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ (P → Q).
+Proof.
+  intros. by apply impl_intro_l; rewrite (to_pure P); apply const_elim_l.
+Qed.
+
+Lemma tac_wand_intro Δ Δ' i P Q :
+  envs_app false (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_persistent Δ Δ' i P P' Q :
+  ToPersistentP 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).
+Proof.
+  intros. by apply wand_intro_l; rewrite (to_pure P); apply const_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.
+Proof. done. Qed.
+Global Instance to_wand_impl P Q : ToWand (P → Q) P Q.
+Proof. apply impl_wand. Qed.
+Global Instance to_wand_iff_l P Q : ToWand (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.
+Proof. apply and_elim_r', impl_wand. 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)%I →
+  ToWand 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) Δ'
+             (* remove [i] and make [j] spatial *)
+  end = Some Δ'' →
+  Δ'' ⊢ Q → Δ ⊢ Q.
+Proof.
+  intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
+  - rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
+    destruct q.
+    + by rewrite assoc (to_wand R) always_wand wand_elim_r right_id wand_elim_r.
+    + by rewrite assoc (to_wand R) always_elim wand_elim_r right_id wand_elim_r.
+  - rewrite envs_lookup_sound //; simpl.
+    rewrite envs_lookup_sound // (envs_replace_sound' _ Δ'') //; simpl.
+    destruct q.
+    + by rewrite right_id assoc (to_wand R) always_elim wand_elim_r wand_elim_r.
+    + by rewrite assoc (to_wand R) wand_elim_r right_id wand_elim_r.
+Qed.
+
+Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js P1 P2 R Q :
+  envs_lookup_delete j Δ = Some (q, R, Δ')%I →
+  ToWand R P1 P2 →
+  ('(Δ1,Δ2) ← envs_split lr js Δ';
+    Δ2' ← envs_app (envs_persistent Δ1 && q) (Esnoc Enil j P2) Δ2;
+    Some (Δ1,Δ2')) = Some (Δ1,Δ2') → (* does not preserve position of [j] *)
+  Δ1 ⊢ P1 → Δ2' ⊢ Q → Δ ⊢ Q.
+Proof.
+  intros [? ->]%envs_lookup_delete_Some ?? HP1 <-.
+  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.
+  destruct q, (envs_persistent Δ1) eqn:?; simplify_eq/=.
+  - rewrite right_id (to_wand R) (persistentP Δ1) HP1.
+    by rewrite assoc -always_sep wand_elim_l wand_elim_r.
+  - by rewrite right_id (to_wand R) always_elim assoc HP1 wand_elim_l wand_elim_r.
+  - by rewrite right_id (to_wand R) assoc HP1 wand_elim_l wand_elim_r.
+  - by rewrite right_id (to_wand R) assoc HP1 wand_elim_l wand_elim_r. 
+Qed.
+
+Lemma tac_specialize_range_persistent Δ Δ' Δ'' j q P1 P2 R Q :
+  envs_lookup_delete j Δ = Some (q, R, Δ')%I →
+  ToWand R P1 P2 → PersistentP P1 →
+  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' →
+  Δ' ⊢ P1 → Δ'' ⊢ Q → Δ ⊢ Q.
+Proof.
+  intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
+  rewrite envs_lookup_sound //.
+  rewrite -(idemp uPred_and (envs_delete _ _ _)).
+  rewrite {1}HP1 (persistentP P1) always_and_sep_l assoc.
+  rewrite envs_simple_replace_sound' //; simpl. destruct q.
+  - by rewrite right_id (to_wand R) -always_sep wand_elim_l wand_elim_r.
+  - by rewrite right_id (to_wand R) always_elim wand_elim_l wand_elim_r.
+Qed.
+
+Lemma tac_specialize_domain_persistent Δ Δ' Δ'' j q P1 P2 P2' R Q :
+  envs_lookup_delete j Δ = Some (q, R, Δ')%I →
+  ToWand R P1 P2 → ToPersistentP P2 P2' →
+  envs_replace j q true (Esnoc Enil j P2') Δ = Some Δ'' →
+  Δ' ⊢ P1 → Δ'' ⊢ Q → Δ ⊢ Q.
+Proof.
+  intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
+  rewrite -(idemp uPred_and Δ) {1}envs_lookup_sound //; simpl; rewrite HP1.
+  rewrite envs_replace_sound //; simpl.
+  rewrite (sep_elim_r _ (_ -★ _)) right_id. destruct q.
+  - rewrite (to_wand R) always_elim wand_elim_l.
+    by rewrite (to_persistentP P2) always_and_sep_l' wand_elim_r.
+  - rewrite (to_wand R) wand_elim_l.
+    by rewrite (to_persistentP P2) always_and_sep_l' wand_elim_r.
+Qed.
+
+Lemma tac_revert Δ Δ' i p P Q :
+  envs_lookup_delete i Δ = Some (p,P,Δ') →
+  Δ' ⊢ (if p then □ P → Q else P -★ Q) → Δ ⊢ Q.
+Proof.
+  intros ? HQ. rewrite envs_lookup_delete_sound //; simpl. destruct p.
+  - by rewrite HQ -always_and_sep_l impl_elim_r.
+  - by rewrite HQ wand_elim_r.
+Qed.
+
+Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P Q :
+  envs_split lr js Δ = Some (Δ1,Δ2) →
+  envs_app (envs_persistent Δ1) (Esnoc Enil j P) Δ2 = Some Δ2' →
+  Δ1 ⊢ P → Δ2' ⊢ Q → Δ ⊢ Q.
+Proof.
+  intros ?? HP ?. rewrite envs_split_sound //.
+  destruct (envs_persistent Δ1) eqn:?.
+  - rewrite (persistentP Δ1) HP envs_app_sound //; simpl.
+    by rewrite right_id wand_elim_r.
+  - rewrite HP envs_app_sound //; simpl. by rewrite right_id wand_elim_r.
+Qed.
+
+Lemma tac_assert_persistent Δ Δ' j P Q :
+  PersistentP P →
+  envs_app true (Esnoc Enil j P) Δ = Some Δ' →
+  Δ ⊢ P → Δ' ⊢ Q → Δ ⊢ Q.
+Proof.
+  intros ?? HP ?.
+  rewrite -(idemp uPred_and Δ) {1}HP envs_app_sound //; simpl.
+  by rewrite right_id {1}(persistentP P) always_and_sep_l wand_elim_r.
+Qed.
+
+Lemma tac_pose_proof Δ Δ' j P Q :
+  True ⊢ P → envs_app true (Esnoc Enil j P) Δ = Some Δ' →
+  Δ' ⊢ Q → Δ ⊢ Q.
+Proof.
+  intros HP ? <-. rewrite envs_app_sound //; simpl.
+  by rewrite -HP left_id always_const wand_True.
+Qed.
+
+Lemma tac_apply Δ Δ' i p R P1 P2 :
+  envs_lookup_delete i Δ = Some (p, R, Δ')%I → ToWand R P1 P2 →
+  Δ' ⊢ P1 → Δ ⊢ P2.
+Proof.
+  intros ?? HP1. rewrite envs_lookup_delete_sound' //.
+  by rewrite (to_wand R) HP1 wand_elim_l.
+Qed.
+
+(** * Rewriting *)
+Lemma tac_rewrite Δ i p Pxy (lr : bool) Q :
+  envs_lookup i Δ = Some (p, Pxy) →
+  ∀ {A : cofeT} x y (Φ : A → uPred M),
+    Pxy ⊢ (x ≡ y)%I →
+    Q ⊣⊢ Φ (if lr then y else x) →
+    (∀ n, Proper (dist n ==> dist n) Φ) →
+    Δ ⊢ Φ (if lr then x else y) → Δ ⊢ Q.
+Proof.
+  intros ? A x y ? HPxy -> ?; apply eq_rewrite; auto.
+  rewrite {1}envs_lookup_sound' //; rewrite sep_elim_l HPxy.
+  destruct lr; auto using eq_sym.
+Qed.
+
+Lemma tac_rewrite_in Δ i p Pxy j q P (lr : bool) Q :
+  envs_lookup i Δ = Some (p, Pxy) →
+  envs_lookup j Δ = Some (q, P)%I →
+  ∀ {A : cofeT} Δ' x y (Φ : A → uPred M),
+    Pxy ⊢ (x ≡ y)%I →
+    P ⊣⊢ Φ (if lr then y else x) →
+    (∀ n, Proper (dist n ==> dist n) Φ) →
+    envs_simple_replace j q (Esnoc Enil j (Φ (if lr then x else y))) Δ = Some Δ' →
+    Δ' ⊢ Q → Δ ⊢ Q.
+Proof.
+  intros ?? A Δ' x y Φ HPxy HP ?? <-.
+  rewrite -(idemp uPred_and Δ) {2}(envs_lookup_sound' _ i) //.
+  rewrite sep_elim_l HPxy always_and_sep_r.
+  rewrite (envs_simple_replace_sound _ _ j) //; simpl. destruct q.
+  - rewrite HP right_id -assoc; apply wand_elim_r'. destruct lr.
+    + apply (eq_rewrite x y (λ y, □ Φ y -★ Δ')%I); eauto with I. solve_proper.
+    + apply (eq_rewrite y x (λ y, □ Φ y -★ Δ')%I); eauto using eq_sym with I.
+      solve_proper.
+  - rewrite HP right_id -assoc; apply wand_elim_r'. destruct lr.
+    + apply (eq_rewrite x y (λ y, Φ y -★ Δ')%I); eauto with I. solve_proper.
+    + apply (eq_rewrite y x (λ y, Φ y -★ Δ')%I); eauto using eq_sym with I.
+      solve_proper.
+Qed.
+
+(** * Conjunction splitting *)
+Class AndSplit (P Q1 Q2 : uPred M) := and_split : (Q1 ∧ Q2) ⊢ P.
+Arguments and_split : clear implicits.
+
+Global Instance and_split_and P1 P2 : AndSplit (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.
+
+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.
+
+(** * Separating conjunction splitting *)
+Class SepSplit (P Q1 Q2 : uPred M) := sep_split : (Q1 ★ Q2) ⊢ P.
+Arguments sep_split : clear implicits.
+
+Global Instance sep_split_sep P1 P2 : SepSplit (P1 ★ P2) P1 P2 | 100.
+Proof. done. 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.
+
+Lemma tac_sep_split Δ Δ1 Δ2 lr js P Q1 Q2 :
+  SepSplit 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.
+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 →
+  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.
+Proof.
+  intros [? ->]%envs_lookup_delete_Some [? ->]%envs_lookup_delete_Some ?? <-.
+  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.
+    + rewrite envs_lookup_sound // envs_app_sound //; simpl.
+      by rewrite right_id assoc always_elim (sep_split 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.
+    + rewrite envs_lookup_sound // envs_app_sound //; simpl.
+      by rewrite right_id assoc (sep_split P) wand_elim_r.
+Qed.
+
+(** * Conjunction/separating conjunction elimination *)
+Class SepDestruct (p : bool) (P Q1 Q2 : uPred M) :=
+  sep_destruct : if p then □ P ⊢ □ (Q1 ∧ Q2) else P ⊢ (Q1 ★ Q2).
+Arguments sep_destruct : clear implicits.
+Lemma sep_destruct_spatial p P Q1 Q2 : P ⊢ (Q1 ★ Q2) → SepDestruct p P Q1 Q2.
+Proof. destruct p; simpl=>->; by rewrite ?sep_and. Qed.
+
+Global Instance sep_destruct_sep p P Q : SepDestruct p (P ★ Q) P Q.
+Proof. by apply sep_destruct_spatial. Qed.
+Global Instance sep_destruct_ownM p (a b : M) :
+  SepDestruct p (uPred_ownM (a â‹… b)) (uPred_ownM a) (uPred_ownM b).
+Proof. apply sep_destruct_spatial. by rewrite ownM_op. Qed.
+
+Global Instance sep_destruct_and P Q : SepDestruct true (P ∧ Q) P Q.
+Proof. done. Qed.
+Global Instance sep_destruct_and_persistent_l P Q :
+  PersistentP P → SepDestruct false (P ∧ Q) P Q.
+Proof. intros; red. by rewrite always_and_sep_l. Qed.
+Global Instance sep_destruct_and_persistent_r P Q :
+  PersistentP Q → SepDestruct false (P ∧ Q) P Q.
+Proof. intros; red. by rewrite 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.
+  destruct p=> /= HP.
+  - by rewrite -later_and !always_later HP.
+  - by rewrite -later_sep HP.
+Qed.
+
+Lemma tac_sep_destruct Δ Δ' i p j1 j2 P P1 P2 Q :
+  envs_lookup i Δ = Some (p, P)%I → SepDestruct 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. destruct p.
+  - by rewrite (sep_destruct true P) right_id (comm uPred_and) wand_elim_r.
+  - by rewrite (sep_destruct false P) right_id (comm uPred_sep P1) wand_elim_r.
+Qed.
+
+(** * Framing *)
+Class Frame (R P Q : uPred M) := frame : (R ★ Q) ⊢ P.
+Arguments frame : clear implicits.
+
+Global Instance frame_here R : Frame R R True | 1.
+Proof. by rewrite /Frame right_id. Qed.
+Global Instance frame_here_l R P : Frame R (R ★ P) P | 0.
+Proof. done. Qed.
+Global Instance frame_here_r R P : Frame R (P ★ R) P | 0.
+Proof. by rewrite /Frame comm. Qed.
+Global Instance frame_here_and_l R P : Frame R (R ∧ P) P | 0.
+Proof. by rewrite /Frame sep_and. Qed.
+Global Instance frame_here_and_r R P : Frame R (P ∧ R) P | 0.
+Proof. by rewrite /Frame sep_and comm. Qed.
+Global Instance frame_sep_l R P1 P2 Q :
+  Frame R P1 Q → Frame R (P1 ★ P2) (Q ★ P2).
+Proof. rewrite /Frame => <-. solve_sep_entails. Qed.
+Global Instance frame_sep_r R P1 P2 Q :
+  Frame R P2 Q → Frame R (P1 ★ P2) (P1 ★ Q).
+Proof. rewrite /Frame => <-. solve_sep_entails. Qed.
+Global Instance frame_or R P1 P2 Q1 Q2 :
+  Frame R P1 Q1 → Frame R P2 Q2 → Frame R (P1 ∨ P2) (Q1 ∨ Q2).
+Proof. rewrite /Frame=> <- <-. by rewrite -sep_or_l. Qed.
+Global Instance frame_exist {A} R (Φ Ψ : A → uPred M) :
+  (∀ a, Frame R (Φ a) (Ψ a)) → Frame R (∃ x, Φ x) (∃ x, Ψ x).
+Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
+Global Instance frame_forall {A} R (Φ Ψ : A → uPred M) :
+  (∀ a, Frame R (Φ a) (Ψ a)) → Frame R (∀ x, Φ x) (∀ x, Ψ x).
+Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
+
+Lemma tac_frame Δ Δ' i p R P Q :
+  envs_lookup_delete i Δ = Some (p, R, Δ')%I → Frame R P Q →
+  (if p then Δ else Δ') ⊢ Q → Δ ⊢ P.
+Proof.
+  intros [? ->]%envs_lookup_delete_Some ? HQ; destruct p.
+  - by rewrite envs_lookup_persistent_sound // HQ always_elim.
+  - rewrite envs_lookup_sound //; simpl. by rewrite HQ.
+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.
+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.
+
+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.
+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.
+
+Lemma tac_or_destruct Δ Δ1 Δ2 i p j1 j2 P P1 P2 Q :
+  envs_lookup i Δ = Some (p, P)%I → OrDestruct 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 //. destruct p.
+  - rewrite (or_destruct P) always_or sep_or_r; apply or_elim. simpl.
+    + 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 (or_destruct P) 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.
+Qed.
+
+(** * Forall *)
+Lemma tac_forall_intro {A} Δ (Φ : A → uPred M) : (∀ a, Δ ⊢ Φ a) → Δ ⊢ (∀ a, Φ a).
+Proof. apply forall_intro. Qed.
+
+Lemma tac_forall_specialize {A} Δ Δ' i p (Φ : A → uPred M) Q a :
+  envs_lookup i Δ = Some (p, ∀ a, Φ a)%I →
+  envs_simple_replace i p (Esnoc Enil i (Φ a)) Δ = Some Δ' →
+  Δ' ⊢ Q → Δ ⊢ Q.
+Proof.
+  intros. rewrite envs_simple_replace_sound //; simpl.
+  destruct p; by rewrite /= right_id (forall_elim a) wand_elim_r.
+Qed.
+
+Lemma tac_forall_revert {A} Δ (Φ : A → uPred M) :
+  Δ ⊢ (∀ a, Φ a) → (∀ a, Δ ⊢ Φ a).
+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) Φ.
+Proof. done. Qed.
+
+Lemma tac_exist {A} Δ P (Φ : A → uPred M) a : ExistSplit P Φ → Δ ⊢ Φ a → Δ ⊢ P.
+Proof. intros. 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) Φ.
+Proof. done. Qed.
+Global Instance exist_destruct_later {A} P (Φ : A → uPred M) :
+  Inhabited A → ExistDestruct P Φ → ExistDestruct (▷ P) (λ a, ▷ (Φ a))%I.
+Proof. rewrite /ExistDestruct=> ? ->. by rewrite later_exist. Qed.
+
+Lemma tac_exist_destruct {A} Δ i p j P (Φ : A → uPred M) Q :
+  envs_lookup i Δ = Some (p, P)%I → ExistDestruct P Φ →
+  (∀ a, ∃ Δ',
+    envs_simple_replace i p (Esnoc Enil j (Φ a)) Δ = Some Δ' ∧ Δ' ⊢ Q) →
+  Δ ⊢ Q.
+Proof.
+  intros ?? HΦ. rewrite envs_lookup_sound //. destruct p.
+  - rewrite (exist_destruct P) always_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 (exist_destruct P) 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.
diff --git a/proofmode/environments.v b/proofmode/environments.v
new file mode 100644
index 0000000000000000000000000000000000000000..356e1fbba9c1d8361b0f0d4806c75461bebd1ec5
--- /dev/null
+++ b/proofmode/environments.v
@@ -0,0 +1,201 @@
+From iris.prelude Require Export strings.
+From iris.algebra Require Export base.
+From iris.prelude Require Import stringmap.
+
+Inductive env (A : Type) : Type :=
+  | Enil : env A
+  | Esnoc : env A → string → A → env A.
+Arguments Enil {_}.
+Arguments Esnoc {_} _ _%string _.
+
+Local Notation "x ← y ; z" := (match y with Some x => z | None => None end).
+Local Notation "' ( x1 , x2 ) ← y ; z" :=
+  (match y with Some (x1,x2) => z | None => None end).
+Local Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
+  (match y with Some (x1,x2,x3) => z | None => None end).
+
+Fixpoint env_lookup {A} (i : string) (Γ : env A) : option A :=
+  match Γ with
+  | Enil => None
+  | Esnoc Γ j x => if decide (i = j) then Some x else env_lookup i Γ
+  end.
+Local Notation "Γ !! j" := (env_lookup j Γ).
+
+Inductive env_wf {A} : env A → Prop :=
+  | Enil_wf : env_wf Enil
+  | Esnoc_wf Γ i x : Γ !! i = None → env_wf Γ → env_wf (Esnoc Γ i x).
+
+Fixpoint env_to_list {A} (E : env A) : list A :=
+  match E with Enil => [] | Esnoc Γ _ x => x :: env_to_list Γ end.
+Coercion env_to_list : env >-> list.
+Instance env_dom {A} : Dom (env A) stringset :=
+  fix go Γ := let _ : Dom _ _ := @go in
+  match Γ with Enil => ∅ | Esnoc Γ i _ => {[ i ]} ∪ dom stringset Γ end.
+
+Fixpoint env_app {A} (Γapp : env A) (Γ : env A) : option (env A) :=
+  match Γapp with
+  | Enil => Some Γ
+  | Esnoc Γapp i x =>
+     Γ' ← env_app Γapp Γ; 
+     match Γ' !! i with None => Some (Esnoc Γ' i x) | Some _ => None end
+  end.
+Fixpoint env_replace {A} (i: string) (Γi: env A) (Γ: env A) : option (env A) :=
+  match Γ with
+  | Enil => None
+  | Esnoc Γ j x =>
+     if decide (i = j) then env_app Γi Γ else
+     match Γi !! j with
+     | None => Γ' ← env_replace i Γi Γ; Some (Esnoc Γ' j x)
+     | Some _ => None
+     end
+  end.
+Fixpoint env_delete {A} (i : string) (Γ : env A) : env A :=
+  match Γ with
+  | Enil => Enil
+  | Esnoc Γ j x => if decide (i = j) then Γ else Esnoc (env_delete i Γ) j x
+  end.
+Fixpoint env_lookup_delete {A} (i : string) (Γ : env A) : option (A * env A) :=
+  match Γ with
+  | Enil => None
+  | Esnoc Γ j x =>
+     if decide (i = j) then Some (x,Γ)
+     else '(y,Γ') ← env_lookup_delete i Γ; Some (y, Esnoc Γ' j x)
+  end.
+Fixpoint env_split_go {A} (js : list string)
+    (Γ1 Γ2 : env A) : option (env A * env A) :=
+  match js with
+  | [] => Some (Γ1, Γ2)
+  | j::js => '(x,Γ2) ← env_lookup_delete j Γ2; env_split_go js (Esnoc Γ1 j x) Γ2
+  end.
+Definition env_split {A} (js : list string)
+  (Γ : env A) : option (env A * env A) := env_split_go js Enil Γ.
+
+Inductive env_Forall2 {A B} (P : A → B → Prop) : env A → env B → Prop :=
+  | env_Forall2_nil : env_Forall2 P Enil Enil
+  | env_Forall2_snoc Γ1 Γ2 i x y :
+     env_Forall2 P Γ1 Γ2 → P x y → env_Forall2 P (Esnoc Γ1 i x) (Esnoc Γ2 i y).
+
+Section env.
+Context {A : Type}.
+Implicit Types Γ : env A.
+Implicit Types i : string.
+Implicit Types x : A.
+Hint Resolve Esnoc_wf Enil_wf.
+
+Ltac simplify := repeat (case_match || simplify_option_eq).
+
+Lemma env_lookup_perm Γ i x : Γ !! i = Some x → Γ ≡ₚ x :: env_delete i Γ.
+Proof.
+  induction Γ; intros; simplify; rewrite 1?Permutation_swap; f_equiv; eauto.
+Qed.
+
+Lemma env_app_perm Γ Γapp Γ' :
+  env_app Γapp Γ = Some Γ' → env_to_list Γ' ≡ₚ Γapp ++ Γ.
+Proof. revert Γ'; induction Γapp; intros; simplify; f_equal; auto. Qed.
+Lemma env_app_fresh Γ Γapp Γ' i :
+  env_app Γapp Γ = Some Γ' → Γapp !! i = None → Γ !! i = None → Γ' !! i = None.
+Proof. revert Γ'. induction Γapp; intros; simplify; eauto. Qed.
+Lemma env_app_fresh_1 Γ Γapp Γ' i x :
+  env_app Γapp Γ = Some Γ' → Γ' !! i = None → Γ !! i = None.
+Proof. revert Γ'. induction Γapp; intros; simplify; eauto. Qed.
+Lemma env_app_disjoint Γ Γapp Γ' i :
+  env_app Γapp Γ = Some Γ' → Γapp !! i = None ∨ Γ !! i = None.
+Proof.
+  revert Γ'.
+  induction Γapp; intros; simplify; naive_solver eauto using env_app_fresh_1.
+Qed.
+Lemma env_app_wf Γ Γapp Γ' : env_app Γapp Γ = Some Γ' → env_wf Γ → env_wf Γ'.
+Proof. revert Γ'. induction Γapp; intros; simplify; eauto. Qed.
+
+Lemma env_replace_fresh Γ Γj Γ' i j :
+  env_replace j Γj Γ = Some Γ' →
+  Γj !! i = None → env_delete j Γ !! i = None → Γ' !! i = None.
+Proof. revert Γ'. induction Γ; intros; simplify; eauto using env_app_fresh. Qed.
+Lemma env_replace_wf Γ Γi Γ' i :
+  env_replace i Γi Γ = Some Γ' → env_wf (env_delete i Γ) → env_wf Γ'.
+Proof.
+  revert Γ'. induction Γ; intros ??; simplify; [|inversion_clear 1];
+    eauto using env_app_wf, env_replace_fresh.
+Qed.
+Lemma env_replace_lookup Γ Γi Γ' i :
+  env_replace i Γi Γ = Some Γ' → is_Some (Γ !! i).
+Proof. revert Γ'. induction Γ; intros; simplify; eauto. Qed.
+Lemma env_replace_perm Γ Γi Γ' i :
+  env_replace i Γi Γ = Some Γ' → Γ' ≡ₚ Γi ++ env_delete i Γ.
+Proof.
+  revert Γ'. induction Γ as [|Γ IH j y]=>Γ' ?; simplify_eq/=.
+  destruct (decide (i = j)); simplify_eq/=; auto using env_app_perm.
+  destruct (Γi !! j), (env_replace i Γi Γ) as [Γ''|] eqn:?; simplify_eq/=.
+  rewrite -Permutation_middle; f_equiv; eauto.
+Qed.
+
+Lemma env_lookup_delete_correct Γ i :
+  env_lookup_delete i Γ = x ← Γ !! i; Some (x,env_delete i Γ).
+Proof. induction Γ; intros; simplify; eauto. Qed.
+Lemma env_lookup_delete_Some Γ Γ' i x :
+  env_lookup_delete i Γ = Some (x,Γ') ↔ Γ !! i = Some x ∧ Γ' = env_delete i Γ.
+Proof. rewrite env_lookup_delete_correct; simplify; naive_solver. Qed.
+Lemma env_delete_fresh_eq Γ j : env_wf Γ → env_delete j Γ !! j = None.
+Proof. induction 1; intros; simplify; eauto. Qed.
+Lemma env_delete_fresh Γ i j : Γ !! i = None → env_delete j Γ !! i = None.
+Proof. induction Γ; intros; simplify; eauto. Qed.
+Lemma env_delete_wf Γ j : env_wf Γ → env_wf (env_delete j Γ).
+Proof. induction 1; simplify; eauto using env_delete_fresh. Qed.
+
+Lemma env_split_fresh Γ1 Γ2 Γ1' Γ2' js i :
+  env_split_go js Γ1 Γ2 = Some (Γ1',Γ2') →
+  Γ1 !! i = None → Γ2 !! i = None → Γ1' !! i = None ∧ Γ2' !! i = None.
+Proof.
+  revert Γ1 Γ2.
+  induction js as [|j js IH]=> Γ1 Γ2 ???; simplify_eq/=; eauto.
+  destruct (env_lookup_delete j Γ2) as [[x Γ2'']|] eqn:Hdelete; simplify_eq/=.
+  apply env_lookup_delete_Some in Hdelete as [? ->].
+  eapply IH; eauto; simplify; eauto using env_delete_fresh.
+Qed.
+Lemma env_split_go_wf Γ1 Γ2 Γ1' Γ2' js :
+  env_split_go js Γ1 Γ2 = Some (Γ1',Γ2') →
+  (∀ i, Γ1 !! i = None ∨ Γ2 !! i = None) →
+  env_wf Γ1 → env_wf Γ2 → env_wf Γ1' ∧ env_wf Γ2'.
+Proof.
+  revert Γ1 Γ2.
+  induction js as [|j js IH]=> Γ1 Γ2 ? Hdisjoint ??; simplify_eq/=; auto.
+  destruct (env_lookup_delete j Γ2) as [[x Γ2'']|] eqn:Hdelete; simplify_eq/=.
+  apply env_lookup_delete_Some in Hdelete as [? ->].
+  eapply IH; eauto using env_delete_wf.
+  - intros i; simplify; eauto using env_delete_fresh_eq.
+    destruct (Hdisjoint i); eauto using env_delete_fresh.  
+  - constructor; auto.
+    destruct (Hdisjoint j) as [?|[]%eq_None_not_Some]; eauto.
+Qed.
+Lemma env_split_go_perm Γ1 Γ2 Γ1' Γ2' js :
+  env_split_go js Γ1 Γ2 = Some (Γ1',Γ2') → Γ1 ++ Γ2 ≡ₚ Γ1' ++ Γ2'.
+Proof.
+  revert Γ1 Γ2. induction js as [|j js IH]=> Γ1 Γ2 ?; simplify_eq/=; auto.
+  destruct (env_lookup_delete j Γ2) as [[x Γ2'']|] eqn:Hdelete; simplify_eq/=.
+  apply env_lookup_delete_Some in Hdelete as [? ->].
+  by rewrite -(IH (Esnoc _ _ _) (env_delete _ _)) //=
+    Permutation_middle -env_lookup_perm.
+Qed.
+
+Lemma env_split_fresh_1 Γ Γ1 Γ2 js i :
+  env_split js Γ = Some (Γ1,Γ2) → Γ !! i = None → Γ1 !! i = None.
+Proof. intros. by apply (env_split_fresh Enil Γ Γ1 Γ2 js). Qed.
+Lemma env_split_fresh_2 Γ Γ1 Γ2 js i :
+  env_split js Γ = Some (Γ1,Γ2) → Γ !! i = None → Γ2 !! i = None.
+Proof. intros. by apply (env_split_fresh Enil Γ Γ1 Γ2 js). Qed.
+Lemma env_split_wf_1 Γ Γ1 Γ2 js :
+  env_split js Γ = Some (Γ1,Γ2) → env_wf Γ → env_wf Γ1.
+Proof. intros. apply (env_split_go_wf Enil Γ Γ1 Γ2 js); eauto. Qed.
+Lemma env_split_wf_2 Γ Γ1 Γ2 js :
+  env_split js Γ = Some (Γ1,Γ2) → env_wf Γ → env_wf Γ2.
+Proof. intros. apply (env_split_go_wf Enil Γ Γ1 Γ2 js); eauto. Qed.
+Lemma env_split_perm Γ Γ1 Γ2 js : env_split js Γ = Some (Γ1,Γ2) → Γ ≡ₚ Γ1 ++ Γ2.
+Proof. apply env_split_go_perm. Qed.
+
+Lemma env_Forall2_fresh {B} (P : A → B → Prop) Γ Σ i :
+  env_Forall2 P Γ Σ → Γ !! i = None → Σ !! i = None.
+Proof. by induction 1; simplify. Qed.
+Lemma env_Forall2_wf {B} (P : A → B → Prop) Γ Σ :
+  env_Forall2 P Γ Σ → env_wf Γ → env_wf Σ.
+Proof. induction 1; inversion_clear 1; eauto using env_Forall2_fresh. Qed.
+End env.
diff --git a/proofmode/ghost_ownership.v b/proofmode/ghost_ownership.v
new file mode 100644
index 0000000000000000000000000000000000000000..496b63049a51471eb990d07d3cdb43c2f034767a
--- /dev/null
+++ b/proofmode/ghost_ownership.v
@@ -0,0 +1,15 @@
+From iris.proofmode Require Import coq_tactics.
+From iris.proofmode Require Export tactics.
+From iris.program_logic Require Export ghost_ownership.
+
+Section ghost.
+Context `{inG Λ Σ A}.
+Implicit Types a b : A.
+
+Global Instance sep_destruct_own p γ a b :
+  SepDestruct p (own γ (a ⋅ b)) (own γ a) (own γ b).
+Proof. apply sep_destruct_spatial. 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.
+End ghost.
diff --git a/proofmode/intro_patterns.v b/proofmode/intro_patterns.v
new file mode 100644
index 0000000000000000000000000000000000000000..8abdc219b243a8dc3353314b35d4fb9ae62a9c84
--- /dev/null
+++ b/proofmode/intro_patterns.v
@@ -0,0 +1,132 @@
+From iris.prelude Require Export strings.
+
+Inductive intro_pat :=
+  | IName : string → intro_pat
+  | IAnom : intro_pat
+  | IAnomPure : intro_pat
+  | IClear : intro_pat
+  | IPersistent : intro_pat → intro_pat
+  | IList : list (list intro_pat) → intro_pat
+  | ISimpl : intro_pat
+  | IAlways : intro_pat.
+
+Module intro_pat.
+Inductive token :=
+  | TName : string → token
+  | TAnom : token
+  | TAnomPure : token
+  | TClear : token
+  | TPersistent : token
+  | TBar : token
+  | TBracketL : token
+  | TBracketR : token
+  | TAmp : token
+  | TParenL : token
+  | TParenR : token
+  | TSimpl : token
+  | TAlways : token.
+
+Fixpoint cons_name (kn : string) (k : list token) : list token :=
+  match kn with "" => k | _ => TName (string_rev kn) :: k end.
+Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
+  match s with
+  | "" => rev (cons_name kn k)
+  | String " " s => tokenize_go s (cons_name kn k) ""
+  | String "?" s => tokenize_go s (TAnom :: cons_name kn k) ""
+  | String "%" s => tokenize_go s (TAnomPure :: cons_name kn k) ""
+  | String "_" s => tokenize_go s (TClear :: cons_name kn k) ""
+  | String "#" s => tokenize_go s (TPersistent :: cons_name kn k) ""
+  | String "[" s => tokenize_go s (TBracketL :: cons_name kn k) ""
+  | String "]" s => tokenize_go s (TBracketR :: cons_name kn k) ""
+  | String "|" s => tokenize_go s (TBar :: cons_name kn k) ""
+  | String "(" s => tokenize_go s (TParenL :: cons_name kn k) ""
+  | String ")" s => tokenize_go s (TParenR :: cons_name kn k) ""
+  | String "&" s => tokenize_go s (TAmp :: cons_name kn k) ""
+  | String "!" s => tokenize_go s (TAlways :: cons_name kn k) ""
+  | String "/" (String "=" s) => tokenize_go s (TSimpl :: cons_name kn k) ""
+  | String a s => tokenize_go s k (String a kn)
+  end.
+Definition tokenize (s : string) : list token := tokenize_go s [] "".
+
+Inductive stack_item :=
+  | SPat : intro_pat → stack_item
+  | SPersistent : stack_item
+  | SList : stack_item
+  | SConjList : stack_item
+  | SBar : stack_item
+  | SAmp : stack_item.
+Notation stack := (list stack_item).
+
+Fixpoint close_list (k : stack)
+    (ps : list intro_pat) (pss : list (list intro_pat)) : option stack :=
+  match k with
+  | [] => None
+  | SList :: k => Some (SPat (IList (ps :: pss)) :: k)
+  | SPat pat :: k => close_list k (pat :: ps) pss
+  | SPersistent :: k =>
+     '(p,ps) ← maybe2 (::) ps; close_list k (IPersistent p :: ps) pss
+  | SBar :: k => close_list k [] (ps :: pss)
+  | (SAmp | SConjList) :: _ => None
+  end.
+
+Fixpoint big_conj (ps : list intro_pat) : intro_pat :=
+  match ps with
+  | [] => IList [[]]
+  | [p] => IList [[ p ]]
+  | [p1;p2] => IList [[ p1 ; p2 ]]
+  | p :: ps => IList [[ p ; big_conj ps ]]
+  end.
+
+Fixpoint close_conj_list (k : stack)
+    (cur : option intro_pat) (ps : list intro_pat) : option stack :=
+  match k with
+  | [] => None
+  | SConjList :: k =>
+     ps ← match cur with
+          | None => guard (ps = []); Some [] | Some p => Some (p :: ps)
+          end;
+     Some (SPat (big_conj ps) :: k)
+  | SPat pat :: k => guard (cur = None); close_conj_list k (Some pat) ps
+  | SPersistent :: k => p ← cur; close_conj_list k (Some (IPersistent p)) ps
+  | SAmp :: k => p ← cur; close_conj_list k None (p :: ps)
+  | (SBar | SList) :: _ => None
+  end.
+
+Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
+  match ts with
+  | [] => Some k
+  | TName s :: ts => parse_go ts (SPat (IName s) :: k)
+  | TAnom :: ts => parse_go ts (SPat IAnom :: k)
+  | TAnomPure :: ts => parse_go ts (SPat IAnomPure :: k)
+  | TClear :: ts => parse_go ts (SPat IClear :: k)
+  | TPersistent :: ts => parse_go ts (SPersistent :: k)
+  | TBracketL :: ts => parse_go ts (SList :: k)
+  | TBar :: ts => parse_go ts (SBar :: k)
+  | TBracketR :: ts => close_list k [] [] ≫= parse_go ts
+  | TParenL :: ts => parse_go ts (SConjList :: k)
+  | TAmp :: ts => parse_go ts (SAmp :: k)
+  | TParenR :: ts => close_conj_list k None [] ≫= parse_go ts
+  | TSimpl :: ts => parse_go ts (SPat ISimpl :: k)
+  | TAlways :: ts => parse_go ts (SPat IAlways :: k)
+  end.
+Definition parse (s : string) : option (list intro_pat) :=
+  match k ← parse_go (tokenize s) [SList]; close_list k [] [] with
+  | Some [SPat (IList [ps])] => Some ps
+  | _ => None
+  end.
+
+Ltac parse s :=
+  lazymatch type of s with
+  | list intro_pat => s
+  | string => lazymatch eval vm_compute in (parse s) with
+              | Some ?pats => pats | _ => fail "invalid list intro_pat" s
+              end
+  end.
+Ltac parse_one s :=
+  lazymatch type of s with
+  | intro_pat => s
+  | string => lazymatch eval vm_compute in (parse s) with
+              | Some [?pat] => pat | _ => fail "invalid intro_pat" s
+              end
+  end.
+End intro_pat.
diff --git a/proofmode/invariants.v b/proofmode/invariants.v
new file mode 100644
index 0000000000000000000000000000000000000000..d2161d80e68c22181c3fd6d77f2332c4df7ca698
--- /dev/null
+++ b/proofmode/invariants.v
@@ -0,0 +1,55 @@
+From iris.proofmode Require Import coq_tactics.
+From iris.proofmode Require Export pviewshifts.
+From iris.program_logic Require Export invariants.
+Import uPred.
+
+Section invariants.
+Context {Λ : language} {Σ : iFunctor}.
+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 Φ →
+  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). eapply (inv_fsa fsa); eauto.
+  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 Φ →
+  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).
+  eapply (inv_fsa_timeless fsa); eauto.
+  rewrite envs_app_sound //; simpl. by rewrite right_id HΔ'.
+Qed.
+End invariants.
+
+Tactic Notation "iInv" constr(N) "as" constr(pat) :=
+  let H := iFresh in
+  eapply tac_inv_fsa with _ _ _ _ N H _ _;
+    [let P := match goal with |- FSASplit ?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 *)
+    |iAssumption || fail "iInv: invariant" N "not found"
+    |env_cbv; reflexivity
+    |simpl (* get rid of FSAs *); iDestruct H as pat].
+
+Tactic Notation "iInv>" constr(N) "as" constr(pat) :=
+  let H := iFresh in
+  eapply tac_inv_fsa_timeless with _ _ _ _ N H _ _;
+    [let P := match goal with |- FSASplit ?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 *)
+    |iAssumption || fail "iOpenInv: invariant" N "not found"
+    |let P := match goal with |- TimelessP ?P => P end in
+     apply _ || fail "iInv:" P "not timeless"
+    |env_cbv; reflexivity
+    |simpl (* get rid of FSAs *); iDestruct H as pat].
diff --git a/proofmode/notation.v b/proofmode/notation.v
new file mode 100644
index 0000000000000000000000000000000000000000..028ea31d4916144611735dbbedbf3940d2aae64f
--- /dev/null
+++ b/proofmode/notation.v
@@ -0,0 +1,27 @@
+From iris.proofmode Require Import coq_tactics environments.
+From iris.prelude Require Export strings.
+
+Delimit Scope proof_scope with env.
+Arguments Envs _ _%proof_scope _%proof_scope.
+Arguments Enil {_}.
+Arguments Esnoc {_} _%proof_scope _%string _%uPred_scope.
+
+Notation "​" := Enil (format "​") : proof_scope.
+Notation "​ Γ H : P" := (Esnoc Γ H P)
+  (at level 1, P at level 200,
+   left associativity, format "​ Γ H  :  P '//'") : proof_scope.
+Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ★ Q" :=
+  (of_envs (Envs Γ Δ) ⊢ Q%I)
+  (at level 1, Q at level 200, left associativity,
+  format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ★ '//' Q '//'") :
+  C_scope.
+Notation "Δ '--------------------------------------' ★ Q" :=
+  (of_envs (Envs Enil Δ) ⊢ Q%I)
+  (at level 1, Q at level 200, left associativity,
+  format "Δ '--------------------------------------' ★ '//' Q '//'") : C_scope.
+Notation "Γ '--------------------------------------' □ Q" :=
+  (of_envs (Envs Γ Enil) ⊢ Q%I)
+  (at level 1, Q at level 200, left associativity,
+  format "Γ '--------------------------------------' □ '//' Q '//'")  : C_scope.
+Notation "​​ Q" := (of_envs (Envs Enil Enil) ⊢ Q%I)
+  (at level 1, format "​​ Q") : C_scope.
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
new file mode 100644
index 0000000000000000000000000000000000000000..54968aebec050d4337fd8afddfb241acaf8df3fa
--- /dev/null
+++ b/proofmode/pviewshifts.v
@@ -0,0 +1,235 @@
+From iris.proofmode Require Import coq_tactics spec_patterns.
+From iris.proofmode Require Export tactics.
+From iris.program_logic Require Export pviewshifts.
+Import uPred.
+
+Section pvs.
+Context {Λ : language} {Σ : iFunctor}.
+Implicit Types P Q : iProp Λ Σ.
+
+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 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.
+Global Instance exists_split_pvs {A} E1 E2 P (Φ : A → iProp Λ Σ) :
+  ExistSplit P Φ → ExistSplit (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
+Proof.
+  rewrite /ExistSplit=><-. 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).
+Proof. rewrite /ToWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
+
+Class FSASplit {A} (P : iProp Λ Σ) (E : coPset)
+    (fsa : FSA Λ Σ A) (fsaV : Prop) (Φ : A → iProp Λ Σ) := {
+  fsa_split : fsa E Φ ⊢ P;
+  fsa_split_fsa :> FrameShiftAssertion fsaV fsa;
+}.
+Global Arguments fsa_split {_} _ _ _ _ _ {_}.
+Global Instance fsa_split_pvs E P :
+  FSASplit (|={E}=> P)%I E pvs_fsa True (λ _, P).
+Proof. split. done. apply _. Qed.
+
+Lemma tac_pvs_intro Δ E Q : Δ ⊢ Q → Δ ⊢ |={E}=> Q.
+Proof. intros ->. apply pvs_intro. Qed.
+
+Lemma tac_pvs_elim Δ Δ' E1 E2 E3 i p P Q :
+  envs_lookup i Δ = Some (p, |={E1,E2}=> P)%I →
+  envs_replace i p false (Esnoc Enil i P) Δ = Some Δ' →
+  E2 ⊆ E1 ∪ E3 →
+  Δ' ⊢ (|={E2,E3}=> Q) → Δ ⊢ |={E1,E3}=> Q.
+Proof.
+  intros ??? HQ. rewrite envs_replace_sound //; simpl. destruct p.
+  - by rewrite always_elim right_id pvs_frame_r wand_elim_r HQ pvs_trans.
+  - by rewrite right_id pvs_frame_r wand_elim_r HQ pvs_trans.
+Qed.
+
+Lemma tac_pvs_elim_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E i p P Q Φ :
+  envs_lookup i Δ = Some (p, |={E}=> P)%I → FSASplit 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.
+  eapply tac_pvs_elim; set_solver.
+Qed.
+
+Lemma tac_pvs_timeless Δ Δ' E1 E2 i p P Q :
+  envs_lookup i Δ = Some (p, ▷ P)%I → TimelessP P →
+  envs_simple_replace i p (Esnoc Enil i P) Δ = Some Δ' →
+  Δ' ⊢ (|={E1,E2}=> Q) → Δ ⊢ (|={E1,E2}=> Q).
+Proof.
+  intros ??? HQ. rewrite envs_simple_replace_sound //; simpl.
+  destruct p.
+  - rewrite always_later (pvs_timeless E1 (â–¡ P)%I) pvs_frame_r.
+    by rewrite right_id wand_elim_r HQ pvs_trans; last set_solver.
+  - rewrite (pvs_timeless E1 P) pvs_frame_r right_id wand_elim_r HQ.
+    by rewrite pvs_trans; last set_solver.
+Qed.
+
+Lemma tac_pvs_timeless_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E i p P Q Φ :
+  FSASplit 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.
+  eauto using tac_pvs_timeless.
+Qed.
+
+Hint Immediate env_special_nil_persistent : typeclass_instances.
+Lemma tac_pvs_assert {A} (fsa : FSA Λ Σ A) fsaV Δ Δ1 Δ2 Δ2' E lr js j P Q Φ :
+  FSASplit Q E fsa fsaV Φ →
+  envs_split lr js Δ = Some (Δ1,Δ2) →
+  envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' →
+  Δ1 ⊢ (|={E}=> P) → Δ2' ⊢ fsa E Φ → Δ ⊢ Q.
+Proof.
+  intros ??? HP HQ. rewrite -(fsa_split Q) -fsa_pvs_fsa -HQ envs_split_sound //.
+  rewrite HP envs_app_sound //; simpl.
+  by rewrite right_id pvs_frame_r wand_elim_r.
+Qed.
+End pvs.
+
+Tactic Notation "iPvsIntro" := apply tac_pvs_intro.
+
+Tactic Notation "iPvsCore" constr(H) :=
+  match goal with
+  | |- _ ⊢ |={_,_}=> _ =>
+    eapply tac_pvs_elim with _ _ H _ _;
+      [env_cbv; reflexivity || fail "iPvs:" H "not found"
+      |env_cbv; reflexivity
+      |try (rewrite (idemp_L (∪)); reflexivity)|]
+  | |- _ =>
+    eapply tac_pvs_elim_fsa with _ _ _ _ H _ _ _;
+      [env_cbv; reflexivity || fail "iPvs:" H "not found"
+      |let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
+       apply _ || fail "iPvs: " P "not a pvs"
+      |env_cbv; reflexivity|simpl]
+  end.
+
+Tactic Notation "iPvs" open_constr(H) :=
+  iPoseProof H as (fun H => iPvsCore H; last iDestructHyp H as "?").
+Tactic Notation "iPvs" open_constr(H) "as" constr(pat) :=
+  iPoseProof H as (fun H => iPvsCore H; last iDestructHyp H as pat).
+Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1) "}"
+    constr(pat) :=
+  iPoseProof H as (fun H => iPvsCore H; last iDestructHyp H as { x1 } pat).
+Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) "}" constr(pat) :=
+  iPoseProof H as (fun H => iPvsCore H; last iDestructHyp H as { x1 x2 } pat).
+Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) :=
+  iPoseProof H as (fun H => iPvsCore H; last iDestructHyp H as { x1 x2 x3 } pat).
+Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
+    constr(pat) :=
+  iPoseProof H as (fun H =>
+    iPvsCore H; last iDestructHyp H as { x1 x2 x3 x4 } pat).
+Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) "}" constr(pat) :=
+  iPoseProof H as (fun H =>
+    iPvsCore H; last iDestructHyp H as { x1 x2 x3 x4 x5 } pat).
+Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) "}" constr(pat) :=
+  iPoseProof H as (fun H =>
+    iPvsCore H; last iDestructHyp H as { x1 x2 x3 x4 x5 x6 } pat).
+Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) "}"
+    constr(pat) :=
+  iPoseProof H as (fun H =>
+    iPvsCore H; last iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 } pat).
+Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
+    simple_intropattern(x8) "}" constr(pat) :=
+  iPoseProof H as (fun H =>
+    iPvsCore H; last iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
+
+Tactic Notation "iPvs" open_constr(lem) constr(Hs) :=
+  iPoseProof lem Hs as (fun H => iPvsCore H; last iDestructHyp H as "?").
+Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" constr(pat) :=
+  iPoseProof lem Hs as (fun H => iPvsCore H; last iDestructHyp H as pat).
+Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
+    simple_intropattern(x1) "}" constr(pat) :=
+  iPoseProof lem Hs as (fun H => iPvsCore H; last iDestructHyp H as { x1 } pat).
+Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
+    simple_intropattern(x1) simple_intropattern(x2) "}" constr(pat) :=
+  iPoseProof lem Hs as (fun H =>
+    iPvsCore H; last iDestructHyp H as { x1 x2 } pat).
+Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
+    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3) "}"
+    constr(pat) :=
+  iPoseProof lem Hs as (fun H =>
+    iPvsCore H; last iDestructHyp H as { x1 x2 x3 } pat).
+Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
+    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
+    simple_intropattern(x4) "}" constr(pat) :=
+  iPoseProof lem Hs as (fun H =>
+    iPvsCore H; last iDestructHyp H as { x1 x2 x3 x4 } pat).
+Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
+    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
+    simple_intropattern(x4) simple_intropattern(x5) "}" constr(pat) :=
+  iPoseProof lem Hs as (fun H =>
+    iPvsCore H; last iDestructHyp H as { x1 x2 x3 x4 x5 } pat).
+Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
+    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
+    simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6) "}"
+    constr(pat) :=
+  iPoseProof lem Hs as (fun H =>
+    iPvsCore H; last iDestructHyp H as { x1 x2 x3 x4 x5 x6 } pat).
+Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
+    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
+    simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6)
+    simple_intropattern(x7) "}" constr(pat) :=
+  iPoseProof lem Hs as (fun H =>
+    iPvsCore H; last iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 } pat).
+Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
+    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
+    simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6)
+    simple_intropattern(x7) simple_intropattern(x8) "}" constr(pat) :=
+  iPoseProof lem Hs as (fun H =>
+    iPvsCore H; last iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
+
+Tactic Notation "iTimeless" constr(H) :=
+  match goal with
+  | |- _ ⊢ |={_,_}=> _ =>
+     eapply tac_pvs_timeless with _ H _ _;
+       [env_cbv; reflexivity || fail "iTimeless:" H "not found"
+       |let P := match goal with |- TimelessP ?P => P end in
+        apply _ || fail "iTimeless: " P "not timeless"
+       |env_cbv; reflexivity|simpl]
+  | |- _ =>
+     eapply tac_pvs_timeless_fsa with _ _ _ _ H _ _ _;
+       [let P := match goal with |- FSASplit ?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
+        apply _ || fail "iTimeless: " P "not timeless"
+       |env_cbv; reflexivity|simpl]
+  end.
+
+Tactic Notation "iTimeless" constr(H) "as" constr(Hs) :=
+  iTimeless H; iDestruct H as Hs.
+
+Tactic Notation "iPvsAssert" constr(Q) "as" constr(pat) "with" constr(Hs) :=
+  let H := iFresh in
+  let Hs := spec_pat.parse_one Hs in
+  lazymatch Hs with
+  | SSplit ?lr ?Hs =>
+     eapply tac_pvs_assert with _ _ _ _ _ _ lr Hs H Q _;
+       [let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
+        apply _ || fail "iPvsAssert: " P "not a pvs"
+       |env_cbv; reflexivity || fail "iPvsAssert:" Hs "not found"
+       |env_cbv; reflexivity|
+       |simpl; iDestructHyp H as pat]
+  | ?pat => fail "iPvsAssert: invalid pattern" pat
+  end.
+Tactic Notation "iPvsAssert" constr(Q) "as" constr(pat) :=
+  iPvsAssert Q as pat with "[]".
diff --git a/proofmode/spec_patterns.v b/proofmode/spec_patterns.v
new file mode 100644
index 0000000000000000000000000000000000000000..ad4e4a39fa380803211eac3a00b6c581aac52c8d
--- /dev/null
+++ b/proofmode/spec_patterns.v
@@ -0,0 +1,75 @@
+From iris.prelude Require Export strings.
+
+Inductive spec_pat :=
+  | SSplit : bool → list string → spec_pat
+  | SPersistent : spec_pat
+  | SPure : spec_pat
+  | SAlways : spec_pat
+  | SName : string → spec_pat.
+
+Module spec_pat.
+Inductive token :=
+  | TName : string → token
+  | TMinus : token
+  | TBracketL : token
+  | TBracketR : token
+  | TPersistent : token
+  | TPure : token
+  | TAlways : token.
+
+Fixpoint cons_name (kn : string) (k : list token) : list token :=
+  match kn with "" => k | _ => TName (string_rev kn) :: k end.
+Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
+  match s with
+  | "" => rev (cons_name kn k)
+  | String " " s => tokenize_go s (cons_name kn k) ""
+  | String "-" s => tokenize_go s (TMinus :: cons_name kn k) ""
+  | String "[" s => tokenize_go s (TBracketL :: cons_name kn k) ""
+  | String "]" s => tokenize_go s (TBracketR :: cons_name kn k) ""
+  | String "#" s => tokenize_go s (TPersistent :: cons_name kn k) ""
+  | String "%" s => tokenize_go s (TPure :: cons_name kn k) ""
+  | String "!" s => tokenize_go s (TAlways :: cons_name kn k) ""
+  | String a s => tokenize_go s k (String a kn)
+  end.
+Definition tokenize (s : string) : list token := tokenize_go s [] "".
+
+Fixpoint parse_go (ts : list token) (split : option (bool * list string))
+    (k : list spec_pat) : option (list spec_pat) :=
+  match split with
+  | None =>
+     match ts with
+     | [] => Some (rev k)
+     | TName s :: ts => parse_go ts None (SName s :: k)
+     | TMinus :: TBracketL :: ts => parse_go ts (Some (true,[])) k
+     | TMinus :: ts => parse_go ts None (SSplit true [] :: k)
+     | TBracketL :: ts => parse_go ts (Some (false,[])) k
+     | TAlways :: ts => parse_go ts None (SAlways :: k)
+     | TPersistent :: ts => parse_go ts None (SPersistent :: k)
+     | TPure :: ts => parse_go ts None (SPure :: k)
+     | _ => None
+     end
+  | Some (b, ss) =>
+     match ts with
+     | TName s :: ts => parse_go ts (Some (b,s :: ss)) k
+     | TBracketR :: ts => parse_go ts None (SSplit b (rev ss) :: k)
+     | _ => None
+     end
+  end.
+Definition parse (s : string) : option (list spec_pat) :=
+  parse_go (tokenize s) None [].
+
+Ltac parse s :=
+  lazymatch type of s with
+  | list spec_pat => s
+  | string => lazymatch eval vm_compute in (parse s) with
+              | Some ?pats => pats | _ => fail "invalid list spec_pat" s
+              end
+  end.
+Ltac parse_one s :=
+  lazymatch type of s with
+  | spec_pat => s
+  | string => lazymatch eval vm_compute in (parse s) with
+              | Some [?pat] => pat | _ => fail "invalid spec_pat" s
+              end
+  end.
+End spec_pat.
\ No newline at end of file
diff --git a/proofmode/sts.v b/proofmode/sts.v
new file mode 100644
index 0000000000000000000000000000000000000000..636f8fee5061aaa56e9ce6b3b39ecade63d3be95
--- /dev/null
+++ b/proofmode/sts.v
@@ -0,0 +1,45 @@
+From iris.proofmode Require Import coq_tactics pviewshifts.
+From iris.proofmode Require Export tactics.
+From iris.program_logic Require Export sts.
+Import uPred.
+
+Section sts.
+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 Φ →
+  fsaV →
+  envs_lookup i Δ = Some (false, sts_ownS γ S T) →
+  of_envs Δ ⊢ sts_ctx γ N φ → nclose N ⊆ E →
+  (∀ s, s ∈ S → ∃ Δ',
+    envs_simple_replace i false (Esnoc Enil i (▷ φ s)) Δ = Some Δ' ∧
+    Δ' ⊢ fsa (E ∖ nclose N) (λ a, ∃ s' T',
+      ■ sts.steps (s, T) (s', T') ★ ▷ φ s' ★ (sts_own γ s' T' -★ Φ a))) →
+  Δ ⊢ Q.
+Proof.
+  intros ????? HΔ'. rewrite -(fsa_split Q); eapply (sts_fsaS φ fsa); eauto.
+  rewrite envs_lookup_sound //; simpl; apply sep_mono_r.
+  apply forall_intro=>s; apply wand_intro_l.
+  rewrite -assoc; apply const_elim_sep_l=> Hs.
+  destruct (HΔ' s) as (Δ'&?&?); clear HΔ'; auto.
+  rewrite envs_simple_replace_sound' //; simpl.
+  by rewrite right_id wand_elim_r.
+Qed.
+End sts.
+
+Tactic Notation "iSts" constr(H) "as"
+    simple_intropattern(s) simple_intropattern(Hs) :=
+  match type of H with
+  | string => eapply tac_sts_fsa with _ _ _ _ _ _ H _ _ _ _
+  | 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
+     apply _ || fail "iSts: cannot viewshift in goal" P
+    |try fast_done (* atomic *)
+    |iAssumptionCore || fail "iSts:" H "not found"
+    |iAssumption || fail "iSts: invariant not found"
+    |done || eauto with ndisj (* [eauto with ndisj] is slow *)
+    |intros s Hs; eexists; split; [env_cbv; reflexivity|simpl]].
+Tactic Notation "iSts" constr(H) "as" simple_intropattern(s) := iSts H as s ?.
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
new file mode 100644
index 0000000000000000000000000000000000000000..6f6c6cc681e77df65c47b8f20a01b3d758b55740
--- /dev/null
+++ b/proofmode/tactics.v
@@ -0,0 +1,865 @@
+From iris.proofmode Require Import coq_tactics intro_patterns spec_patterns.
+From iris.algebra Require Export upred.
+From iris.proofmode Require Export notation.
+From iris.prelude Require Import stringmap.
+
+Declare Reduction env_cbv := cbv [
+  env_lookup env_lookup_delete env_delete env_app
+    env_replace env_split_go env_split
+  decide (* operational classes *)
+  sumbool_rec sumbool_rect (* sumbool *)
+  bool_eq_dec bool_rec bool_rect bool_dec eqb andb (* bool *)
+  assci_eq_dec ascii_to_digits Ascii.ascii_dec Ascii.ascii_rec Ascii.ascii_rect
+  string_eq_dec string_rec string_rect (* strings *)
+  env_persistent env_spatial envs_persistent
+  envs_lookup envs_lookup_delete envs_delete envs_app
+    envs_simple_replace envs_replace envs_split].
+Ltac env_cbv :=
+  match goal with |- ?u => let v := eval env_cbv in u in change v end.
+
+Ltac iFresh :=
+  lazymatch goal with
+  |- of_envs ?Δ ⊢ _ =>
+      match goal with
+      | _ => eval vm_compute in (fresh_string_of_set "~" (dom stringset Δ))
+      | _ => eval cbv in (fresh_string_of_set "~" (dom stringset Δ))
+      end
+  | _ => constr:"~"
+  end.
+
+(** * Misc *)
+Tactic Notation "iTypeOf" constr(H) tactic(tac):=
+  let Δ := match goal with |- of_envs ?Δ ⊢ _ => Δ end in
+  match eval env_cbv in (envs_lookup H Δ) with
+  | Some (?p,?P) => tac p P
+  end.
+
+(** * Start a proof *)
+Tactic Notation "iProof" :=
+  lazymatch goal with
+  | |- of_envs _ ⊢ _ => fail "iProof: already in Iris proofmode"
+  | |- True ⊢ _ => apply tac_adequate
+  | |- _ ⊢ _ => apply uPred.wand_entails, tac_adequate
+  end.
+
+(** * Context manipulation *)
+Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
+  eapply tac_rename with _ H1 H2 _ _; (* (i:=H1) (j:=H2) *)
+    [env_cbv; reflexivity || fail "iRename:" H1 "not found"
+    |env_cbv; reflexivity || fail "iRename:" H2 "not fresh"|].
+
+Tactic Notation "iClear" constr(Hs) :=
+  let rec go Hs :=
+    match Hs with
+    | [] => idtac
+    | ?H :: ?Hs =>
+       eapply tac_clear with _ H _ _; (* (i:=H) *)
+         [env_cbv; reflexivity || fail "iClear:" H "not found"|go Hs]
+    end in
+  let Hs := words Hs in go Hs.
+
+Tactic Notation "iClear" "★" :=
+  eapply tac_clear_spatial; [env_cbv; reflexivity|].
+
+(** * Assumptions *)
+Tactic Notation "iExact" constr(H) :=
+  eapply tac_exact with H _; (* (i:=H) *)
+    env_cbv;
+    lazymatch goal with
+    | |- None = Some _ => fail "iExact:" H "not found"
+    | |- Some (_, ?P) = Some _ =>
+       reflexivity || fail "iExact:" H ":" P "does not match goal"
+    end.
+
+Tactic Notation "iAssumptionCore" :=
+  let rec find Γ i P :=
+    match Γ with
+    | Esnoc ?Γ ?j ?Q => first [unify P Q; unify i j| find Γ i P]
+    end in
+  match goal with
+  | |- envs_lookup ?i (Envs ?Γp ?Γs) = Some (_, ?P) =>
+     first [is_evar i; fail 1 | env_cbv; reflexivity]
+  | |- envs_lookup ?i (Envs ?Γp ?Γs) = Some (_, ?P) =>
+     is_evar i; first [find Γp i P | find Γs i P]; env_cbv; reflexivity
+  end.
+Tactic Notation "iAssumption" :=
+  eapply tac_exact; iAssumptionCore;
+  match goal with |- _ = Some (_, ?P) => fail "iAssumption:" P "not found" end.
+
+(** * False *)
+Tactic Notation "iExFalso" := apply tac_ex_falso.
+Tactic Notation "iContradiction" constr(H) := iExFalso; iExact H.
+Tactic Notation "iContradiction" := iExFalso; iAssumption.
+
+(** * Pure introduction *)
+Tactic Notation "iIntro" "{" simple_intropattern(x) "}" :=
+  lazymatch goal with
+  | |- _ ⊢ (∀ _, _) => apply tac_forall_intro; intros x
+  | |- _ ⊢ (?P → _) =>
+     eapply tac_impl_intro_pure;
+       [apply _ || fail "iIntro:" P "not pure"|]; intros x
+  | |- _ ⊢ (?P -★ _) =>
+     eapply tac_wand_intro_pure;
+       [apply _ || fail "iIntro:" P "not pure"|]; intros x
+  | |- _ => intros x
+  end.
+
+(** * Introduction *)
+Tactic Notation "iIntro" constr(H) :=
+  lazymatch goal with
+  | |- _ ⊢ (?Q → _) =>
+    eapply tac_impl_intro with _ H; (* (i:=H) *)
+      [reflexivity || fail "iIntro: introducing " H ":" Q
+                           "into non-empty spatial context"
+      |env_cbv; reflexivity || fail "iIntro:" H "not fresh"|]
+  | |- _ ⊢ (_ -★ _) =>
+    eapply tac_wand_intro with _ H; (* (i:=H) *)
+      [env_cbv; reflexivity || fail "iIntro:" H "not fresh"|]
+  | _ => fail "iIntro: nothing to introduce"
+  end.
+
+Tactic Notation "iIntro" "#" constr(H) :=
+  lazymatch goal with
+  | |- _ ⊢ (?P → _) =>
+    eapply tac_impl_intro_persistent with _ H _; (* (i:=H) *)
+      [apply _ || fail "iIntro: " P " not persistent"
+      |env_cbv; reflexivity || fail "iIntro:" H "not fresh"|]
+  | |- _ ⊢ (?P -★ _) =>
+    eapply tac_wand_intro_persistent with _ H _; (* (i:=H) *)
+      [apply _ || fail "iIntro: " P " not persistent"
+      |env_cbv; reflexivity || fail "iIntro:" H "not fresh"|]
+  | _ => fail "iIntro: nothing to introduce"
+  end.
+
+(** * Making hypotheses persistent or pure *)
+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
+     apply _ || fail "iPersistent:" H ":" Q "not persistent"
+    |env_cbv; reflexivity|].
+
+Tactic Notation "iDuplicate" constr(H1) "as" constr(H2) :=
+  eapply tac_duplicate with _ H1 _ H2 _; (* (i:=H1) (j:=H2) *)
+    [env_cbv; reflexivity || fail "iDuplicate:" H1 "not found"
+    |reflexivity || fail "iDuplicate:" H1 "not in persistent context"
+    |env_cbv; reflexivity || fail "iDuplicate:" H2 "not fresh"|].
+Tactic Notation "iDuplicate" "#" constr(H1) "as" constr(H2) :=
+  iPersistent H1; iDuplicate H1 as H2.
+
+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
+     apply _ || fail "iPure:" H ":" P "not pure"
+    |intros pat].
+Tactic Notation "iPure" constr(H) := iPure H as ?.
+
+Tactic Notation "iPureIntro" := apply uPred.const_intro.
+
+(** * Specialize *)
+Tactic Notation "iForallSpecialize" constr(H) open_constr(x) :=
+  eapply tac_forall_specialize with _ H _ _ x; (* (i:=H) (a:=x) *)
+    [env_cbv; reflexivity || fail "iSpecialize:" H "not found"
+    |env_cbv; reflexivity|].
+
+Tactic Notation "iSpecialize" constr (H) constr(pat) :=
+  let solve_to_wand H1 :=
+    let P := match goal with |- ToWand ?P _ _ => P end in
+    apply _ || fail "iSpecialize:" H1 ":" P "not an implication/wand" in
+  let rec go H1 pats :=
+    lazymatch pats with
+    | [] => idtac
+    | SAlways :: ?pats => iPersistent H1; go H1 pats
+    | SSplit true [] :: SAlways :: ?pats =>
+       eapply tac_specialize_domain_persistent with _ _ H1 _ _ _ _ _;
+         [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
+         |solve_to_wand H1
+         |let Q := match goal with |- ToPersistentP ?Q _ => Q end in
+          apply _ || fail "iSpecialize:" Q "not persistent"
+         |env_cbv; reflexivity
+         | |go H1 pats]
+    | SName ?H2 :: SAlways :: ?pats =>
+       eapply tac_specialize_domain_persistent with _ _ H1 _ _ _ _ _;
+         [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
+         |solve_to_wand H1
+         |let Q := match goal with |- ToPersistentP ?Q _ => Q end in
+          apply _ || fail "iSpecialize:" Q "not persistent"
+         |env_cbv; reflexivity
+         |iExact H2 || fail "iSpecialize:" H2 "not found or wrong type"
+         |go H1 pats]
+    | SName ?H2 :: ?pats =>
+       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"
+         |solve_to_wand H1
+         |env_cbv; reflexivity|go H1 pats]
+    | SPersistent :: ?pats =>
+       eapply tac_specialize_range_persistent with _ _ H1 _ _ _ _;
+         [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
+         |solve_to_wand H1
+         |let Q := match goal with |- PersistentP ?Q => Q end in
+          apply _ || fail "iSpecialize:" Q "not persistent"
+         |env_cbv; reflexivity| |go H1 pats]
+    | SPure :: ?pats =>
+       eapply tac_specialize_range_persistent with _ _ H1 _ _ _ _; (* make custom tac_ lemma *)
+         [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
+         |solve_to_wand H1
+         |let Q := match goal with |- PersistentP ?Q => Q end in
+          apply _ || fail "iSpecialize:" Q "not persistent"
+         |env_cbv; reflexivity|iPureIntro|go H1 pats]
+    | SSplit ?lr ?Hs :: ?pats =>
+       eapply tac_specialize_assert with _ _ _ H1 _ lr Hs _ _ _;
+         [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
+         |solve_to_wand H1
+         |env_cbv; reflexivity || fail "iSpecialize:" Hs "not found"|
+         |go H1 pats]
+    end in
+  repeat (iForallSpecialize H _);
+  let pats := spec_pat.parse pat in go H pats.
+
+Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) "}" :=
+  iForallSpecialize H x1.
+Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1)
+    open_constr(x2) "}" :=
+  iSpecialize H { x1 }; iForallSpecialize H x2.
+Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
+    open_constr(x3) "}" :=
+  iSpecialize H { x1 x2 }; iForallSpecialize H x3.
+Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
+    open_constr(x3) open_constr(x4) "}" :=
+  iSpecialize H { x1 x2 x3 }; iForallSpecialize H x4.
+Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
+     open_constr(x3) open_constr(x4) open_constr(x5) "}" :=
+  iSpecialize H { x1 x2 x3 x4 }; iForallSpecialize H x5.
+Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
+    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6) "}" :=
+  iSpecialize H { x1 x2 x3 x4 x5 }; iForallSpecialize H x6.
+Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
+    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6)
+    open_constr(x7) "}" :=
+  iSpecialize H { x1 x2 x3 x4 x5 x6 }; iForallSpecialize H x7.
+Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
+    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6)
+    open_constr(x7) open_constr(x8) "}" :=
+  iSpecialize H { x1 x2 x3 x4 x5 x6 x7 }; iForallSpecialize H x8.
+
+Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) "}" constr(Hs) :=
+  iSpecialize H { x1 }; iSpecialize H @ Hs.
+Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2) "}"
+    constr(Hs) :=
+  iSpecialize H { x1 x2 }; iSpecialize H @ Hs.
+Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
+    open_constr(x3) "}" constr(Hs) :=
+  iSpecialize H { x1 x2 x3 }; iSpecialize H @ Hs.
+Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
+    open_constr(x3) open_constr(x4) "}" constr(Hs) :=
+  iSpecialize H { x1 x2 x3 x4 }; iSpecialize H @ Hs.
+Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
+    open_constr(x3) open_constr(x4) open_constr(x5) "}" constr(Hs) :=
+  iSpecialize H { x1 x2 x3 x4 x5 }; iSpecialize H @ Hs.
+Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
+    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6) "}"
+    constr(Hs) :=
+  iSpecialize H { x1 x2 x3 x4 x5 x6 }; iSpecialize H @ Hs.
+Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
+    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6)
+    open_constr(x7) "}" constr(Hs) :=
+  iSpecialize H { x1 x2 x3 x4 x5 x6 x7 }; iSpecialize H @ Hs.
+Tactic Notation "iSpecialize" constr (H) "{" open_constr(x1) open_constr(x2)
+    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6)
+    open_constr(x7) open_constr(x8) "}" constr(Hs) :=
+  iSpecialize H { x1 x2 x3 x4 x5 x6 x7 x8 }; iSpecialize H @ Hs.
+
+(** * Pose proof *)
+Tactic Notation "iPoseProof" open_constr(lem) "as" constr(H) :=
+  eapply tac_pose_proof with _ H _; (* (j:=H) *)
+    [first
+       [eapply lem
+       |apply uPred.entails_impl; eapply lem
+       |apply uPred.equiv_iff; eapply lem]
+    |env_cbv; reflexivity || fail "iPoseProof:" H "not fresh"|].
+
+Tactic Notation "iPoseProof" open_constr(lem) constr(Hs) "as" constr(H) :=
+  iPoseProof lem as H; last iSpecialize H Hs.
+
+Tactic Notation "iPoseProof" open_constr(lem) :=
+  let H := iFresh in iPoseProof lem as H.
+Tactic Notation "iPoseProof" open_constr(lem) constr(Hs) :=
+  let H := iFresh in iPoseProof lem Hs as H.
+
+Tactic Notation "iPoseProof" open_constr(lem) "as" tactic(tac) :=
+  lazymatch type of lem with
+  | string => tac lem
+  | _ => let H := iFresh in iPoseProof lem as H; last tac H; try apply _
+  end.
+
+Tactic Notation "iPoseProof" open_constr(lem) constr(Hs) "as" tactic(tac) :=
+  iPoseProof lem as (fun H => iSpecialize H Hs; last tac H).
+
+(** * Apply *)
+Tactic Notation "iApply" open_constr (lem) :=
+  iPoseProof lem as (fun H => repeat (iForallSpecialize H _); first
+    [iExact H
+    |eapply tac_apply with _ H _ _ _;
+       [env_cbv; reflexivity || fail "iApply:" lem "not found"
+       |apply _ || fail "iApply: cannot apply" lem|]]).
+Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) "}" :=
+  iSpecialize H { x1 }; last iApply H.
+Tactic Notation "iApply" open_constr (H) "{" open_constr(x1)
+    open_constr(x2) "}" :=
+  iSpecialize H { x1 x2 }; last iApply H.
+Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
+    open_constr(x3) "}" :=
+  iSpecialize H { x1 x2 x3 }; last iApply H.
+Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
+    open_constr(x3) open_constr(x4) "}" :=
+  iSpecialize H { x1 x2 x3 x4 }; last iApply H.
+Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
+     open_constr(x3) open_constr(x4) open_constr(x5) "}" :=
+  iSpecialize H { x1 x2 x3 x4 x5 }; last iApply H.
+Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
+    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6) "}" :=
+  iSpecialize H { x1 x2 x3 x4 x5 x6 }; last iApply H.
+Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
+    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6)
+    open_constr(x7) "}" :=
+  iSpecialize H { x1 x2 x3 x4 x5 x6 x7 }; last iApply H.
+Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
+    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6)
+    open_constr(x7) open_constr(x8) "}" :=
+  iSpecialize H { x1 x2 x3 x4 x5 x6 x7 x8 }; last iApply H.
+
+(* this is wrong *)
+Tactic Notation "iApply" open_constr (lem) constr(Hs) :=
+  iPoseProof lem Hs as (fun H => first
+    [iExact H
+    |eapply tac_apply with _ H _ _ _;
+       [env_cbv; reflexivity || fail "iApply:" lem "not found"
+       |apply _ || fail "iApply: cannot apply" lem|]]).
+Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) "}" constr(Hs) :=
+  iSpecialize H { x1 }; last iApply H Hs.
+Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2) "}"
+    constr(Hs) :=
+  iSpecialize H { x1 x2 }; last iApply H Hs.
+Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
+    open_constr(x3) "}" constr(Hs) :=
+  iSpecialize H { x1 x2 x3 }; last iApply H Hs.
+Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
+    open_constr(x3) open_constr(x4) "}" constr(Hs) :=
+  iSpecialize H { x1 x2 x3 x4 }; last iApply H Hs.
+Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
+    open_constr(x3) open_constr(x4) open_constr(x5) "}" constr(Hs) :=
+  iSpecialize H { x1 x2 x3 x4 x5 }; last iApply H Hs.
+Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
+    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6) "}"
+    constr(Hs) :=
+  iSpecialize H { x1 x2 x3 x4 x5 x6 }; last iApply H Hs.
+Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
+    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6)
+    open_constr(x7) "}" constr(Hs) :=
+  iSpecialize H { x1 x2 x3 x4 x5 x6 x7 }; last iApply H Hs.
+Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
+    open_constr(x3) open_constr(x4) open_constr(x5) open_constr(x6)
+    open_constr(x7) open_constr(x8) "}" constr(Hs) :=
+  iSpecialize H { x1 x2 x3 x4 x5 x6 x7 x8 }; last iApply H Hs.
+
+(** * Revert *)
+Tactic Notation "iForallRevert" ident(x) :=
+  match type of x with
+  | _ : Prop => revert x; apply tac_pure_revert
+  | _ => revert x; apply tac_forall_revert
+  end.
+
+Tactic Notation "iImplRevert" constr(H) :=
+  eapply tac_revert with _ H _ _; (* (i:=H) *)
+    [env_cbv; reflexivity || fail "iRevert:" H "not found"
+    |env_cbv].
+
+Tactic Notation "iRevert" constr(Hs) :=
+  let rec go H2s :=
+    match H2s with [] => idtac | ?H2 :: ?H2s => go H2s; iImplRevert H2 end in
+  let Hs := words Hs in go Hs.
+
+Tactic Notation "iRevert" "{" ident(x1) "}" :=
+  iForallRevert x1.
+Tactic Notation "iRevert" "{" ident(x1) ident(x2) "}" :=
+  iForallRevert x2; iRevert { x1 }.
+Tactic Notation "iRevert" "{" ident(x1) ident(x2) ident(x3) "}" :=
+  iForallRevert x3; iRevert { x1 x2 }.
+Tactic Notation "iRevert" "{" ident(x1) ident(x2) ident(x3) ident(x4) "}" :=
+  iForallRevert x4; iRevert { x1 x2 x3 }.
+Tactic Notation "iRevert" "{" ident(x1) ident(x2) ident(x3) ident(x4)
+    ident(x5) "}" :=
+  iForallRevert x5; iRevert { x1 x2 x3 x4 }.
+Tactic Notation "iRevert" "{" ident(x1) ident(x2) ident(x3) ident(x4)
+    ident(x5) ident(x6) "}" :=
+  iForallRevert x6; iRevert { x1 x2 x3 x4 x5 }.
+Tactic Notation "iRevert" "{" ident(x1) ident(x2) ident(x3) ident(x4)
+    ident(x5) ident(x6) ident(x7) "}" :=
+  iForallRevert x7; iRevert { x1 x2 x3 x4 x5 x6 }.
+Tactic Notation "iRevert" "{" ident(x1) ident(x2) ident(x3) ident(x4)
+    ident(x5) ident(x6) ident(x7) ident(x8) "}" :=
+  iForallRevert x8; iRevert { x1 x2 x3 x4 x5 x6 x7 }.
+
+Tactic Notation "iRevert" "{" ident(x1) "}" constr(Hs) :=
+  iRevert Hs; iRevert { x1 }.
+Tactic Notation "iRevert" "{" ident(x1) ident(x2) "}" constr(Hs) :=
+  iRevert Hs; iRevert { x1 x2 }.
+Tactic Notation "iRevert" "{" ident(x1) ident(x2) ident(x3) "}" constr(Hs) :=
+  iRevert Hs; iRevert { x1 x2 x3 }.
+Tactic Notation "iRevert" "{" ident(x1) ident(x2) ident(x3) ident(x4) "}"
+    constr(Hs) :=
+  iRevert Hs; iRevert { x1 x2 x3 x4 }.
+Tactic Notation "iRevert" "{" ident(x1) ident(x2) ident(x3) ident(x4)
+    ident(x5) "}" constr(Hs) :=
+  iRevert Hs; iRevert { x1 x2 x3 x4 x5 }.
+Tactic Notation "iRevert" "{" ident(x1) ident(x2) ident(x3) ident(x4)
+    ident(x5) ident(x6) "}" constr(Hs) :=
+  iRevert Hs; iRevert { x1 x2 x3 x4 x5 x6 }.
+Tactic Notation "iRevert" "{" ident(x1) ident(x2) ident(x3) ident(x4)
+    ident(x5) ident(x6) ident(x7) "}" constr(Hs) :=
+  iRevert Hs; iRevert { x1 x2 x3 x4 x5 x6 x7 }.
+Tactic Notation "iRevert" "{" ident(x1) ident(x2) ident(x3) ident(x4)
+    ident(x5) ident(x6) ident(x7) ident(x8) "}" constr(Hs) :=
+  iRevert Hs; iRevert { x1 x2 x3 x4 x5 x6 x7 x8 }.
+
+(** * Disjunction *)
+Tactic Notation "iLeft" :=
+  eapply tac_or_l;
+    [let P := match goal with |- OrSplit ?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
+     apply _ || fail "iRight:" P "not a disjunction"|].
+
+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
+     apply _ || fail "iOrDestruct:" H ":" P "not a disjunction"
+    |env_cbv; reflexivity || fail "iOrDestruct:" H1 "not fresh"
+    |env_cbv; reflexivity || fail "iOrDestruct:" H2 "not fresh"| |].
+
+(** * Conjunction and separating conjunction *)
+Tactic Notation "iSplit" :=
+  eapply tac_and_split;
+    [let P := match goal with |- AndSplit ?P _ _ => P end in
+     apply _ || fail "iSplit:" P "not a conjunction"| |].
+
+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
+     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
+     apply _ || fail "iSplitR:" P "not a separating conjunction"
+    |env_cbv; reflexivity || fail "iSplitR: hypotheses" Hs "not found"| |].
+
+Tactic Notation "iSplitL" := iSplitR "".
+Tactic Notation "iSplitR" := iSplitL "".
+
+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
+     apply _ || fail "iSepDestruct:" H ":" P "not separating destructable"
+    |env_cbv; reflexivity || fail "iSepDestruct:" H1 "or" H2 " not fresh"|].
+
+Tactic Notation "iFrame" constr(Hs) :=
+  let rec go Hs :=
+    match Hs with
+    | [] => idtac
+    | ?H :: ?Hs =>
+       eapply tac_frame with _ H _ _ _;
+         [env_cbv; reflexivity || fail "iFrame:" H "not found"
+         |let R := match goal with |- Frame ?R _ _ => R end in
+          apply _ || fail "iFrame: cannot frame" R
+         |lazy iota beta; go Hs]
+    end
+  in let Hs := words Hs in go Hs.
+
+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
+     apply _ || fail "iCombine: cannot combine" H1 ":" P1 "and" H2 ":" P2
+    |env_cbv; reflexivity || fail "iCombine:" H "not fresh"|].
+
+(** * Existential *)
+Tactic Notation "iExists" open_constr(x1) :=
+  eapply tac_exist with _ x1 ;
+    [let P := match goal with |- ExistSplit ?P _ => P end in
+     apply _ || fail "iExists:" P "not an existential"
+    |cbv beta].
+
+Tactic Notation "iExists" open_constr(x1) "," open_constr(x2) :=
+  iExists x1; iExists x2.
+Tactic Notation "iExists" open_constr(x1) "," open_constr(x2) ","
+    open_constr(x3) :=
+  iExists x1; iExists x2, x3.
+Tactic Notation "iExists" open_constr(x1) "," open_constr(x2) ","
+    open_constr(x3) "," open_constr(x4) :=
+  iExists x1; iExists x2, x3, x4.
+Tactic Notation "iExists" open_constr(x1) "," open_constr(x2) ","
+    open_constr(x3) "," open_constr(x4) "," open_constr(x5) :=
+  iExists x1; iExists x2, x3, x4, x5.
+Tactic Notation "iExists" open_constr(x1) "," open_constr(x2) ","
+    open_constr(x3) "," open_constr(x4) "," open_constr(x5) ","
+    open_constr(x6) :=
+  iExists x1; iExists x2, x3, x4, x5, x6.
+Tactic Notation "iExists" open_constr(x1) "," open_constr(x2) ","
+    open_constr(x3) "," open_constr(x4) "," open_constr(x5) ","
+    open_constr(x6) "," open_constr(x7) :=
+  iExists x1; iExists x2, x3, x4, x5, x6, x7.
+Tactic Notation "iExists" open_constr(x1) "," open_constr(x2) ","
+    open_constr(x3) "," open_constr(x4) "," open_constr(x5) ","
+    open_constr(x6) "," open_constr(x7) "," open_constr(x8) :=
+  iExists x1; iExists x2, x3, x4, x5, x6, x7, x8.
+
+Tactic Notation "iExistDestruct" constr(H) "as" ident(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
+     apply _ || fail "iExistDestruct:" H ":" P "not an existential"|];
+  intros x; eexists; split;
+    [env_cbv; reflexivity || fail "iExistDestruct:" Hx "not fresh"|].
+
+(** * Destruct tactic *)
+Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
+  let rec go Hz pat :=
+    lazymatch pat with
+    | IAnom => idtac
+    | IAnomPure => iPure Hz
+    | IClear => iClear Hz
+    | IName ?y => iRename Hz into y
+    | IPersistent ?pat => iPersistent Hz; go Hz pat
+    | IList [[]] => iContradiction Hz
+    | IList [[?pat1; ?pat2]] =>
+       let Hy := iFresh in iSepDestruct Hz as Hz Hy; go Hz pat1; go Hy pat2
+    | IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [go Hz pat1|go Hz pat2]
+    | _ => fail "iDestruct:" pat "invalid"
+    end
+  in let pat := intro_pat.parse_one pat in go H pat.
+
+Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1) "}"
+    constr(pat) :=
+  iExistDestruct H as x1 H; iDestructHyp H as @ pat.
+Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) "}" constr(pat) :=
+  iExistDestruct H as x1 H; iDestructHyp H as { x2 } pat.
+Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) :=
+  iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 } pat.
+Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
+    constr(pat) :=
+  iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 x4 } pat.
+Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) "}" constr(pat) :=
+  iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 x4 x5 } pat.
+Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) "}" constr(pat) :=
+  iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 x4 x5 x6 } pat.
+Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) "}"
+    constr(pat) :=
+  iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 x4 x5 x6 x7 } pat.
+Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
+    simple_intropattern(x8) "}" constr(pat) :=
+  iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 x4 x5 x6 x7 x8 } pat.
+
+Tactic Notation "iDestruct" open_constr(H) "as" constr(pat) :=
+  iPoseProof H as (fun H => iDestructHyp H as pat).
+Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1) "}"
+    constr(pat) :=
+  iPoseProof H as (fun H => iDestructHyp H as { x1 } pat).
+Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) "}" constr(pat) :=
+  iPoseProof H as (fun H => iDestructHyp H as { x1 x2 } pat).
+Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) :=
+  iPoseProof H as (fun H => iDestructHyp H as { x1 x2 x3 } pat).
+Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
+    constr(pat) :=
+  iPoseProof H as (fun H => iDestructHyp H as { x1 x2 x3 x4 } pat).
+Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) "}" constr(pat) :=
+  iPoseProof H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 } pat).
+Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) "}" constr(pat) :=
+  iPoseProof H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 } pat).
+Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) "}"
+    constr(pat) :=
+  iPoseProof H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 } pat).
+Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
+    simple_intropattern(x8) "}" constr(pat) :=
+  iPoseProof H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
+
+Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "as" constr(pat) :=
+  iPoseProof lem as (fun H => iSpecialize H Hs; last iDestructHyp H as pat).
+Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "as" "{"
+    simple_intropattern(x1) "}" constr(pat) :=
+  iPoseProof lem as (fun H => iSpecialize H Hs;
+    last iDestructHyp H as { x1 } pat).
+Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "as" "{"
+    simple_intropattern(x1) simple_intropattern(x2) "}" constr(pat) :=
+  iPoseProof lem as (fun H => iSpecialize H Hs;
+    last iDestructHyp H as { x1 x2 } pat).
+Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "as" "{"
+    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3) "}"
+    constr(pat) :=
+  iPoseProof lem as (fun H => iSpecialize H Hs;
+    last iDestructHyp H as { x1 x2 x3 } pat).
+Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "as" "{"
+    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
+    simple_intropattern(x4) "}" constr(pat) :=
+  iPoseProof lem as (fun H => iSpecialize H Hs;
+    last iDestructHyp H as { x1 x2 x3 x4 } pat).
+Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "as" "{"
+    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
+    simple_intropattern(x4) simple_intropattern(x5) "}" constr(pat) :=
+  iPoseProof lem as (fun H => iSpecialize H Hs;
+    last iDestructHyp H as { x1 x2 x3 x4 x5 } pat).
+Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "as" "{"
+    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
+    simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6) "}"
+    constr(pat) :=
+  iPoseProof lem as (fun H => iSpecialize H Hs;
+    last iDestructHyp H as { x1 x2 x3 x4 x5 x6 } pat).
+Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "as" "{"
+    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
+    simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6)
+    simple_intropattern(x7) "}" constr(pat) :=
+  iPoseProof lem as (fun H => iSpecialize H Hs;
+    last iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 } pat).
+Tactic Notation "iDestruct" open_constr(lem) constr(Hs) "as" "{"
+    simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
+    simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6)
+    simple_intropattern(x7) simple_intropattern(x8) "}" constr(pat) :=
+  iPoseProof lem as (fun H => iSpecialize H Hs;
+    last iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
+
+Tactic Notation "iDestruct" open_constr(H) "as" "%" simple_intropattern(pat) :=
+  let Htmp := iFresh in iDestruct H as Htmp; iPure Htmp as pat.
+Tactic Notation "iDestruct" open_constr(H) constr(Hs)
+    "as" "%" simple_intropattern(pat) :=
+  let Htmp := iFresh in iDestruct H Hs as Htmp; iPure Htmp as pat.
+
+(** * Always *)
+Tactic Notation "iAlways":=
+   apply tac_always_intro;
+     [reflexivity || fail "iAlways: spatial context non-empty"|].
+
+(** * Introduction tactic *)
+Tactic Notation "iIntros" constr(pat) :=
+  let rec go pats :=
+    lazymatch pats with
+    | [] => idtac
+    | ISimpl :: ?pats => simpl; go pats
+    | IAlways :: ?pats => iAlways; go pats
+    | IPersistent (IName ?H) :: ?pats => iIntro #H; go pats
+    | IName ?H :: ?pats => iIntro H; go pats
+    | IPersistent IAnom :: ?pats => let H := iFresh in iIntro #H; go pats
+    | IAnom :: ?pats => let H := iFresh in iIntro H; go pats
+    | IAnomPure :: ?pats => iPureIntro; go pats
+    | IPersistent ?pat :: ?pats =>
+       let H := iFresh in iIntro #H; iDestructHyp H as pat; go pats
+    | ?pat :: ?pats =>
+       let H := iFresh in iIntro H; iDestructHyp H as pat; go pats
+    | _ => fail "iIntro: failed with" pats
+    end
+  in let pats := intro_pat.parse pat in try iProof; go pats.
+
+Tactic Notation "iIntros" "{" simple_intropattern(x1) "}" :=
+  try iProof; iIntro { x1 }.
+Tactic Notation "iIntros" "{" simple_intropattern(x1)
+    simple_intropattern(x2) "}" :=
+  iIntros { x1 }; iIntro { x2 }.
+Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
+    simple_intropattern(x3) "}" :=
+  iIntros { x1 x2 }; iIntro { x3 }.
+Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
+    simple_intropattern(x3) simple_intropattern(x4) "}" :=
+  iIntros { x1 x2 x3 }; iIntro { x4 }.
+Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
+    simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5) "}" :=
+  iIntros { x1 x2 x3 x4 }; iIntro { x5 }.
+Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
+    simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
+    simple_intropattern(x6) "}" :=
+  iIntros { x1 x2 x3 x4 x5 }; iIntro { x6 }.
+Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
+    simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
+    simple_intropattern(x6) simple_intropattern(x7) "}" :=
+  iIntros { x1 x2 x3 x4 x5 x6 }; iIntro { x7 }.
+Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
+    simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
+    simple_intropattern(x6) simple_intropattern(x7) simple_intropattern(x8) "}" :=
+  iIntros { x1 x2 x3 x4 x5 x6 x7 }; iIntro { x8 }.
+
+Tactic Notation "iIntros" "{" simple_intropattern(x1) "}" constr(p) :=
+  iIntros { x1 }; iIntros p.
+Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
+    "}" constr(p) :=
+  iIntros { x1 x2 }; iIntros p.
+Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
+    simple_intropattern(x3) "}" constr(p) :=
+  iIntros { x1 x2 x3 }; iIntros p.
+Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
+    simple_intropattern(x3) simple_intropattern(x4) "}" constr(p) :=
+  iIntros { x1 x2 x3 x4 }; iIntros p.
+Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
+    simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
+    "}" constr(p) :=
+  iIntros { x1 x2 x3 x4 x5 }; iIntros p.
+Tactic Notation "iIntros" "{"simple_intropattern(x1) simple_intropattern(x2)
+    simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
+    simple_intropattern(x6) "}" constr(p) :=
+  iIntros { x1 x2 x3 x4 x5 x6 }; iIntros p.
+Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
+    simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
+    simple_intropattern(x6) simple_intropattern(x7) "}" constr(p) :=
+  iIntros { x1 x2 x3 x4 x5 x6 x7 }; iIntros p.
+Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
+    simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
+    simple_intropattern(x6) simple_intropattern(x7) simple_intropattern(x8)
+    "}" constr(p) :=
+  iIntros { x1 x2 x3 x4 x5 x6 x7 x8 }; iIntros p.
+
+(** * Later *)
+Tactic Notation "iNext":=
+  eapply tac_next;
+    [apply _
+    |let P := match goal with |- upred_tactics.StripLaterL ?P _ => P end in
+     apply _ || fail "iNext:" P "does not contain laters"|].
+
+Tactic Notation "iLöb" "as" constr (H) :=
+  eapply tac_löb with _ H;
+    [reflexivity || fail "iLöb: non-empty spatial context"
+    |env_cbv; reflexivity || fail "iLöb:" H "not fresh"|].
+
+Tactic Notation "iLöb" "{" ident(x1) "}" "as" constr (H) :=
+  iRevert { x1 }; iLöb as H; iIntros { x1 }.
+Tactic Notation "iLöb" "{" ident(x1) ident(x2) "}" "as" constr (H) :=
+  iRevert { x1 x2 }; iLöb as H; iIntros { x1 x2 }.
+Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) "}" "as" constr (H) :=
+  iRevert { x1 x2 x3 }; iLöb as H; iIntros { x1 x2 x3 }.
+Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4) "}" "as"
+    constr (H):=
+  iRevert { x1 x2 x3 x4 }; iLöb as H; iIntros { x1 x2 x3 x4 }.
+Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
+    ident(x5) "}" "as" constr (H) :=
+  iRevert { x1 x2 x3 x4 x5 }; iLöb as H; iIntros { x1 x2 x3 x4 x5 }.
+Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
+    ident(x5) ident(x6) "}" "as" constr (H) :=
+  iRevert { x1 x2 x3 x4 x5 x6 }; iLöb as H; iIntros { x1 x2 x3 x4 x5 x6 }.
+Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
+    ident(x5) ident(x6) ident(x7) "}" "as" constr (H) :=
+  iRevert { x1 x2 x3 x4 x5 x6 x7 }; iLöb as H; iIntros { x1 x2 x3 x4 x5 x6 x7 }.
+Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
+    ident(x5) ident(x6) ident(x7) ident(x8) "}" "as" constr (H) :=
+  iRevert { x1 x2 x3 x4 x5 x6 x7 x8 };
+    iLöb as H; iIntros { x1 x2 x3 x4 x5 x6 x7 x8 }.
+
+Tactic Notation "iLöb" constr(Hs) "as" constr (H) :=
+  iRevert Hs; iLöb as H; iIntros Hs.
+Tactic Notation "iLöb" "{" ident(x1) "}" constr(Hs) "as" constr (H) :=
+  iRevert { x1 } Hs; iLöb as H; iIntros { x1 } Hs.
+Tactic Notation "iLöb" "{" ident(x1) ident(x2) "}" constr(Hs) "as" constr (H) :=
+  iRevert { x1 x2 } Hs; iLöb as H; iIntros { x1 x2 } Hs.
+Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) "}" constr(Hs) "as"
+    constr (H) :=
+  iRevert { x1 x2 x3 } Hs; iLöb as H; iIntros { x1 x2 x3 } Hs.
+Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4) "}"
+    constr(Hs) "as" constr (H) :=
+  iRevert { x1 x2 x3 x4 } Hs; iLöb as H; iIntros { x1 x2 x3 x4 } Hs.
+Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
+    ident(x5) "}" constr(Hs) "as" constr (H) :=
+  iRevert { x1 x2 x3 x4 x5 } Hs; iLöb as H; iIntros { x1 x2 x3 x4 x5 } Hs.
+Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
+    ident(x5) ident(x6) "}" constr(Hs) "as" constr (H) :=
+  iRevert { x1 x2 x3 x4 x5 x6 } Hs; iLöb as H; iIntros { x1 x2 x3 x4 x5 x6 } Hs.
+Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
+    ident(x5) ident(x6) ident(x7) "}" constr(Hs) "as" constr (H) :=
+  iRevert { x1 x2 x3 x4 x5 x6 x7 } Hs;
+    iLöb as H; iIntros { x1 x2 x3 x4 x5 x6 x7 } Hs.
+Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
+    ident(x5) ident(x6) ident(x7) ident(x8) "}" constr(Hs) "as" constr (H) :=
+  iRevert { x1 x2 x3 x4 x5 x6 x7 x8 } Hs;
+    iLöb as H; iIntros { x1 x2 x3 x4 x5 x6 x7 x8 } Hs.
+
+(** * Assert *)
+Tactic Notation "iAssert" constr(Q) "as" constr(pat) "with" constr(Hs) :=
+  let H := iFresh in
+  let Hs := spec_pat.parse_one Hs in
+  lazymatch Hs with
+  | SSplit ?lr ?Hs =>
+     eapply tac_assert with _ _ _ lr Hs H Q; (* (js:=Hs) (j:=H) (P:=Q) *)
+       [env_cbv; reflexivity || fail "iAssert:" Hs "not found"
+       |env_cbv; reflexivity|
+       |iDestructHyp H as pat]
+  | SPersistent =>
+     eapply tac_assert_persistent with _ H Q; (* (j:=H) (P:=Q) *)
+       [apply _ || fail "iAssert:" Q "not persistent"
+       |env_cbv; reflexivity|
+       |iDestructHyp H as pat]
+  | ?pat => fail "iAssert: invalid pattern" pat
+  end.
+Tactic Notation "iAssert" constr(Q) "as" constr(pat) :=
+  iAssert Q as pat with "[]".
+
+(** * Rewrite *)
+Ltac iRewriteFindPred :=
+  match goal with
+  | |- _ ⊣⊢ ?Φ ?x =>
+     generalize x;
+     match goal with |- (∀ y, @?Ψ y ⊣⊢ _) => unify Φ Ψ; reflexivity end
+  end.
+
+Tactic Notation "iRewriteCore" constr(lr) constr(Heq) :=
+  eapply (tac_rewrite _ Heq _ _ lr);
+    [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
+    |let P := match goal with |- ?P ⊢ _ => P end in
+     reflexivity || fail "iRewrite:" Heq ":" P "not an equality"
+    |iRewriteFindPred
+    |intros ??? ->; reflexivity|lazy beta].
+Tactic Notation "iRewrite" constr(Heq) := iRewriteCore false Heq.
+Tactic Notation "iRewrite" "-" constr(Heq) := iRewriteCore true Heq.
+
+Tactic Notation "iRewriteCore" constr(lr) constr(Heq) "in" constr(H) :=
+  eapply (tac_rewrite_in _ Heq _ _ H _ _ lr);
+    [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
+    |env_cbv; reflexivity || fail "iRewrite:" H "not found"
+    |let P := match goal with |- ?P ⊢ _ => P end in
+     reflexivity || fail "iRewrite:" Heq ":" P "not an equality"
+    |iRewriteFindPred
+    |intros ??? ->; reflexivity
+    |env_cbv; reflexivity|lazy beta].
+Tactic Notation "iRewrite" constr(Heq) "in" constr(H) :=
+  iRewriteCore false Heq in H.
+Tactic Notation "iRewrite" "-" constr(Heq) "in" constr(H) :=
+  iRewriteCore true Heq in H.
+
+(* Make sure that by and done solve trivial things in proof mode *)
+Hint Extern 0 (of_envs _ ⊢ _) => by apply tac_pure_intro.
+Hint Extern 0 (of_envs _ ⊢ _) => iAssumption.
diff --git a/proofmode/weakestpre.v b/proofmode/weakestpre.v
new file mode 100644
index 0000000000000000000000000000000000000000..30ebfd256a4b1ccb912d0284c5c110a1127fb2fd
--- /dev/null
+++ b/proofmode/weakestpre.v
@@ -0,0 +1,14 @@
+From iris.proofmode Require Import coq_tactics.
+From iris.proofmode Require Export pviewshifts.
+From iris.program_logic Require Export weakestpre.
+Import uPred.
+
+Section weakestpre.
+Context {Λ : language} {Σ : iFunctor}.
+Implicit Types P Q : iProp Λ Σ.
+Implicit Types Φ : val Λ → iProp Λ Σ.
+
+Global Instance fsa_split_wp E e Φ :
+  FSASplit (WP e @ E {{ Φ }})%I E (wp_fsa e) (language.atomic e) Φ.
+Proof. split. done. apply _. Qed.
+End weakestpre.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index c52dc3c6d1cc7acfce20e8a610a216764d9aa57f..1fa2f66c2334bf09d601a19f8a037bc6d1d400bc 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -1,6 +1,6 @@
 (** This file is essentially a bunch of testcases. *)
 From iris.program_logic Require Import ownership hoare auth.
-From iris.heap_lang Require Import wp_tactics heap notation.
+From iris.heap_lang Require Import proofmode notation.
 Import uPred.
 
 Section LangTests.
@@ -26,12 +26,8 @@ Section LiftingTests.
   Lemma heap_e_spec E N :
      nclose N ⊆ E → heap_ctx N ⊢ WP heap_e @ E {{ λ v, v = #2 }}.
   Proof.
-    rewrite /heap_e=>HN. rewrite -(wp_mask_weaken N E) //.
-    wp eapply wp_alloc; eauto. apply forall_intro=>l; apply wand_intro_l.
-    wp_let. wp eapply wp_load; eauto with I. apply sep_mono_r, wand_intro_l.
-    wp_op. wp eapply wp_store; eauto with I. apply sep_mono_r, wand_intro_l.
-    wp_seq. wp eapply wp_load; eauto with I. apply sep_mono_r, wand_intro_l.
-      by apply const_intro.
+    iIntros {HN} "#?". rewrite /heap_e. iApply (wp_mask_weaken N); first done.
+    wp_alloc l as "Hl". wp_let. wp_load. wp_op. wp_store. wp_seq. by wp_load.
   Qed.
 
   Definition FindPred : val :=
@@ -43,30 +39,27 @@ Section LiftingTests.
       if: '"x" ≤ #0 then -^FindPred (-'"x" + #2) #0 else ^FindPred '"x" #0.
 
   Lemma FindPred_spec n1 n2 E Φ :
-    n1 < n2 → 
+    n1 < n2 →
     Φ #(n2 - 1) ⊢ WP FindPred #n2 #n1 @ E {{ Φ }}.
   Proof.
-    revert n1. wp_rec=> n1 Hn.
-    wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
-    - rewrite (forall_elim (n1 + 1)) const_equiv; last omega.
-      by rewrite left_id -always_wand_impl always_elim wand_elim_r.
-    - rewrite -pvs_intro. assert (n1 = n2 - 1) as -> by omega; auto with I.
+    iIntros {Hn} "HΦ". iLöb {n1 Hn} "HΦ" as "IH".
+    wp_rec. wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
+    - iApply "IH" "% HΦ". omega.
+    - iPvsIntro. by assert (n1 = n2 - 1) as -> by omega.
   Qed.
 
   Lemma Pred_spec n E Φ : ▷ Φ #(n - 1) ⊢ WP Pred #n @ E {{ Φ }}.
   Proof.
-    wp_lam. wp_op=> ?; wp_if.
+    iIntros "HΦ". wp_lam. wp_op=> ?; wp_if.
     - wp_op. wp_op.
-      ewp apply FindPred_spec; last omega.
+      wp_apply FindPred_spec; first omega.
       wp_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega.
-    - by ewp apply FindPred_spec; eauto with omega.
+    - wp_apply FindPred_spec; eauto with omega.
   Qed.
 
   Lemma Pred_user E :
     (True : iProp) ⊢ WP let: "x" := Pred #42 in ^Pred '"x" @ E {{ λ v, v = #40 }}.
-  Proof.
-    intros. ewp apply Pred_spec. wp_let. ewp apply Pred_spec. auto with I.
-  Qed.
+  Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
 End LiftingTests.
 
 Section ClosedProofs.
@@ -75,8 +68,8 @@ Section ClosedProofs.
 
   Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ λ v, v = #2 }}.
   Proof.
-    apply ht_alt. rewrite (heap_alloc nroot ⊤); last by rewrite nclose_nroot.
-    apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
-    rewrite -heap_e_spec; first by eauto with I. by rewrite nclose_nroot.
+    iProof. iIntros "! Hσ".
+    iPvs (heap_alloc nroot) "Hσ" as {h} "[? _]"; first by rewrite nclose_nroot.
+    by iApply heap_e_spec; first by rewrite nclose_nroot.
   Qed.
 End ClosedProofs.
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index 4514a09318fd9a6bc51f3cebf5e934d642662084..1ac6ff266fdf4a89b1b192f8c5cd32ea28556ee5 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -1,11 +1,12 @@
-From iris.program_logic Require Import saved_one_shot hoare tactics.
+From iris.program_logic Require Import saved_one_shot hoare.
 From iris.heap_lang.lib.barrier Require Import proof specification.
-From iris.heap_lang Require Import notation par.
+From iris.heap_lang Require Import notation par proofmode.
+From iris.proofmode Require Import invariants.
 Import uPred.
 
 Definition client eM eW1 eW2 : expr [] :=
-  (let: "b" := newbarrier #() in (eM ;; ^signal '"b") ||
-                              ((^wait '"b" ;; eW1) || (^wait '"b" ;; eW2))).
+  let: "b" := newbarrier #() in
+  (eM ;; ^signal '"b") || ((^wait '"b" ;; eW1) || (^wait '"b" ;; eW2)).
 
 Section proof.
 Context (G : cFunctor).
@@ -14,92 +15,67 @@ Context (heapN N : namespace).
 Local Notation iProp := (iPropG heap_lang Σ).
 Local Notation X := (G iProp).
 
-Definition barrier_res γ (P : X → iProp) : iProp :=
-  (∃ x:X, one_shot_own γ x ★ P x)%I.
+Definition barrier_res γ (Φ : X → iProp) : iProp :=
+  (∃ x, one_shot_own γ x ★ Φ x)%I.
 
-
-Lemma worker_spec e γ l (P Q : X → iProp) (R : iProp) :
-  R ⊢ (∀ x, {{ P x }} e {{ λ _, Q x }}) →
-  R ⊢ (recv heapN N l (barrier_res γ P)) →
-  R ⊢ WP wait (%l) ;; e {{ λ _, barrier_res γ Q }}.
+Lemma worker_spec e γ l (Φ Ψ : X → iProp) :
+  (recv heapN N l (barrier_res γ Φ) ★ ∀ x, {{ Φ x }} e {{ λ _, Ψ x }})
+  ⊢ WP wait (%l) ;; e {{ λ _, barrier_res γ Ψ }}.
 Proof.
-  intros He HΦ. rewrite -[R](idemp (∧)%I) {1}He HΦ always_and_sep_l {He HΦ}.
-  ewp (eapply wait_spec). ecancel [recv _ _ l _]. apply wand_intro_r. wp_seq.
-  rewrite /barrier_res sep_exist_l. apply exist_elim=>x.
-  rewrite (forall_elim x) /ht always_elim impl_wand !assoc.
-  to_front [P x; _ -★ _]%I. rewrite wand_elim_r !wp_frame_r.
-  apply wp_mono=>v. by rewrite -(exist_intro x) comm.
+  iIntros "[Hl #He]". wp_apply wait_spec; iFrame "Hl".
+  iIntros "Hγ"; iDestruct "Hγ" as {x} "[#Hγ Hx]".
+  wp_seq. iApply wp_wand_l. iSplitR; [|by iApply "He" "!"].
+  iIntros {v} "?"; iExists x; by iSplit.
 Qed.
 
-Context (P' : iProp) (P P1 P2 Q Q1 Q2 : X -n> iProp).
-Context {P_split : ∀ x:X, P x ⊢ (P1 x ★ P2 x)}.
-Context {Q_join  : ∀ x:X, (Q1 x ★ Q2 x) ⊢ Q x}.
+Context (P : iProp) (Φ Φ1 Φ2 Ψ Ψ1 Ψ2 : X -n> iProp).
+Context {Φ_split : ∀ x, Φ x ⊢ (Φ1 x ★ Φ2 x)}.
+Context {Ψ_join  : ∀ x, (Ψ1 x ★ Ψ2 x) ⊢ Ψ x}.
 
-Lemma P_res_split γ :
-  barrier_res γ P ⊢ (barrier_res γ P1 ★ barrier_res γ P2).
+Lemma P_res_split γ : barrier_res γ Φ ⊢ (barrier_res γ Φ1 ★ barrier_res γ Φ2).
 Proof.
-  rewrite /barrier_res. apply exist_elim=>x. do 2 rewrite -(exist_intro x).
-  rewrite P_split {1}[one_shot_own _ _]always_sep_dup.
-  solve_sep_entails.
+  iIntros "Hγ"; iDestruct "Hγ" as {x} "[#Hγ Hx]".
+  iDestruct Φ_split "Hx" as "[H1 H2]". by iSplitL "H1"; iExists x; iSplit.
 Qed.
 
-Lemma Q_res_join γ :
-  (barrier_res γ Q1 ★ barrier_res γ Q2) ⊢ ▷ barrier_res γ Q.
+Lemma Q_res_join γ : (barrier_res γ Ψ1 ★ barrier_res γ Ψ2) ⊢ ▷ barrier_res γ Ψ.
 Proof.
-  rewrite /barrier_res sep_exist_r. apply exist_elim=>x1.
-  rewrite sep_exist_l. apply exist_elim=>x2.
-  rewrite [one_shot_own γ x1]always_sep_dup.
-  to_front [one_shot_own γ x1; one_shot_own γ x2]. rewrite one_shot_agree.
-  strip_later. rewrite -(exist_intro x1) -Q_join.
-  ecancel [one_shot_own γ _; Q1 _].
-  eapply (eq_rewrite x2 x1 (λ x, Q2 x)); last by eauto with I.
-  { (* FIXME typeclass search should find this. *)
-    apply cofe_mor_ne. }
-  rewrite eq_sym. eauto with I.
+  iIntros "[Hγ Hγ']";
+  iDestruct "Hγ" as {x} "[#Hγ Hx]"; iDestruct "Hγ'" as {x'} "[#Hγ' Hx']".
+  iDestruct (one_shot_agree γ x x') "- !" as "Hxx"; first (by iSplit).
+  iNext. iRewrite -"Hxx" in "Hx'".
+  iExists x; iFrame "Hγ". iApply Ψ_join; by iSplitL "Hx".
 Qed.
 
-Lemma client_spec (eM eW1 eW2 : expr []) (eM' eW1' eW2' : expr ("b" :b: [])) (R : iProp) :
+Lemma client_spec_new (eM eW1 eW2 : expr []) (eM' eW1' eW2' : expr ("b" :b: [])) :
   heapN ⊥ N → eM' = wexpr' eM → eW1' = wexpr' eW1 → eW2' = wexpr' eW2 →
-  R ⊢ ({{ P' }} eM {{ λ _, ∃ x, P x }}) →
-  R ⊢ (∀ x, {{ P1 x }} eW1 {{ λ _, Q1 x }}) →
-  R ⊢ (∀ x, {{ P2 x }} eW2 {{ λ _, Q2 x }}) →
-  R ⊢ heap_ctx heapN →
-  R ⊢ P' →
-  R ⊢ WP client eM' eW1' eW2' {{ λ _, ∃ γ, barrier_res γ Q }}.
+  (heap_ctx heapN ★ P
+  ★ {{ P }} eM {{ λ _, ∃ x, Φ x }}
+  ★ (∀ x, {{ Φ1 x }} eW1 {{ λ _, Ψ1 x }})
+  ★ (∀ x, {{ Φ2 x }} eW2 {{ λ _, Ψ2 x }}))
+  ⊢ WP client eM' eW1' eW2' {{ λ _, ∃ γ, barrier_res γ Ψ }}.
 Proof.
-  intros HN -> -> -> HeM HeW1 HeW2 Hheap HP'.
-  rewrite -4!{1}[R](idemp (∧)%I) {1}HeM {1}HeW1 {1}HeW2 {1}Hheap {1}HP' !always_and_sep_l {Hheap} /client.
-  to_front []. rewrite one_shot_alloc !pvs_frame_r !sep_exist_r.
-  apply wp_strip_pvs, exist_elim=>γ. rewrite {1}[heap_ctx _]always_sep_dup.
-  (ewp (eapply (newbarrier_spec heapN N (barrier_res γ P)))); last done.
-  cancel [heap_ctx heapN]. apply forall_intro=>l. apply wand_intro_r.
-  set (workers_post (v : val) := (barrier_res γ Q1 ★ barrier_res γ Q2)%I).
-  wp_let. (ewp (eapply wp_par with (Ψ1 := λ _, True%I) (Ψ2 := workers_post))); last first.
-  { done. } (* FIXME why does this simple goal even appear? *)
-  rewrite {1}[heap_ctx _]always_sep_dup. cancel [heap_ctx heapN].
-  sep_split left: [one_shot_pending γ; send _ _ _ _ ; P'; {{ _ }} eM {{ _ }}]%I.
-  { (* Main thread. *)
-    wp_focus eM. rewrite /ht always_elim impl_wand wand_elim_r !wp_frame_l.
-    apply wp_mono=>v. wp_seq. rewrite !sep_exist_l. apply exist_elim=>x.
-    rewrite (one_shot_init _ γ x) !pvs_frame_r. apply wp_strip_pvs.
-    ewp (eapply signal_spec). ecancel [send _ _ _ _].
-    by rewrite /barrier_res -(exist_intro x). }
-  sep_split right: [].
-  - (* Worker threads. *)
-    rewrite recv_mono; last exact: P_res_split. rewrite (recv_split _ _ ⊤) //.
-    rewrite ?pvs_frame_r !pvs_frame_l. apply wp_strip_pvs.
-    (ewp (eapply wp_par with (Ψ1 := λ _, barrier_res γ Q1) (Ψ2 := λ _, barrier_res γ Q2))); last first.
-    { done. } ecancel [heap_ctx _].
-    sep_split left: [recv _ _ _ (barrier_res γ P1); ∀ _, {{ _ }} eW1 {{ _ }}]%I.
-    { eapply worker_spec; eauto with I. }
-    sep_split left: [recv _ _ _ (barrier_res γ P2); ∀ _, {{ _ }} eW2 {{ _ }}]%I.
-    { eapply worker_spec; eauto with I. }
-    rewrite /workers_post. do 2 apply forall_intro=>_. 
-    (* FIXME: this should work: rewrite -later_intro. *)
-    apply wand_intro_r. rewrite -later_intro. solve_sep_entails.
-  - (* Merging. *)
-    rewrite /workers_post. do 2 apply forall_intro=>_. apply wand_intro_r.
-    rewrite !left_id Q_res_join. strip_later. by rewrite -(exist_intro γ).
+  iIntros {HN -> -> ->} "/= (#Hh&HP&#He&#He1&#He2)"; rewrite /client.
+  iPvs one_shot_alloc as {γ} "Hγ".
+  wp_apply (newbarrier_spec heapN N (barrier_res γ Φ)); auto.
+  iFrame "Hh". iIntros {l} "[Hr Hs]".
+  set (workers_post (v : val) := (barrier_res γ Ψ1 ★ barrier_res γ Ψ2)%I).
+  wp_let. wp_apply (wp_par _ _ (λ _, True)%I workers_post); first done.
+  iFrame "Hh". iSplitL "HP Hs Hγ"; [|iSplitL "Hr"].
+  - wp_focus eM. iApply wp_wand_l; iSplitR "HP"; [|iApply "He" "HP"].
+    iIntros {v} "HP"; iDestruct "HP" as {x} "HP". wp_let.
+    iPvs (one_shot_init _ _ x) "Hγ" as "Hx".
+    iApply signal_spec; iFrame "Hs"; iSplit; last done.
+    iExists x; by iSplitL "Hx".
+  - iDestruct recv_weaken "[] Hr" as "Hr".
+    { iIntros "?". by iApply P_res_split "-". }
+    iPvs recv_split "Hr" as "[H1 H2]"; first done.
+    wp_apply (wp_par _ _ (λ _, barrier_res γ Ψ1)%I
+      (λ _, barrier_res γ Ψ2)%I); first done.
+    iSplit; [done|]; iSplitL "H1"; [|iSplitL "H2"].
+    + by iApply worker_spec; iSplitL "H1".
+    + by iApply worker_spec; iSplitL "H2".
+    + iIntros {v1 v2} "?". by iNext.
+  - iIntros {_ v} "[_ H]"; iPoseProof Q_res_join "H". by iNext; iExists γ.
 Qed.
-
 End proof.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 68aa967add037ddd595ea6363c27da1af3e8abf8..1ac4946399412c15b6200cc82663b43e97eb5eac 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -1,6 +1,7 @@
 From iris.algebra Require Import one_shot dec_agree.
 From iris.program_logic Require Import hoare.
-From iris.heap_lang Require Import heap assert wp_tactics notation.
+From iris.heap_lang Require Import heap assert proofmode notation.
+From iris.proofmode Require Import invariants ghost_ownership.
 Import uPred.
 
 Definition one_shot_example : val := λ: <>,
@@ -40,96 +41,44 @@ Lemma wp_one_shot (Φ : val → iProp) :
     □ WP f2 #() {{ λ g, □ WP g #() {{ λ _, True }} }} -★ Φ (f1,f2)%V)
   ⊢ WP one_shot_example #() {{ Φ }}.
 Proof.
-  wp_let.
-  wp eapply wp_alloc; eauto with I.
-  apply forall_intro=> l; apply wand_intro_l.
-  eapply sep_elim_True_l; first by apply (own_alloc OneShotPending).
-  rewrite !pvs_frame_r; apply wp_strip_pvs.
-  rewrite !sep_exist_r; apply exist_elim=>γ.
-  (* TODO: this is horrible *)
-  trans (heap_ctx heapN ★ (|==> inv N (one_shot_inv γ l)) ★
-    (∀ f1 f2 : val,
-      (∀ n : Z, □ WP f1 #n {{ λ w, w = #true ∨ w = #false }}) ★
-      □ WP f2 #() {{ λ g, □ WP g #() {{ λ _, True }} }} -★ Φ (f1, f2)%V))%I.
-  { ecancel [heap_ctx _; ∀ _, _]%I. rewrite -inv_alloc // -later_intro.
-    apply or_intro_l'. solve_sep_entails. }
-  rewrite pvs_frame_r pvs_frame_l; apply wp_strip_pvs; wp_let.
-  rewrite -pvs_intro.
-  rewrite !assoc 2!forall_elim; eapply wand_apply_r'; first done.
-  rewrite (always_sep_dup (_ ★ _)); apply sep_mono.
-  - apply forall_intro=>n. apply: always_intro. wp_let.
-    eapply (wp_inv_timeless _ _ _ (one_shot_inv γ l)); eauto 10 with I.
-    rewrite (True_intro (inv _ _)) right_id.
-    apply wand_intro_r; rewrite sep_or_l; apply or_elim.
-    + rewrite -wp_pvs.
-      wp eapply wp_cas_suc; eauto with I ndisj.
-      rewrite (True_intro (heap_ctx _)) left_id.
-      ecancel [l ↦ _]%I; apply wand_intro_l.
-      rewrite (own_update); (* FIXME: canonical structures are not working *)
-        last by apply (one_shot_update_shoot (DecAgree n : dec_agreeR _)).
-      rewrite pvs_frame_l; apply pvs_mono, sep_intro_True_r; eauto with I.
-      rewrite /one_shot_inv -or_intro_r -(exist_intro n).
-      solve_sep_entails.
-    + rewrite sep_exist_l; apply exist_elim=>m.
-      eapply wp_cas_fail with (v':=InjRV #m) (q:=1%Qp);
-        eauto with I ndisj; strip_later.
-      ecancel [l ↦ _]%I; apply wand_intro_l, sep_intro_True_r; eauto with I.
-      rewrite /one_shot_inv -or_intro_r -(exist_intro m).
-      solve_sep_entails.
-  - apply: always_intro. wp_seq.
-    wp_focus (Load (%l))%I.
-    eapply (wp_inv_timeless _ _ _ (one_shot_inv γ l)); eauto 10 with I.
-    apply wand_intro_r.
-    trans (heap_ctx heapN ★ inv N (one_shot_inv γ l) ★ ∃ v, l ↦ v ★
-      ((v = InjLV #0 ★ own γ OneShotPending) ∨
-       ∃ n : Z, v = InjRV #n ★ own γ (Shot (DecAgree n))))%I.
-    { rewrite assoc. apply sep_mono_r, or_elim.
-      + rewrite -(exist_intro (InjLV #0)). rewrite -or_intro_l const_equiv //.
-        solve_sep_entails.
-      + apply exist_elim=> n. rewrite -(exist_intro (InjRV #n)) -(exist_intro n).
-        apply sep_mono_r, or_intro_r', sep_intro_True_l; eauto with I. }
-    rewrite !sep_exist_l; apply exist_elim=> w.
-    eapply wp_load with (q:=1%Qp) (v:=w); eauto with I ndisj.
-    rewrite -later_intro; cancel [l ↦ w]%I.
-    rewrite -later_intro; apply wand_intro_l.
-    trans (heap_ctx heapN ★ inv N (one_shot_inv γ l) ★ one_shot_inv γ l ★
-      (w = InjLV #0 ∨ (∃ n : Z, w = InjRV #n ★ own γ (Shot (DecAgree n)))))%I.
-    { cancel [heap_ctx heapN]. rewrite !sep_or_l; apply or_elim.
-      + rewrite -or_intro_l. ecancel [inv _ _]%I.
-        rewrite [(_ ★ _)%I]comm -assoc. apply const_elim_sep_l=>->.
-        rewrite const_equiv // right_id /one_shot_inv -or_intro_l .
-        solve_sep_entails.
-      + rewrite -or_intro_r !sep_exist_l; apply exist_elim=> n.
-        rewrite -(exist_intro n). ecancel [inv _ _]%I.
-        rewrite [(_ ★ _)%I]comm -assoc. apply const_elim_sep_l=>->.
-        rewrite const_equiv // left_id /one_shot_inv -or_intro_r.
-        rewrite -(exist_intro n) {1}(always_sep_dup (own _ _)).
-        solve_sep_entails. }
-    cancel [one_shot_inv γ l].
-    wp_let. rewrite -pvs_intro. apply: always_intro. wp_seq.
-    rewrite !sep_or_l; apply or_elim.
-    { rewrite assoc.
-      apply const_elim_sep_r=>->. wp_case; wp_seq; rewrite -pvs_intro; eauto with I. }
-    rewrite !sep_exist_l; apply exist_elim=> n.
-    rewrite [(w=_ ★ _)%I]comm !assoc; apply const_elim_sep_r=>->.
-    (* FIXME: why do we need to fold? *)
-    wp_case; fold of_val. wp_let. wp_focus (Load (%l))%I.
-    eapply (wp_inv_timeless _ _ _ (one_shot_inv γ l)); eauto 10 with I.
-    rewrite (True_intro (inv _ _)) right_id.
-    apply wand_intro_r; rewrite sep_or_l; apply or_elim.
-    + rewrite (True_intro (heap_ctx _)) (True_intro (l ↦ _)) !left_id.
-      rewrite -own_op own_valid_l one_shot_validI /= left_absorb.
-      apply False_elim.
-    + rewrite !sep_exist_l; apply exist_elim=> m.
-      eapply wp_load with (q:=1%Qp) (v:=InjRV #m); eauto with I ndisj; strip_later.
-      cancel [l ↦ InjRV #m]%I. apply wand_intro_r.
-      rewrite (True_intro (heap_ctx heapN)) left_id.
-      rewrite -own_op own_valid_l one_shot_validI Shot_op /= discrete_valid.
-      rewrite -assoc. apply const_elim_sep_l=> /dec_agree_op_inv [->].
-      rewrite dec_agree_idemp. apply sep_intro_True_r.
-      { rewrite /one_shot_inv -or_intro_r -(exist_intro m). solve_sep_entails. }
-      wp_case; fold of_val. wp_let. rewrite -wp_assert'.
-      wp_op; by eauto using later_intro with I.
+  iIntros "[#? Hf] /=".
+  rewrite /one_shot_example. wp_seq. wp_alloc l as "Hl". wp_let.
+  iPvs (own_alloc OneShotPending) as {γ} "Hγ"; first done.
+  iPvs (inv_alloc N _ (one_shot_inv γ l)) "[Hl Hγ]" as "#HN"; first done.
+  { iNext. iLeft. by iSplitL "Hl". }
+  iPvsIntro. iApply "Hf"; iSplit.
+  - iIntros {n} "!". wp_let.
+    iInv> N as "[[Hl Hγ]|H]"; last iDestruct "H" as {m} "[Hl Hγ]".
+    + iApply wp_pvs. wp_cas_suc. iSplitL; [|by iLeft; iPvsIntro].
+      iPvs own_update "Hγ" as "Hγ".
+      { (* FIXME: canonical structures are not working *)
+        by apply (one_shot_update_shoot (DecAgree n : dec_agreeR _)). }
+      iPvsIntro; iRight; iExists n; by iSplitL "Hl".
+    + wp_cas_fail. iSplitL. iRight; iExists m; by iSplitL "Hl". by iRight.
+  - iIntros "!". wp_seq. wp_focus (! _)%E. iInv> N as "Hγ".
+    iAssert (∃ v, l ↦ v ★ ((v = InjLV #0 ★ own γ OneShotPending) ∨
+       ∃ n : Z, v = InjRV #n ★ own γ (Shot (DecAgree n))))%I as "Hv" with "-".
+    { iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as {m} "[Hl Hγ]".
+      + iExists (InjLV #0). iFrame "Hl". iLeft; by iSplit.
+      + iExists (InjRV #m). iFrame "Hl". iRight; iExists m; by iSplit. }
+    iDestruct "Hv" as {v} "[Hl Hv]". wp_load.
+    iAssert (one_shot_inv γ l ★ (v = InjLV #0 ∨ ∃ n : Z,
+      v = InjRV #n ★ own γ (Shot (DecAgree n))))%I as "[Hl #Hv]" with "-".
+    { iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as {m} "[% ?]"; subst.
+      + iSplit. iLeft; by iSplitL "Hl". by iLeft.
+      + iSplit. iRight; iExists m; by iSplitL "Hl". iRight; iExists m; by iSplit. }
+    iFrame "Hl". wp_let. iPvsIntro. iIntros "!". wp_seq.
+    iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as {m} "[% Hγ']"; subst.
+    { wp_case. wp_seq. by iPvsIntro. }
+    wp_case. wp_let. wp_focus (! _)%E.
+    iInv> N as "[[Hl Hγ]|Hinv]"; last iDestruct "Hinv" as {m'} "[Hl Hγ]".
+    { iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct own_valid "Hγ" as "%". }
+    wp_load.
+    iCombine "Hγ" "Hγ'" as "Hγ".
+    iDestruct own_valid "Hγ !" as % [=->]%dec_agree_op_inv.
+    iSplitL "Hl"; [iRight; iExists m; by iSplit|].
+    wp_case. wp_let. iApply wp_assert'. wp_op=>?; simplify_eq/=.
+    iSplit. done. by iNext.
 Qed.
 
 Lemma hoare_one_shot (Φ : val → iProp) :
@@ -139,12 +88,10 @@ Lemma hoare_one_shot (Φ : val → iProp) :
       {{ True }} Snd ff #() {{ λ g, {{ True }} g #() {{ λ _, True }} }}
     }}.
 Proof.
-  apply: always_intro; rewrite left_id -wp_one_shot /=.
-  cancel [heap_ctx heapN].
-  apply forall_intro=> f1; apply forall_intro=> f2.
-  apply wand_intro_l; rewrite right_id; apply sep_mono.
-  - apply forall_mono=>n. apply always_mono; rewrite left_id. by wp_proj.
-  - apply always_mono; rewrite left_id. wp_proj.
-    apply wp_mono=> v. by apply always_mono; rewrite left_id.
+  iIntros "#? ! _". iApply wp_one_shot. iSplit; first done.
+  iIntros {f1 f2} "[#Hf1 #Hf2]"; iSplit.
+  - iIntros {n} "! _". wp_proj. iApply "Hf1" "!".
+  - iIntros "! _". wp_proj.
+    iApply wp_wand_l; iFrame "Hf2". by iIntros {v} "#? ! _".
 Qed.
 End proof.
diff --git a/tests/proofmode.v b/tests/proofmode.v
new file mode 100644
index 0000000000000000000000000000000000000000..60a80287ef644951653cdd0240843c2093409b5c
--- /dev/null
+++ b/tests/proofmode.v
@@ -0,0 +1,42 @@
+From iris.proofmode Require Import tactics.
+
+Lemma demo_1 (M : cmraT) (P1 P2 P3 : nat → uPred M) :
+  True ⊢ (∀ (x y : nat) a b,
+    x ≡ y →
+    □ (uPred_ownM (a ⋅ b) -★
+    (∃ y1 y2 c, P1 ((x + y1) + y2) ∧ True ∧ □ uPred_ownM c) -★
+    ▷ (∀ z, P2 z) -★
+    ▷ (∀ n m : nat, P1 n → □ ((True ∧ P2 n) → □ (n = n ↔ P3 n))) -★
+    ▷ (x = 0) ∨ ∃ x z, ▷ P3 (x + z) ★ uPred_ownM b ★ uPred_ownM (core b))).
+Proof.
+  iIntros {i [|j] a b ?} "! [Ha Hb] H1 H2 H3"; setoid_subst.
+  { iLeft. by iNext. }
+  iRight.
+  iDestruct "H1" as {z1 z2 c} "(H1&_&#Hc)".
+  iRevert {a b} "Ha Hb". iIntros {b a} "Hb Ha".
+  iAssert (uPred_ownM (a â‹… core a))%I as "[Ha #Hac]" with "[Ha]".
+  { by rewrite cmra_core_r. }
+  iFrame "Ha Hac".
+  iExists (S j + z1), z2.
+  iNext.
+  iApply "H3" { _ 0 } "H1 ! [H2] !".
+  - iSplit. done. iApply "H2".
+  - done.
+Qed.
+
+Lemma demo_2 (M : cmraT) (P1 P2 P3 P4 Q : uPred M) (P5 : nat → uPredC M):
+    (P2 ★ (P3 ★ Q) ★ True ★ P1 ★ P2 ★ (P4 ★ (∃ x:nat, P5 x ∨ P3)) ★ True)
+  ⊢ (P1 -★ (True ★ True) -★ (((P2 ∧ False ∨ P2 ∧ 0 = 0) ★ P3) ★ Q ★ P1 ★ True) ∧
+     (P2 ∨ False) ∧ (False → P5 0)).
+Proof.
+  (* Intro-patterns do something :) *)
+  iIntros "[H2 ([H3 HQ]&?&H1&H2'&foo&_)] ? [??]".
+  (* To test destruct: can also be part of the intro-pattern *)
+  iDestruct "foo" as "[_ meh]".
+  repeat iSplit; [|by iLeft|iIntros "#[]"].
+  iFrame "H2".
+  (* split takes a list of hypotheses just for the LHS *)
+  iSplitL "H3".
+  * iFrame "H3". by iRight.
+  * iSplitL "HQ". iAssumption. by iSplitL "H1".
+Qed.
\ No newline at end of file