diff --git a/_CoqProject b/_CoqProject
index fdfda5bfd88b4a21bba3f60bceb2b135fbb8b12f..eb0723ecaac62d28e1a208a9181461ffcccb9f7a 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -27,7 +27,8 @@ theories/algebra/deprecated.v
theories/algebra/proofmode_classes.v
theories/bi/interface.v
theories/bi/derived_connectives.v
-theories/bi/derived_laws.v
+theories/bi/derived_laws_bi.v
+theories/bi/derived_laws_sbi.v
theories/bi/plainly.v
theories/bi/big_op.v
theories/bi/updates.v
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 2f4352e1d769aaa453d04087d31d757e6383a8c2..8686bc3939499f0341591c34997b63a274069874 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -1,8 +1,7 @@
From iris.base_logic Require Export upred.
-From iris.bi Require Export derived_laws.
+From iris.bi Require Export bi.
Set Default Proof Using "Type".
-Import upred.uPred.
-Import interface.bi derived_laws.bi.
+Import upred.uPred bi.
Module uPred.
Section derived.
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 4fe308424257bf7b870f7091073562b357f8ff20..82739945d0122589cc5d02c1461d3b9a753c8527 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -100,8 +100,7 @@ Qed.
Lemma box_alloc : box N ∅ True%I.
Proof.
- iIntros; iExists (λ _, True)%I; iSplit; last by auto.
- iNext. by rewrite big_opM_empty.
+ iIntros. iExists (λ _, True)%I. iSplit; by auto.
Qed.
Lemma slice_insert_empty E q f Q P :
diff --git a/theories/bi/bi.v b/theories/bi/bi.v
index d00050dc4309fbd0a9f0b4f3fbfd6b50001e244c..b1d4c8a7826b010556fbd4783ca6a587c0b4ea1d 100644
--- a/theories/bi/bi.v
+++ b/theories/bi/bi.v
@@ -1,9 +1,11 @@
-From iris.bi Require Export derived_laws big_op updates plainly embedding.
+From iris.bi Require Export derived_laws_bi derived_laws_sbi
+ big_op updates plainly embedding.
Set Default Proof Using "Type".
Module Import bi.
Export bi.interface.bi.
- Export bi.derived_laws.bi.
+ Export bi.derived_laws_bi.bi.
+ Export bi.derived_laws_sbi.bi.
Export bi.big_op.bi.
End bi.
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index dc04b291af6d325a3d7117f9c23c5c129e557998..593bc540b0d161a8b3c0b01d6d1ee88a0aae843f 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -1,6 +1,5 @@
From iris.algebra Require Export big_op.
-From iris.bi Require Export derived_laws.
-From iris.bi Require Import plainly.
+From iris.bi Require Import derived_laws_sbi plainly.
From stdpp Require Import countable fin_collections functions.
Set Default Proof Using "Type".
@@ -42,7 +41,7 @@ Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P) X)
(** * Properties *)
Module bi.
-Import interface.bi derived_laws.bi.
+Import interface.bi derived_laws_bi.bi.
Section bi_big_op.
Context {PROP : bi}.
Implicit Types Ps Qs : list PROP.
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws_bi.v
similarity index 73%
rename from theories/bi/derived_laws.v
rename to theories/bi/derived_laws_bi.v
index 3b96f873ebe5f8e64e162532042468c179df97cd..c8e0f57dd67146e83b85be8818b87f562aa2b505 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws_bi.v
@@ -1439,492 +1439,4 @@ Global Instance limit_preserving_Persistent {A:ofeT} `{Cofe A} (Φ : A → PROP)
Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
End bi_derived.
-Section sbi_derived.
-Context {PROP : sbi}.
-Implicit Types φ : Prop.
-Implicit Types P Q R : PROP.
-Implicit Types Ps : list PROP.
-Implicit Types A : Type.
-
-(* Force implicit argument PROP *)
-Notation "P ⊢ Q" := (@bi_entails PROP P%I Q%I).
-Notation "P ⊣⊢ Q" := (equiv (A:=bi_car PROP) P%I Q%I).
-
-Hint Resolve or_elim or_intro_l' or_intro_r' True_intro False_elim.
-Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro.
-
-Global Instance internal_eq_proper (A : ofeT) :
- Proper ((≡) ==> (≡) ==> (⊣⊢)) (@sbi_internal_eq PROP A) := ne_proper_2 _.
-Global Instance later_proper :
- Proper ((⊣⊢) ==> (⊣⊢)) (@sbi_later PROP) := ne_proper _.
-
-(* Equality *)
-Hint Resolve internal_eq_refl.
-Hint Extern 100 (NonExpansive _) => solve_proper.
-
-Lemma equiv_internal_eq {A : ofeT} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
-Proof. intros ->. auto. Qed.
-Lemma internal_eq_rewrite' {A : ofeT} a b (Ψ : A → PROP) P
- {HΨ : NonExpansive Ψ} : (P ⊢ a ≡ b) → (P ⊢ Ψ a) → P ⊢ Ψ b.
-Proof.
- intros Heq HΨa. rewrite -(idemp bi_and P) {1}Heq HΨa.
- apply impl_elim_l'. by apply internal_eq_rewrite.
-Qed.
-
-Lemma internal_eq_sym {A : ofeT} (a b : A) : a ≡ b ⊢ b ≡ a.
-Proof. apply (internal_eq_rewrite' a b (λ b, b ≡ a)%I); auto. Qed.
-Lemma internal_eq_iff P Q : P ≡ Q ⊢ P ↔ Q.
-Proof. apply (internal_eq_rewrite' P Q (λ Q, P ↔ Q))%I; auto using iff_refl. Qed.
-
-Lemma f_equiv {A B : ofeT} (f : A → B) `{!NonExpansive f} x y :
- x ≡ y ⊢ f x ≡ f y.
-Proof. apply (internal_eq_rewrite' x y (λ y, f x ≡ f y)%I); auto. Qed.
-
-Lemma prod_equivI {A B : ofeT} (x y : A * B) : x ≡ y ⊣⊢ x.1 ≡ y.1 ∧ x.2 ≡ y.2.
-Proof.
- apply (anti_symm _).
- - apply and_intro; apply f_equiv; apply _.
- - rewrite {3}(surjective_pairing x) {3}(surjective_pairing y).
- apply (internal_eq_rewrite' (x.1) (y.1) (λ a, (x.1,x.2) ≡ (a,y.2))%I); auto.
- apply (internal_eq_rewrite' (x.2) (y.2) (λ b, (x.1,x.2) ≡ (x.1,b))%I); auto.
-Qed.
-Lemma sum_equivI {A B : ofeT} (x y : A + B) :
- x ≡ y ⊣⊢
- match x, y with
- | inl a, inl a' => a ≡ a' | inr b, inr b' => b ≡ b' | _, _ => False
- end.
-Proof.
- apply (anti_symm _).
- - apply (internal_eq_rewrite' x y (λ y,
- match x, y with
- | inl a, inl a' => a ≡ a' | inr b, inr b' => b ≡ b' | _, _ => False
- end)%I); auto.
- destruct x; auto.
- - destruct x as [a|b], y as [a'|b']; auto; apply f_equiv, _.
-Qed.
-Lemma option_equivI {A : ofeT} (x y : option A) :
- x ≡ y ⊣⊢ match x, y with
- | Some a, Some a' => a ≡ a' | None, None => True | _, _ => False
- end.
-Proof.
- apply (anti_symm _).
- - apply (internal_eq_rewrite' x y (λ y,
- match x, y with
- | Some a, Some a' => a ≡ a' | None, None => True | _, _ => False
- end)%I); auto.
- destruct x; auto.
- - destruct x as [a|], y as [a'|]; auto. apply f_equiv, _.
-Qed.
-
-Lemma sig_equivI {A : ofeT} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊣⊢ x ≡ y.
-Proof. apply (anti_symm _). apply sig_eq. apply f_equiv, _. Qed.
-
-Lemma ofe_fun_equivI {A} {B : A → ofeT} (f g : ofe_fun B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
-Proof.
- apply (anti_symm _); auto using fun_ext.
- apply (internal_eq_rewrite' f g (λ g, ∀ x : A, f x ≡ g x)%I); auto.
- intros n h h' Hh; apply forall_ne=> x; apply internal_eq_ne; auto.
-Qed.
-Lemma ofe_morC_equivI {A B : ofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
-Proof.
- apply (anti_symm _).
- - apply (internal_eq_rewrite' f g (λ g, ∀ x : A, f x ≡ g x)%I); auto.
- - rewrite -(ofe_fun_equivI (ofe_mor_car _ _ f) (ofe_mor_car _ _ g)).
- set (h1 (f : A -n> B) :=
- exist (λ f : A -c> B, NonExpansive (f : A → B)) f (ofe_mor_ne A B f)).
- set (h2 (f : sigC (λ f : A -c> B, NonExpansive (f : A → B))) :=
- @CofeMor A B (`f) (proj2_sig f)).
- assert (∀ f, h2 (h1 f) = f) as Hh by (by intros []).
- assert (NonExpansive h2) by (intros ??? EQ; apply EQ).
- by rewrite -{2}[f]Hh -{2}[g]Hh -f_equiv -sig_equivI.
-Qed.
-
-Lemma pure_internal_eq {A : ofeT} (x y : A) : ⌜x ≡ y⌠⊢ x ≡ y.
-Proof. apply pure_elim'=> ->. apply internal_eq_refl. Qed.
-Lemma discrete_eq {A : ofeT} (a b : A) : Discrete a → a ≡ b ⊣⊢ ⌜a ≡ bâŒ.
-Proof.
- intros. apply (anti_symm _); auto using discrete_eq_1, pure_internal_eq.
-Qed.
-
-Lemma absorbingly_internal_eq {A : ofeT} (x y : A) : <absorb> (x ≡ y) ⊣⊢ x ≡ y.
-Proof.
- apply (anti_symm _), absorbingly_intro.
- apply wand_elim_r', (internal_eq_rewrite' x y (λ y, True -∗ x ≡ y)%I); auto.
- apply wand_intro_l, internal_eq_refl.
-Qed.
-Lemma persistently_internal_eq {A : ofeT} (a b : A) : <pers> (a ≡ b) ⊣⊢ a ≡ b.
-Proof.
- apply (anti_symm (⊢)).
- { by rewrite persistently_elim_absorbingly absorbingly_internal_eq. }
- apply (internal_eq_rewrite' a b (λ b, <pers> (a ≡ b))%I); auto.
- rewrite -(internal_eq_refl emp%I a). apply persistently_emp_intro.
-Qed.
-
-Global Instance internal_eq_absorbing {A : ofeT} (x y : A) :
- Absorbing (x ≡ y : PROP)%I.
-Proof. by rewrite /Absorbing absorbingly_internal_eq. Qed.
-Global Instance internal_eq_persistent {A : ofeT} (a b : A) :
- Persistent (a ≡ b : PROP)%I.
-Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed.
-
-(* Equality under a later. *)
-Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A → PROP)
- {HΨ : Contractive Ψ} : ▷ (a ≡ b) ⊢ Ψ a → Ψ b.
-Proof.
- rewrite later_eq_2. move: HΨ=>/contractive_alt [g [? HΨ]]. rewrite !HΨ.
- by apply internal_eq_rewrite.
-Qed.
-Lemma internal_eq_rewrite_contractive' {A : ofeT} a b (Ψ : A → PROP) P
- {HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
-Proof.
- rewrite later_eq_2. move: HΨ=>/contractive_alt [g [? HΨ]]. rewrite !HΨ.
- by apply internal_eq_rewrite'.
-Qed.
-
-Lemma later_equivI {A : ofeT} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y).
-Proof. apply (anti_symm _); auto using later_eq_1, later_eq_2. Qed.
-
-(* Later derived *)
-Hint Resolve later_mono.
-Global Instance later_mono' : Proper ((⊢) ==> (⊢)) (@sbi_later PROP).
-Proof. intros P Q; apply later_mono. Qed.
-Global Instance later_flip_mono' :
- Proper (flip (⊢) ==> flip (⊢)) (@sbi_later PROP).
-Proof. intros P Q; apply later_mono. Qed.
-
-Lemma later_intro P : P ⊢ ▷ P.
-Proof.
- rewrite -(and_elim_l (▷ P)%I P) -(löb (▷ P ∧ P)%I).
- apply impl_intro_l. by rewrite {1}(and_elim_r (â–· P)%I).
-Qed.
-
-Lemma later_True : ▷ True ⊣⊢ True.
-Proof. apply (anti_symm (⊢)); auto using later_intro. Qed.
-Lemma later_emp `{!BiAffine PROP} : ▷ emp ⊣⊢ emp.
-Proof. by rewrite -True_emp later_True. Qed.
-Lemma later_forall {A} (Φ : A → PROP) : (▷ ∀ a, Φ a) ⊣⊢ (∀ a, ▷ Φ a).
-Proof.
- apply (anti_symm _); auto using later_forall_2.
- apply forall_intro=> x. by rewrite (forall_elim x).
-Qed.
-Lemma later_exist_2 {A} (Φ : A → PROP) : (∃ a, ▷ Φ a) ⊢ ▷ (∃ a, Φ a).
-Proof. apply exist_elim; eauto using exist_intro. Qed.
-Lemma later_exist `{Inhabited A} (Φ : A → PROP) : ▷ (∃ a, Φ a) ⊣⊢ (∃ a, ▷ Φ a).
-Proof.
- apply: anti_symm; [|apply later_exist_2].
- rewrite later_exist_false. apply or_elim; last done.
- rewrite -(exist_intro inhabitant); auto.
-Qed.
-Lemma later_and P Q : ▷ (P ∧ Q) ⊣⊢ ▷ P ∧ ▷ Q.
-Proof. rewrite !and_alt later_forall. by apply forall_proper=> -[]. Qed.
-Lemma later_or P Q : ▷ (P ∨ Q) ⊣⊢ ▷ P ∨ ▷ Q.
-Proof. rewrite !or_alt later_exist. by apply exist_proper=> -[]. Qed.
-Lemma later_impl P Q : ▷ (P → Q) ⊢ ▷ P → ▷ Q.
-Proof. apply impl_intro_l. by rewrite -later_and impl_elim_r. Qed.
-Lemma later_sep P Q : ▷ (P ∗ Q) ⊣⊢ ▷ P ∗ ▷ Q.
-Proof. apply (anti_symm _); auto using later_sep_1, later_sep_2. Qed.
-Lemma later_wand P Q : ▷ (P -∗ Q) ⊢ ▷ P -∗ ▷ Q.
-Proof. apply wand_intro_l. by rewrite -later_sep wand_elim_r. Qed.
-Lemma later_iff P Q : ▷ (P ↔ Q) ⊢ ▷ P ↔ ▷ Q.
-Proof. by rewrite /bi_iff later_and !later_impl. Qed.
-Lemma later_persistently P : ▷ <pers> P ⊣⊢ <pers> ▷ P.
-Proof. apply (anti_symm _); auto using later_persistently_1, later_persistently_2. Qed.
-Lemma later_affinely_2 P : <affine> ▷ P ⊢ ▷ <affine> P.
-Proof. rewrite /bi_affinely later_and. auto using later_intro. Qed.
-Lemma later_intuitionistically_2 P : □ ▷ P ⊢ ▷ □ P.
-Proof. by rewrite /bi_intuitionistically -later_persistently later_affinely_2. Qed.
-Lemma later_intuitionistically_if_2 p P : □?p ▷ P ⊢ ▷ □?p P.
-Proof. destruct p; simpl; auto using later_intuitionistically_2. Qed.
-Lemma later_absorbingly P : ▷ <absorb> P ⊣⊢ <absorb> ▷ P.
-Proof. by rewrite /bi_absorbingly later_sep later_True. Qed.
-
-Global Instance later_persistent P : Persistent P → Persistent (▷ P).
-Proof. intros. by rewrite /Persistent -later_persistently {1}(persistent P). Qed.
-Global Instance later_absorbing P : Absorbing P → Absorbing (▷ P).
-Proof. intros ?. by rewrite /Absorbing -later_absorbingly absorbing. Qed.
-
-(* Iterated later modality *)
-Global Instance laterN_ne m : NonExpansive (@sbi_laterN PROP m).
-Proof. induction m; simpl. by intros ???. solve_proper. Qed.
-Global Instance laterN_proper m :
- Proper ((⊣⊢) ==> (⊣⊢)) (@sbi_laterN PROP m) := ne_proper _.
-
-Lemma laterN_0 P : ▷^0 P ⊣⊢ P.
-Proof. done. Qed.
-Lemma later_laterN n P : ▷^(S n) P ⊣⊢ ▷ ▷^n P.
-Proof. done. Qed.
-Lemma laterN_later n P : ▷^(S n) P ⊣⊢ ▷^n ▷ P.
-Proof. induction n; f_equiv/=; auto. Qed.
-Lemma laterN_plus n1 n2 P : ▷^(n1 + n2) P ⊣⊢ ▷^n1 ▷^n2 P.
-Proof. induction n1; f_equiv/=; auto. Qed.
-Lemma laterN_le n1 n2 P : n1 ≤ n2 → ▷^n1 P ⊢ ▷^n2 P.
-Proof. induction 1; simpl; by rewrite -?later_intro. Qed.
-
-Lemma laterN_mono n P Q : (P ⊢ Q) → ▷^n P ⊢ ▷^n Q.
-Proof. induction n; simpl; auto. Qed.
-Global Instance laterN_mono' n : Proper ((⊢) ==> (⊢)) (@sbi_laterN PROP n).
-Proof. intros P Q; apply laterN_mono. Qed.
-Global Instance laterN_flip_mono' n :
- Proper (flip (⊢) ==> flip (⊢)) (@sbi_laterN PROP n).
-Proof. intros P Q; apply laterN_mono. Qed.
-
-Lemma laterN_intro n P : P ⊢ ▷^n P.
-Proof. induction n as [|n IH]; simpl; by rewrite -?later_intro. Qed.
-
-Lemma laterN_True n : ▷^n True ⊣⊢ True.
-Proof. apply (anti_symm (⊢)); auto using laterN_intro, True_intro. Qed.
-Lemma laterN_emp `{!BiAffine PROP} n : ▷^n emp ⊣⊢ emp.
-Proof. by rewrite -True_emp laterN_True. Qed.
-Lemma laterN_forall {A} n (Φ : A → PROP) : (▷^n ∀ a, Φ a) ⊣⊢ (∀ a, ▷^n Φ a).
-Proof. induction n as [|n IH]; simpl; rewrite -?later_forall ?IH; auto. Qed.
-Lemma laterN_exist_2 {A} n (Φ : A → PROP) : (∃ a, ▷^n Φ a) ⊢ ▷^n (∃ a, Φ a).
-Proof. apply exist_elim; eauto using exist_intro, laterN_mono. Qed.
-Lemma laterN_exist `{Inhabited A} n (Φ : A → PROP) :
- (▷^n ∃ a, Φ a) ⊣⊢ ∃ a, ▷^n Φ a.
-Proof. induction n as [|n IH]; simpl; rewrite -?later_exist ?IH; auto. Qed.
-Lemma laterN_and n P Q : ▷^n (P ∧ Q) ⊣⊢ ▷^n P ∧ ▷^n Q.
-Proof. induction n as [|n IH]; simpl; rewrite -?later_and ?IH; auto. Qed.
-Lemma laterN_or n P Q : ▷^n (P ∨ Q) ⊣⊢ ▷^n P ∨ ▷^n Q.
-Proof. induction n as [|n IH]; simpl; rewrite -?later_or ?IH; auto. Qed.
-Lemma laterN_impl n P Q : ▷^n (P → Q) ⊢ ▷^n P → ▷^n Q.
-Proof. apply impl_intro_l. by rewrite -laterN_and impl_elim_r. Qed.
-Lemma laterN_sep n P Q : ▷^n (P ∗ Q) ⊣⊢ ▷^n P ∗ ▷^n Q.
-Proof. induction n as [|n IH]; simpl; rewrite -?later_sep ?IH; auto. Qed.
-Lemma laterN_wand n P Q : ▷^n (P -∗ Q) ⊢ ▷^n P -∗ ▷^n Q.
-Proof. apply wand_intro_l. by rewrite -laterN_sep wand_elim_r. Qed.
-Lemma laterN_iff n P Q : ▷^n (P ↔ Q) ⊢ ▷^n P ↔ ▷^n Q.
-Proof. by rewrite /bi_iff laterN_and !laterN_impl. Qed.
-Lemma laterN_persistently n P : ▷^n <pers> P ⊣⊢ <pers> ▷^n P.
-Proof. induction n as [|n IH]; simpl; auto. by rewrite IH later_persistently. Qed.
-Lemma laterN_affinely_2 n P : <affine> ▷^n P ⊢ ▷^n <affine> P.
-Proof. rewrite /bi_affinely laterN_and. auto using laterN_intro. Qed.
-Lemma laterN_intuitionistically_2 n P : □ ▷^n P ⊢ ▷^n □ P.
-Proof. by rewrite /bi_intuitionistically -laterN_persistently laterN_affinely_2. Qed.
-Lemma laterN_intuitionistically_if_2 n p P : □?p ▷^n P ⊢ ▷^n □?p P.
-Proof. destruct p; simpl; auto using laterN_intuitionistically_2. Qed.
-Lemma laterN_absorbingly n P : ▷^n <absorb> P ⊣⊢ <absorb> ▷^n P.
-Proof. by rewrite /bi_absorbingly laterN_sep laterN_True. Qed.
-
-Global Instance laterN_persistent n P : Persistent P → Persistent (▷^n P).
-Proof. induction n; apply _. Qed.
-Global Instance laterN_absorbing n P : Absorbing P → Absorbing (▷^n P).
-Proof. induction n; apply _. Qed.
-
-(* Except-0 *)
-Global Instance except_0_ne : NonExpansive (@sbi_except_0 PROP).
-Proof. solve_proper. Qed.
-Global Instance except_0_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@sbi_except_0 PROP).
-Proof. solve_proper. Qed.
-Global Instance except_0_mono' : Proper ((⊢) ==> (⊢)) (@sbi_except_0 PROP).
-Proof. solve_proper. Qed.
-Global Instance except_0_flip_mono' :
- Proper (flip (⊢) ==> flip (⊢)) (@sbi_except_0 PROP).
-Proof. solve_proper. Qed.
-
-Lemma except_0_intro P : P ⊢ ◇ P.
-Proof. rewrite /sbi_except_0; auto. Qed.
-Lemma except_0_mono P Q : (P ⊢ Q) → ◇ P ⊢ ◇ Q.
-Proof. by intros ->. Qed.
-Lemma except_0_idemp P : ◇ ◇ P ⊣⊢ ◇ P.
-Proof. apply (anti_symm _); rewrite /sbi_except_0; auto. Qed.
-
-Lemma except_0_True : ◇ True ⊣⊢ True.
-Proof. rewrite /sbi_except_0. apply (anti_symm _); auto. Qed.
-Lemma except_0_emp `{!BiAffine PROP} : ◇ emp ⊣⊢ emp.
-Proof. by rewrite -True_emp except_0_True. Qed.
-Lemma except_0_or P Q : ◇ (P ∨ Q) ⊣⊢ ◇ P ∨ ◇ Q.
-Proof. rewrite /sbi_except_0. apply (anti_symm _); auto. Qed.
-Lemma except_0_and P Q : ◇ (P ∧ Q) ⊣⊢ ◇ P ∧ ◇ Q.
-Proof. by rewrite /sbi_except_0 or_and_l. Qed.
-Lemma except_0_sep P Q : ◇ (P ∗ Q) ⊣⊢ ◇ P ∗ ◇ Q.
-Proof.
- rewrite /sbi_except_0. apply (anti_symm _).
- - apply or_elim; last by auto using sep_mono.
- by rewrite -!or_intro_l -persistently_pure -later_sep -persistently_sep_dup.
- - rewrite sep_or_r !sep_or_l {1}(later_intro P) {1}(later_intro Q).
- rewrite -!later_sep !left_absorb right_absorb. auto.
-Qed.
-Lemma except_0_forall {A} (Φ : A → PROP) : ◇ (∀ a, Φ a) ⊣⊢ ∀ a, ◇ Φ a.
-Proof.
- apply (anti_symm _).
- { apply forall_intro=> a. by rewrite (forall_elim a). }
- trans (▷ (∀ a : A, Φ a) ∧ (∀ a : A, ◇ Φ a))%I.
- { apply and_intro, reflexivity. rewrite later_forall. apply forall_mono=> a.
- apply or_elim; auto using later_intro. }
- rewrite later_false_em and_or_r. apply or_elim.
- { rewrite and_elim_l. apply or_intro_l. }
- apply or_intro_r', forall_intro=> a. rewrite !(forall_elim a).
- by rewrite and_or_l impl_elim_l and_elim_r idemp.
-Qed.
-Lemma except_0_exist_2 {A} (Φ : A → PROP) : (∃ a, ◇ Φ a) ⊢ ◇ ∃ a, Φ a.
-Proof. apply exist_elim=> a. by rewrite (exist_intro a). Qed.
-Lemma except_0_exist `{Inhabited A} (Φ : A → PROP) :
- ◇ (∃ a, Φ a) ⊣⊢ (∃ a, ◇ Φ a).
-Proof.
- apply (anti_symm _); [|by apply except_0_exist_2]. apply or_elim.
- - rewrite -(exist_intro inhabitant). by apply or_intro_l.
- - apply exist_mono=> a. apply except_0_intro.
-Qed.
-Lemma except_0_later P : ◇ ▷ P ⊢ ▷ P.
-Proof. by rewrite /sbi_except_0 -later_or False_or. Qed.
-Lemma except_0_persistently P : ◇ <pers> P ⊣⊢ <pers> ◇ P.
-Proof.
- by rewrite /sbi_except_0 persistently_or -later_persistently persistently_pure.
-Qed.
-Lemma except_0_affinely_2 P : <affine> ◇ P ⊢ ◇ <affine> P.
-Proof. rewrite /bi_affinely except_0_and. auto using except_0_intro. Qed.
-Lemma except_0_intuitionistically_2 P : □ ◇ P ⊢ ◇ □ P.
-Proof. by rewrite /bi_intuitionistically -except_0_persistently except_0_affinely_2. Qed.
-Lemma except_0_intuitionistically_if_2 p P : □?p ◇ P ⊢ ◇ □?p P.
-Proof. destruct p; simpl; auto using except_0_intuitionistically_2. Qed.
-Lemma except_0_absorbingly P : ◇ <absorb> P ⊣⊢ <absorb> ◇ P.
-Proof. by rewrite /bi_absorbingly except_0_sep except_0_True. Qed.
-
-Lemma except_0_frame_l P Q : P ∗ ◇ Q ⊢ ◇ (P ∗ Q).
-Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed.
-Lemma except_0_frame_r P Q : ◇ P ∗ Q ⊢ ◇ (P ∗ Q).
-Proof. by rewrite {1}(except_0_intro Q) except_0_sep. Qed.
-
-Lemma later_affinely_1 `{!Timeless (emp%I : PROP)} P : ▷ <affine> P ⊢ ◇ <affine> ▷ P.
-Proof.
- rewrite /bi_affinely later_and (timeless emp%I) except_0_and.
- by apply and_mono, except_0_intro.
-Qed.
-
-Global Instance except_0_persistent P : Persistent P → Persistent (◇ P).
-Proof. rewrite /sbi_except_0; apply _. Qed.
-Global Instance except_0_absorbing P : Absorbing P → Absorbing (◇ P).
-Proof. rewrite /sbi_except_0; apply _. Qed.
-
-(* Timeless instances *)
-Global Instance Timeless_proper : Proper ((≡) ==> iff) (@Timeless PROP).
-Proof. solve_proper. Qed.
-
-Global Instance pure_timeless φ : Timeless (⌜φ⌠: PROP)%I.
-Proof.
- rewrite /Timeless /sbi_except_0 pure_alt later_exist_false.
- apply or_elim, exist_elim; [auto|]=> Hφ. rewrite -(exist_intro Hφ). auto.
-Qed.
-Global Instance emp_timeless `{BiAffine PROP} : Timeless (emp : PROP)%I.
-Proof. rewrite -True_emp. apply _. Qed.
-
-Global Instance and_timeless P Q : Timeless P → Timeless Q → Timeless (P ∧ Q).
-Proof. intros; rewrite /Timeless except_0_and later_and; auto. Qed.
-Global Instance or_timeless P Q : Timeless P → Timeless Q → Timeless (P ∨ Q).
-Proof. intros; rewrite /Timeless except_0_or later_or; auto. Qed.
-
-Global Instance impl_timeless P Q : Timeless Q → Timeless (P → Q).
-Proof.
- rewrite /Timeless=> HQ. rewrite later_false_em.
- apply or_mono, impl_intro_l; first done.
- rewrite -{2}(löb Q); apply impl_intro_l.
- rewrite HQ /sbi_except_0 !and_or_r. apply or_elim; last auto.
- by rewrite assoc (comm _ _ P) -assoc !impl_elim_r.
-Qed.
-Global Instance sep_timeless P Q: Timeless P → Timeless Q → Timeless (P ∗ Q).
-Proof.
- intros; rewrite /Timeless except_0_sep later_sep; auto using sep_mono.
-Qed.
-
-Global Instance wand_timeless P Q : Timeless Q → Timeless (P -∗ Q).
-Proof.
- rewrite /Timeless=> HQ. rewrite later_false_em.
- apply or_mono, wand_intro_l; first done.
- rewrite -{2}(löb Q); apply impl_intro_l.
- rewrite HQ /sbi_except_0 !and_or_r. apply or_elim; last auto.
- by rewrite (comm _ P) persistent_and_sep_assoc impl_elim_r wand_elim_l.
-Qed.
-Global Instance forall_timeless {A} (Ψ : A → PROP) :
- (∀ x, Timeless (Ψ x)) → Timeless (∀ x, Ψ x).
-Proof.
- rewrite /Timeless=> HQ. rewrite except_0_forall later_forall.
- apply forall_mono; auto.
-Qed.
-Global Instance exist_timeless {A} (Ψ : A → PROP) :
- (∀ x, Timeless (Ψ x)) → Timeless (∃ x, Ψ x).
-Proof.
- rewrite /Timeless=> ?. rewrite later_exist_false. apply or_elim.
- - rewrite /sbi_except_0; auto.
- - apply exist_elim=> x. rewrite -(exist_intro x); auto.
-Qed.
-Global Instance persistently_timeless P : Timeless P → Timeless (<pers> P).
-Proof.
- intros. rewrite /Timeless /sbi_except_0 later_persistently_1.
- by rewrite (timeless P) /sbi_except_0 persistently_or {1}persistently_elim.
-Qed.
-
-Global Instance affinely_timeless P :
- Timeless (emp%I : PROP) → Timeless P → Timeless (<affine> P).
-Proof. rewrite /bi_affinely; apply _. Qed.
-Global Instance absorbingly_timeless P : Timeless P → Timeless (<absorb> P).
-Proof. rewrite /bi_absorbingly; apply _. Qed.
-
-Global Instance eq_timeless {A : ofeT} (a b : A) :
- Discrete a → Timeless (a ≡ b : PROP)%I.
-Proof. intros. rewrite /Discrete !discrete_eq. apply (timeless _). Qed.
-Global Instance from_option_timeless {A} P (Ψ : A → PROP) (mx : option A) :
- (∀ x, Timeless (Ψ x)) → Timeless P → Timeless (from_option Ψ P mx).
-Proof. destruct mx; apply _. Qed.
-
-(* Big op stuff *)
-Global Instance sbi_later_monoid_and_homomorphism :
- MonoidHomomorphism bi_and bi_and (≡) (@sbi_later PROP).
-Proof. split; [split|]; try apply _. apply later_and. apply later_True. Qed.
-Global Instance sbi_laterN_and_homomorphism n :
- MonoidHomomorphism bi_and bi_and (≡) (@sbi_laterN PROP n).
-Proof. split; [split|]; try apply _. apply laterN_and. apply laterN_True. Qed.
-Global Instance sbi_except_0_and_homomorphism :
- MonoidHomomorphism bi_and bi_and (≡) (@sbi_except_0 PROP).
-Proof. split; [split|]; try apply _. apply except_0_and. apply except_0_True. Qed.
-
-Global Instance sbi_later_monoid_or_homomorphism :
- WeakMonoidHomomorphism bi_or bi_or (≡) (@sbi_later PROP).
-Proof. split; try apply _. apply later_or. Qed.
-Global Instance sbi_laterN_or_homomorphism n :
- WeakMonoidHomomorphism bi_or bi_or (≡) (@sbi_laterN PROP n).
-Proof. split; try apply _. apply laterN_or. Qed.
-Global Instance sbi_except_0_or_homomorphism :
- WeakMonoidHomomorphism bi_or bi_or (≡) (@sbi_except_0 PROP).
-Proof. split; try apply _. apply except_0_or. Qed.
-
-Global Instance sbi_later_monoid_sep_weak_homomorphism :
- WeakMonoidHomomorphism bi_sep bi_sep (≡) (@sbi_later PROP).
-Proof. split; try apply _. apply later_sep. Qed.
-Global Instance sbi_laterN_sep_weak_homomorphism n :
- WeakMonoidHomomorphism bi_sep bi_sep (≡) (@sbi_laterN PROP n).
-Proof. split; try apply _. apply laterN_sep. Qed.
-Global Instance sbi_except_0_sep_weak_homomorphism :
- WeakMonoidHomomorphism bi_sep bi_sep (≡) (@sbi_except_0 PROP).
-Proof. split; try apply _. apply except_0_sep. Qed.
-
-Global Instance sbi_later_monoid_sep_homomorphism `{!BiAffine PROP} :
- MonoidHomomorphism bi_sep bi_sep (≡) (@sbi_later PROP).
-Proof. split; try apply _. apply later_emp. Qed.
-Global Instance sbi_laterN_sep_homomorphism `{!BiAffine PROP} n :
- MonoidHomomorphism bi_sep bi_sep (≡) (@sbi_laterN PROP n).
-Proof. split; try apply _. apply laterN_emp. Qed.
-Global Instance sbi_except_0_sep_homomorphism `{!BiAffine PROP} :
- MonoidHomomorphism bi_sep bi_sep (≡) (@sbi_except_0 PROP).
-Proof. split; try apply _. apply except_0_emp. Qed.
-
-Global Instance sbi_later_monoid_sep_entails_weak_homomorphism :
- WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@sbi_later PROP).
-Proof. split; try apply _. intros P Q. by rewrite later_sep. Qed.
-Global Instance sbi_laterN_sep_entails_weak_homomorphism n :
- WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@sbi_laterN PROP n).
-Proof. split; try apply _. intros P Q. by rewrite laterN_sep. Qed.
-Global Instance sbi_except_0_sep_entails_weak_homomorphism :
- WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@sbi_except_0 PROP).
-Proof. split; try apply _. intros P Q. by rewrite except_0_sep. Qed.
-
-Global Instance sbi_later_monoid_sep_entails_homomorphism :
- MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@sbi_later PROP).
-Proof. split; try apply _. apply later_intro. Qed.
-Global Instance sbi_laterN_sep_entails_homomorphism n :
- MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@sbi_laterN PROP n).
-Proof. split; try apply _. apply laterN_intro. Qed.
-Global Instance sbi_except_0_sep_entails_homomorphism :
- MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@sbi_except_0 PROP).
-Proof. split; try apply _. apply except_0_intro. Qed.
-End sbi_derived.
End bi.
diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_sbi.v
new file mode 100644
index 0000000000000000000000000000000000000000..58b8605c37396bc6a80d94f4800474a1b052ec57
--- /dev/null
+++ b/theories/bi/derived_laws_sbi.v
@@ -0,0 +1,496 @@
+From iris.bi Require Export derived_laws_bi.
+From iris.algebra Require Import monoid.
+From stdpp Require Import hlist.
+
+Module bi.
+Import interface.bi.
+Import derived_laws_bi.bi.
+Section sbi_derived.
+Context {PROP : sbi}.
+Implicit Types φ : Prop.
+Implicit Types P Q R : PROP.
+Implicit Types Ps : list PROP.
+Implicit Types A : Type.
+
+(* Force implicit argument PROP *)
+Notation "P ⊢ Q" := (@bi_entails PROP P%I Q%I).
+Notation "P ⊣⊢ Q" := (equiv (A:=bi_car PROP) P%I Q%I).
+
+Hint Resolve or_elim or_intro_l' or_intro_r' True_intro False_elim.
+Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro.
+
+Global Instance internal_eq_proper (A : ofeT) :
+ Proper ((≡) ==> (≡) ==> (⊣⊢)) (@sbi_internal_eq PROP A) := ne_proper_2 _.
+Global Instance later_proper :
+ Proper ((⊣⊢) ==> (⊣⊢)) (@sbi_later PROP) := ne_proper _.
+
+(* Equality *)
+Hint Resolve internal_eq_refl.
+Hint Extern 100 (NonExpansive _) => solve_proper.
+
+Lemma equiv_internal_eq {A : ofeT} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
+Proof. intros ->. auto. Qed.
+Lemma internal_eq_rewrite' {A : ofeT} a b (Ψ : A → PROP) P
+ {HΨ : NonExpansive Ψ} : (P ⊢ a ≡ b) → (P ⊢ Ψ a) → P ⊢ Ψ b.
+Proof.
+ intros Heq HΨa. rewrite -(idemp bi_and P) {1}Heq HΨa.
+ apply impl_elim_l'. by apply internal_eq_rewrite.
+Qed.
+
+Lemma internal_eq_sym {A : ofeT} (a b : A) : a ≡ b ⊢ b ≡ a.
+Proof. apply (internal_eq_rewrite' a b (λ b, b ≡ a)%I); auto. Qed.
+Lemma internal_eq_iff P Q : P ≡ Q ⊢ P ↔ Q.
+Proof. apply (internal_eq_rewrite' P Q (λ Q, P ↔ Q))%I; auto using iff_refl. Qed.
+
+Lemma f_equiv {A B : ofeT} (f : A → B) `{!NonExpansive f} x y :
+ x ≡ y ⊢ f x ≡ f y.
+Proof. apply (internal_eq_rewrite' x y (λ y, f x ≡ f y)%I); auto. Qed.
+
+Lemma prod_equivI {A B : ofeT} (x y : A * B) : x ≡ y ⊣⊢ x.1 ≡ y.1 ∧ x.2 ≡ y.2.
+Proof.
+ apply (anti_symm _).
+ - apply and_intro; apply f_equiv; apply _.
+ - rewrite {3}(surjective_pairing x) {3}(surjective_pairing y).
+ apply (internal_eq_rewrite' (x.1) (y.1) (λ a, (x.1,x.2) ≡ (a,y.2))%I); auto.
+ apply (internal_eq_rewrite' (x.2) (y.2) (λ b, (x.1,x.2) ≡ (x.1,b))%I); auto.
+Qed.
+Lemma sum_equivI {A B : ofeT} (x y : A + B) :
+ x ≡ y ⊣⊢
+ match x, y with
+ | inl a, inl a' => a ≡ a' | inr b, inr b' => b ≡ b' | _, _ => False
+ end.
+Proof.
+ apply (anti_symm _).
+ - apply (internal_eq_rewrite' x y (λ y,
+ match x, y with
+ | inl a, inl a' => a ≡ a' | inr b, inr b' => b ≡ b' | _, _ => False
+ end)%I); auto.
+ destruct x; auto.
+ - destruct x as [a|b], y as [a'|b']; auto; apply f_equiv, _.
+Qed.
+Lemma option_equivI {A : ofeT} (x y : option A) :
+ x ≡ y ⊣⊢ match x, y with
+ | Some a, Some a' => a ≡ a' | None, None => True | _, _ => False
+ end.
+Proof.
+ apply (anti_symm _).
+ - apply (internal_eq_rewrite' x y (λ y,
+ match x, y with
+ | Some a, Some a' => a ≡ a' | None, None => True | _, _ => False
+ end)%I); auto.
+ destruct x; auto.
+ - destruct x as [a|], y as [a'|]; auto. apply f_equiv, _.
+Qed.
+
+Lemma sig_equivI {A : ofeT} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊣⊢ x ≡ y.
+Proof. apply (anti_symm _). apply sig_eq. apply f_equiv, _. Qed.
+
+Lemma ofe_fun_equivI {A} {B : A → ofeT} (f g : ofe_fun B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
+Proof.
+ apply (anti_symm _); auto using fun_ext.
+ apply (internal_eq_rewrite' f g (λ g, ∀ x : A, f x ≡ g x)%I); auto.
+ intros n h h' Hh; apply forall_ne=> x; apply internal_eq_ne; auto.
+Qed.
+Lemma ofe_morC_equivI {A B : ofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
+Proof.
+ apply (anti_symm _).
+ - apply (internal_eq_rewrite' f g (λ g, ∀ x : A, f x ≡ g x)%I); auto.
+ - rewrite -(ofe_fun_equivI (ofe_mor_car _ _ f) (ofe_mor_car _ _ g)).
+ set (h1 (f : A -n> B) :=
+ exist (λ f : A -c> B, NonExpansive (f : A → B)) f (ofe_mor_ne A B f)).
+ set (h2 (f : sigC (λ f : A -c> B, NonExpansive (f : A → B))) :=
+ @CofeMor A B (`f) (proj2_sig f)).
+ assert (∀ f, h2 (h1 f) = f) as Hh by (by intros []).
+ assert (NonExpansive h2) by (intros ??? EQ; apply EQ).
+ by rewrite -{2}[f]Hh -{2}[g]Hh -f_equiv -sig_equivI.
+Qed.
+
+Lemma pure_internal_eq {A : ofeT} (x y : A) : ⌜x ≡ y⌠⊢ x ≡ y.
+Proof. apply pure_elim'=> ->. apply internal_eq_refl. Qed.
+Lemma discrete_eq {A : ofeT} (a b : A) : Discrete a → a ≡ b ⊣⊢ ⌜a ≡ bâŒ.
+Proof.
+ intros. apply (anti_symm _); auto using discrete_eq_1, pure_internal_eq.
+Qed.
+
+Lemma absorbingly_internal_eq {A : ofeT} (x y : A) : <absorb> (x ≡ y) ⊣⊢ x ≡ y.
+Proof.
+ apply (anti_symm _), absorbingly_intro.
+ apply wand_elim_r', (internal_eq_rewrite' x y (λ y, True -∗ x ≡ y)%I); auto.
+ apply wand_intro_l, internal_eq_refl.
+Qed.
+Lemma persistently_internal_eq {A : ofeT} (a b : A) : <pers> (a ≡ b) ⊣⊢ a ≡ b.
+Proof.
+ apply (anti_symm (⊢)).
+ { by rewrite persistently_elim_absorbingly absorbingly_internal_eq. }
+ apply (internal_eq_rewrite' a b (λ b, <pers> (a ≡ b))%I); auto.
+ rewrite -(internal_eq_refl emp%I a). apply persistently_emp_intro.
+Qed.
+
+Global Instance internal_eq_absorbing {A : ofeT} (x y : A) :
+ Absorbing (x ≡ y : PROP)%I.
+Proof. by rewrite /Absorbing absorbingly_internal_eq. Qed.
+Global Instance internal_eq_persistent {A : ofeT} (a b : A) :
+ Persistent (a ≡ b : PROP)%I.
+Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed.
+
+(* Equality under a later. *)
+Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A → PROP)
+ {HΨ : Contractive Ψ} : ▷ (a ≡ b) ⊢ Ψ a → Ψ b.
+Proof.
+ rewrite later_eq_2. move: HΨ=>/contractive_alt [g [? HΨ]]. rewrite !HΨ.
+ by apply internal_eq_rewrite.
+Qed.
+Lemma internal_eq_rewrite_contractive' {A : ofeT} a b (Ψ : A → PROP) P
+ {HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
+Proof.
+ rewrite later_eq_2. move: HΨ=>/contractive_alt [g [? HΨ]]. rewrite !HΨ.
+ by apply internal_eq_rewrite'.
+Qed.
+
+Lemma later_equivI {A : ofeT} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y).
+Proof. apply (anti_symm _); auto using later_eq_1, later_eq_2. Qed.
+
+(* Later derived *)
+Hint Resolve later_mono.
+Global Instance later_mono' : Proper ((⊢) ==> (⊢)) (@sbi_later PROP).
+Proof. intros P Q; apply later_mono. Qed.
+Global Instance later_flip_mono' :
+ Proper (flip (⊢) ==> flip (⊢)) (@sbi_later PROP).
+Proof. intros P Q; apply later_mono. Qed.
+
+Lemma later_intro P : P ⊢ ▷ P.
+Proof.
+ rewrite -(and_elim_l (▷ P)%I P) -(löb (▷ P ∧ P)%I).
+ apply impl_intro_l. by rewrite {1}(and_elim_r (â–· P)%I).
+Qed.
+
+Lemma later_True : ▷ True ⊣⊢ True.
+Proof. apply (anti_symm (⊢)); auto using later_intro. Qed.
+Lemma later_emp `{!BiAffine PROP} : ▷ emp ⊣⊢ emp.
+Proof. by rewrite -True_emp later_True. Qed.
+Lemma later_forall {A} (Φ : A → PROP) : (▷ ∀ a, Φ a) ⊣⊢ (∀ a, ▷ Φ a).
+Proof.
+ apply (anti_symm _); auto using later_forall_2.
+ apply forall_intro=> x. by rewrite (forall_elim x).
+Qed.
+Lemma later_exist_2 {A} (Φ : A → PROP) : (∃ a, ▷ Φ a) ⊢ ▷ (∃ a, Φ a).
+Proof. apply exist_elim; eauto using exist_intro. Qed.
+Lemma later_exist `{Inhabited A} (Φ : A → PROP) : ▷ (∃ a, Φ a) ⊣⊢ (∃ a, ▷ Φ a).
+Proof.
+ apply: anti_symm; [|apply later_exist_2].
+ rewrite later_exist_false. apply or_elim; last done.
+ rewrite -(exist_intro inhabitant); auto.
+Qed.
+Lemma later_and P Q : ▷ (P ∧ Q) ⊣⊢ ▷ P ∧ ▷ Q.
+Proof. rewrite !and_alt later_forall. by apply forall_proper=> -[]. Qed.
+Lemma later_or P Q : ▷ (P ∨ Q) ⊣⊢ ▷ P ∨ ▷ Q.
+Proof. rewrite !or_alt later_exist. by apply exist_proper=> -[]. Qed.
+Lemma later_impl P Q : ▷ (P → Q) ⊢ ▷ P → ▷ Q.
+Proof. apply impl_intro_l. by rewrite -later_and impl_elim_r. Qed.
+Lemma later_sep P Q : ▷ (P ∗ Q) ⊣⊢ ▷ P ∗ ▷ Q.
+Proof. apply (anti_symm _); auto using later_sep_1, later_sep_2. Qed.
+Lemma later_wand P Q : ▷ (P -∗ Q) ⊢ ▷ P -∗ ▷ Q.
+Proof. apply wand_intro_l. by rewrite -later_sep wand_elim_r. Qed.
+Lemma later_iff P Q : ▷ (P ↔ Q) ⊢ ▷ P ↔ ▷ Q.
+Proof. by rewrite /bi_iff later_and !later_impl. Qed.
+Lemma later_persistently P : ▷ <pers> P ⊣⊢ <pers> ▷ P.
+Proof. apply (anti_symm _); auto using later_persistently_1, later_persistently_2. Qed.
+Lemma later_affinely_2 P : <affine> ▷ P ⊢ ▷ <affine> P.
+Proof. rewrite /bi_affinely later_and. auto using later_intro. Qed.
+Lemma later_intuitionistically_2 P : □ ▷ P ⊢ ▷ □ P.
+Proof. by rewrite /bi_intuitionistically -later_persistently later_affinely_2. Qed.
+Lemma later_intuitionistically_if_2 p P : □?p ▷ P ⊢ ▷ □?p P.
+Proof. destruct p; simpl; auto using later_intuitionistically_2. Qed.
+Lemma later_absorbingly P : ▷ <absorb> P ⊣⊢ <absorb> ▷ P.
+Proof. by rewrite /bi_absorbingly later_sep later_True. Qed.
+
+Global Instance later_persistent P : Persistent P → Persistent (▷ P).
+Proof. intros. by rewrite /Persistent -later_persistently {1}(persistent P). Qed.
+Global Instance later_absorbing P : Absorbing P → Absorbing (▷ P).
+Proof. intros ?. by rewrite /Absorbing -later_absorbingly absorbing. Qed.
+
+(* Iterated later modality *)
+Global Instance laterN_ne m : NonExpansive (@sbi_laterN PROP m).
+Proof. induction m; simpl. by intros ???. solve_proper. Qed.
+Global Instance laterN_proper m :
+ Proper ((⊣⊢) ==> (⊣⊢)) (@sbi_laterN PROP m) := ne_proper _.
+
+Lemma laterN_0 P : ▷^0 P ⊣⊢ P.
+Proof. done. Qed.
+Lemma later_laterN n P : ▷^(S n) P ⊣⊢ ▷ ▷^n P.
+Proof. done. Qed.
+Lemma laterN_later n P : ▷^(S n) P ⊣⊢ ▷^n ▷ P.
+Proof. induction n; f_equiv/=; auto. Qed.
+Lemma laterN_plus n1 n2 P : ▷^(n1 + n2) P ⊣⊢ ▷^n1 ▷^n2 P.
+Proof. induction n1; f_equiv/=; auto. Qed.
+Lemma laterN_le n1 n2 P : n1 ≤ n2 → ▷^n1 P ⊢ ▷^n2 P.
+Proof. induction 1; simpl; by rewrite -?later_intro. Qed.
+
+Lemma laterN_mono n P Q : (P ⊢ Q) → ▷^n P ⊢ ▷^n Q.
+Proof. induction n; simpl; auto. Qed.
+Global Instance laterN_mono' n : Proper ((⊢) ==> (⊢)) (@sbi_laterN PROP n).
+Proof. intros P Q; apply laterN_mono. Qed.
+Global Instance laterN_flip_mono' n :
+ Proper (flip (⊢) ==> flip (⊢)) (@sbi_laterN PROP n).
+Proof. intros P Q; apply laterN_mono. Qed.
+
+Lemma laterN_intro n P : P ⊢ ▷^n P.
+Proof. induction n as [|n IH]; simpl; by rewrite -?later_intro. Qed.
+
+Lemma laterN_True n : ▷^n True ⊣⊢ True.
+Proof. apply (anti_symm (⊢)); auto using laterN_intro, True_intro. Qed.
+Lemma laterN_emp `{!BiAffine PROP} n : ▷^n emp ⊣⊢ emp.
+Proof. by rewrite -True_emp laterN_True. Qed.
+Lemma laterN_forall {A} n (Φ : A → PROP) : (▷^n ∀ a, Φ a) ⊣⊢ (∀ a, ▷^n Φ a).
+Proof. induction n as [|n IH]; simpl; rewrite -?later_forall ?IH; auto. Qed.
+Lemma laterN_exist_2 {A} n (Φ : A → PROP) : (∃ a, ▷^n Φ a) ⊢ ▷^n (∃ a, Φ a).
+Proof. apply exist_elim; eauto using exist_intro, laterN_mono. Qed.
+Lemma laterN_exist `{Inhabited A} n (Φ : A → PROP) :
+ (▷^n ∃ a, Φ a) ⊣⊢ ∃ a, ▷^n Φ a.
+Proof. induction n as [|n IH]; simpl; rewrite -?later_exist ?IH; auto. Qed.
+Lemma laterN_and n P Q : ▷^n (P ∧ Q) ⊣⊢ ▷^n P ∧ ▷^n Q.
+Proof. induction n as [|n IH]; simpl; rewrite -?later_and ?IH; auto. Qed.
+Lemma laterN_or n P Q : ▷^n (P ∨ Q) ⊣⊢ ▷^n P ∨ ▷^n Q.
+Proof. induction n as [|n IH]; simpl; rewrite -?later_or ?IH; auto. Qed.
+Lemma laterN_impl n P Q : ▷^n (P → Q) ⊢ ▷^n P → ▷^n Q.
+Proof. apply impl_intro_l. by rewrite -laterN_and impl_elim_r. Qed.
+Lemma laterN_sep n P Q : ▷^n (P ∗ Q) ⊣⊢ ▷^n P ∗ ▷^n Q.
+Proof. induction n as [|n IH]; simpl; rewrite -?later_sep ?IH; auto. Qed.
+Lemma laterN_wand n P Q : ▷^n (P -∗ Q) ⊢ ▷^n P -∗ ▷^n Q.
+Proof. apply wand_intro_l. by rewrite -laterN_sep wand_elim_r. Qed.
+Lemma laterN_iff n P Q : ▷^n (P ↔ Q) ⊢ ▷^n P ↔ ▷^n Q.
+Proof. by rewrite /bi_iff laterN_and !laterN_impl. Qed.
+Lemma laterN_persistently n P : ▷^n <pers> P ⊣⊢ <pers> ▷^n P.
+Proof. induction n as [|n IH]; simpl; auto. by rewrite IH later_persistently. Qed.
+Lemma laterN_affinely_2 n P : <affine> ▷^n P ⊢ ▷^n <affine> P.
+Proof. rewrite /bi_affinely laterN_and. auto using laterN_intro. Qed.
+Lemma laterN_intuitionistically_2 n P : □ ▷^n P ⊢ ▷^n □ P.
+Proof. by rewrite /bi_intuitionistically -laterN_persistently laterN_affinely_2. Qed.
+Lemma laterN_intuitionistically_if_2 n p P : □?p ▷^n P ⊢ ▷^n □?p P.
+Proof. destruct p; simpl; auto using laterN_intuitionistically_2. Qed.
+Lemma laterN_absorbingly n P : ▷^n <absorb> P ⊣⊢ <absorb> ▷^n P.
+Proof. by rewrite /bi_absorbingly laterN_sep laterN_True. Qed.
+
+Global Instance laterN_persistent n P : Persistent P → Persistent (▷^n P).
+Proof. induction n; apply _. Qed.
+Global Instance laterN_absorbing n P : Absorbing P → Absorbing (▷^n P).
+Proof. induction n; apply _. Qed.
+
+(* Except-0 *)
+Global Instance except_0_ne : NonExpansive (@sbi_except_0 PROP).
+Proof. solve_proper. Qed.
+Global Instance except_0_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@sbi_except_0 PROP).
+Proof. solve_proper. Qed.
+Global Instance except_0_mono' : Proper ((⊢) ==> (⊢)) (@sbi_except_0 PROP).
+Proof. solve_proper. Qed.
+Global Instance except_0_flip_mono' :
+ Proper (flip (⊢) ==> flip (⊢)) (@sbi_except_0 PROP).
+Proof. solve_proper. Qed.
+
+Lemma except_0_intro P : P ⊢ ◇ P.
+Proof. rewrite /sbi_except_0; auto. Qed.
+Lemma except_0_mono P Q : (P ⊢ Q) → ◇ P ⊢ ◇ Q.
+Proof. by intros ->. Qed.
+Lemma except_0_idemp P : ◇ ◇ P ⊣⊢ ◇ P.
+Proof. apply (anti_symm _); rewrite /sbi_except_0; auto. Qed.
+
+Lemma except_0_True : ◇ True ⊣⊢ True.
+Proof. rewrite /sbi_except_0. apply (anti_symm _); auto. Qed.
+Lemma except_0_emp `{!BiAffine PROP} : ◇ emp ⊣⊢ emp.
+Proof. by rewrite -True_emp except_0_True. Qed.
+Lemma except_0_or P Q : ◇ (P ∨ Q) ⊣⊢ ◇ P ∨ ◇ Q.
+Proof. rewrite /sbi_except_0. apply (anti_symm _); auto. Qed.
+Lemma except_0_and P Q : ◇ (P ∧ Q) ⊣⊢ ◇ P ∧ ◇ Q.
+Proof. by rewrite /sbi_except_0 or_and_l. Qed.
+Lemma except_0_sep P Q : ◇ (P ∗ Q) ⊣⊢ ◇ P ∗ ◇ Q.
+Proof.
+ rewrite /sbi_except_0. apply (anti_symm _).
+ - apply or_elim; last by auto using sep_mono.
+ by rewrite -!or_intro_l -persistently_pure -later_sep -persistently_sep_dup.
+ - rewrite sep_or_r !sep_or_l {1}(later_intro P) {1}(later_intro Q).
+ rewrite -!later_sep !left_absorb right_absorb. auto.
+Qed.
+Lemma except_0_forall {A} (Φ : A → PROP) : ◇ (∀ a, Φ a) ⊣⊢ ∀ a, ◇ Φ a.
+Proof.
+ apply (anti_symm _).
+ { apply forall_intro=> a. by rewrite (forall_elim a). }
+ trans (▷ (∀ a : A, Φ a) ∧ (∀ a : A, ◇ Φ a))%I.
+ { apply and_intro, reflexivity. rewrite later_forall. apply forall_mono=> a.
+ apply or_elim; auto using later_intro. }
+ rewrite later_false_em and_or_r. apply or_elim.
+ { rewrite and_elim_l. apply or_intro_l. }
+ apply or_intro_r', forall_intro=> a. rewrite !(forall_elim a).
+ by rewrite and_or_l impl_elim_l and_elim_r idemp.
+Qed.
+Lemma except_0_exist_2 {A} (Φ : A → PROP) : (∃ a, ◇ Φ a) ⊢ ◇ ∃ a, Φ a.
+Proof. apply exist_elim=> a. by rewrite (exist_intro a). Qed.
+Lemma except_0_exist `{Inhabited A} (Φ : A → PROP) :
+ ◇ (∃ a, Φ a) ⊣⊢ (∃ a, ◇ Φ a).
+Proof.
+ apply (anti_symm _); [|by apply except_0_exist_2]. apply or_elim.
+ - rewrite -(exist_intro inhabitant). by apply or_intro_l.
+ - apply exist_mono=> a. apply except_0_intro.
+Qed.
+Lemma except_0_later P : ◇ ▷ P ⊢ ▷ P.
+Proof. by rewrite /sbi_except_0 -later_or False_or. Qed.
+Lemma except_0_persistently P : ◇ <pers> P ⊣⊢ <pers> ◇ P.
+Proof.
+ by rewrite /sbi_except_0 persistently_or -later_persistently persistently_pure.
+Qed.
+Lemma except_0_affinely_2 P : <affine> ◇ P ⊢ ◇ <affine> P.
+Proof. rewrite /bi_affinely except_0_and. auto using except_0_intro. Qed.
+Lemma except_0_intuitionistically_2 P : □ ◇ P ⊢ ◇ □ P.
+Proof. by rewrite /bi_intuitionistically -except_0_persistently except_0_affinely_2. Qed.
+Lemma except_0_intuitionistically_if_2 p P : □?p ◇ P ⊢ ◇ □?p P.
+Proof. destruct p; simpl; auto using except_0_intuitionistically_2. Qed.
+Lemma except_0_absorbingly P : ◇ <absorb> P ⊣⊢ <absorb> ◇ P.
+Proof. by rewrite /bi_absorbingly except_0_sep except_0_True. Qed.
+
+Lemma except_0_frame_l P Q : P ∗ ◇ Q ⊢ ◇ (P ∗ Q).
+Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed.
+Lemma except_0_frame_r P Q : ◇ P ∗ Q ⊢ ◇ (P ∗ Q).
+Proof. by rewrite {1}(except_0_intro Q) except_0_sep. Qed.
+
+Lemma later_affinely_1 `{!Timeless (emp%I : PROP)} P : ▷ <affine> P ⊢ ◇ <affine> ▷ P.
+Proof.
+ rewrite /bi_affinely later_and (timeless emp%I) except_0_and.
+ by apply and_mono, except_0_intro.
+Qed.
+
+Global Instance except_0_persistent P : Persistent P → Persistent (◇ P).
+Proof. rewrite /sbi_except_0; apply _. Qed.
+Global Instance except_0_absorbing P : Absorbing P → Absorbing (◇ P).
+Proof. rewrite /sbi_except_0; apply _. Qed.
+
+(* Timeless instances *)
+Global Instance Timeless_proper : Proper ((≡) ==> iff) (@Timeless PROP).
+Proof. solve_proper. Qed.
+
+Global Instance pure_timeless φ : Timeless (⌜φ⌠: PROP)%I.
+Proof.
+ rewrite /Timeless /sbi_except_0 pure_alt later_exist_false.
+ apply or_elim, exist_elim; [auto|]=> Hφ. rewrite -(exist_intro Hφ). auto.
+Qed.
+Global Instance emp_timeless `{BiAffine PROP} : Timeless (emp : PROP)%I.
+Proof. rewrite -True_emp. apply _. Qed.
+
+Global Instance and_timeless P Q : Timeless P → Timeless Q → Timeless (P ∧ Q).
+Proof. intros; rewrite /Timeless except_0_and later_and; auto. Qed.
+Global Instance or_timeless P Q : Timeless P → Timeless Q → Timeless (P ∨ Q).
+Proof. intros; rewrite /Timeless except_0_or later_or; auto. Qed.
+
+Global Instance impl_timeless P Q : Timeless Q → Timeless (P → Q).
+Proof.
+ rewrite /Timeless=> HQ. rewrite later_false_em.
+ apply or_mono, impl_intro_l; first done.
+ rewrite -{2}(löb Q); apply impl_intro_l.
+ rewrite HQ /sbi_except_0 !and_or_r. apply or_elim; last auto.
+ by rewrite assoc (comm _ _ P) -assoc !impl_elim_r.
+Qed.
+Global Instance sep_timeless P Q: Timeless P → Timeless Q → Timeless (P ∗ Q).
+Proof.
+ intros; rewrite /Timeless except_0_sep later_sep; auto using sep_mono.
+Qed.
+
+Global Instance wand_timeless P Q : Timeless Q → Timeless (P -∗ Q).
+Proof.
+ rewrite /Timeless=> HQ. rewrite later_false_em.
+ apply or_mono, wand_intro_l; first done.
+ rewrite -{2}(löb Q); apply impl_intro_l.
+ rewrite HQ /sbi_except_0 !and_or_r. apply or_elim; last auto.
+ by rewrite (comm _ P) persistent_and_sep_assoc impl_elim_r wand_elim_l.
+Qed.
+Global Instance forall_timeless {A} (Ψ : A → PROP) :
+ (∀ x, Timeless (Ψ x)) → Timeless (∀ x, Ψ x).
+Proof.
+ rewrite /Timeless=> HQ. rewrite except_0_forall later_forall.
+ apply forall_mono; auto.
+Qed.
+Global Instance exist_timeless {A} (Ψ : A → PROP) :
+ (∀ x, Timeless (Ψ x)) → Timeless (∃ x, Ψ x).
+Proof.
+ rewrite /Timeless=> ?. rewrite later_exist_false. apply or_elim.
+ - rewrite /sbi_except_0; auto.
+ - apply exist_elim=> x. rewrite -(exist_intro x); auto.
+Qed.
+Global Instance persistently_timeless P : Timeless P → Timeless (<pers> P).
+Proof.
+ intros. rewrite /Timeless /sbi_except_0 later_persistently_1.
+ by rewrite (timeless P) /sbi_except_0 persistently_or {1}persistently_elim.
+Qed.
+
+Global Instance affinely_timeless P :
+ Timeless (emp%I : PROP) → Timeless P → Timeless (<affine> P).
+Proof. rewrite /bi_affinely; apply _. Qed.
+Global Instance absorbingly_timeless P : Timeless P → Timeless (<absorb> P).
+Proof. rewrite /bi_absorbingly; apply _. Qed.
+
+Global Instance eq_timeless {A : ofeT} (a b : A) :
+ Discrete a → Timeless (a ≡ b : PROP)%I.
+Proof. intros. rewrite /Discrete !discrete_eq. apply (timeless _). Qed.
+Global Instance from_option_timeless {A} P (Ψ : A → PROP) (mx : option A) :
+ (∀ x, Timeless (Ψ x)) → Timeless P → Timeless (from_option Ψ P mx).
+Proof. destruct mx; apply _. Qed.
+
+(* Big op stuff *)
+Global Instance sbi_later_monoid_and_homomorphism :
+ MonoidHomomorphism bi_and bi_and (≡) (@sbi_later PROP).
+Proof. split; [split|]; try apply _. apply later_and. apply later_True. Qed.
+Global Instance sbi_laterN_and_homomorphism n :
+ MonoidHomomorphism bi_and bi_and (≡) (@sbi_laterN PROP n).
+Proof. split; [split|]; try apply _. apply laterN_and. apply laterN_True. Qed.
+Global Instance sbi_except_0_and_homomorphism :
+ MonoidHomomorphism bi_and bi_and (≡) (@sbi_except_0 PROP).
+Proof. split; [split|]; try apply _. apply except_0_and. apply except_0_True. Qed.
+
+Global Instance sbi_later_monoid_or_homomorphism :
+ WeakMonoidHomomorphism bi_or bi_or (≡) (@sbi_later PROP).
+Proof. split; try apply _. apply later_or. Qed.
+Global Instance sbi_laterN_or_homomorphism n :
+ WeakMonoidHomomorphism bi_or bi_or (≡) (@sbi_laterN PROP n).
+Proof. split; try apply _. apply laterN_or. Qed.
+Global Instance sbi_except_0_or_homomorphism :
+ WeakMonoidHomomorphism bi_or bi_or (≡) (@sbi_except_0 PROP).
+Proof. split; try apply _. apply except_0_or. Qed.
+
+Global Instance sbi_later_monoid_sep_weak_homomorphism :
+ WeakMonoidHomomorphism bi_sep bi_sep (≡) (@sbi_later PROP).
+Proof. split; try apply _. apply later_sep. Qed.
+Global Instance sbi_laterN_sep_weak_homomorphism n :
+ WeakMonoidHomomorphism bi_sep bi_sep (≡) (@sbi_laterN PROP n).
+Proof. split; try apply _. apply laterN_sep. Qed.
+Global Instance sbi_except_0_sep_weak_homomorphism :
+ WeakMonoidHomomorphism bi_sep bi_sep (≡) (@sbi_except_0 PROP).
+Proof. split; try apply _. apply except_0_sep. Qed.
+
+Global Instance sbi_later_monoid_sep_homomorphism `{!BiAffine PROP} :
+ MonoidHomomorphism bi_sep bi_sep (≡) (@sbi_later PROP).
+Proof. split; try apply _. apply later_emp. Qed.
+Global Instance sbi_laterN_sep_homomorphism `{!BiAffine PROP} n :
+ MonoidHomomorphism bi_sep bi_sep (≡) (@sbi_laterN PROP n).
+Proof. split; try apply _. apply laterN_emp. Qed.
+Global Instance sbi_except_0_sep_homomorphism `{!BiAffine PROP} :
+ MonoidHomomorphism bi_sep bi_sep (≡) (@sbi_except_0 PROP).
+Proof. split; try apply _. apply except_0_emp. Qed.
+
+Global Instance sbi_later_monoid_sep_entails_weak_homomorphism :
+ WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@sbi_later PROP).
+Proof. split; try apply _. intros P Q. by rewrite later_sep. Qed.
+Global Instance sbi_laterN_sep_entails_weak_homomorphism n :
+ WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@sbi_laterN PROP n).
+Proof. split; try apply _. intros P Q. by rewrite laterN_sep. Qed.
+Global Instance sbi_except_0_sep_entails_weak_homomorphism :
+ WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@sbi_except_0 PROP).
+Proof. split; try apply _. intros P Q. by rewrite except_0_sep. Qed.
+
+Global Instance sbi_later_monoid_sep_entails_homomorphism :
+ MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@sbi_later PROP).
+Proof. split; try apply _. apply later_intro. Qed.
+Global Instance sbi_laterN_sep_entails_homomorphism n :
+ MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@sbi_laterN PROP n).
+Proof. split; try apply _. apply laterN_intro. Qed.
+Global Instance sbi_except_0_sep_entails_homomorphism :
+ MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@sbi_except_0 PROP).
+Proof. split; try apply _. apply except_0_intro. Qed.
+End sbi_derived.
+End bi.
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 5426213bcae764dfa57aaf3e475a011baeaea309..90453b0e6571d12706cba8f8ea4d3aa5f8544163 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -1,5 +1,5 @@
From iris.algebra Require Import monoid.
-From iris.bi Require Import interface derived_laws big_op plainly updates.
+From iris.bi Require Import interface derived_laws_sbi big_op plainly updates.
From stdpp Require Import hlist.
Class Embed (A B : Type) := embed : A → B.
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index 13198641e5769e0841ed10a2150566b16cc28911..f343197cdc557d5fe8dad7d9d8624c32c8a5734f 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -1,6 +1,6 @@
-From iris.bi Require Import derived_laws.
+From iris.bi Require Import derived_laws_sbi.
From iris.algebra Require Import monoid.
-Import interface.bi derived_laws.bi.
+Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
Class Plainly (A : Type) := plainly : A → A.
Hint Mode Plainly ! : typeclass_instances.
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 40669d7517d369de6b5039cd57c3133bdfb767b7..d35e4007968df31d3e72fb7952e0d41de26e8099 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -1,5 +1,5 @@
From stdpp Require Import coPset.
-From iris.bi Require Import interface derived_laws big_op plainly.
+From iris.bi Require Import interface derived_laws_sbi big_op plainly.
(* We first define operational type classes for the notations, and then later
bundle these operational type classes with the laws. *)
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 4669dfb17a853ca7da4ef8b96f0c84e41214ee7b..8fc614bf61663c9b44102ef86d5d7d39444400d1 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -1089,7 +1089,7 @@ Proof.
Qed.
(* We add a useless hypothesis [BiEmbed PROP PROP'] in order to make
- sure this iinstance is not used when there is no embedding between
+ sure this instance is not used when there is no embedding between
PROP and PROP'.
The first [`{BiEmbed PROP PROP'}] is not considered as a premise by
Coq TC search mechanism because the rest of the hypothesis is dependent
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 3ee4366f7692c31de22b5760cd9d4d507dde2ea9..f4475fcfb286d2edbbdd25f03f078e912c032f01 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1,6 +1,6 @@
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Import base intro_patterns spec_patterns sel_patterns.
-From iris.bi Require Export bi big_op.
+From iris.bi Require Export bi.
From stdpp Require Import namespaces.
From iris.proofmode Require Export classes notation.
From iris.proofmode Require Import class_instances.