From afae72fd182e61506387a7d86b8b5aa6f59c146c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 5 Oct 2016 22:45:45 +0200
Subject: [PATCH] No longer put proof mode class instances in their own file.

---
 _CoqProject                           |  4 --
 heap_lang/adequacy.v                  |  2 +-
 heap_lang/heap.v                      |  2 +-
 heap_lang/lib/counter.v               |  2 +-
 heap_lang/lib/spawn.v                 |  2 +-
 heap_lang/lib/spin_lock.v             |  2 +-
 heap_lang/lib/ticket_lock.v           |  2 +-
 heap_lang/lifting.v                   |  2 +-
 heap_lang/proofmode.v                 |  3 +-
 program_logic/adequacy.v              |  2 +-
 program_logic/auth.v                  |  4 +-
 program_logic/boxes.v                 |  4 +-
 program_logic/cancelable_invariants.v |  2 +-
 program_logic/ectx_lifting.v          |  2 +-
 program_logic/ghost_ownership.v       | 14 +++++++
 program_logic/hoare.v                 |  2 +-
 program_logic/invariants.v            | 28 +++++++++++++-
 program_logic/lifting.v               |  2 +-
 program_logic/ownership.v             |  2 +-
 program_logic/pviewshifts.v           | 53 +++++++++++++++++++++++++-
 program_logic/sts.v                   |  4 +-
 program_logic/thread_local.v          |  3 +-
 program_logic/viewshifts.v            |  4 +-
 program_logic/weakestpre.v            | 31 ++++++++++++++-
 proofmode/ghost_ownership.v           | 15 --------
 proofmode/invariants.v                | 29 --------------
 proofmode/pviewshifts.v               | 54 ---------------------------
 proofmode/weakestpre.v                | 32 ----------------
 tests/atomic.v                        |  3 +-
 tests/counter.v                       |  2 +-
 tests/joining_existentials.v          |  2 +-
 tests/one_shot.v                      |  2 +-
 tests/proofmode.v                     |  2 +-
 33 files changed, 153 insertions(+), 166 deletions(-)
 delete mode 100644 proofmode/ghost_ownership.v
 delete mode 100644 proofmode/invariants.v
 delete mode 100644 proofmode/pviewshifts.v
 delete mode 100644 proofmode/weakestpre.v

diff --git a/_CoqProject b/_CoqProject
index 1a100843d..6f18679ed 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -116,15 +116,11 @@ tests/list_reverse.v
 tests/tree_sum.v
 tests/counter.v
 proofmode/coq_tactics.v
-proofmode/pviewshifts.v
 proofmode/environments.v
 proofmode/intro_patterns.v
 proofmode/spec_patterns.v
 proofmode/sel_patterns.v
 proofmode/tactics.v
 proofmode/notation.v
-proofmode/invariants.v
-proofmode/weakestpre.v
-proofmode/ghost_ownership.v
 proofmode/classes.v
 proofmode/class_instances.v
diff --git a/heap_lang/adequacy.v b/heap_lang/adequacy.v
index 89990989d..a5c116b0b 100644
--- a/heap_lang/adequacy.v
+++ b/heap_lang/adequacy.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre adequacy.
 From iris.heap_lang Require Export heap.
 From iris.program_logic Require Import auth ownership.
 From iris.heap_lang Require Import proofmode notation.
-From iris.proofmode Require Import tactics weakestpre.
+From iris.proofmode Require Import tactics.
 
 Definition heapΣ : gFunctors := #[authΣ heapUR; irisΣ heap_lang].
 
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 58f5b6192..11f538b90 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -2,7 +2,7 @@ From iris.heap_lang Require Export lifting.
 From iris.algebra Require Import upred_big_op gmap frac dec_agree.
 From iris.program_logic Require Export invariants ghost_ownership.
 From iris.program_logic Require Import ownership auth.
-From iris.proofmode Require Import weakestpre.
+From iris.proofmode Require Import tactics.
 Import uPred.
 (* TODO: The entire construction could be generalized to arbitrary languages that have
    a finmap as their state. Or maybe even beyond "as their state", i.e. arbitrary
diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v
index f318d1b6b..96769c478 100644
--- a/heap_lang/lib/counter.v
+++ b/heap_lang/lib/counter.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
-From iris.proofmode Require Import invariants tactics.
+From iris.proofmode Require Import tactics.
 From iris.program_logic Require Import auth.
 From iris.heap_lang Require Import proofmode notation.
 
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index ce437f6ca..05a045314 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
-From iris.proofmode Require Import invariants tactics.
+From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import excl.
 
diff --git a/heap_lang/lib/spin_lock.v b/heap_lang/lib/spin_lock.v
index 138568fff..71db16199 100644
--- a/heap_lang/lib/spin_lock.v
+++ b/heap_lang/lib/spin_lock.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
-From iris.proofmode Require Import invariants tactics.
+From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import excl.
 From iris.heap_lang.lib Require Import lock.
diff --git a/heap_lang/lib/ticket_lock.v b/heap_lang/lib/ticket_lock.v
index d4994cd76..157b85465 100644
--- a/heap_lang/lib/ticket_lock.v
+++ b/heap_lang/lib/ticket_lock.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
-From iris.proofmode Require Import invariants.
+From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import auth gset.
 From iris.heap_lang.lib Require Export lock.
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 3c8b7494f..278165adb 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import ownership ectx_lifting. (* for ownP *)
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics.
-From iris.proofmode Require Import weakestpre.
+From iris.proofmode Require Import tactics.
 From iris.prelude Require Import fin_maps.
 Import uPred.
 
diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index 1a0a66e79..9e07d30d9 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -1,5 +1,6 @@
+From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import coq_tactics.
-From iris.proofmode Require Export weakestpre.
+From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Export wp_tactics heap.
 Import uPred.
 
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index 5569939f7..4b6540a71 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -1,7 +1,7 @@
 From iris.program_logic Require Export weakestpre.
 From iris.algebra Require Import gmap auth agree gset coPset upred_big_op.
 From iris.program_logic Require Import ownership.
-From iris.proofmode Require Import tactics weakestpre.
+From iris.proofmode Require Import tactics.
 Import uPred.
 
 Record adequate {Λ} (e1 : expr Λ) (σ1 : state Λ) (φ : val Λ → Prop) := {
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 99231ad4b..d8a586dbe 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -1,7 +1,7 @@
-From iris.program_logic Require Export pviewshifts.
+From iris.program_logic Require Export invariants.
 From iris.algebra Require Export auth.
 From iris.algebra Require Import gmap.
-From iris.proofmode Require Import invariants.
+From iris.proofmode Require Import tactics.
 Import uPred.
 
 (* The CMRA we need. *)
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index fc41df57d..f5ea2bb99 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -1,6 +1,6 @@
-From iris.program_logic Require Export pviewshifts.
+From iris.program_logic Require Export invariants.
 From iris.algebra Require Import auth gmap agree upred_big_op.
-From iris.proofmode Require Import tactics invariants.
+From iris.proofmode Require Import tactics.
 Import uPred.
 
 (** The CMRAs we need. *)
diff --git a/program_logic/cancelable_invariants.v b/program_logic/cancelable_invariants.v
index a7fadea60..486f22b64 100644
--- a/program_logic/cancelable_invariants.v
+++ b/program_logic/cancelable_invariants.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export invariants.
 From iris.algebra Require Export frac.
-From iris.proofmode Require Import invariants tactics.
+From iris.proofmode Require Import tactics.
 Import uPred.
 
 Class cinvG Σ := cinv_inG :> inG Σ fracR.
diff --git a/program_logic/ectx_lifting.v b/program_logic/ectx_lifting.v
index 0c35491a5..b43ead95e 100644
--- a/program_logic/ectx_lifting.v
+++ b/program_logic/ectx_lifting.v
@@ -1,7 +1,7 @@
 (** Some derived lemmas for ectx-based languages *)
 From iris.program_logic Require Export ectx_language weakestpre lifting.
 From iris.program_logic Require Import ownership.
-From iris.proofmode Require Import weakestpre.
+From iris.proofmode Require Import tactics.
 
 Section wp.
 Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index 721feaa00..dc9840967 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -1,5 +1,6 @@
 From iris.program_logic Require Export model.
 From iris.algebra Require Import iprod gmap.
+From iris.proofmode Require Import classes.
 Import uPred.
 
 (** The class [inG Σ A] expresses that the CMRA [A] is in the list of functors
@@ -145,3 +146,16 @@ Proof.
   - apply cmra_transport_valid, ucmra_unit_valid.
   - intros x; destruct inG_prf. by rewrite left_id.
 Qed.
+
+(** Proofmode class instances *)
+Section proofmode_classes.
+  Context `{inG Σ A}.
+  Implicit Types a b : A.
+
+  Global Instance into_and_own p γ a b1 b2 :
+    IntoOp a b1 b2 → IntoAnd p (own γ a) (own γ b1) (own γ b2).
+  Proof. intros. apply mk_into_and_sep. by rewrite (into_op a) own_op. Qed.
+  Global Instance from_sep_own γ a b1 b2 :
+    FromOp a b1 b2 → FromSep (own γ a) (own γ b1) (own γ b2).
+  Proof. intros. by rewrite /FromSep -own_op from_op. Qed.
+End proofmode_classes.
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 817a21e29..912f193a0 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Export weakestpre viewshifts.
-From iris.proofmode Require Import weakestpre.
+From iris.proofmode Require Import tactics.
 
 Definition ht `{irisG Λ Σ} (E : coPset) (P : iProp Σ)
     (e : expr Λ) (Φ : val Λ → iProp Σ) : iProp Σ :=
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index ca670bf1b..08b7407ae 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export pviewshifts.
 From iris.program_logic Require Export namespaces.
 From iris.program_logic Require Import ownership.
 From iris.algebra Require Import gmap.
-From iris.proofmode Require Import pviewshifts.
+From iris.proofmode Require Import tactics coq_tactics intro_patterns.
 Import uPred.
 
 (** Derived forms and lemmas about them. *)
@@ -61,3 +61,29 @@ Proof.
   iIntros "!==> {$HP} HP". iApply "Hclose"; auto.
 Qed.
 End inv.
+
+Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
+  let Htmp := iFresh in
+  let patback := intro_pat.parse_one Hclose in
+  let pat := constr:(IList [[IName Htmp; patback]]) in
+  iVs (inv_open _ N with "[#]") as pat;
+    [idtac|iAssumption || fail "iInv: invariant" N "not found"|idtac];
+    [solve_ndisj || match goal with |- ?P => fail "iInv: cannot solve" P end
+    |tac Htmp].
+
+Tactic Notation "iInv" constr(N) "as" constr(pat) constr(Hclose) :=
+   iInvCore N as (fun H => iDestruct H as pat) Hclose.
+Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1) ")"
+    constr(pat) constr(Hclose) :=
+   iInvCore N as (fun H => iDestruct H as (x1) pat) Hclose.
+Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) ")" constr(pat) constr(Hclose) :=
+   iInvCore N as (fun H => iDestruct H as (x1 x2) pat) Hclose.
+Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) ")"
+    constr(pat) constr(Hclose) :=
+   iInvCore N as (fun H => iDestruct H as (x1 x2 x3) pat) Hclose.
+Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
+    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
+    constr(pat) constr(Hclose) :=
+   iInvCore N as (fun H => iDestruct H as (x1 x2 x3 x4) pat) Hclose.
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 16ef16d2a..c27eea3e8 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -1,7 +1,7 @@
 From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import ownership.
 From iris.algebra Require Export upred_big_op.
-From iris.proofmode Require Import pviewshifts.
+From iris.proofmode Require Import tactics.
 
 Section lifting.
 Context `{irisG Λ Σ}.
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index efe524366..6af5bfac1 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export iris.
 From iris.algebra Require Import gmap auth agree gset coPset upred_big_op.
-From iris.proofmode Require Import ghost_ownership tactics.
+From iris.proofmode Require Import tactics.
 
 Definition invariant_unfold {Σ} (P : iProp Σ) : agree (later (iPreProp Σ)) :=
   to_agree (Next (iProp_unfold P)).
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 971cbaa60..540074e9c 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -1,7 +1,7 @@
 From iris.program_logic Require Export iris.
 From iris.program_logic Require Import ownership.
 From iris.algebra Require Import upred_big_op gmap.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import tactics classes.
 Import uPred.
 
 Program Definition pvs_def `{irisG Λ Σ}
@@ -136,3 +136,54 @@ Proof.
   intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -pvs_sep.
 Qed.
 End pvs.
+
+(** Proofmode class instances *)
+Section proofmode_classes.
+  Context `{irisG Λ Σ}.
+  Implicit Types P Q : iProp Σ.
+
+  Global Instance from_pure_pvs E P φ : FromPure P φ → FromPure (|={E}=> P) φ.
+  Proof. rewrite /FromPure. intros <-. apply pvs_intro. Qed.
+
+  Global Instance from_assumption_pvs E p P Q :
+    FromAssumption p P (|=r=> Q) → FromAssumption p P (|={E}=> Q)%I.
+  Proof. rewrite /FromAssumption=>->. apply rvs_pvs. Qed.
+
+  Global Instance into_wand_pvs E1 E2 R P Q :
+    IntoWand R P Q → IntoWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
+  Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
+
+  Global Instance from_sep_pvs E P Q1 Q2 :
+    FromSep P Q1 Q2 → FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
+  Proof. rewrite /FromSep=><-. apply pvs_sep. Qed.
+
+  Global Instance or_split_pvs E1 E2 P Q1 Q2 :
+    FromOr P Q1 Q2 → FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
+  Proof. rewrite /FromOr=><-. apply or_elim; apply pvs_mono; auto with I. Qed.
+
+  Global Instance exists_split_pvs {A} E1 E2 P (Φ : A → iProp Σ) :
+    FromExist P Φ → FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
+  Proof.
+    rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
+  Qed.
+
+  Global Instance frame_pvs E1 E2 R P Q :
+    Frame R P Q → Frame R (|={E1,E2}=> P) (|={E1,E2}=> Q).
+  Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.
+
+  Global Instance is_except_last_pvs E1 E2 P : IsExceptLast (|={E1,E2}=> P).
+  Proof. by rewrite /IsExceptLast except_last_pvs. Qed.
+
+  Global Instance from_vs_pvs E P : FromVs (|={E}=> P) P.
+  Proof. by rewrite /FromVs -rvs_pvs. Qed.
+
+  Global Instance elim_vs_rvs_pvs E1 E2 P Q :
+    ElimVs (|=r=> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q).
+  Proof. by rewrite /ElimVs (rvs_pvs E1) pvs_frame_r wand_elim_r pvs_trans. Qed.
+  Global Instance elim_vs_pvs_pvs E1 E2 E3 P Q :
+    ElimVs (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
+  Proof. by rewrite /ElimVs pvs_frame_r wand_elim_r pvs_trans. Qed.
+End proofmode_classes.
+
+Hint Extern 2 (coq_tactics.of_envs _ ⊢ _) =>
+  match goal with |- _ ⊢ |={_}=> _ => iVsIntro end.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index a27c28ce6..5163df446 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -1,6 +1,6 @@
-From iris.program_logic Require Export pviewshifts.
+From iris.program_logic Require Export invariants.
 From iris.algebra Require Export sts.
-From iris.proofmode Require Import invariants.
+From iris.proofmode Require Import tactics.
 Import uPred.
 
 (** The CMRA we need. *)
diff --git a/program_logic/thread_local.v b/program_logic/thread_local.v
index d3126bf03..5be913c45 100644
--- a/program_logic/thread_local.v
+++ b/program_logic/thread_local.v
@@ -1,5 +1,6 @@
+From iris.program_logic Require Export invariants.
 From iris.algebra Require Export gmap gset coPset.
-From iris.proofmode Require Import invariants tactics.
+From iris.proofmode Require Import tactics.
 Import uPred.
 
 Definition tlN : namespace := nroot .@ "tl".
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index d7b188265..13a286abb 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -1,5 +1,5 @@
-From iris.program_logic Require Export pviewshifts.
-From iris.proofmode Require Import pviewshifts invariants.
+From iris.program_logic Require Export invariants.
+From iris.proofmode Require Import tactics.
 
 Definition vs `{irisG Λ Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
   (□ (P → |={E1,E2}=> Q))%I.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 432700e15..9c8d93f85 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export pviewshifts.
 From iris.program_logic Require Import ownership.
 From iris.algebra Require Import upred_big_op.
 From iris.prelude Require Export coPset.
-From iris.proofmode Require Import tactics pviewshifts.
+From iris.proofmode Require Import tactics classes.
 Import uPred.
 
 Definition wp_pre `{irisG Λ Σ}
@@ -211,3 +211,32 @@ Lemma wp_wand_r E e Φ Ψ :
   WP e @ E {{ Φ }} ★ (∀ v, Φ v -★ Ψ v) ⊢ WP e @ E {{ Ψ }}.
 Proof. by rewrite comm wp_wand_l. Qed.
 End wp.
+
+(** Proofmode class instances *)
+Section proofmode_classes.
+  Context `{irisG Λ Σ}.
+  Implicit Types P Q : iProp Σ.
+  Implicit Types Φ : val Λ → iProp Σ.
+
+  Global Instance frame_wp E e R Φ Ψ :
+    (∀ v, Frame R (Φ v) (Ψ v)) → Frame R (WP e @ E {{ Φ }}) (WP e @ E {{ Ψ }}).
+  Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
+
+  Global Instance is_except_last_wp E e Φ : IsExceptLast (WP e @ E {{ Φ }}).
+  Proof. by rewrite /IsExceptLast -{2}pvs_wp -except_last_pvs -pvs_intro. Qed.
+
+  Global Instance elim_vs_rvs_wp E e P Φ :
+    ElimVs (|=r=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
+  Proof. by rewrite /ElimVs (rvs_pvs E) pvs_frame_r wand_elim_r pvs_wp. Qed.
+
+  Global Instance elim_vs_pvs_wp E e P Φ :
+    ElimVs (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
+  Proof. by rewrite /ElimVs pvs_frame_r wand_elim_r pvs_wp. Qed.
+
+  (* lower precedence, if possible, it should always pick elim_vs_pvs_wp *)
+  Global Instance elim_vs_pvs_wp_atomic E1 E2 e P Φ :
+    atomic e →
+    ElimVs (|={E1,E2}=> P) P
+           (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
+  Proof. intros. by rewrite /ElimVs pvs_frame_r wand_elim_r wp_atomic. Qed.
+End proofmode_classes.
diff --git a/proofmode/ghost_ownership.v b/proofmode/ghost_ownership.v
deleted file mode 100644
index d09303599..000000000
--- a/proofmode/ghost_ownership.v
+++ /dev/null
@@ -1,15 +0,0 @@
-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 into_and_own p γ a b1 b2 :
-  IntoOp a b1 b2 → IntoAnd p (own γ a) (own γ b1) (own γ b2).
-Proof. intros. apply mk_into_and_sep. by rewrite (into_op a) own_op. Qed.
-Global Instance from_sep_own γ a b1 b2 :
-  FromOp a b1 b2 → FromSep (own γ a) (own γ b1) (own γ b2).
-Proof. intros. by rewrite /FromSep -own_op from_op. Qed.
-End ghost.
diff --git a/proofmode/invariants.v b/proofmode/invariants.v
deleted file mode 100644
index d5813093e..000000000
--- a/proofmode/invariants.v
+++ /dev/null
@@ -1,29 +0,0 @@
-From iris.proofmode Require Export tactics pviewshifts.
-From iris.program_logic Require Export invariants.
-From iris.proofmode Require Import coq_tactics intro_patterns.
-
-Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
-  let Htmp := iFresh in
-  let patback := intro_pat.parse_one Hclose in
-  let pat := constr:(IList [[IName Htmp; patback]]) in
-  iVs (inv_open _ N with "[#]") as pat;
-    [idtac|iAssumption || fail "iInv: invariant" N "not found"|idtac];
-    [solve_ndisj || match goal with |- ?P => fail "iInv: cannot solve" P end
-    |tac Htmp].
-
-Tactic Notation "iInv" constr(N) "as" constr(pat) constr(Hclose) :=
-   iInvCore N as (fun H => iDestruct H as pat) Hclose.
-Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1) ")"
-    constr(pat) constr(Hclose) :=
-   iInvCore N as (fun H => iDestruct H as (x1) pat) Hclose.
-Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
-    simple_intropattern(x2) ")" constr(pat) constr(Hclose) :=
-   iInvCore N as (fun H => iDestruct H as (x1 x2) pat) Hclose.
-Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
-    simple_intropattern(x2) simple_intropattern(x3) ")"
-    constr(pat) constr(Hclose) :=
-   iInvCore N as (fun H => iDestruct H as (x1 x2 x3) pat) Hclose.
-Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
-    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
-    constr(pat) constr(Hclose) :=
-   iInvCore N as (fun H => iDestruct H as (x1 x2 x3 x4) pat) Hclose.
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
deleted file mode 100644
index 599068a75..000000000
--- a/proofmode/pviewshifts.v
+++ /dev/null
@@ -1,54 +0,0 @@
-From iris.proofmode Require Import coq_tactics.
-From iris.proofmode Require Export tactics ghost_ownership.
-From iris.program_logic Require Export pviewshifts.
-Import uPred.
-
-Section pvs.
-Context `{irisG Λ Σ}.
-Implicit Types P Q : iProp Σ.
-
-Global Instance from_pure_pvs E P φ : FromPure P φ → FromPure (|={E}=> P) φ.
-Proof. rewrite /FromPure. intros <-. apply pvs_intro. Qed.
-
-Global Instance from_assumption_pvs E p P Q :
-  FromAssumption p P (|=r=> Q) → FromAssumption p P (|={E}=> Q)%I.
-Proof. rewrite /FromAssumption=>->. apply rvs_pvs. Qed.
-
-Global Instance into_wand_pvs E1 E2 R P Q :
-  IntoWand R P Q → IntoWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
-Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
-
-Global Instance from_sep_pvs E P Q1 Q2 :
-  FromSep P Q1 Q2 → FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
-Proof. rewrite /FromSep=><-. apply pvs_sep. Qed.
-
-Global Instance or_split_pvs E1 E2 P Q1 Q2 :
-  FromOr P Q1 Q2 → FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
-Proof. rewrite /FromOr=><-. apply or_elim; apply pvs_mono; auto with I. Qed.
-
-Global Instance exists_split_pvs {A} E1 E2 P (Φ : A → iProp Σ) :
-  FromExist P Φ → FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
-Proof.
-  rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
-Qed.
-
-Global Instance frame_pvs E1 E2 R P Q :
-  Frame R P Q → Frame R (|={E1,E2}=> P) (|={E1,E2}=> Q).
-Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.
-
-Global Instance is_except_last_pvs E1 E2 P : IsExceptLast (|={E1,E2}=> P).
-Proof. by rewrite /IsExceptLast except_last_pvs. Qed.
-
-Global Instance from_vs_pvs E P : FromVs (|={E}=> P) P.
-Proof. by rewrite /FromVs -rvs_pvs. Qed.
-
-Global Instance elim_vs_rvs_pvs E1 E2 P Q :
-  ElimVs (|=r=> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 2.
-Proof. by rewrite /ElimVs (rvs_pvs E1) pvs_frame_r wand_elim_r pvs_trans. Qed.
-Global Instance elim_vs_pvs_pvs E1 E2 E3 P Q :
-  ElimVs (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q) | 1.
-Proof. by rewrite /ElimVs pvs_frame_r wand_elim_r pvs_trans. Qed.
-End pvs.
-
-Hint Extern 2 (of_envs _ ⊢ _) =>
-  match goal with |- _ ⊢ |={_}=> _ => iVsIntro end.
diff --git a/proofmode/weakestpre.v b/proofmode/weakestpre.v
deleted file mode 100644
index 09e31c181..000000000
--- a/proofmode/weakestpre.v
+++ /dev/null
@@ -1,32 +0,0 @@
-From iris.proofmode Require Export classes pviewshifts.
-From iris.proofmode Require Import coq_tactics.
-From iris.program_logic Require Export weakestpre.
-Import uPred.
-
-Section weakestpre.
-Context `{irisG Λ Σ}.
-Implicit Types P Q : iProp Σ.
-Implicit Types Φ : val Λ → iProp Σ.
-
-Global Instance frame_wp E e R Φ Ψ :
-  (∀ v, Frame R (Φ v) (Ψ v)) → Frame R (WP e @ E {{ Φ }}) (WP e @ E {{ Ψ }}).
-Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
-
-Global Instance is_except_last_wp E e Φ : IsExceptLast (WP e @ E {{ Φ }}).
-Proof. by rewrite /IsExceptLast -{2}pvs_wp -except_last_pvs -pvs_intro. Qed.
-
-Global Instance elim_vs_rvs_wp E e P Φ :
-  ElimVs (|=r=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}) | 2.
-Proof. by rewrite /ElimVs (rvs_pvs E) pvs_frame_r wand_elim_r pvs_wp. Qed.
-
-Global Instance elim_vs_pvs_wp E e P Φ :
-  ElimVs (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}) | 1.
-Proof. by rewrite /ElimVs pvs_frame_r wand_elim_r pvs_wp. Qed.
-
-(* lower precedence, if possible, it should always pick elim_vs_pvs_wp *)
-Global Instance elim_vs_pvs_wp_atomic E1 E2 e P Φ :
-  atomic e →
-  ElimVs (|={E1,E2}=> P) P
-         (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
-Proof. intros. by rewrite /ElimVs pvs_frame_r wand_elim_r wp_atomic. Qed.
-End weakestpre.
diff --git a/tests/atomic.v b/tests/atomic.v
index a26f9ee60..0b978bab8 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -1,7 +1,7 @@
 From iris.program_logic Require Export hoare weakestpre pviewshifts ownership.
 From iris.algebra Require Import upred_big_op.
 From iris.prelude Require Export coPset.
-From iris.proofmode Require Import tactics pviewshifts weakestpre.
+From iris.proofmode Require Import tactics.
 Import uPred.
 
 Section atomic.
@@ -42,7 +42,6 @@ Section atomic.
 End atomic.
 
 From iris.heap_lang Require Export lang proofmode notation.
-From iris.proofmode Require Import invariants.
 
 Section incr.
   Context `{!heapG Σ} (N : namespace).
diff --git a/tests/counter.v b/tests/counter.v
index 8d5bb62c1..92d7c61c2 100644
--- a/tests/counter.v
+++ b/tests/counter.v
@@ -5,7 +5,7 @@ under max can be found in `heap_lang/lib/counter.v`. *)
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.program_logic Require Export hoare.
-From iris.proofmode Require Import invariants tactics.
+From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
 Import uPred.
 
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index 78adb9719..3aa32e4ff 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -3,7 +3,7 @@ From iris.heap_lang Require Export lang.
 From iris.algebra Require Import excl agree csum.
 From iris.heap_lang.lib.barrier Require Import proof specification.
 From iris.heap_lang Require Import notation par proofmode.
-From iris.proofmode Require Import invariants.
+From iris.proofmode Require Import tactics.
 
 Definition one_shotR (Σ : gFunctors) (F : cFunctor) :=
   csumR (exclR unitC) (agreeR $ laterC $ F (iPreProp Σ)).
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 92598f562..1bf218843 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
 From iris.algebra Require Import excl dec_agree csum.
 From iris.heap_lang Require Import assert proofmode notation.
-From iris.proofmode Require Import invariants.
+From iris.proofmode Require Import tactics.
 
 Definition one_shot_example : val := λ: <>,
   let: "x" := ref NONE in (
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 496993c03..73f1f0a83 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From iris.proofmode Require Import pviewshifts invariants.
+From iris.program_logic Require Import invariants.
 
 Lemma demo_0 {M : ucmraT} (P Q : uPred M) :
   □ (P ∨ Q) ⊢ (∀ x, x = 0 ∨ x = 1) → (Q ∨ P).
-- 
GitLab