_CoqProject

@@ -72,10 +72,14 @@ iris/bi/derived_laws.v
 iris/bi/derived_laws_later.v
 iris/bi/plainly.v
 iris/bi/internal_eq.v
+iris/bi/cmra_valid.v
 iris/bi/big_op.v
 iris/bi/updates.v
 iris/bi/ascii.v
 iris/bi/bi.v
+iris/bi/sbi.v
+iris/bi/sbi_unfold.v
+iris/bi/algebra.v
 iris/bi/monpred.v
 iris/bi/embedding.v
 iris/bi/weakestpre.v
@@ -93,7 +97,6 @@ iris/base_logic/bi.v
 iris/base_logic/derived.v
 iris/base_logic/proofmode.v
 iris/base_logic/base_logic.v
-iris/base_logic/algebra.v
 iris/base_logic/bupd_alt.v
 iris/base_logic/lib/iprop.v
 iris/base_logic/lib/own.v
@@ -147,6 +150,7 @@ iris/proofmode/class_instances_updates.v
 iris/proofmode/class_instances_embedding.v
 iris/proofmode/class_instances_plainly.v
 iris/proofmode/class_instances_internal_eq.v
+iris/proofmode/class_instances_cmra_valid.v
 iris/proofmode/class_instances_frame.v
 iris/proofmode/class_instances_make.v
 iris/proofmode/monpred.v
@@ -187,7 +191,7 @@ iris_heap_lang/lib/array.v
 iris_heap_lang/lib/logatom_lock.v
 
 iris_unstable/algebra/list.v
-iris_unstable/base_logic/algebra.v
+iris_unstable/bi/algebra.v
 iris_unstable/base_logic/mono_list.v
 iris_unstable/heap_lang/interpreter.v
 

iris/base_logic/base_logic.v

 From iris.bi Require Export bi.
-From iris.base_logic Require Export derived proofmode algebra.
+From iris.base_logic Require Export derived proofmode.
 From iris.prelude Require Import options.
 
 (* The trick of having multiple [uPred] modules, which are all exported in

iris/base_logic/bi.v

-From iris.bi Require Export derived_connectives extensions updates internal_eq plainly.
+From iris.bi Require Export derived_connectives extensions.
+From iris.bi Require Export sbi updates internal_eq plainly cmra_valid.
+From iris.si_logic Require Export bi.
+From iris.bi Require Import derived_laws derived_laws_later.
 From iris.base_logic Require Export upred.
 From iris.prelude Require Import options.
 Import uPred_primitive.
@@ -6,10 +9,19 @@ Import uPred_primitive.
 (** BI instances for [uPred], and re-stating the remaining primitive laws in
 terms of the BI interface. This file does *not* unseal. *)
 
+Definition uPred_pure {M} (φ : Prop) : uPred M := uPred_si_pure ⌜ φ ⌝.
 Definition uPred_emp {M} : uPred M := uPred_pure True.
 
 Local Existing Instance entails_po.
 
+(* We need this property multiple times, so let's prove it once. *)
+Local Lemma True_intro M P : uPred_entails (M:=M) P (uPred_pure True).
+Proof.
+  trans (uPred_si_pure (∀ x : False, True) : uPred M).
+  - etrans; last apply si_pure_forall_2. by apply forall_intro.
+  - by apply si_pure_mono, bi.True_intro.
+Qed.
+
 Lemma uPred_bi_mixin (M : ucmra) :
   BiMixin
     uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
@@ -18,7 +30,7 @@ Proof.
   split.
   - exact: entails_po.
   - exact: equiv_entails.
-  - exact: pure_ne.
+  - intros n φ1 φ2 Hφ. apply si_pure_ne. by rewrite Hφ.
   - exact: and_ne.
   - exact: or_ne.
   - exact: impl_ne.
@@ -26,8 +38,14 @@ Proof.
   - exact: exist_ne.
   - exact: sep_ne.
   - exact: wand_ne.
-  - exact: pure_intro.
-  - exact: pure_elim'.
+  - (* φ → P ⊢ ⌜ φ ⌝ (ADMISSIBLE) *)
+    intros φ P ?. etrans; first by apply True_intro.
+    by apply si_pure_mono, bi.pure_intro.
+  - (* (φ → True ⊢ P) → (⌜ φ ⌝ ⊢ P) (ADMISSIBLE) *)
+    intros φ P HφP. etrans; last apply persistently_elim.
+    etrans; last apply si_pure_si_emp_valid.
+    apply si_pure_mono. apply bi.pure_elim'=> ?.
+    rewrite -(si_emp_valid_si_pure True). by apply si_emp_valid_mono, HφP.
   - exact: and_elim_l.
   - exact: and_elim_r.
   - exact: and_intro.
@@ -62,7 +80,7 @@ Proof.
     trans (uPred_forall (M:=M) (λ _ : False, uPred_persistently uPred_emp)).
     + apply forall_intro=>-[].
     + etrans; first exact: persistently_forall_2.
-      apply persistently_mono. exact: pure_intro.
+      apply persistently_mono, True_intro.
   - (* ((<pers> P) ∧ (<pers> Q)) ⊢ <pers> (P ∧ Q) (ADMISSIBLE) *)
     intros P Q.
     trans (uPred_forall (M:=M) (λ b : bool, uPred_persistently (if b then P else Q))).
@@ -77,8 +95,7 @@ Proof.
   - (* <pers> P ∗ Q ⊢ <pers> P (ADMISSIBLE) *)
     intros. etrans; first exact: sep_comm'.
     etrans; last exact: True_sep_2.
-    apply sep_mono; last done.
-    exact: pure_intro.
+    apply sep_mono; last done. apply True_intro.
   - exact: persistently_and_sep_l_1.
 Qed.
 
@@ -106,46 +123,30 @@ Canonical Structure uPredI (M : ucmra) : bi :=
      bi_bi_later_mixin := uPred_bi_later_mixin M;
      bi_bi_persistently_mixin := uPred_bi_persistently_mixin M |}.
 
-Lemma uPred_internal_eq_mixin M : BiInternalEqMixin (uPredI M) (@uPred_internal_eq M).
+Lemma uPred_sbi_mixin M : SbiMixin (uPredI M) uPred_si_pure uPred_si_emp_valid.
 Proof.
   split.
-  - exact: internal_eq_ne.
-  - exact: @internal_eq_refl.
-  - exact: @internal_eq_rewrite.
-  - exact: @fun_ext.
-  - exact: @sig_eq.
-  - exact: @discrete_eq_1.
-  - exact: @later_eq_1.
-  - exact: @later_eq_2.
+  - exact: si_pure_ne.
+  - exact: si_emp_valid_ne.
+  - exact: si_pure_mono.
+  - exact: si_emp_valid_mono.
+  - exact: si_pure_impl_2.
+  - exact: @si_pure_forall_2.
+  - exact: si_pure_later.
+  - (* Absorbing (<si_pure> Pi) (ADMISSIBLE) *)
+    intros Pi. apply True_sep_2.
+  - exact: @si_emp_valid_later_1.
+  - (* <si_emp_valid> P -∗ <si_emp_valid> <affine> P (ADMISSIBLE) *)
+    intros P. apply si_emp_valid_mono, and_intro; [|done].
+    apply bi.True_intro.
+  - exact: si_emp_valid_si_pure.
+  - exact: si_pure_si_emp_valid.
 Qed.
-Global Instance uPred_internal_eq M : BiInternalEq (uPredI M) :=
-  {| bi_internal_eq_mixin := uPred_internal_eq_mixin M |}.
-
-Lemma uPred_plainly_mixin M : BiPlainlyMixin (uPredI M) uPred_plainly.
-Proof.
-  split.
-  - exact: plainly_ne.
-  - exact: plainly_mono.
-  - exact: plainly_elim_persistently.
-  - exact: plainly_idemp_2.
-  - exact: @plainly_forall_2.
-  - exact: plainly_impl_plainly.
-  - (* P ⊢ ■ emp (ADMISSIBLE) *)
-    intros P.
-    trans (uPred_forall (M:=M) (λ _ : False , uPred_plainly uPred_emp)).
-    + apply forall_intro=>[[]].
-    + etrans; first exact: plainly_forall_2.
-      apply plainly_mono. exact: pure_intro.
-  - (* ■ P ∗ Q ⊢ ■ P (ADMISSIBLE) *)
-    intros P Q. etrans; last exact: True_sep_2.
-    etrans; first exact: sep_comm'.
-    apply sep_mono; last done.
-    exact: pure_intro.
-  - exact: later_plainly_1.
-  - exact: later_plainly_2.
-Qed.
-Global Instance uPred_plainly M : BiPlainly (uPredI M) :=
-  {| bi_plainly_mixin := uPred_plainly_mixin M |}.
+Lemma uPred_sbi_prop_ext_mixin M : SbiPropExtMixin (uPredI M) uPred_si_emp_valid.
+Proof. split. apply prop_ext_2. Qed.
+Global Instance uPred_sbi M : Sbi (uPredI M) :=
+  {| sbi_sbi_mixin := uPred_sbi_mixin M;
+     sbi_sbi_prop_ext_mixin := uPred_sbi_prop_ext_mixin M |}.
 
 Lemma uPred_bupd_mixin M : BiBUpdMixin (uPredI M) uPred_bupd.
 Proof.
@@ -156,12 +157,13 @@ Proof.
   - exact: bupd_trans.
   - exact: bupd_frame_r.
 Qed.
-Global Instance uPred_bi_bupd M : BiBUpd (uPredI M) := {| bi_bupd_mixin := uPred_bupd_mixin M |}.
+Global Instance uPred_bi_bupd M : BiBUpd (uPredI M) :=
+  {| bi_bupd_mixin := uPred_bupd_mixin M |}.
 
 (** extra BI instances *)
 
 Global Instance uPred_affine M : BiAffine (uPredI M) | 0.
-Proof. intros P. exact: pure_intro. Qed.
+Proof. intros P. exact: bi.pure_intro. Qed.
 (* Also add this to the global hint database, otherwise [eauto] won't work for
 many lemmas that have [BiAffine] as a premise. *)
 Global Hint Immediate uPred_affine : core.
@@ -170,22 +172,23 @@ Global Instance uPred_persistently_forall M : BiPersistentlyForall (uPredI M).
 Proof. exact: @persistently_forall_2. Qed.
 
 Global Instance uPred_pure_forall M : BiPureForall (uPredI M).
-Proof. exact: @pure_forall_2. Qed.
+Proof.
+  intros A φ. etrans; [apply si_pure_forall_2|].
+  apply si_pure_mono, pure_forall_2.
+Qed.
 
 Global Instance uPred_later_contractive {M} : BiLaterContractive (uPredI M).
 Proof. exact: @later_contractive. Qed.
 
-Global Instance uPred_persistently_impl_plainly M : BiPersistentlyImplPlainly (uPredI M).
-Proof. exact: persistently_impl_plainly. Qed.
-
-Global Instance uPred_plainly_exist_1 M : BiPlainlyExist (uPredI M).
-Proof. exact: @plainly_exist_1. Qed.
+Global Instance uPred_sbi_emp_valid_exist {M} : SbiEmpValidExist (uPredI M).
+Proof. exact: @si_emp_valid_exist_1. Qed.
 
-Global Instance uPred_prop_ext M : BiPropExt (uPredI M).
-Proof. exact: prop_ext_2. Qed.
+Global Instance uPred_persistently_impl_si_pure M :
+  BiPersistentlyImplSiPure (uPredI M).
+Proof. exact: persistently_impl_si_pure. Qed.
 
-Global Instance uPred_bi_bupd_plainly M : BiBUpdPlainly (uPredI M).
-Proof. exact: bupd_plainly. Qed.
+Global Instance uPred_bi_bupd_sbi M : BiBUpdSbi (uPredI M).
+Proof. exact: bupd_si_pure. Qed.
 
 (** Re-state/export lemmas about Iris-specific primitive connectives (own, valid) *)
 
@@ -202,16 +205,16 @@ Section restate.
   Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
 
   Global Instance ownM_ne : NonExpansive (@uPred_ownM M) := uPred_primitive.ownM_ne.
-  Global Instance cmra_valid_ne {A : cmra} : NonExpansive (@uPred_cmra_valid M A) :=
-    uPred_primitive.cmra_valid_ne.
 
   (** Re-exporting primitive lemmas that are not in any interface *)
+  Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
+  Proof. exact: uPred_primitive.ownM_valid. Qed.
   Lemma ownM_op (a1 a2 : M) :
     uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ∗ uPred_ownM a2.
   Proof. exact: uPred_primitive.ownM_op. Qed.
   Lemma persistently_ownM_core (a : M) : uPred_ownM a ⊢ <pers> uPred_ownM (core a).
   Proof. exact: uPred_primitive.persistently_ownM_core. Qed.
-  Lemma ownM_unit P : P ⊢ (uPred_ownM ε).
+  Lemma ownM_unit P : P ⊢ uPred_ownM ε.
   Proof. exact: uPred_primitive.ownM_unit. Qed.
   Lemma later_ownM a : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b).
   Proof. exact: uPred_primitive.later_ownM. Qed.
@@ -219,49 +222,19 @@ Section restate.
     x ~~>: Φ → uPred_ownM x ⊢ |==> ∃ y, ⌜Φ y⌝ ∧ uPred_ownM y.
   Proof. exact: uPred_primitive.bupd_ownM_updateP. Qed.
 
-  (** This is really just a special case of an entailment
-  between two [siProp], but we do not have the infrastructure
-  to express the more general case. This temporary proof rule will
-  be replaced by the proper one eventually. *)
-  Lemma internal_eq_entails {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
-    (a1 ≡ a2 ⊢ b1 ≡ b2) ↔ (∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2).
-  Proof. exact: uPred_primitive.internal_eq_entails. Qed.
-
-  Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
-  Proof. exact: uPred_primitive.ownM_valid. Qed.
-  Lemma cmra_valid_intro {A : cmra} P (a : A) : ✓ a → P ⊢ (✓ a).
-  Proof. exact: uPred_primitive.cmra_valid_intro. Qed.
-  Lemma cmra_valid_elim {A : cmra} (a : A) : ✓ a ⊢ ⌜ ✓{0} a ⌝.
-  Proof. exact: uPred_primitive.cmra_valid_elim. Qed.
-  Lemma plainly_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢ ■ ✓ a.
-  Proof. exact: uPred_primitive.plainly_cmra_valid_1. Qed.
-  Lemma cmra_valid_weaken {A : cmra} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
-  Proof. exact: uPred_primitive.cmra_valid_weaken. Qed.
-
-  (** This is really just a special case of an entailment
-  between two [siProp], but we do not have the infrastructure
-  to express the more general case. This temporary proof rule will
-  be replaced by the proper one eventually. *)
-  Lemma valid_entails {A B : cmra} (a : A) (b : B) :
-    (∀ n, ✓{n} a → ✓{n} b) → ✓ a ⊢ ✓ b.
-  Proof. exact: uPred_primitive.valid_entails. Qed.
-
-  (** Consistency/soundness statement *)
-  Lemma pure_soundness φ : (⊢@{uPredI M} ⌜ φ ⌝) → φ.
-  Proof. apply pure_soundness. Qed.
-
-  Lemma internal_eq_soundness {A : ofe} (x y : A) : (⊢@{uPredI M} x ≡ y) → x ≡ y.
-  Proof. apply internal_eq_soundness. Qed.
-
-  Lemma later_soundness P : (⊢ ▷ P) → ⊢ P.
-  Proof. apply later_soundness. Qed.
-
   (** We restate the unsealing lemmas for the BI layer. The sealing lemmas
   are partially applied so that they also rewrite under binders. *)
-  Local Lemma uPred_emp_unseal : bi_emp = @upred.uPred_pure_def M True.
-  Proof. by rewrite -upred.uPred_pure_unseal. Qed.
-  Local Lemma uPred_pure_unseal : bi_pure = @upred.uPred_pure_def M.
-  Proof. by rewrite -upred.uPred_pure_unseal. Qed.
+  Local Lemma uPred_emp_unseal :
+    bi_emp = @upred.uPred_si_pure_def M (siprop.siProp_pure_def True).
+  Proof. by rewrite -upred.uPred_si_pure_unseal -siprop.siProp_pure_unseal. Qed.
+  Local Lemma uPred_pure_unseal :
+    bi_pure = λ φ, @upred.uPred_si_pure_def M (siprop.siProp_pure_def φ).
+  Proof. by rewrite -upred.uPred_si_pure_unseal -siprop.siProp_pure_unseal. Qed.
+  Local Lemma uPred_si_pure_unseal : si_pure = @upred.uPred_si_pure_def M.
+  Proof. by rewrite -upred.uPred_si_pure_unseal. Qed.
+  Local Lemma uPred_si_emp_valid_unseal :
+    si_emp_valid = @upred.uPred_si_emp_valid_def M.
+  Proof. by rewrite -upred.uPred_si_emp_valid_unseal. Qed.
   Local Lemma uPred_and_unseal : bi_and = @upred.uPred_and_def M.
   Proof. by rewrite -upred.uPred_and_unseal. Qed.
   Local Lemma uPred_or_unseal : bi_or = @upred.uPred_or_def M.
@@ -272,15 +245,10 @@ Section restate.
   Proof. by rewrite -upred.uPred_forall_unseal. Qed.
   Local Lemma uPred_exist_unseal : @bi_exist _ = @upred.uPred_exist_def M.
   Proof. by rewrite -upred.uPred_exist_unseal. Qed.
-  Local Lemma uPred_internal_eq_unseal :
-    @internal_eq _ _ = @upred.uPred_internal_eq_def M.
-  Proof. by rewrite -upred.uPred_internal_eq_unseal. Qed.
   Local Lemma uPred_sep_unseal : bi_sep = @upred.uPred_sep_def M.
   Proof. by rewrite -upred.uPred_sep_unseal. Qed.
   Local Lemma uPred_wand_unseal : bi_wand = @upred.uPred_wand_def M.
   Proof. by rewrite -upred.uPred_wand_unseal. Qed.
-  Local Lemma uPred_plainly_unseal : plainly = @upred.uPred_plainly_def M.
-  Proof. by rewrite -upred.uPred_plainly_unseal. Qed.
   Local Lemma uPred_persistently_unseal :
     bi_persistently = @upred.uPred_persistently_def M.
   Proof. by rewrite -upred.uPred_persistently_unseal. Qed.
@@ -290,11 +258,13 @@ Section restate.
   Proof. by rewrite -upred.uPred_bupd_unseal. Qed.
 
   Local Definition uPred_unseal :=
-    (uPred_emp_unseal, uPred_pure_unseal, uPred_and_unseal, uPred_or_unseal,
+    (uPred_emp_unseal, uPred_pure_unseal,
+    uPred_si_pure_unseal, uPred_si_emp_valid_unseal,
+    uPred_and_unseal, uPred_or_unseal,
     uPred_impl_unseal, uPred_forall_unseal, uPred_exist_unseal,
-    uPred_internal_eq_unseal, uPred_sep_unseal, uPred_wand_unseal,
-    uPred_plainly_unseal, uPred_persistently_unseal, uPred_later_unseal,
-    upred.uPred_ownM_unseal, upred.uPred_cmra_valid_unseal, @uPred_bupd_unseal).
+    uPred_sep_unseal, uPred_wand_unseal,
+    uPred_persistently_unseal, uPred_later_unseal,
+    upred.uPred_ownM_unseal, @uPred_bupd_unseal).
 End restate.
 
 (** A tactic for rewriting with the above lemmas. Unfolds [uPred] goals that use

iris/base_logic/bupd_alt.v

@@ -7,7 +7,7 @@ Set Default Proof Using "Type*".
 
 (** This file contains an alternative version of basic updates, that is
 expression in terms of just the plain modality [■]. *)
-Definition bupd_alt {PROP : bi} `{!BiPlainly PROP} (P : PROP) : PROP :=
+Definition bupd_alt {PROP : bi} `{!Sbi PROP} (P : PROP) : PROP :=
   ∀ R, (P -∗ ■ R) -∗ ■ R.
 
 (** This definition is stated for any BI with a plain modality. The above
@@ -28,7 +28,7 @@ The first two points are shown for any BI with a plain modality. *)
 Local Coercion uPred_holds : uPred >-> Funclass.
 
 Section bupd_alt.
-  Context {PROP : bi} `{!BiPlainly PROP}.
+  Context {PROP : bi} `{!Sbi PROP}.
   Implicit Types P Q R : PROP.
   Notation bupd_alt := (@bupd_alt PROP _).
 
@@ -57,7 +57,8 @@ Section bupd_alt.
 
   (** Any modality conforming with [BiBUpdPlainly] entails the alternative
   definition *)
-  Lemma bupd_bupd_alt `{!BiBUpd PROP, !BiBUpdPlainly PROP} P : (|==> P) ⊢ bupd_alt P.
+  Lemma bupd_bupd_alt `{!BiBUpd PROP, !BiBUpdSbi PROP, !BiAffine PROP} P :
+    (|==> P) ⊢ bupd_alt P.
   Proof. iIntros "HP" (R) "H". by iMod ("H" with "HP") as "?". Qed.
 
   (** We get the usual rule for frame preserving updates if we have an [own]
@@ -79,7 +80,7 @@ End bupd_alt.
 (** The alternative definition entails the ordinary basic update *)
 Lemma bupd_alt_bupd {M} (P : uPred M) : bupd_alt P ⊢ |==> P.
 Proof.
-  rewrite /bupd_alt. uPred.unseal; split=> n x Hx H k y ? Hxy.
+  rewrite /bupd_alt /plainly. uPred.unseal; split=> n x Hx H k y ? Hxy.
   unshelve refine (H {| uPred_holds k _ :=
     ∃ x' : M, ✓{k} (x' ⋅ y) ∧ P k x' |} k y _ _ _).
   - intros n1 n2 x1 x2 (z&?&?) _ ?.
@@ -101,7 +102,8 @@ Lemma ownM_updateP {M : ucmra} x (Φ : M → Prop) (R : uPred M) :
   x ~~>: Φ →
   uPred_ownM x ∗ (∀ y, ⌜Φ y⌝ -∗ uPred_ownM y -∗ ■ R) ⊢ ■ R.
 Proof.
-  uPred.unseal=> Hup; split; intros n z Hv (?&z2&?&[z1 ?]&HR); ofe_subst.
+  intros Hup. rewrite /plainly. uPred.unseal.
+  split. intros n z Hv (?&z2&?&[z1 ?]&HR); ofe_subst.
   destruct (Hup n (Some (z1 ⋅ z2))) as (y&?&?); simpl in *.
   { by rewrite assoc. }
   refine (HR y n z1 _ _ _ n y _ _ _); auto.

iris/base_logic/derived.v

@@ -20,12 +20,8 @@ Section derived.
 
   (** Propers *)
   Global Instance ownM_proper: Proper ((≡) ==> (⊣⊢)) (@uPred_ownM M) := ne_proper _.
-  Global Instance cmra_valid_proper {A : cmra} :
-    Proper ((≡) ==> (⊣⊢)) (@uPred_cmra_valid M A) := ne_proper _.
 
   (** Own and valid derived *)
-  Lemma persistently_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢@{uPredI M} <pers> (✓ a).
-  Proof. by rewrite {1}plainly_cmra_valid_1 plainly_elim_persistently. Qed.
   Lemma intuitionistically_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
   Proof.
     rewrite /bi_intuitionistically affine_affinely=>?; apply (anti_symm _);
@@ -33,25 +29,11 @@ Section derived.
     by rewrite {1}persistently_ownM_core core_id_core.
   Qed.
   Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊢ False.
-  Proof. intros. rewrite ownM_valid cmra_valid_elim. by apply pure_elim'. Qed.
+  Proof. intros. rewrite ownM_valid bi_cmra_valid_elim. by apply pure_elim'. Qed.
   Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
   Proof. intros a b [b' ->]. by rewrite ownM_op sep_elim_l. Qed.
   Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True.
   Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_unit. Qed.
-  Lemma plainly_cmra_valid {A : cmra} (a : A) : ■ ✓ a ⊣⊢ ✓ a.
-  Proof. apply (anti_symm _), plainly_cmra_valid_1. apply plainly_elim, _. Qed.
-  Lemma intuitionistically_cmra_valid {A : cmra} (a : A) : □ ✓ a ⊣⊢ ✓ a.
-  Proof.
-    rewrite /bi_intuitionistically affine_affinely. intros; apply (anti_symm _);
-      first by rewrite persistently_elim.
-    apply:persistently_cmra_valid_1.
-  Qed.
-  Lemma discrete_valid {A : cmra} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
-  Proof.
-    apply (anti_symm _).
-    - rewrite cmra_valid_elim. by apply pure_mono, cmra_discrete_valid.
-    - apply pure_elim'=> ?. by apply cmra_valid_intro.
-  Qed.
 
   Lemma bupd_ownM_update x y : x ~~> y → uPred_ownM x ⊢ |==> uPred_ownM y.
   Proof.
@@ -60,27 +42,16 @@ Section derived.
   Qed.
 
   (** Timeless instances *)
-  Global Instance valid_timeless {A : cmra} `{!CmraDiscrete A} (a : A) :
-    Timeless (✓ a : uPred M)%I.
-  Proof. rewrite /Timeless !discrete_valid. apply (timeless _). Qed.
   Global Instance ownM_timeless (a : M) : Discrete a → Timeless (uPred_ownM a).
   Proof.
     intros ?. rewrite /Timeless later_ownM. apply exist_elim=> b.
     rewrite (timeless (a≡b)) (except_0_intro (uPred_ownM b)) -except_0_and.
     apply except_0_mono. rewrite internal_eq_sym.
     apply (internal_eq_rewrite' b a (uPred_ownM) _);
-      auto using and_elim_l, and_elim_r.
+      [solve_proper|auto using and_elim_l, and_elim_r..].
   Qed.
 
-  (** Plainness *)
-  Global Instance cmra_valid_plain {A : cmra} (a : A) :
-    Plain (✓ a : uPred M)%I.
-  Proof. rewrite /Persistent. apply plainly_cmra_valid_1. Qed.
-
   (** Persistence *)
-  Global Instance cmra_valid_persistent {A : cmra} (a : A) :
-    Persistent (✓ a : uPred M)%I.
-  Proof. rewrite /Persistent. apply persistently_cmra_valid_1. Qed.
   Global Instance ownM_persistent a : CoreId a → Persistent (@uPred_ownM M a).
   Proof.
     intros. rewrite /Persistent -{2}(core_id_core a). apply persistently_ownM_core.
@@ -91,36 +62,6 @@ Section derived.
     MonoidHomomorphism op uPred_sep (≡) (@uPred_ownM M).
   Proof. split; [split|]; try apply _; [apply ownM_op | apply ownM_unit']. Qed.
 
-  (** Derive [NonExpansive]/[Contractive] from an internal statement *)
-  Lemma ne_internal_eq {A B : ofe} (f : A → B) :
-    NonExpansive f ↔ ∀ x1 x2, x1 ≡ x2 ⊢ f x1 ≡ f x2.
-  Proof.
-    split; [apply f_equivI|].
-    intros Hf n x1 x2. by eapply internal_eq_entails.
-  Qed.
-
-  Lemma ne_2_internal_eq {A B C : ofe} (f : A → B → C) :
-    NonExpansive2 f ↔ ∀ x1 x2 y1 y2, x1 ≡ x2 ∧ y1 ≡ y2 ⊢ f x1 y1 ≡ f x2 y2.
-  Proof.
-    split.
-    - intros Hf x1 x2 y1 y2.
-      change ((x1,y1).1 ≡ (x2,y2).1 ∧ (x1,y1).2 ≡ (x2,y2).2
-        ⊢ uncurry f (x1,y1) ≡ uncurry f (x2,y2)).
-      rewrite -prod_equivI. apply ne_internal_eq. solve_proper.
-    - intros Hf n x1 x2 Hx y1 y2 Hy.
-      change (uncurry f (x1,y1) ≡{n}≡ uncurry f (x2,y2)).
-      apply ne_internal_eq; [|done].
-      intros [??] [??]. rewrite prod_equivI. apply Hf.
-  Qed.
-
-  Lemma contractive_internal_eq {A B : ofe} (f : A → B) :
-    Contractive f ↔ ∀ x1 x2, ▷ (x1 ≡ x2) ⊢ f x1 ≡ f x2.
-  Proof.
-    split; [apply f_equivI_contractive|].
-    intros Hf n x1 x2 Hx. specialize (Hf x1 x2).
-    rewrite -later_equivI internal_eq_entails in Hf. apply Hf. by f_contractive.
-  Qed.
-
   (** Soundness statement for our modalities: facts derived under modalities in
   the empty context also without the modalities.
   For basic updates, soundness only holds for plain propositions. *)
@@ -128,7 +69,10 @@ Section derived.
   Proof. rewrite bupd_elim. done. Qed.
 
   Lemma laterN_soundness P n : (⊢ ▷^n P) → ⊢ P.
-  Proof. induction n; eauto using later_soundness. Qed.
+  Proof.
+    induction n as [|n IH]; intros ?; simpl; [done|].
+    by apply IH, later_soundness.
+  Qed.
 
   (** As pure demonstration, we also show that this holds for an arbitrary nesting
   of modalities. We have to do a bit of work to be able to state this theorem
@@ -153,7 +97,7 @@ Section derived.
     move: H. apply bi_emp_valid_mono.
     induction ms as [|m ms IH]; first done; simpl.
     destruct m; simpl; rewrite IH.
-    - rewrite -later_intro. apply bupd_elim. apply _.
+    - rewrite -later_intro. apply: bupd_elim.
     - done.
     - rewrite -later_intro persistently_elim. done.
     - rewrite -later_intro plainly_elim. done.
@@ -163,6 +107,6 @@ Section derived.
   modalities. Again this is just for demonstration and probably not practically
   useful. *)
   Corollary consistency : ¬ ⊢@{uPredI M} False.
-  Proof. intros H. by eapply pure_soundness. Qed.
+  Proof. apply: pure_soundness. Qed.
 End derived.
 End uPred.

iris/base_logic/lib/boxes.v

@@ -94,7 +94,7 @@ Lemma box_own_agree γ Q1 Q2 :
   box_own_prop γ Q1 ∗ box_own_prop γ Q2 ⊢ ▷ (Q1 ≡ Q2).
 Proof.
   rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_r.
-  by rewrite option_validI /= agree_validI agree_equivI later_equivI /=.
+  by rewrite option_validI /= agree_op_invI agree_equivI later_equivI /=.
 Qed.
 
 Lemma box_alloc : ⊢ box N ∅ True.

iris/base_logic/lib/cancelable_invariants.v

@@ -47,7 +47,7 @@ Section proofs.
   Proof. split; [done|]. apply _. Qed.
 
   Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 -∗ cinv_own γ q2 -∗ ⌜q1 + q2 ≤ 1⌝%Qp.
-  Proof. rewrite -frac_valid -uPred.discrete_valid. apply (own_valid_2 γ q1 q2). Qed.
+  Proof. rewrite -frac_valid -bi_cmra_discrete_valid. apply (own_valid_2 γ q1 q2). Qed.
 
   Lemma cinv_own_1_l γ q : cinv_own γ 1 -∗ cinv_own γ q -∗ False.
   Proof.

iris/base_logic/lib/fancy_updates.v

@@ -82,24 +82,24 @@ Proof. rewrite /BiBUpdFUpd uPred_fupd_unseal. by iIntros (E P) ">? [$ $] !> !>".
 
 (** The interaction laws with the plainly modality are only supported when
   we opt out of the support for later credits. *)
-Global Instance uPred_bi_fupd_plainly_no_lc `{!invGS_gen HasNoLc Σ} :
-  BiFUpdPlainly (uPredI (iResUR Σ)).
+Global Instance uPred_bi_fupd_sbi_no_lc `{!invGS_gen HasNoLc Σ} :
+  BiFUpdSbi (uPredI (iResUR Σ)).
 Proof.
   split; rewrite uPred_fupd_unseal /uPred_fupd_def.
-  - iIntros (E P) "H [Hw HE]".
-    iAssert (◇ ■ P)%I as "#>HP".
+  - iIntros (E Pi) "H [Hw HE]".
+    iAssert (◇ <si_pure> Pi)%I as "#>HP".
     { by iMod ("H" with "[$]") as "(_ & _ & HP)". }
     by iFrame.
-  - iIntros (E P Q) "[H HQ] [Hw HE]".
-    iAssert (◇ ■ P)%I as "#>HP".
+  - iIntros (E Pi Q) "[H HQ] [Hw HE]".
+    iAssert (◇ <si_pure> Pi)%I as "#>HP".
     { by iMod ("H" with "HQ [$]") as "(_ & _ & HP)". }
     by iFrame.
-  - iIntros (E P) "H [Hw HE]".
-    iAssert (▷ ◇ ■ P)%I as "#HP".
+  - iIntros (E Pi) "H [Hw HE]".
+    iAssert (▷ ◇ <si_pure> Pi)%I as "#HP".
     { iNext. by iMod ("H" with "[$]") as "(_ & _ & HP)". }
     iFrame. iIntros "!> !> !>". by iMod "HP".
-  - iIntros (E A Φ) "HΦ [Hw HE]".
-    iAssert (◇ ■ ∀ x : A, Φ x)%I as "#>HP".
+  - iIntros (E A Φi) "HΦ [Hw HE]".
+    iAssert (◇ ∀ x : A, <si_pure> Φi x)%I as "#>HP".
     { iIntros (x). by iMod ("HΦ" with "[$Hw $HE]") as "(_&_&?)". }
     by iFrame.
 Qed.

iris/base_logic/lib/own.v

@@ -105,11 +105,9 @@ Local Instance iRes_singleton_ne γ : NonExpansive (@iRes_singleton Σ A _ γ).
 Proof. by intros n a a' Ha; apply discrete_fun_singleton_ne; rewrite Ha. Qed.
 Local Lemma iRes_singleton_validI γ a : ✓ (iRes_singleton γ a) ⊢@{iPropI Σ} ✓ a.
 Proof.
-  rewrite /iRes_singleton.
-  rewrite discrete_fun_validI (forall_elim (inG_id i)) discrete_fun_lookup_singleton.
-  rewrite singleton_validI.
-  trans (✓ cmra_transport inG_prf a : iProp Σ)%I; last by destruct inG_prf.
-  apply valid_entails=> n. apply inG_unfold_validN.
+  sbi_unfold=> n. rewrite /iRes_singleton.
+  rewrite discrete_fun_singleton_validN singleton_validN inG_unfold_validN.
+  by destruct inG_prf.
 Qed.
 Local Lemma iRes_singleton_op γ a1 a2 :
   iRes_singleton γ (a1 ⋅ a2) ≡ iRes_singleton γ a1 ⋅ iRes_singleton γ a2.
@@ -204,7 +202,7 @@ Proof.
   rewrite and_exist_l. f_equiv=> b. rewrite and_exist_l. apply exist_elim=> r'.
   rewrite assoc. apply and_mono_l.
   etrans; [|apply ownM_mono, (cmra_included_l _ r')].
-  eapply (internal_eq_rewrite' _ _ uPred_ownM _); [apply and_elim_r|].
+  eapply (internal_eq_rewrite' _ _ uPred_ownM _ _); [apply and_elim_r|].
   apply and_elim_l.
 Qed.
 

iris/base_logic/proofmode.v

@@ -9,17 +9,6 @@ Section class_instances.
   Context {M : ucmra}.
   Implicit Types P Q R : uPred M.
 
-  Global Instance into_pure_cmra_valid `{!CmraDiscrete A} (a : A) :
-    @IntoPure (uPredI M) (✓ a) (✓ a).
-  Proof. rewrite /IntoPure. by rewrite uPred.discrete_valid. Qed.
-
-  Global Instance from_pure_cmra_valid {A : cmra} (a : A) :
-    @FromPure (uPredI M) false (✓ a) (✓ a).
-  Proof.
-    rewrite /FromPure /=. eapply bi.pure_elim=> // ?.
-    rewrite -uPred.cmra_valid_intro //.
-  Qed.
-
   Global Instance from_sep_ownM (a b1 b2 : M) :
     IsOp a b1 b2 →
     FromSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).

iris/base_logic/upred.v

 From iris.algebra Require Export cmra updates.
 From iris.bi Require Import notation.
+From iris.si_logic Require Import siprop.
 From iris.prelude Require Import options.
 
 Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|] : core.
@@ -253,14 +254,25 @@ Inductive uPred_entails {M} (P Q : uPred M) : Prop :=
 Global Hint Resolve uPred_mono : uPred_def.
 
 (** logical connectives *)
-Local Program Definition uPred_pure_def {M} (φ : Prop) : uPred M :=
-  {| uPred_holds n x := φ |}.
-Solve Obligations with done.
-Local Definition uPred_pure_aux : seal (@uPred_pure_def). Proof. by eexists. Qed.
-Definition uPred_pure := uPred_pure_aux.(unseal).
-Global Arguments uPred_pure {M}.
-Local Definition uPred_pure_unseal :
-  @uPred_pure = @uPred_pure_def := uPred_pure_aux.(seal_eq).
+Local Program Definition uPred_si_pure_def {M} (Pi : siProp) : uPred M :=
+  {| uPred_holds n x := siProp_holds Pi n |}.
+Solve Obligations with naive_solver eauto using siProp_closed.
+Local Definition uPred_si_pure_aux : seal (@uPred_si_pure_def).
+Proof. by eexists. Qed.
+Definition uPred_si_pure := uPred_si_pure_aux.(unseal).
+Global Arguments uPred_si_pure {M}.
+Local Definition uPred_si_pure_unseal :
+  @uPred_si_pure = @uPred_si_pure_def := uPred_si_pure_aux.(seal_eq).
+
+Local Program Definition uPred_si_emp_valid_def {M} (P : uPred M) : siProp :=
+  {| siProp_holds n := P n ε |}.
+Solve Obligations with naive_solver eauto with uPred_def.
+Local Definition uPred_si_emp_valid_aux : seal (@uPred_si_emp_valid_def).
+Proof. by eexists. Qed.
+Definition uPred_si_emp_valid := uPred_si_emp_valid_aux.(unseal).
+Global Arguments uPred_si_emp_valid {M}.
+Local Definition uPred_si_emp_valid_unseal :
+  @uPred_si_emp_valid = @uPred_si_emp_valid_def := uPred_si_emp_valid_aux.(seal_eq).
 
 Local Program Definition uPred_and_def {M} (P Q : uPred M) : uPred M :=
   {| uPred_holds n x := P n x ∧ Q n x |}.
@@ -312,16 +324,6 @@ Global Arguments uPred_exist {M A}.
 Local Definition uPred_exist_unseal :
   @uPred_exist = @uPred_exist_def := uPred_exist_aux.(seal_eq).
 
-Local Program Definition uPred_internal_eq_def {M} {A : ofe} (a1 a2 : A) : uPred M :=
-  {| uPred_holds n x := a1 ≡{n}≡ a2 |}.
-Solve Obligations with naive_solver eauto 2 using dist_le.
-Local Definition uPred_internal_eq_aux : seal (@uPred_internal_eq_def).
-Proof. by eexists. Qed.
-Definition uPred_internal_eq := uPred_internal_eq_aux.(unseal).
-Global Arguments uPred_internal_eq {M A}.
-Local Definition uPred_internal_eq_unseal :
-  @uPred_internal_eq = @uPred_internal_eq_def := uPred_internal_eq_aux.(seal_eq).
-
 Local Program Definition uPred_sep_def {M} (P Q : uPred M) : uPred M :=
   {| uPred_holds n x := ∃ x1 x2, x ≡{n}≡ x1 ⋅ x2 ∧ P n x1 ∧ Q n x2 |}.
 Next Obligation.
@@ -349,18 +351,6 @@ Global Arguments uPred_wand {M}.
 Local Definition uPred_wand_unseal :
   @uPred_wand = @uPred_wand_def := uPred_wand_aux.(seal_eq).
 
-(* Equivalently, this could be `∀ y, P n y`.  That's closer to the intuition
-   of "embedding the step-indexed logic in Iris", but the two are equivalent
-   because Iris is afine.  The following is easier to work with. *)
-Local Program Definition uPred_plainly_def {M} (P : uPred M) : uPred M :=
-  {| uPred_holds n x := P n ε |}.
-Solve Obligations with naive_solver eauto using uPred_mono, ucmra_unit_validN.
-Local Definition uPred_plainly_aux : seal (@uPred_plainly_def). Proof. by eexists. Qed.
-Definition uPred_plainly := uPred_plainly_aux.(unseal).
-Global Arguments uPred_plainly {M}.
-Local Definition uPred_plainly_unseal :
-  @uPred_plainly = @uPred_plainly_def := uPred_plainly_aux.(seal_eq).
-
 Local Program Definition uPred_persistently_def {M} (P : uPred M) : uPred M :=
   {| uPred_holds n x := P n (core x) |}.
 Solve Obligations with naive_solver eauto using uPred_mono, cmra_core_monoN.
@@ -394,16 +384,6 @@ Global Arguments uPred_ownM {M}.
 Local Definition uPred_ownM_unseal :
   @uPred_ownM = @uPred_ownM_def := uPred_ownM_aux.(seal_eq).
 
-Local Program Definition uPred_cmra_valid_def {M} {A : cmra} (a : A) : uPred M :=
-  {| uPred_holds n x := ✓{n} a |}.
-Solve Obligations with naive_solver eauto 2 using cmra_validN_le.
-Local Definition uPred_cmra_valid_aux : seal (@uPred_cmra_valid_def).
-Proof. by eexists. Qed.
-Definition uPred_cmra_valid := uPred_cmra_valid_aux.(unseal).
-Global Arguments uPred_cmra_valid {M A}.
-Local Definition uPred_cmra_valid_unseal :
-  @uPred_cmra_valid = @uPred_cmra_valid_def := uPred_cmra_valid_aux.(seal_eq).
-
 Local Program Definition uPred_bupd_def {M} (Q : uPred M) : uPred M :=
   {| uPred_holds n x := ∀ k yf,
       k ≤ n → ✓{k} (x ⋅ yf) → ∃ x', ✓{k} (x' ⋅ yf) ∧ Q k x' |}.
@@ -420,19 +400,17 @@ Global Arguments uPred_bupd {M}.
 Local Definition uPred_bupd_unseal :
   @uPred_bupd = @uPred_bupd_def := uPred_bupd_aux.(seal_eq).
 
-(** Global uPred-specific Notation *)
-Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : bi_scope.
-
 (** Primitive logical rules.
     These are not directly usable later because they do not refer to the BI
     connectives. *)
 Module uPred_primitive.
 Local Definition uPred_unseal :=
-  (uPred_pure_unseal, uPred_and_unseal, uPred_or_unseal, uPred_impl_unseal,
-  uPred_forall_unseal, uPred_exist_unseal, uPred_internal_eq_unseal,
-  uPred_sep_unseal, uPred_wand_unseal, uPred_plainly_unseal,
+  (uPred_si_pure_unseal, uPred_si_emp_valid_unseal,
+  uPred_and_unseal, uPred_or_unseal, uPred_impl_unseal,
+  uPred_forall_unseal, uPred_exist_unseal,
+  uPred_sep_unseal, uPred_wand_unseal,
   uPred_persistently_unseal, uPred_later_unseal, uPred_ownM_unseal,
-  uPred_cmra_valid_unseal, @uPred_bupd_unseal).
+  @uPred_bupd_unseal).
 Ltac unseal :=
   rewrite !uPred_unseal /=.
 
@@ -442,6 +420,7 @@ Section primitive.
   Implicit Types P Q : uPred M.
   Implicit Types A : Type.
   Local Arguments uPred_holds {_} !_ _ _ /.
+  Local Arguments siProp_holds !_ _ /.
   Local Hint Immediate uPred_in_entails : core.
 
   (** The notations below are implicitly local due to the section, so we do not
@@ -451,9 +430,11 @@ Section primitive.
   Notation "P ⊣⊢ Q" := (@uPred_equiv M P%I Q%I) : stdpp_scope.
   Notation "(⊣⊢)" := (@uPred_equiv M) (only parsing) : stdpp_scope.
 
-  Notation "'True'" := (uPred_pure True) : bi_scope.
-  Notation "'False'" := (uPred_pure False) : bi_scope.
-  Notation "'⌜' φ '⌝'" := (uPred_pure φ%type%stdpp) : bi_scope.
+  Notation "<si_pure> Pi" := (uPred_si_pure Pi) : bi_scope.
+  Notation "<si_emp_valid> P" := (uPred_si_emp_valid P).
+  Notation "'⌜' φ '⌝'" := (<si_pure> siProp_pure φ%type%stdpp)%I : bi_scope.
+  Notation "'True'" := ⌜ True ⌝%I : bi_scope.
+  Notation "'False'" := ⌜ False ⌝%I : bi_scope.
   Infix "∧" := uPred_and : bi_scope.
   Infix "∨" := uPred_or : bi_scope.
   Infix "→" := uPred_impl : bi_scope.
@@ -464,8 +445,6 @@ Section primitive.
   Infix "∗" := uPred_sep : bi_scope.
   Infix "-∗" := uPred_wand : bi_scope.
   Notation "□ P" := (uPred_persistently P) : bi_scope.
-  Notation "■ P" := (uPred_plainly P) : bi_scope.
-  Notation "x ≡ y" := (uPred_internal_eq x y) : bi_scope.
   Notation "▷ P" := (uPred_later P) : bi_scope.
   Notation "|==> P" := (uPred_bupd P) : bi_scope.
 
@@ -492,8 +471,14 @@ Section primitive.
   Qed.
 
   (** Non-expansiveness and setoid morphisms *)
-  Lemma pure_ne n : Proper (iff ==> dist n) (@uPred_pure M).
-  Proof. intros φ1 φ2 Hφ. by unseal; split=> -[|m] ?; try apply Hφ. Qed.
+  Lemma si_pure_ne : NonExpansive (@uPred_si_pure M).
+  Proof. intros n Pi Pi' HPi. unseal; split; intros; by apply HPi. Qed.
+
+  Lemma si_emp_valid_ne : NonExpansive (@uPred_si_emp_valid M).
+  Proof.
+    intros n P P' HP.
+    unseal; split; intros; apply HP; auto using ucmra_unit_validN.
+  Qed.
 
   Lemma and_ne : NonExpansive2 (@uPred_and M).
   Proof.
@@ -529,14 +514,6 @@ Section primitive.
       apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
   Qed.
 
-  Lemma internal_eq_ne (A : ofe) :
-    NonExpansive2 (@uPred_internal_eq M A).
-  Proof.
-    intros n x x' Hx y y' Hy; split=> n' z; unseal; split; intros; simpl in *.
-    - by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
-    - by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
-  Qed.
-
   Lemma forall_ne A n :
     Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_forall M A).
   Proof.
@@ -556,12 +533,6 @@ Section primitive.
     eapply HPQ; eauto using cmra_validN_S.
   Qed.
 
-  Lemma plainly_ne : NonExpansive (@uPred_plainly M).
-  Proof.
-    intros n P1 P2 HP.
-    unseal; split=> n' x; split; apply HP; eauto using ucmra_unit_validN.
-  Qed.
-
   Lemma persistently_ne : NonExpansive (@uPred_persistently M).
   Proof.
     intros n P1 P2 HP.
@@ -574,13 +545,6 @@ Section primitive.
     unseal; split=> n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia.
   Qed.
 
-  Lemma cmra_valid_ne {A : cmra} :
-    NonExpansive (@uPred_cmra_valid M A).
-  Proof.
-    intros n a b Ha; unseal; split=> n' x ? /=.
-    by rewrite (dist_le _ _ _ _ Ha); last lia.
-  Qed.
-
   Lemma bupd_ne : NonExpansive (@uPred_bupd M).
   Proof.
     intros n P Q HPQ.
@@ -589,14 +553,59 @@ Section primitive.
       exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l.
   Qed.
 
-  (** Introduction and elimination rules *)
-  Lemma pure_intro φ P : φ → P ⊢ ⌜φ⌝.
-  Proof. by intros ?; unseal; split. Qed.
-  Lemma pure_elim' φ P : (φ → True ⊢ P) → ⌜φ⌝ ⊢ P.
-  Proof. unseal; intros HP; split=> n x ??. by apply HP. Qed.
-  Lemma pure_forall_2 {A} (φ : A → Prop) : (∀ x : A, ⌜φ x⌝) ⊢ ⌜∀ x : A, φ x⌝.
+  (** Rules for the [siProp] embedding *)
+  Lemma si_pure_mono Pi Qi : siProp_entails Pi Qi → <si_pure> Pi ⊢ <si_pure> Qi.
+  Proof. intros HPQi. unseal; split=> n ??. apply HPQi. Qed.
+  Lemma si_emp_valid_mono P Q :
+    (P ⊢ Q) → siProp_entails (<si_emp_valid> P) (<si_emp_valid> Q).
+  Proof. intros HPQ. unseal; split=> n. apply HPQ, ucmra_unit_validN. Qed.
+
+  Lemma si_pure_impl_2 Pi Qi :
+    (<si_pure> Pi → <si_pure> Qi) ⊢ <si_pure> siProp_impl Pi Qi.
+  Proof.
+    unseal; siProp_primitive.unseal. split; simpl; eauto using cmra_validN_le.
+  Qed.
+  Lemma si_pure_forall_2 {A} (Φi : A → siProp) :
+   (∀ x, <si_pure> Φi x) ⊢ <si_pure> siProp_forall Φi.
+  Proof. by unseal; siProp_primitive.unseal. Qed.
+  Lemma si_pure_later Pi : <si_pure> siProp_later Pi ⊣⊢ ▷ <si_pure> Pi.
+  Proof. by unseal; siProp_primitive.unseal. Qed.
+
+  Lemma si_emp_valid_later_1 P :
+    siProp_entails (<si_emp_valid> ▷ P) (siProp_later (<si_emp_valid> P)).
+  Proof. by unseal; siProp_primitive.unseal. Qed.
+  Lemma si_emp_valid_exist_1 {A} (Φ : A → uPred M) :
+    siProp_entails (<si_emp_valid> ∃ x, Φ x)
+                   (siProp_exist (λ x, <si_emp_valid> Φ x)).
+  Proof. by unseal; siProp_primitive.unseal. Qed.
+
+  Lemma si_emp_valid_si_pure Pi :
+    <si_emp_valid> (<si_pure> Pi : uPred M)%I ≡ Pi.
   Proof. by unseal. Qed.
+  Lemma si_pure_si_emp_valid P :
+    <si_pure> <si_emp_valid> P ⊢ □ P.
+  Proof.
+    unseal. split=> /= n x _ ?.
+    eapply uPred_mono with n ε; eauto using ucmra_unit_leastN.
+  Qed.
 
+  Lemma persistently_impl_si_pure Pi Q :
+    (<si_pure> Pi → □ Q) ⊢ □ (<si_pure> Pi → Q).
+  Proof.
+    unseal; split=> /= n x ? HPQ n' x' ????.
+    eapply uPred_mono with n' (core x)=>//; [|by apply cmra_included_includedN].
+    apply (HPQ n' x); eauto using cmra_validN_le.
+  Qed.
+
+  Lemma prop_ext_2 P Q :
+    siProp_entails (<si_emp_valid> ((P -∗ Q) ∧ (Q -∗ P)))
+                   (siProp_internal_eq P Q).
+  Proof.
+    unseal; siProp_primitive.unseal.
+    split=> n /=. setoid_rewrite (left_id ε op). split; naive_solver.
+  Qed.
+
+  (** Introduction and elimination rules *)
   Lemma and_elim_l P Q : P ∧ Q ⊢ P.
   Proof. by unseal; split=> n x ? [??]. Qed.
   Lemma and_elim_r P Q : P ∧ Q ⊢ Q.
@@ -642,7 +651,8 @@ Section primitive.
   Qed.
   Lemma True_sep_1 P : P ⊢ True ∗ P.
   Proof.
-    unseal; split; intros n x ??. exists (core x), x. by rewrite cmra_core_l.
+    unseal; siProp_primitive.unseal; split; intros n x ??.
+    exists (core x), x. by rewrite cmra_core_l.
   Qed.
   Lemma True_sep_2 P : True ∗ P ⊢ P.
   Proof.
@@ -694,40 +704,6 @@ Section primitive.
     by rewrite cmra_core_l.
   Qed.
 
-  (** Plainly *)
-  Lemma plainly_mono P Q : (P ⊢ Q) → ■ P ⊢ ■ Q.
-  Proof. intros HP; unseal; split=> n x ? /=. apply HP, ucmra_unit_validN. Qed.
-  Lemma plainly_elim_persistently P : ■ P ⊢ □ P.
-  Proof. unseal; split; simpl; eauto using uPred_mono, ucmra_unit_leastN. Qed.
-  Lemma plainly_idemp_2 P : ■ P ⊢ ■ ■ P.
-  Proof. unseal; split=> n x ?? //. Qed.
-
-  Lemma plainly_forall_2 {A} (Ψ : A → uPred M) : (∀ a, ■ Ψ a) ⊢ (■ ∀ a, Ψ a).
-  Proof. by unseal. Qed.
-  Lemma plainly_exist_1 {A} (Ψ : A → uPred M) : (■ ∃ a, Ψ a) ⊢ (∃ a, ■ Ψ a).
-  Proof. by unseal. Qed.
-
-  Lemma prop_ext_2 P Q : ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q.
-  Proof.
-    unseal; split=> n x ? /=. setoid_rewrite (left_id ε op). split; naive_solver.
-  Qed.
-
-  (* The following two laws are very similar, and indeed they hold not just for □
-     and ■, but for any modality defined as `M P n x := ∀ y, R x y → P n y`. *)
-  Lemma persistently_impl_plainly P Q : (■ P → □ Q) ⊢ □ (■ P → Q).
-  Proof.
-    unseal; split=> /= n x ? HPQ n' x' ????.
-    eapply uPred_mono with n' (core x)=>//; [|by apply cmra_included_includedN].
-    apply (HPQ n' x); eauto using cmra_validN_le.
-  Qed.
-
-  Lemma plainly_impl_plainly P Q : (■ P → ■ Q) ⊢ ■ (■ P → Q).
-  Proof.
-    unseal; split=> /= n x ? HPQ n' x' ????.
-    eapply uPred_mono with n' ε=>//; [|by apply cmra_included_includedN].
-    apply (HPQ n' x); eauto using cmra_validN_le.
-  Qed.
-
   (** Later *)
   Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
   Proof.
@@ -761,7 +737,7 @@ Section primitive.
 
   Lemma later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P).
   Proof.
-    unseal; split=> -[|n] x ? /= HP; [by left|right].
+    unseal; siProp_primitive.unseal; split=> -[|n] x ? /= HP; [by left|right].
     intros [|n'] x' ????; eauto using uPred_mono, cmra_included_includedN.
   Qed.
 
@@ -769,53 +745,6 @@ Section primitive.
   Proof. by unseal. Qed.
   Lemma later_persistently_2 P : □ ▷ P ⊢ ▷ □ P.
   Proof. by unseal. Qed.
-  Lemma later_plainly_1 P : ▷ ■ P ⊢ ■ ▷ P.
-  Proof. by unseal. Qed.
-  Lemma later_plainly_2 P : ■ ▷ P ⊢ ▷ ■ P.
-  Proof. by unseal. Qed.
-
-  (** Internal equality *)
-  Lemma internal_eq_refl {A : ofe} P (a : A) : P ⊢ (a ≡ a).
-  Proof. unseal; by split=> n x ??; simpl. Qed.
-  Lemma internal_eq_rewrite {A : ofe} a b (Ψ : A → uPred M) :
-    NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
-  Proof. intros HΨ. unseal; split=> n x ?? n' x' ??? Ha. by apply HΨ with n a. Qed.
-
-  Lemma fun_ext {A} {B : A → ofe} (g1 g2 : discrete_fun B) :
-    (∀ i, g1 i ≡ g2 i) ⊢ g1 ≡ g2.
-  Proof. by unseal. Qed.
-  Lemma sig_eq {A : ofe} (P : A → Prop) (x y : sigO P) :
-    proj1_sig x ≡ proj1_sig y ⊢ x ≡ y.
-  Proof. by unseal. Qed.
-
-  Lemma later_eq_1 {A : ofe} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y).
-  Proof.
-    unseal. split. intros [|n]; simpl; [done|].
-    intros ?? Heq; apply Heq; auto.
-  Qed.
-  Lemma later_eq_2 {A : ofe} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y.
-  Proof.
-    unseal. split. intros n ? ? Hn; split; intros m Hlt; simpl in *.
-    destruct n as [|n]; first lia.
-    eauto using dist_le with si_solver.
-  Qed.
-
-  Lemma discrete_eq_1 {A : ofe} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ b⌝.
-  Proof.
-    unseal=> ?. split=> n x ?. by apply (discrete_iff n).
-  Qed.
-
-  (** This is really just a special case of an entailment
-  between two [siProp], but we do not have the infrastructure
-  to express the more general case. This temporary proof rule will
-  be replaced by the proper one eventually. *)
-  Lemma internal_eq_entails {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
-    (a1 ≡ a2 ⊢ b1 ≡ b2) ↔ (∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2).
-  Proof.
-    split.
-    - unseal=> -[Hsi] n. apply (Hsi _ ε), ucmra_unit_validN.
-    - unseal=> Hsi. split=>n x ?. apply Hsi.
-  Qed.
 
   (** Basic update modality *)
   Lemma bupd_intro P : P ⊢ |==> P.
@@ -839,11 +768,10 @@ Section primitive.
     exists (x' ⋅ x2); split; first by rewrite -assoc.
     exists x', x2. eauto using uPred_mono, cmra_validN_op_l, cmra_validN_op_r.
   Qed.
-  Lemma bupd_plainly P : (|==> ■ P) ⊢ P.
+  Lemma bupd_si_pure Pi : (|==> <si_pure> Pi) ⊢ <si_pure> Pi.
   Proof.
     unseal; split => n x Hnx /= Hng.
     destruct (Hng n ε) as [? [_ Hng']]; try rewrite right_id; auto.
-    eapply uPred_mono; eauto using ucmra_unit_leastN.
   Qed.
 
   (** Own *)
@@ -865,9 +793,11 @@ Section primitive.
   Qed.
   Lemma ownM_unit P : P ⊢ (uPred_ownM ε).
   Proof. unseal; split=> n x ??; by  exists x; rewrite left_id. Qed.
-  Lemma later_ownM a : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b).
+  Lemma later_ownM a :
+    ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ <si_pure> siProp_internal_eq a b.
   Proof.
-    unseal; split=> -[|n] x /= ? Hax; first by eauto using ucmra_unit_leastN.
+    unseal; siProp_primitive.unseal.
+    split=> -[|n] x /= ? Hax; first by eauto using ucmra_unit_leastN.
     destruct Hax as [y ?].
     destruct (cmra_extend n x a y) as (a'&y'&Hx&?&?); auto using cmra_validN_S.
     exists a'. rewrite Hx. eauto using cmra_includedN_l.
@@ -876,52 +806,17 @@ Section primitive.
   Lemma bupd_ownM_updateP x (Φ : M → Prop) :
     x ~~>: Φ → uPred_ownM x ⊢ |==> ∃ y, ⌜Φ y⌝ ∧ uPred_ownM y.
   Proof.
-    unseal=> Hup; split=> n x2 ? [x3 Hx] k yf ??.
+    unseal; siProp_primitive.unseal=> Hup; split=> n x2 ? [x3 Hx] k yf ??.
     destruct (Hup k (Some (x3 ⋅ yf))) as (y&?&?); simpl in *.
     { rewrite /= assoc -(dist_le _ _ _ _ Hx); auto. }
     exists (y ⋅ x3); split; first by rewrite -assoc.
     exists y; eauto using cmra_includedN_l.
   Qed.
 
-  (** Valid *)
-  Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
-  Proof.
-    unseal; split=> n x Hv [a' ?]; ofe_subst; eauto using cmra_validN_op_l.
-  Qed.
-  Lemma cmra_valid_intro {A : cmra} P (a : A) : ✓ a → P ⊢ (✓ a).
-  Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. Qed.
-  Lemma cmra_valid_elim {A : cmra} (a : A) : ✓ a ⊢ ⌜ ✓{0} a ⌝.
-  Proof. unseal; split=> n x ??; apply cmra_validN_le with n; auto. Qed.
-  Lemma plainly_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢ ■ ✓ a.
-  Proof. by unseal. Qed.
-  Lemma cmra_valid_weaken {A : cmra} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
-  Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.
-
-  (** This is really just a special case of an entailment
-  between two [siProp], but we do not have the infrastructure
-  to express the more general case. This temporary proof rule will
-  be replaced by the proper one eventually. *)
-  Lemma valid_entails {A B : cmra} (a : A) (b : B) :
-    (∀ n, ✓{n} a → ✓{n} b) → ✓ a ⊢ ✓ b.
-  Proof. unseal=> Hval. split=>n x ?. apply Hval. Qed.
-
-  (** Consistency/soundness statement *)
-  (** The lemmas [pure_soundness] and [internal_eq_soundness] should become an
-  instance of [siProp] soundness in the future. *)
-  Lemma pure_soundness φ : (True ⊢ ⌜ φ ⌝) → φ.
-  Proof. unseal=> -[H]. by apply (H 0 ε); eauto using ucmra_unit_validN. Qed.
-
-  Lemma internal_eq_soundness {A : ofe} (x y : A) : (True ⊢ x ≡ y) → x ≡ y.
-  Proof.
-    unseal=> -[H]. apply equiv_dist=> n.
-    by apply (H n ε); eauto using ucmra_unit_validN.
-  Qed.
-
-  Lemma later_soundness P : (True ⊢ ▷ P) → (True ⊢ P).
+  Lemma ownM_valid (a : M) : uPred_ownM a ⊢ <si_pure> siProp_cmra_valid a.
   Proof.
-    unseal=> -[HP]; split=> n x Hx _.
-    apply uPred_mono with n ε; eauto using ucmra_unit_leastN.
-    by apply (HP (S n)); eauto using ucmra_unit_validN.
+    unseal; siProp_primitive.unseal.
+    split=> n x Hv [a' ?]; ofe_subst; eauto using cmra_validN_op_l.
   Qed.
 End primitive.
 End uPred_primitive.

iris/base_logic/algebra.v → iris/bi/algebra.v

 From iris.algebra Require Import cmra view auth agree csum list excl gmap.
 From iris.algebra.lib Require Import excl_auth gmap_view dfrac_agree.
-From iris.base_logic Require Import bi derived.
+From iris.bi Require Export sbi_unfold derived_laws.
 From iris.prelude Require Import options.
-
-(** Internalized properties of our CMRA constructions. *)
-Local Coercion uPred_holds : uPred >-> Funclass.
-
-Section upred.
-  Context {M : ucmra}.
-
-  (* Force implicit argument M *)
-  Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P Q).
-  Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
-  Notation "⊢ Q" := (bi_entails (PROP:=uPredI M) True Q).
+Local Set Default Proof Using "Type*".
+
+Section algebra.
+  Context `{!Sbi PROP}.
+
+  (* Force implicit argument [PROP] *)
+  Notation "P ⊢ Q" := (bi_entails (PROP:=PROP) P Q).
+  Notation "P ⊣⊢ Q" := (equiv (A:=PROP) P%I Q%I).
+  Notation "⊢ Q" := (bi_emp_valid (PROP:=PROP) Q).
+
+  Lemma ucmra_unit_validI {A : ucmra} : ⊢ ✓ (ε : A).
+  Proof. sbi_unfold. apply ucmra_unit_validN. Qed.
+  Lemma cmra_validI_op_r {A : cmra} (x y : A) : ✓ (x ⋅ y) ⊢ ✓ y.
+  Proof. sbi_unfold=> n. apply cmra_validN_op_r. Qed.
+  Lemma cmra_validI_op_l {A : cmra} (x y : A) : ✓ (x ⋅ y) ⊢ ✓ x.
+  Proof. sbi_unfold=> n. apply cmra_validN_op_l. Qed.
+  Lemma cmra_later_opI `{!CmraTotal A} (x y1 y2 : A) :
+    ▷ (✓ x ∧ x ≡ y1 ⋅ y2) ⊢ ∃ z1 z2, x ≡ z1 ⋅ z2 ∧ ▷ (z1 ≡ y1) ∧ ▷ (z2 ≡ y2).
+  Proof.
+    sbi_unfold=> -[|n].
+    - intros _. exists x, (core x). by rewrite cmra_core_r.
+    - intros [??].
+      destruct (cmra_extend n x y1 y2) as (z1 & z2 & ? & ? & ?); [done..|].
+      exists z1, z2. auto using equiv_dist.
+  Qed.
+  Lemma cmra_morphism_validI {A B : cmra} (f : A → B) `{!CmraMorphism f} x :
+    ✓ x ⊢ ✓ (f x).
+  Proof. sbi_unfold=> n. by apply cmra_morphism_validN. Qed.
 
   Lemma prod_validI {A B : cmra} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
-  Proof. by uPred.unseal. Qed.
+  Proof. by sbi_unfold. Qed.
   Lemma option_validI {A : cmra} (mx : option A) :
-    ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True : uPred M end.
-  Proof. uPred.unseal. by destruct mx. Qed.
+    ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True end.
+  Proof. destruct mx; by sbi_unfold. Qed.
   Lemma discrete_fun_validI {A} {B : A → ucmra} (g : discrete_fun B) :
     ✓ g ⊣⊢ ∀ i, ✓ g i.
-  Proof. by uPred.unseal. Qed.
+  Proof. by sbi_unfold. Qed.
 
   Section gmap_ofe.
     Context `{Countable K} {A : ofe}.
@@ -29,11 +46,11 @@ Section upred.
     Implicit Types i : K.
 
     Lemma gmap_equivI m1 m2 : m1 ≡ m2 ⊣⊢ ∀ i, m1 !! i ≡ m2 !! i.
-    Proof. by uPred.unseal. Qed.
+    Proof. by sbi_unfold. Qed.
 
     Lemma gmap_union_equiv_eqI m m1 m2 :
       m ≡ m1 ∪ m2 ⊣⊢ ∃ m1' m2', ⌜ m = m1' ∪ m2' ⌝ ∧ m1' ≡ m1 ∧ m2' ≡ m2.
-    Proof. uPred.unseal; split=> n x _. apply gmap_union_dist_eq. Qed.
+    Proof. sbi_unfold=> n. apply gmap_union_dist_eq. Qed.
   End gmap_ofe.
 
   Section gmap_cmra.
@@ -41,16 +58,9 @@ Section upred.
     Implicit Types m : gmap K A.
 
     Lemma gmap_validI m : ✓ m ⊣⊢ ∀ i, ✓ (m !! i).
-    Proof. by uPred.unseal. Qed.
+    Proof. by sbi_unfold. Qed.
     Lemma singleton_validI i x : ✓ ({[ i := x ]} : gmap K A) ⊣⊢ ✓ x.
-    Proof.
-      rewrite gmap_validI. apply: anti_symm.
-      - rewrite (bi.forall_elim i) lookup_singleton option_validI. done.
-      - apply bi.forall_intro=>j. destruct (decide (i = j)) as [<-|Hne].
-        + rewrite lookup_singleton option_validI. done.
-        + rewrite lookup_singleton_ne // option_validI.
-          apply bi.True_intro.
-    Qed.
+    Proof. sbi_unfold=> n. apply singleton_validN. Qed.
   End gmap_cmra.
 
   Section list_ofe.
@@ -58,16 +68,26 @@ Section upred.
     Implicit Types l : list A.
 
     Lemma list_equivI l1 l2 : l1 ≡ l2 ⊣⊢ ∀ i, l1 !! i ≡ l2 !! i.
-    Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed.
+    Proof. sbi_unfold. intros n. apply list_dist_lookup. Qed.
   End list_ofe.
 
   Section excl.
     Context {A : ofe}.
     Implicit Types x : excl A.
 
+    Lemma excl_equivI x y :
+      x ≡ y ⊣⊢ match x, y with
+                          | Excl a, Excl b => a ≡ b
+                          | ExclBot, ExclBot => True
+                          | _, _ => False
+                          end.
+    Proof.
+      destruct x, y; sbi_unfold; (split; [by inversion 1|by try constructor]).
+    Qed.
+
     Lemma excl_validI x :
       ✓ x ⊣⊢ if x is ExclBot then False else True.
-    Proof. uPred.unseal. by destruct x. Qed.
+    Proof. destruct x; sbi_unfold; (split; [by inversion 1|by try constructor]). Qed.
   End excl.
 
   Section agree.
@@ -76,31 +96,17 @@ Section upred.
     Implicit Types x y : agree A.
 
     Lemma agree_equivI a b : to_agree a ≡ to_agree b ⊣⊢ (a ≡ b).
-    Proof.
-      uPred.unseal. do 2 split.
-      - intros Hx. exact: (inj to_agree).
-      - intros Hx. exact: to_agree_ne.
-    Qed.
-    Lemma agree_validI x y : ✓ (x ⋅ y) ⊢ x ≡ y.
-    Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_invN. Qed.
+    Proof. sbi_unfold=> n. apply: inj_iff. Qed.
+    Lemma agree_op_invI x y : ✓ (x ⋅ y) ⊢ x ≡ y.
+    Proof. sbi_unfold=> n. apply agree_op_invN. Qed.
 
     Lemma to_agree_validI a : ⊢ ✓ to_agree a.
-    Proof. uPred.unseal; done. Qed.
+    Proof. by sbi_unfold. Qed.
     Lemma to_agree_op_validI a b : ✓ (to_agree a ⋅ to_agree b) ⊣⊢ a ≡ b.
-    Proof.
-      apply bi.entails_anti_sym.
-      - rewrite agree_validI. by rewrite agree_equivI.
-      - pose (Ψ := (λ x : A, ✓ (to_agree a ⋅ to_agree x) : uPred M)%I).
-        assert (NonExpansive Ψ) as ? by solve_proper.
-        rewrite (internal_eq_rewrite a b Ψ).
-        eapply bi.impl_elim; first reflexivity.
-        etrans; first apply bi.True_intro.
-        subst Ψ; simpl.
-        rewrite agree_idemp. apply to_agree_validI.
-    Qed.
+    Proof. sbi_unfold. apply to_agree_op_validN. Qed.
 
     Lemma to_agree_uninjI x : ✓ x ⊢ ∃ a, to_agree a ≡ x.
-    Proof. uPred.unseal. split=> n y _. exact: to_agree_uninjN. Qed.
+    Proof. sbi_unfold=> n. exact: to_agree_uninjN. Qed.
 
     (** Derived lemma: If two [x y : agree O] compose to some [to_agree a],
       they are internally equal, and also equal to the [to_agree a].
@@ -113,9 +119,10 @@ Section upred.
       x ⋅ y ≡ to_agree a ⊢ x ≡ y ∧ y ≡ to_agree a.
     Proof.
       assert (x ⋅ y ≡ to_agree a ⊢ x ≡ y) as Hxy_equiv.
-      { rewrite -(agree_validI x y) internal_eq_sym.
-        apply: (internal_eq_rewrite' _ _ (λ o, ✓ o)%I); first done.
-        rewrite -to_agree_validI. apply bi.True_intro. }
+      { rewrite -(agree_op_invI x y) internal_eq_sym.
+        apply: (internal_eq_rewrite' _ _ (λ o, ✓ o)%I); [solve_proper|done|].
+        rewrite -(bi.absorbing_absorbingly (✓ _)).
+        rewrite -to_agree_validI bi.absorbingly_emp_True. apply bi.True_intro. }
       apply bi.and_intro; first done.
       rewrite -{1}(idemp bi_and (_ ≡ _)%I) {1}Hxy_equiv. apply bi.impl_elim_l'.
       apply: (internal_eq_rewrite' _ _
@@ -124,6 +131,23 @@ Section upred.
     Qed.
   End agree.
 
+  Section csum_ofe.
+    Context {A B : ofe}.
+    Implicit Types a : A.
+    Implicit Types b : B.
+
+    Lemma csum_equivI (x y : csum A B) :
+      x ≡ y ⊣⊢ match x, y with
+                          | Cinl a, Cinl a' => a ≡ a'
+                          | Cinr b, Cinr b' => b ≡ b'
+                          | CsumBot, CsumBot => True
+                          | _, _ => False
+                          end.
+    Proof.
+      destruct x, y; sbi_unfold; (split; [by inversion 1|by try constructor]).
+    Qed.
+  End csum_ofe.
+
   Section csum_cmra.
     Context {A B : cmra}.
     Implicit Types a : A.
@@ -135,7 +159,7 @@ Section upred.
                         | Cinr b => ✓ b
                         | CsumBot => False
                         end.
-    Proof. uPred.unseal. by destruct x. Qed.
+    Proof. destruct x; by sbi_unfold. Qed.
   End csum_cmra.
 
   Section view.
@@ -145,62 +169,60 @@ Section upred.
     Implicit Types b : B.
     Implicit Types x y : view rel.
 
-    Lemma view_both_dfrac_validI_1 (relI : uPred M) dq a b :
-      (∀ n (x : M), rel n a b → relI n x) →
-      ✓ (●V{dq} a ⋅ ◯V b : view rel) ⊢ ⌜✓dq⌝ ∧ relI.
+    Lemma view_both_dfrac_validI_1 (relI : siProp) dq a b :
+      (∀ n, rel n a b → siProp_holds relI n) →
+      ✓ (●V{dq} a ⋅ ◯V b : view rel) ⊢ ⌜✓dq⌝ ∧ <si_pure> relI.
     Proof.
-      intros Hrel. uPred.unseal. split=> n x _ /=.
-      rewrite /uPred_holds /= view_both_dfrac_validN. by move=> [? /Hrel].
+      intros. sbi_unfold=> n. rewrite view_both_dfrac_validN. naive_solver.
     Qed.
-    Lemma view_both_dfrac_validI_2 (relI : uPred M) dq a b :
-      (∀ n (x : M), relI n x → rel n a b) →
-      ⌜✓dq⌝ ∧ relI ⊢ ✓ (●V{dq} a ⋅ ◯V b : view rel).
+    Lemma view_both_dfrac_validI_2 (relI : siProp) dq a b :
+      (∀ n, siProp_holds relI n → rel n a b) →
+      ⌜✓dq⌝ ∧ <si_pure> relI ⊢ ✓ (●V{dq} a ⋅ ◯V b : view rel).
     Proof.
-      intros Hrel. uPred.unseal. split=> n x _ /=.
-      rewrite /uPred_holds /= view_both_dfrac_validN. by move=> [? /Hrel].
+      intros. sbi_unfold=> n. rewrite view_both_dfrac_validN. naive_solver.
     Qed.
-    Lemma view_both_dfrac_validI (relI : uPred M) dq a b :
-      (∀ n (x : M), rel n a b ↔ relI n x) →
-      ✓ (●V{dq} a ⋅ ◯V b : view rel) ⊣⊢ ⌜✓dq⌝ ∧ relI.
+    Lemma view_both_dfrac_validI (relI : siProp) dq a b :
+      (∀ n, rel n a b ↔ siProp_holds relI n) →
+      ✓ (●V{dq} a ⋅ ◯V b : view rel) ⊣⊢ ⌜✓dq⌝ ∧ <si_pure> relI.
     Proof.
       intros. apply (anti_symm _);
         [apply view_both_dfrac_validI_1|apply view_both_dfrac_validI_2]; naive_solver.
     Qed.
 
-    Lemma view_both_validI_1 (relI : uPred M) a b :
-      (∀ n (x : M), rel n a b → relI n x) →
-      ✓ (●V a ⋅ ◯V b : view rel) ⊢ relI.
+    Lemma view_both_validI_1 (relI : siProp) a b :
+      (∀ n, rel n a b → siProp_holds relI n) →
+      ✓ (●V a ⋅ ◯V b : view rel) ⊢ <si_pure> relI.
     Proof. intros. by rewrite view_both_dfrac_validI_1 // bi.and_elim_r. Qed.
-    Lemma view_both_validI_2 (relI : uPred M) a b :
-      (∀ n (x : M), relI n x → rel n a b) →
-      relI ⊢ ✓ (●V a ⋅ ◯V b : view rel).
+    Lemma view_both_validI_2 (relI : siProp) a b :
+      (∀ n, siProp_holds relI n → rel n a b) →
+      <si_pure> relI ⊢ ✓ (●V a ⋅ ◯V b : view rel).
     Proof.
       intros. rewrite -view_both_dfrac_validI_2 //.
       apply bi.and_intro; [|done]. by apply bi.pure_intro.
     Qed.
-    Lemma view_both_validI (relI : uPred M) a b :
-      (∀ n (x : M), rel n a b ↔ relI n x) →
-      ✓ (●V a ⋅ ◯V b : view rel) ⊣⊢ relI.
+    Lemma view_both_validI (relI : siProp) a b :
+      (∀ n, rel n a b ↔ siProp_holds relI n) →
+      ✓ (●V a ⋅ ◯V b : view rel) ⊣⊢ <si_pure> relI.
     Proof.
       intros. apply (anti_symm _);
         [apply view_both_validI_1|apply view_both_validI_2]; naive_solver.
     Qed.
 
-    Lemma view_auth_dfrac_validI (relI : uPred M) dq a :
-      (∀ n (x : M), relI n x ↔ rel n a ε) →
-      ✓ (●V{dq} a : view rel) ⊣⊢ ⌜✓dq⌝ ∧ relI.
+    Lemma view_auth_dfrac_validI (relI : siProp) dq a :
+      (∀ n, siProp_holds relI n ↔ rel n a ε) →
+      ✓ (●V{dq} a : view rel) ⊣⊢ ⌜✓dq⌝ ∧ <si_pure> relI.
     Proof.
       intros. rewrite -(right_id ε op (●V{dq} a)). by apply view_both_dfrac_validI.
     Qed.
-    Lemma view_auth_validI (relI : uPred M) a :
-      (∀ n (x : M), relI n x ↔ rel n a ε) →
-      ✓ (●V a : view rel) ⊣⊢ relI.
+    Lemma view_auth_validI (relI : siProp) a :
+      (∀ n, siProp_holds relI n ↔ rel n a ε) →
+      ✓ (●V a : view rel) ⊣⊢ <si_pure> relI.
     Proof. intros. rewrite -(right_id ε op (●V a)). by apply view_both_validI. Qed.
 
-    Lemma view_frag_validI (relI : uPred M) b :
-      (∀ n (x : M), relI n x ↔ ∃ a, rel n a b) →
-      ✓ (◯V b : view rel) ⊣⊢ relI.
-    Proof. uPred.unseal=> Hrel. split=> n x _. by rewrite Hrel. Qed.
+    Lemma view_frag_validI (relI : siProp) b :
+      (∀ n, siProp_holds relI n ↔ ∃ a, rel n a b) →
+      ✓ (◯V b : view rel) ⊣⊢ <si_pure> relI.
+    Proof. intros Hrel. sbi_unfold=> n. by rewrite Hrel. Qed.
   End view.
 
   Section auth.
@@ -209,33 +231,22 @@ Section upred.
     Implicit Types x y : auth A.
 
     Lemma auth_auth_dfrac_validI dq a : ✓ (●{dq} a) ⊣⊢ ⌜✓dq⌝ ∧ ✓ a.
-    Proof.
-      apply view_auth_dfrac_validI=> n. uPred.unseal; split; [|by intros [??]].
-      split; [|done]. apply ucmra_unit_leastN.
-    Qed.
+    Proof. sbi_unfold=> n. apply auth_auth_dfrac_validN. Qed.
     Lemma auth_auth_validI a : ✓ (● a) ⊣⊢ ✓ a.
-    Proof.
-      by rewrite auth_auth_dfrac_validI bi.pure_True // left_id.
-    Qed.
+    Proof. sbi_unfold=> n. apply auth_auth_validN. Qed.
     Lemma auth_auth_dfrac_op_validI dq1 dq2 a1 a2 :
       ✓ (●{dq1} a1 ⋅ ●{dq2} a2) ⊣⊢ ✓ (dq1 ⋅ dq2) ∧ (a1 ≡ a2) ∧ ✓ a1.
-    Proof. uPred.unseal; split => n x _. apply auth_auth_dfrac_op_validN. Qed.
+    Proof. sbi_unfold=> n. apply auth_auth_dfrac_op_validN. Qed.
 
     Lemma auth_frag_validI a : ✓ (◯ a) ⊣⊢ ✓ a.
-    Proof.
-      apply view_frag_validI=> n x.
-      rewrite auth_view_rel_exists. by uPred.unseal.
-    Qed.
+    Proof. sbi_unfold=> n. apply auth_frag_validN. Qed.
 
     Lemma auth_both_dfrac_validI dq a b :
       ✓ (●{dq} a ⋅ ◯ b) ⊣⊢ ⌜✓dq⌝ ∧ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
-    Proof. apply view_both_dfrac_validI=> n. by uPred.unseal. Qed.
+    Proof.  sbi_unfold=> n. apply auth_both_dfrac_validN. Qed.
     Lemma auth_both_validI a b :
       ✓ (● a ⋅ ◯ b) ⊣⊢ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
-    Proof.
-      by rewrite auth_both_dfrac_validI bi.pure_True // left_id.
-    Qed.
-
+    Proof. sbi_unfold=> n. apply auth_both_validN. Qed.
   End auth.
 
   Section excl_auth.
@@ -243,11 +254,7 @@ Section upred.
     Implicit Types a b : A.
 
     Lemma excl_auth_agreeI a b : ✓ (●E a ⋅ ◯E b) ⊢ (a ≡ b).
-    Proof.
-      rewrite auth_both_validI bi.and_elim_l.
-      apply bi.exist_elim=> -[[c|]|];
-        by rewrite option_equivI /= excl_equivI //= bi.False_elim.
-    Qed.
+    Proof. sbi_unfold=> n. apply excl_auth_agreeN. Qed.
   End excl_auth.
 
   Section dfrac_agree.
@@ -255,18 +262,11 @@ Section upred.
     Implicit Types a b : A.
 
     Lemma dfrac_agree_validI dq a : ✓ (to_dfrac_agree dq a) ⊣⊢ ⌜✓ dq⌝.
-    Proof.
-      rewrite prod_validI /= uPred.discrete_valid. apply bi.entails_anti_sym.
-      - by rewrite bi.and_elim_l.
-      - apply bi.and_intro; first done. etrans; last apply to_agree_validI.
-        apply bi.True_intro.
-    Qed.
+    Proof. sbi_unfold=> n. rewrite /to_dfrac_agree pair_validN. naive_solver. Qed.
 
     Lemma dfrac_agree_validI_2 dq1 dq2 a b :
       ✓ (to_dfrac_agree dq1 a ⋅ to_dfrac_agree dq2 b) ⊣⊢ ⌜✓ (dq1 ⋅ dq2)⌝ ∧ (a ≡ b).
-    Proof.
-      rewrite prod_validI /= uPred.discrete_valid to_agree_op_validI //.
-    Qed.
+    Proof. rewrite prod_validI /= bi_cmra_discrete_valid to_agree_op_validI //. Qed.
 
     Lemma frac_agree_validI q a : ✓ (to_frac_agree q a) ⊣⊢ ⌜(q ≤ 1)%Qp⌝.
     Proof.
@@ -287,19 +287,11 @@ Section upred.
     Lemma gmap_view_both_validI m k dq v :
       ✓ (gmap_view_auth (DfracOwn 1) m ⋅ gmap_view_frag k dq v) ⊢
       ✓ dq ∧ m !! k ≡ Some v.
-    Proof.
-      rewrite /gmap_view_auth /gmap_view_frag. apply view_both_validI_1.
-      intros n a. uPred.unseal. apply gmap_view.gmap_view_rel_lookup.
-    Qed.
+    Proof. sbi_unfold=> n. apply gmap_view_both_validN. Qed.
 
     Lemma gmap_view_frag_op_validI k dq1 dq2 v1 v2 :
       ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ⊣⊢
       ✓ (dq1 ⋅ dq2) ∧ v1 ≡ v2.
-    Proof.
-      rewrite /gmap_view_frag -view_frag_op. apply view_frag_validI=> n x.
-      rewrite gmap_view.gmap_view_rel_exists singleton_op singleton_validN.
-      rewrite -pair_op pair_validN to_agree_op_validN. by uPred.unseal.
-    Qed.
-
+    Proof. sbi_unfold=> n. apply gmap_view_frag_op_validN. Qed.
   End gmap_view.
-End upred.
+End algebra.

iris/bi/bi.v

 From iris.bi Require Export derived_laws derived_laws_later big_op.
-From iris.bi Require Export updates internal_eq plainly embedding.
+From iris.bi Require Export updates embedding.
+From iris.bi Require Export sbi sbi_unfold internal_eq plainly cmra_valid algebra.
 From iris.prelude Require Import options.
 
 Module Import bi.

iris/bi/cmra_valid.v

+From iris.algebra Require Export cmra.
+From iris.bi Require Export sbi plainly.
+From iris.bi Require Import derived_laws_later.
+From iris.prelude Require Import options.
+
+Definition bi_cmra_valid `{!Sbi PROP} {A : cmra} (a : A) : PROP :=
+  <si_pure> siProp_cmra_valid a.
+Global Arguments bi_cmra_valid : simpl never.
+Global Typeclasses Opaque bi_cmra_valid.
+Global Instance: Params (@bi_cmra_valid) 3 := {}.
+Notation "✓ a" := (bi_cmra_valid a) : bi_scope.
+
+Section cmra_valid.
+  Context `{!Sbi PROP}.
+  Implicit Types P Q : PROP.
+
+  (* Force implicit argument PROP *)
+  Notation "P ⊢ Q" := (P ⊢@{PROP} Q).
+  Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q).
+
+  Global Instance bi_cmra_valid_ne {A : cmra} :
+    NonExpansive (@bi_cmra_valid PROP _ A).
+  Proof.
+    intros n x x' ?. by apply si_pure_ne, siProp_primitive.cmra_valid_ne.
+  Qed.
+  Global Instance bi_cmra_valid_proper {A : cmra} :
+    Proper ((≡) ==> (⊣⊢)) (@bi_cmra_valid PROP _ A).
+  Proof. apply ne_proper, _. Qed.
+
+  Lemma bi_cmra_valid_intro {A : cmra} P (a : A) : ✓ a → P ⊢ (✓ a).
+  Proof.
+    intros. rewrite (bi.True_intro P) -si_pure_pure.
+    by apply si_pure_mono, siProp_primitive.cmra_valid_intro.
+  Qed.
+  Lemma bi_cmra_valid_elim {A : cmra} (a : A) : ✓ a ⊢ ⌜ ✓{0} a ⌝.
+  Proof.
+    rewrite -si_pure_pure.
+    by apply si_pure_mono, siProp_primitive.cmra_valid_elim.
+  Qed.
+  (* FIXME: Remove in favor of cmra_validN_op_r *)
+  Lemma bi_cmra_valid_weaken {A : cmra} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
+  Proof. by apply si_pure_mono, siProp_primitive.cmra_valid_weaken. Qed.
+  Lemma bi_cmra_valid_entails {A B : cmra} (a : A) (b : B) :
+    (✓ a ⊢ ✓ b) ↔ ∀ n, ✓{n} a → ✓{n} b.
+  Proof. rewrite si_pure_entails. apply siProp_primitive.valid_entails. Qed.
+
+  Lemma si_pure_cmra_valid {A : cmra} (a : A) : <si_pure> ✓ a ⊣⊢ ✓ a.
+  Proof. done. Qed.
+  Lemma persistently_cmra_valid {A : cmra} (a : A) : <pers> ✓ a ⊣⊢ ✓ a.
+  Proof. apply persistently_si_pure. Qed.
+  Lemma plainly_cmra_valid {A : cmra} (a : A) : ■ ✓ a ⊣⊢ ✓ a.
+  Proof. apply plainly_si_pure. Qed.
+  Lemma intuitionistically_cmra_valid `{!BiAffine PROP} {A : cmra} (a : A) :
+    □ ✓ a ⊣⊢ ✓ a.
+  Proof.
+    by rewrite bi.intuitionistically_into_persistently persistently_cmra_valid.
+  Qed.
+  Lemma bi_cmra_discrete_valid `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
+  Proof.
+    apply (anti_symm _).
+    - rewrite bi_cmra_valid_elim. by apply bi.pure_mono, cmra_discrete_valid.
+    - apply bi.pure_elim'=> ?. by apply bi_cmra_valid_intro.
+  Qed.
+
+  Global Instance bi_cmra_valid_timeless `{!CmraDiscrete A} (a : A) :
+    Timeless (PROP:=PROP) (✓ a).
+  Proof. rewrite /Timeless !bi_cmra_discrete_valid. apply (timeless _). Qed.
+
+  Global Instance bi_cmra_valid_plain {A : cmra} (a : A) :
+    Plain (PROP:=PROP) (✓ a).
+  Proof. rewrite -plainly_cmra_valid. apply _. Qed.
+
+  Global Instance bi_cmra_valid_absorbing {A : cmra} (a : A) :
+    Absorbing (PROP:=PROP) (✓ a).
+  Proof. rewrite -persistently_cmra_valid. apply _. Qed.
+
+  Global Instance bi_cmra_valid_persistent {A : cmra} (a : A) :
+    Persistent (PROP:=PROP) (✓ a).
+  Proof. rewrite -persistently_cmra_valid. apply _. Qed.
+End cmra_valid.

iris/bi/derived_laws_later.v

@@ -354,9 +354,10 @@ Global Instance impl_timeless `{!BiLöb PROP} P Q : Timeless Q → Timeless (P
 Proof.
   rewrite /Timeless=> HQ. rewrite later_false_em.
   apply or_mono, impl_intro_l; first done.
+  rewrite impl_curry -(comm bi_and P) -impl_curry impl_elim_r.
   rewrite -{2}(löb Q). apply impl_intro_l.
   rewrite HQ /bi_except_0 !and_or_r. apply or_elim; last auto.
-  by rewrite assoc (comm _ _ P) -assoc !impl_elim_r.
+  by rewrite impl_elim_r.
 Qed.
 Global Instance sep_timeless P Q: Timeless P → Timeless Q → Timeless (P ∗ Q).
 Proof.

iris/bi/embedding.v

@@ -3,9 +3,9 @@ From iris.bi Require Import interface derived_laws_later big_op.
 From iris.bi Require Import plainly updates internal_eq.
 From iris.prelude Require Import options.
 
-(* We enable primitive projections in this file to improve the performance of the Iris proofmode:
-    primitive projections for the bi-records makes the proofmode faster.
-*)
+(* We enable primitive projections in this file to improve the performance of
+the Iris proofmode: primitive projections for the bi-records makes the proofmode
+faster. *)
 Local Set Primitive Projections.
 
 (* The sections add extra BI assumptions, which is only picked up with [Type*]. *)
@@ -26,13 +26,6 @@ Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := {
   bi_embed_mixin_mono : Proper ((⊢) ==> (⊢)) (embed (A:=PROP1) (B:=PROP2));
   bi_embed_mixin_emp_valid_inj (P : PROP1) :
     (⊢@{PROP2} ⎡P⎤) → ⊢ P;
-  (** The following axiom expresses that the embedding is injective in the OFE
-  sense. Instead of this axiom being expressed in terms of [siProp] or
-  externally (i.e., as [Inj (dist n) (dist n) embed]), it is expressed using the
-  internal equality of _any other_ BI [PROP']. This is more general, as we do
-  not have any machinary to embed [siProp] into a BI with internal equality. *)
-  bi_embed_mixin_interal_inj {PROP' : bi} `{!BiInternalEq PROP'} (P Q : PROP1) :
-    ⎡P⎤ ≡ ⎡Q⎤ ⊢@{PROP'} (P ≡ Q);
   bi_embed_mixin_emp_2 : emp ⊢@{PROP2} ⎡emp⎤;
   bi_embed_mixin_impl_2 (P Q : PROP1) :
     (⎡P⎤ → ⎡Q⎤) ⊢@{PROP2} ⎡P → Q⎤;
@@ -66,12 +59,6 @@ Class BiEmbedLater (PROP1 PROP2 : bi) `{!BiEmbed PROP1 PROP2} :=
 Global Hint Mode BiEmbedLater ! - - : typeclass_instances.
 Global Hint Mode BiEmbedLater - ! - : typeclass_instances.
 
-Class BiEmbedInternalEq (PROP1 PROP2 : bi)
-    `{!BiEmbed PROP1 PROP2, !BiInternalEq PROP1, !BiInternalEq PROP2} :=
-  embed_internal_eq_1 (A : ofe) (x y : A) : ⎡x ≡ y⎤ ⊢@{PROP2} x ≡ y.
-Global Hint Mode BiEmbedInternalEq ! - - - - : typeclass_instances.
-Global Hint Mode BiEmbedInternalEq - ! - - - : typeclass_instances.
-
 Class BiEmbedBUpd (PROP1 PROP2 : bi)
     `{!BiEmbed PROP1 PROP2, !BiBUpd PROP1, !BiBUpd PROP2} :=
   embed_bupd P : ⎡|==> P⎤ ⊣⊢@{PROP2} |==> ⎡P⎤.
@@ -84,11 +71,14 @@ Class BiEmbedFUpd (PROP1 PROP2 : bi)
 Global Hint Mode BiEmbedFUpd - ! - - - : typeclass_instances.
 Global Hint Mode BiEmbedFUpd ! - - - - : typeclass_instances.
 
-Class BiEmbedPlainly (PROP1 PROP2 : bi)
-    `{!BiEmbed PROP1 PROP2, !BiPlainly PROP1, !BiPlainly PROP2} :=
-  embed_plainly (P : PROP1) : ⎡■ P⎤ ⊣⊢@{PROP2} ■ ⎡P⎤.
-Global Hint Mode BiEmbedPlainly - ! - - - : typeclass_instances.
-Global Hint Mode BiEmbedPlainly ! - - - - : typeclass_instances.
+Class BiEmbedSbi (PROP1 PROP2 : bi)
+    `{!BiEmbed PROP1 PROP2, !Sbi PROP1, !Sbi PROP2} := {
+  embed_si_emp_valid (P : PROP1) :
+    <si_emp_valid> ⎡ P ⎤ ⊣⊢@{siPropI} <si_emp_valid> P;
+  embed_si_pure_1 Pi : ⎡ <si_pure> Pi ⎤ ⊢@{PROP2} <si_pure> Pi;
+}.
+Global Hint Mode BiEmbedSbi - ! - - - : typeclass_instances.
+Global Hint Mode BiEmbedSbi ! - - - - : typeclass_instances.
 
 Section embed_laws.
   Context {PROP1 PROP2 : bi} `{!BiEmbed PROP1 PROP2}.
@@ -102,9 +92,6 @@ Section embed_laws.
   Proof. eapply bi_embed_mixin_mono, bi_embed_mixin. Qed.
   Lemma embed_emp_valid_inj P : (⊢@{PROP2} ⎡P⎤) → ⊢ P.
   Proof. eapply bi_embed_mixin_emp_valid_inj, bi_embed_mixin. Qed.
-  Lemma embed_interal_inj `{!BiInternalEq PROP'} (P Q : PROP1) :
-    ⎡P⎤ ≡ ⎡Q⎤ ⊢@{PROP'} (P ≡ Q).
-  Proof. eapply bi_embed_mixin_interal_inj, bi_embed_mixin. Qed.
   Lemma embed_emp_2 : emp ⊢ ⎡emp⎤.
   Proof. eapply bi_embed_mixin_emp_2, bi_embed_mixin. Qed.
   Lemma embed_impl_2 P Q : (⎡P⎤ → ⎡Q⎤) ⊢ ⎡P → Q⎤.
@@ -123,8 +110,8 @@ End embed_laws.
 
 Section embed.
   Context {PROP1 PROP2 : bi} `{!BiEmbed PROP1 PROP2}.
-  Local Notation embed := (embed (A:=PROP1) (B:=PROP2)).
-  Local Notation "⎡ P ⎤" := (embed P) : bi_scope.
+  Notation embed := (embed (A:=bi_car PROP1) (B:=bi_car PROP2)).
+  Notation "⎡ P ⎤" := (embed P) : bi_scope.
   Implicit Types P Q R : PROP1.
 
   Global Instance embed_proper : Proper ((≡) ==> (≡)) embed.
@@ -293,27 +280,34 @@ Section embed.
     Qed.
   End later.
 
-  Section internal_eq.
-    Context `{!BiInternalEq PROP1, !BiInternalEq PROP2, !BiEmbedInternalEq PROP1 PROP2}.
+  Section sbi.
+    Context `{!Sbi PROP1, !Sbi PROP2, !BiEmbedSbi PROP1 PROP2}.
 
-    Lemma embed_internal_eq (A : ofe) (x y : A) : ⎡x ≡ y⎤ ⊣⊢@{PROP2} x ≡ y.
+    Lemma embed_si_pure Pi : ⎡<si_pure> Pi⎤ ⊣⊢ <si_pure> Pi.
+    Proof.
+      apply (anti_symm _); [apply embed_si_pure_1|].
+      rewrite -(si_pure_si_emp_valid_elim ⎡ _ ⎤).
+      by rewrite embed_si_emp_valid si_emp_valid_si_pure.
+    Qed.
+
+    Lemma embed_interal_inj P Q : ⎡P⎤ ≡ ⎡Q⎤ ⊢@{siProp} P ≡ Q.
     Proof.
-      apply bi.equiv_entails; split; [apply embed_internal_eq_1|].
-      etrans; [apply (internal_eq_rewrite x y (λ y, ⎡x ≡ y⎤%I)); solve_proper|].
-      rewrite -(internal_eq_refl True%I) embed_pure.
-      eapply bi.impl_elim; [done|]. apply bi.True_intro.
+      intros. rewrite !prop_ext. rewrite /bi_wand_iff !si_emp_valid_and.
+      by rewrite -!embed_wand !embed_si_emp_valid.
     Qed.
-  End internal_eq.
 
-  Section plainly.
-    Context `{!BiPlainly PROP1, !BiPlainly PROP2, !BiEmbedPlainly PROP1 PROP2}.
+    Lemma embed_internal_eq (A : ofe) (x y : A) : ⎡x ≡ y⎤ ⊣⊢@{PROP2} x ≡ y.
+    Proof. apply embed_si_pure. Qed.
+
+    Lemma embed_plainly P : ⎡■ P⎤ ⊣⊢ ■ ⎡P⎤.
+    Proof. by rewrite /plainly embed_si_pure embed_si_emp_valid. Qed.
 
     Lemma embed_plainly_if p P : ⎡■?p P⎤ ⊣⊢ ■?p ⎡P⎤.
     Proof. destruct p; simpl; auto using embed_plainly. Qed.
 
     Lemma embed_plain (P : PROP1) : Plain P → Plain (PROP:=PROP2) ⎡P⎤.
     Proof. intros ?. by rewrite /Plain {1}(plain P) embed_plainly. Qed.
-  End plainly.
+  End sbi.
 End embed.
 
 (* Not defined using an ordinary [Instance] because the default
@@ -339,7 +333,6 @@ Section embed_embed.
     - solve_proper.
     - solve_proper.
     - intros P. by rewrite !embed_emp_valid.
-    - intros PROP' ? P Q. by rewrite !embed_interal_inj.
     - by rewrite -!embed_emp_2.
     - intros P Q. by rewrite -!embed_impl.
     - intros A Φ. by rewrite -!embed_forall.
@@ -362,11 +355,14 @@ Section embed_embed.
     BiEmbedLater PROP1 PROP2 → BiEmbedLater PROP2 PROP3 →
     BiEmbedLater PROP1 PROP3.
   Proof. intros ?? P. by rewrite !embed_embed_alt !embed_later. Qed.
-  Lemma embed_embed_internal_eq
-      `{!BiInternalEq PROP1, !BiInternalEq PROP2, !BiInternalEq PROP3} :
-    BiEmbedInternalEq PROP1 PROP2 → BiEmbedInternalEq PROP2 PROP3 →
-    BiEmbedInternalEq PROP1 PROP3.
-  Proof. intros ?? A x y. by rewrite !embed_embed_alt !embed_internal_eq. Qed.
+  Lemma embed_embed_sbi `{!Sbi PROP1, !Sbi PROP2, !Sbi PROP3} :
+    BiEmbedSbi PROP1 PROP2 → BiEmbedSbi PROP2 PROP3 →
+    BiEmbedSbi PROP1 PROP3.
+  Proof.
+    intros ??; split.
+    - intros P. by rewrite embed_embed_alt !embed_si_emp_valid.
+    - intros Pi. by rewrite embed_embed_alt !embed_si_pure.
+  Qed.
   Lemma embed_embed_bupd `{!BiBUpd PROP1, !BiBUpd PROP2, !BiBUpd PROP3} :
     BiEmbedBUpd PROP1 PROP2 → BiEmbedBUpd PROP2 PROP3 →
     BiEmbedBUpd PROP1 PROP3.
@@ -375,9 +371,4 @@ Section embed_embed.
     BiEmbedFUpd PROP1 PROP2 → BiEmbedFUpd PROP2 PROP3 →
     BiEmbedFUpd PROP1 PROP3.
   Proof. intros ?? E1 E2 P. by rewrite !embed_embed_alt !embed_fupd. Qed.
-  Lemma embed_embed_plainly
-      `{!BiPlainly PROP1, !BiPlainly PROP2, !BiPlainly PROP3} :
-    BiEmbedPlainly PROP1 PROP2 → BiEmbedPlainly PROP2 PROP3 →
-    BiEmbedPlainly PROP1 PROP3.
-  Proof. intros ?? P. by rewrite !embed_embed_alt !embed_plainly. Qed.
 End embed_embed.

iris/bi/internal_eq.v

-From iris.bi Require Import derived_laws_later big_op.
-From iris.prelude Require Import options.
 From iris.algebra Require Import excl csum.
-Import interface.bi derived_laws.bi derived_laws_later.bi.
-
-(* We enable primitive projections in this file to improve the performance of the Iris proofmode:
-    primitive projections for the bi-records makes the proofmode faster.
-*)
-Local Set Primitive Projections.
-
-(** This file defines a type class for BIs with a notion of internal equality.
-Internal equality is not part of the [bi] canonical structure as [internal_eq]
-can only be given a definition that satisfies [NonExpansive2 internal_eq] _and_
-[▷ (x ≡ y) ⊢ Next x ≡ Next y] if the BI is step-indexed. *)
-Class InternalEq (PROP : Type) :=
-  internal_eq : ∀ {A : ofe}, A → A → PROP.
-Global Arguments internal_eq {_ _ _} _ _ : simpl never.
-Global Hint Mode InternalEq ! : typeclass_instances.
-Global Instance: Params (@internal_eq) 3 := {}.
+From iris.bi Require Export sbi.
+From iris.bi Require Import derived_laws_later.
+From iris.prelude Require Import options.
+
+Definition internal_eq `{!Sbi PROP} {A : ofe} (a b : A) : PROP :=
+  <si_pure> siProp_internal_eq a b.
+Global Arguments internal_eq : simpl never.
 Global Typeclasses Opaque internal_eq.
+Global Instance: Params (@internal_eq) 3 := {}.
 
 Infix "≡" := internal_eq : bi_scope.
 Infix "≡@{ A }" := (internal_eq (A := A)) (only parsing) : bi_scope.
-
 Notation "( X ≡.)" := (internal_eq X) (only parsing) : bi_scope.
 Notation "(.≡ X )" := (λ Y, Y ≡ X)%I (only parsing) : bi_scope.
 Notation "(≡@{ A } )" := (internal_eq (A:=A)) (only parsing) : bi_scope.
 
-(* Mixins allow us to create instances easily without having to use Program *)
-Record BiInternalEqMixin (PROP : bi) `(!InternalEq PROP) := {
-  bi_internal_eq_mixin_internal_eq_ne (A : ofe) : NonExpansive2 (@internal_eq PROP _ A);
-  bi_internal_eq_mixin_internal_eq_refl {A : ofe} (P : PROP) (a : A) : P ⊢ a ≡ a;
-  bi_internal_eq_mixin_internal_eq_rewrite {A : ofe} a b (Ψ : A → PROP) :
-    NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b;
-  bi_internal_eq_mixin_fun_extI {A} {B : A → ofe} (f g : discrete_fun B) :
-    (∀ x, f x ≡ g x) ⊢@{PROP} f ≡ g;
-  bi_internal_eq_mixin_sig_equivI_1 {A : ofe} (P : A → Prop) (x y : sig P) :
-    `x ≡ `y ⊢@{PROP} x ≡ y;
-  bi_internal_eq_mixin_discrete_eq_1 {A : ofe} (a b : A) :
-    Discrete a → a ≡ b ⊢@{PROP} ⌜a ≡ b⌝;
-  bi_internal_eq_mixin_later_equivI_1 {A : ofe} (x y : A) :
-    Next x ≡ Next y ⊢@{PROP} ▷ (x ≡ y);
-  bi_internal_eq_mixin_later_equivI_2 {A : ofe} (x y : A) :
-    ▷ (x ≡ y) ⊢@{PROP} Next x ≡ Next y;
-}.
-
-Class BiInternalEq (PROP : bi) := {
-  bi_internal_eq_internal_eq :> InternalEq PROP;
-  bi_internal_eq_mixin : BiInternalEqMixin PROP bi_internal_eq_internal_eq;
-}.
-Global Hint Mode BiInternalEq ! : typeclass_instances.
-Global Arguments bi_internal_eq_internal_eq : simpl never.
-
-Section internal_eq_laws.
-  Context {PROP : bi} `{!BiInternalEq PROP}.
-  Implicit Types P Q : PROP.
-
-  Global Instance internal_eq_ne (A : ofe) : NonExpansive2 (@internal_eq PROP _ A).
-  Proof. eapply bi_internal_eq_mixin_internal_eq_ne, (bi_internal_eq_mixin). Qed.
-
-  Lemma internal_eq_refl {A : ofe} P (a : A) : P ⊢ a ≡ a.
-  Proof. eapply bi_internal_eq_mixin_internal_eq_refl, bi_internal_eq_mixin. Qed.
-  Lemma internal_eq_rewrite {A : ofe} a b (Ψ : A → PROP) :
-    NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
-  Proof. eapply bi_internal_eq_mixin_internal_eq_rewrite, bi_internal_eq_mixin. Qed.
-
-  Lemma fun_extI {A} {B : A → ofe} (f g : discrete_fun B) :
-    (∀ x, f x ≡ g x) ⊢@{PROP} f ≡ g.
-  Proof. eapply bi_internal_eq_mixin_fun_extI, bi_internal_eq_mixin. Qed.
-  Lemma sig_equivI_1 {A : ofe} (P : A → Prop) (x y : sig P) :
-    `x ≡ `y ⊢@{PROP} x ≡ y.
-  Proof. eapply bi_internal_eq_mixin_sig_equivI_1, bi_internal_eq_mixin. Qed.
-  Lemma discrete_eq_1 {A : ofe} (a b : A) :
-    Discrete a → a ≡ b ⊢@{PROP} ⌜a ≡ b⌝.
-  Proof. eapply bi_internal_eq_mixin_discrete_eq_1, bi_internal_eq_mixin. Qed.
+(** A version of the constructor of [SbiPropExtMixin] stated using [≡@{siProp}]
+instead of [siProp_internal_eq]. *)
+Lemma sbi_prop_ext_mixin_make {PROP : bi} (empv : SiEmpValid PROP) :
+  (∀ P Q : PROP, <si_emp_valid> (P ∗-∗ Q) ⊢@{siPropI} P ≡ Q) →
+  SbiPropExtMixin PROP empv.
+Proof. done. Qed.
 
-  Lemma later_equivI_1 {A : ofe} (x y : A) : Next x ≡ Next y ⊢@{PROP} ▷ (x ≡ y).
-  Proof. eapply bi_internal_eq_mixin_later_equivI_1, bi_internal_eq_mixin. Qed.
-  Lemma later_equivI_2 {A : ofe} (x y : A) : ▷ (x ≡ y) ⊢@{PROP} Next x ≡ Next y.
-  Proof. eapply bi_internal_eq_mixin_later_equivI_2, bi_internal_eq_mixin. Qed.
-End internal_eq_laws.
+Section internal_eq.
+  Context `{!Sbi PROP}.
+  Implicit Types P Q : PROP.
 
-(* Derived laws *)
-Section internal_eq_derived.
-  Context {PROP : bi} `{!BiInternalEq PROP}.
-  Implicit Types P : PROP.
+  Local Hint Resolve bi.or_elim bi.or_intro_l' bi.or_intro_r' : core.
+  Local Hint Resolve bi.True_intro bi.False_elim : core.
+  Local Hint Resolve bi.and_elim_l' bi.and_elim_r' bi.and_intro : core.
+  Local Hint Resolve bi.forall_intro : core.
+  Local Hint Extern 100 (NonExpansive _) => solve_proper : core.
 
   (* Force implicit argument PROP *)
   Notation "P ⊢ Q" := (P ⊢@{PROP} Q).
   Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q).
 
-  Global Instance internal_eq_proper (A : ofe) :
-    Proper ((≡) ==> (≡) ==> (⊣⊢)) (@internal_eq PROP _ A) := ne_proper_2 _.
+  Lemma prop_ext_2 P Q : <si_emp_valid> (P ∗-∗ Q) ⊢@{siPropI} P ≡ Q.
+  Proof. apply sbi_mixin_prop_ext_2, sbi_sbi_prop_ext_mixin. Qed.
 
-  (* Equality *)
-  Local Hint Resolve or_elim or_intro_l' or_intro_r' True_intro False_elim : core.
-  Local Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro : core.
-  Local Hint Resolve internal_eq_refl : core.
-  Local Hint Extern 100 (NonExpansive _) => solve_proper : core.
+  Global Instance internal_eq_ne (A : ofe) : NonExpansive2 (@internal_eq PROP _ A).
+  Proof.
+    intros n x x' ? y y' ?. by apply si_pure_ne, siProp_primitive.internal_eq_ne.
+  Qed.
+  Global Instance internal_eq_proper (A : ofe) :
+    Proper ((≡) ==> (≡) ==> (⊣⊢)) (@internal_eq PROP _ A).
+  Proof. apply (ne_proper_2 _). Qed.
 
+  Lemma internal_eq_refl {A : ofe} P (a : A) : P ⊢ a ≡ a.
+  Proof.
+    rewrite (bi.True_intro P) -si_pure_pure.
+    apply si_pure_mono, siProp_primitive.internal_eq_refl.
+  Qed.
   Lemma equiv_internal_eq {A : ofe} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
-  Proof. intros ->. auto. Qed.
-  Lemma internal_eq_rewrite' {A : ofe} a b (Ψ : A → PROP) P
-    {HΨ : NonExpansive Ψ} : (P ⊢ a ≡ b) → (P ⊢ Ψ a) → P ⊢ Ψ b.
+  Proof. intros ->. apply internal_eq_refl. Qed.
+  Lemma pure_internal_eq {A : ofe} (x y : A) : ⌜x ≡ y⌝ ⊢ x ≡ y.
+  Proof. apply bi.pure_elim'=> ->. apply internal_eq_refl. Qed.
+
+  Local Hint Resolve equiv_internal_eq : core.
+
+  Lemma internal_eq_rewrite {A : ofe} a b (Ψ : A → PROP) :
+    NonExpansive Ψ →
+    internal_eq a b ⊢ Ψ a → Ψ b.
+  Proof.
+    intros. (* [True -∗] makes [True -∗ Ψ a → Ψ a'] persistent, needed for
+    [si_pure_si_emp_valid_elim] *)
+    pose (Φ a' := (<si_emp_valid> (True -∗ Ψ a → Ψ a'))%I).
+    assert (⊢ Φ a) as HΦa.
+    { apply si_emp_valid_emp_valid, bi.wand_intro_l.
+      by rewrite right_id -bi.entails_impl_True. }
+    trans (<si_pure> (Φ a → Φ b) : PROP)%I.
+    - apply si_pure_mono. apply siProp_primitive.internal_eq_rewrite.
+      solve_proper.
+    - unfold bi_emp_valid in HΦa. rewrite -HΦa left_id.
+      rewrite /Φ si_pure_si_emp_valid_elim.
+      by rewrite -(bi.True_intro emp)%I left_id.
+  Qed.
+  Lemma internal_eq_rewrite' {A : ofe} a b (Ψ : A → PROP) P :
+    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.
+    intros HΨ Heq HΨa. rewrite -(idemp bi_and P) {1}Heq HΨa.
+    apply bi.impl_elim_l'. by apply internal_eq_rewrite.
   Qed.
 
-  Lemma internal_eq_sym {A : ofe} (a b : A) : a ≡ b ⊢ b ≡ a.
+  Lemma internal_eq_sym {A : ofe} (a b : A) : a ≡ b ⊢@{PROP} 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_equivI {A B : ofe} (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 f_equivI_contractive {A B : ofe} (f : A → B) `{Hf : !Contractive f} x y :
-    ▷ (x ≡ y) ⊢ f x ≡ f y.
+
+  (** Equality of data types *)
+  Lemma discrete_eq_1 {A : ofe} (a b : A) :
+    TCOr (Discrete a) (Discrete b) → a ≡ b ⊢@{PROP} ⌜a ≡ b⌝.
   Proof.
-    rewrite later_equivI_2. move: Hf=>/contractive_alt [g [? Hfg]]. rewrite !Hfg.
-    by apply f_equivI.
+    intros. rewrite -si_pure_pure. destruct select (TCOr _ _).
+    - by apply si_pure_mono, siProp_primitive.discrete_eq_1.
+    - rewrite internal_eq_sym (symmetry_iff (≡)).
+      by apply si_pure_mono, siProp_primitive.discrete_eq_1.
   Qed.
+  Lemma discrete_eq {A : ofe} (a b : A) :
+    TCOr (Discrete a) (Discrete b) → a ≡ b ⊣⊢ ⌜a ≡ b⌝.
+  Proof.
+    intros. apply (anti_symm _); auto using discrete_eq_1, pure_internal_eq.
+  Qed.
+
+  Lemma fun_extI {A} {B : A → ofe} (f g : discrete_fun B) :
+    (∀ x, f x ≡ g x) ⊢@{PROP} f ≡ g.
+  Proof.
+    rewrite /internal_eq -si_pure_forall.
+    by apply si_pure_mono, siProp_primitive.fun_extI.
+  Qed.
+  Lemma sig_equivI_1 {A : ofe} (P : A → Prop) (x y : sig P) :
+    `x ≡ `y ⊢@{PROP} x ≡ y.
+  Proof. by apply si_pure_mono, siProp_primitive.sig_equivI_1. Qed.
 
   Lemma prod_equivI {A B : ofe} (x y : A * B) : x ≡ y ⊣⊢ x.1 ≡ y.1 ∧ x.2 ≡ y.2.
   Proof.
     apply (anti_symm _).
-    - apply and_intro; apply f_equivI; apply _.
+    - apply bi.and_intro; apply f_equivI; 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.
@@ -214,17 +208,18 @@ Section internal_eq_derived.
     Proof.
       apply (anti_symm _).
       - apply (internal_eq_rewrite' x y (λ y,
-                 ∃ eq : projT1 x = projT1 y,
-                   rew eq in projT2 x ≡ projT2 y))%I;
-            [| done | exact: (exist_intro' _ _ eq_refl) ].
-        move => n [a pa] [b pb] [/=]; intros -> => /= Hab.
-        apply exist_ne => ?. by rewrite Hab.
-      - apply exist_elim. move: x y => [a pa] [b pb] /=. intros ->; simpl.
-        apply f_equivI, _.
+                 ∃ eq : projT1 x = projT1 y, rew eq in projT2 x ≡ projT2 y))%I.
+        + move => n [a pa] [b pb] [/=]; intros -> => /= Hab.
+          apply bi.exist_ne => ?. by rewrite Hab.
+        + done.
+        + rewrite -(bi.exist_intro eq_refl) /=. auto.
+      - apply bi.exist_elim. move: x y => [a pa] [b pb] /=. intros ->; simpl.
+        apply (f_equivI _).
     Qed.
   End sigT_equivI.
 
-  Lemma discrete_fun_equivI {A} {B : A → ofe} (f g : discrete_fun B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
+  Lemma discrete_fun_equivI {A} {B : A → ofe} (f g : discrete_fun B) :
+    f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
   Proof.
     apply (anti_symm _); auto using fun_extI.
     apply (internal_eq_rewrite' f g (λ g, ∀ x : A, f x ≡ g x)%I); auto.
@@ -243,26 +238,11 @@ Section internal_eq_derived.
       by rewrite -{2}[f]Hh -{2}[g]Hh -f_equivI -sig_equivI.
   Qed.
 
-  Lemma pure_internal_eq {A : ofe} (x y : A) : ⌜x ≡ y⌝ ⊢ x ≡ y.
-  Proof. apply pure_elim'=> ->. apply internal_eq_refl. Qed.
-  Lemma discrete_eq {A : ofe} (a b : A) : Discrete a → a ≡ b ⊣⊢ ⌜a ≡ b⌝.
-  Proof.
-    intros. apply (anti_symm _); auto using discrete_eq_1, pure_internal_eq.
-  Qed.
-
+  (** Modalities *)
   Lemma absorbingly_internal_eq {A : ofe} (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.
+  Proof. apply absorbingly_si_pure. Qed.
   Lemma persistently_internal_eq {A : ofe} (a b : A) : <pers> (a ≡ b) ⊣⊢ a ≡ b.
-  Proof.
-    apply (anti_symm (⊢)).
-    { by rewrite persistently_into_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.
+  Proof. apply persistently_si_pure. Qed.
 
   Global Instance internal_eq_absorbing {A : ofe} (x y : A) :
     Absorbing (PROP:=PROP) (x ≡ y).
@@ -271,26 +251,122 @@ Section internal_eq_derived.
     Persistent (PROP:=PROP) (a ≡ b).
   Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed.
 
-  (* Equality under a later. *)
-  Lemma internal_eq_rewrite_contractive {A : ofe} a b (Ψ : A → PROP)
-    {HΨ : Contractive Ψ} : ▷ (a ≡ b) ⊢ Ψ a → Ψ b.
+  (** Equality under a later. *)
+  Lemma later_equivI_1 {A : ofe} (x y : A) : Next x ≡ Next y ⊢@{PROP} ▷ (x ≡ y).
   Proof.
-    rewrite f_equivI_contractive. apply (internal_eq_rewrite (Ψ a) (Ψ b) id _).
+    rewrite /internal_eq -si_pure_later.
+    by apply si_pure_mono, siProp_primitive.later_equivI_1.
   Qed.
-  Lemma internal_eq_rewrite_contractive' {A : ofe} a b (Ψ : A → PROP) P
-    {HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
+  Lemma later_equivI_2 {A : ofe} (x y : A) : ▷ (x ≡ y) ⊢@{PROP} Next x ≡ Next y.
   Proof.
-    rewrite later_equivI_2. move: HΨ=>/contractive_alt [g [? HΨ]]. rewrite !HΨ.
-    by apply internal_eq_rewrite'.
+    rewrite /internal_eq -si_pure_later.
+    by apply si_pure_mono, siProp_primitive.later_equivI_2.
   Qed.
-
   Lemma later_equivI {A : ofe} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y).
   Proof. apply (anti_symm _); auto using later_equivI_1, later_equivI_2. Qed.
-  Lemma later_equivI_prop_2 `{!Contractive (bi_later (PROP:=PROP))} P Q :
-    ▷ (P ≡ Q) ⊢ (▷ P) ≡ (▷ Q).
-  Proof. apply (f_equivI_contractive _). Qed.
+
+  Lemma f_equivI_contractive {A B : ofe} (f : A → B) `{Hf : !Contractive f} x y :
+    ▷ (x ≡ y) ⊢ f x ≡ f y.
+  Proof.
+    rewrite later_equivI_2. move: Hf=>/contractive_alt [g [? Hfg]].
+    rewrite !Hfg. by apply f_equivI.
+  Qed.
+
+  Lemma internal_eq_rewrite_contractive {A : ofe} a b (Ψ : A → PROP) :
+    Contractive Ψ →
+    ▷ (a ≡ b) ⊢ Ψ a → Ψ b.
+  Proof.
+    intros. rewrite f_equivI_contractive.
+    apply (internal_eq_rewrite (Ψ a) (Ψ b) id _).
+  Qed.
+  Lemma internal_eq_rewrite_contractive' {A : ofe} a b (Ψ : A → PROP) P :
+    Contractive Ψ →
+    (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
+  Proof.
+    intros HΨ Heq HΨa. rewrite -(idemp bi_and P) {1}Heq HΨa.
+    apply bi.impl_elim_l'. by apply internal_eq_rewrite_contractive.
+  Qed.
 
   Global Instance eq_timeless {A : ofe} (a b : A) :
-    Discrete a → Timeless (PROP:=PROP) (a ≡ b).
+    TCOr (Discrete a) (Discrete b) → Timeless (PROP:=PROP) (a ≡ b).
   Proof. intros. rewrite /Discrete !discrete_eq. apply (timeless _). Qed.
-End internal_eq_derived.
+
+  (** Equality of propositions *)
+  Lemma internal_eq_iff P Q : P ≡ Q ⊢ P ↔ Q.
+  Proof.
+    apply (internal_eq_rewrite' P Q (λ Q, P ↔ Q))%I; auto using bi.iff_refl.
+  Qed.
+  Lemma affinely_internal_eq_wand_iff P Q : <affine> (P ≡ Q) ⊢ P ∗-∗ Q.
+  Proof.
+    apply (internal_eq_rewrite' P Q (λ Q, P ∗-∗ Q))%I; auto.
+    - by rewrite bi.affinely_elim.
+    - rewrite bi.affinely_elim_emp. apply bi.wand_iff_refl.
+  Qed.
+  Lemma internal_eq_wand_iff P Q : P ≡ Q ⊢ <absorb> (P ∗-∗ Q).
+  Proof.
+    rewrite -(bi.persistent_absorbingly_affinely (P ≡ Q)).
+    by rewrite affinely_internal_eq_wand_iff.
+  Qed.
+
+  Lemma si_pure_internal_eq {A : ofe} (x y : A) : <si_pure> (x ≡ y) ⊣⊢ x ≡ y.
+  Proof. done. Qed.
+
+  Lemma prop_ext P Q : P ≡ Q ⊣⊢@{siPropI} <si_emp_valid> (P ∗-∗ Q).
+  Proof.
+    apply (anti_symm _); [|apply prop_ext_2].
+    rewrite -(@si_pure_entails PROP) si_pure_internal_eq.
+    apply (internal_eq_rewrite' P Q
+      (λ Q, <si_pure> <si_emp_valid> (P ∗-∗ Q)))%I; auto.
+    rewrite -bi.wand_iff_refl si_emp_valid_emp si_pure_pure. auto.
+  Qed.
+
+  Lemma later_equivI_prop_2 P Q : ▷ (P ≡ Q) ⊢ (▷ P) ≡ (▷ Q).
+  Proof.
+    rewrite -!si_pure_internal_eq -si_pure_later !prop_ext.
+    by rewrite -si_emp_valid_later bi.later_wand_iff.
+  Qed.
+
+  Lemma internal_eq_soundness {A : ofe} (x y : A) : (⊢@{PROP} x ≡ y) → x ≡ y.
+  Proof.
+    intros ?%si_pure_emp_valid. by apply siProp_primitive.internal_eq_soundness.
+  Qed.
+
+  (** Derive [NonExpansive]/[Contractive] from an internal statement *)
+  Lemma internal_eq_entails {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
+    (a1 ≡ a2 ⊢ b1 ≡ b2) ↔ (∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2).
+  Proof. rewrite si_pure_entails. apply siProp_primitive.internal_eq_entails. Qed.
+
+  Lemma ne_internal_eq {A B : ofe} (f : A → B) :
+    NonExpansive f ↔ ∀ x1 x2, x1 ≡ x2 ⊢ f x1 ≡ f x2.
+  Proof.
+    split; [apply f_equivI|]. intros Hf n x1 x2. by apply internal_eq_entails.
+  Qed.
+
+  Lemma ne_2_internal_eq {A B C : ofe} (f : A → B → C) :
+    NonExpansive2 f ↔ ∀ x1 x2 y1 y2, x1 ≡ x2 ∧ y1 ≡ y2 ⊢ f x1 y1 ≡ f x2 y2.
+  Proof.
+    split.
+    - intros Hf x1 x2 y1 y2.
+      change ((x1,y1).1 ≡ (x2,y2).1 ∧ (x1,y1).2 ≡ (x2,y2).2
+        ⊢ uncurry f (x1,y1) ≡ uncurry f (x2,y2)).
+      rewrite -prod_equivI. apply ne_internal_eq. solve_proper.
+    - intros Hf n x1 x2 Hx y1 y2 Hy.
+      change (uncurry f (x1,y1) ≡{n}≡ uncurry f (x2,y2)).
+      apply ne_internal_eq; [|done].
+      intros [??] [??]. rewrite prod_equivI. apply Hf.
+  Qed.
+
+  Lemma contractive_internal_eq {A B : ofe} (f : A → B) :
+    Contractive f ↔ ∀ x1 x2, ▷ (x1 ≡ x2) ⊢ f x1 ≡ f x2.
+  Proof.
+    split; [apply f_equivI_contractive|].
+    intros Hf n x1 x2 Hx. specialize (Hf x1 x2).
+    rewrite -later_equivI internal_eq_entails in Hf. apply Hf. by f_contractive.
+  Qed.
+
+  Global Instance sbi_later_contractive : BiLaterContractive PROP.
+  Proof using Type*.
+    rewrite /BiLaterContractive.
+    apply contractive_internal_eq, later_equivI_prop_2.
+  Qed.
+End internal_eq.

iris/bi/lib/cmra.v

@@ -6,7 +6,7 @@ From iris.prelude Require Import options.
 (** Derived [≼] connective on [cmra] elements. This can be defined on
     any [bi] that has internal equality [≡]. It corresponds to the
     step-indexed [≼{n}] connective in the [uPred] model. *)
-Definition internal_included `{!BiInternalEq PROP} {A : cmra} (a b : A) : PROP :=
+Definition internal_included `{!Sbi PROP} {A : cmra} (a b : A) : PROP :=
   ∃ c, b ≡ a ⋅ c.
 Global Arguments internal_included {_ _ _} _ _ : simpl never.
 Global Instance: Params (@internal_included) 3 := {}.
@@ -15,7 +15,7 @@ Global Typeclasses Opaque internal_included.
 Infix "≼" := internal_included : bi_scope.
 
 Section internal_included_laws.
-  Context `{!BiInternalEq PROP}.
+  Context `{!Sbi PROP}.
   Implicit Type A B : cmra.
 
   (* Force implicit argument PROP *)
@@ -149,4 +149,4 @@ Section internal_included_laws.
     + iIntros "[%z Hz]". iRewrite "Hz". by rewrite assoc agree_idemp.
     + iIntros "H". by iExists _.
   Qed.
-End internal_included_laws.
+End internal_included_laws.
\ No newline at end of file

iris/bi/lib/core.v

@@ -6,7 +6,7 @@ Import bi.
 (** The "core" of an assertion is its maximal persistent part,
     i.e. the conjunction of all persistent assertions that are weaker
     than P (as in, implied by P). *)
-Definition coreP `{!BiPlainly PROP} (P : PROP) : PROP :=
+Definition coreP `{!Sbi PROP} (P : PROP) : PROP :=
   (* TODO: Looks like we want notation for affinely-plainly; that lets us avoid
   using conjunction/implication here. *)
   ∀ Q : PROP, <affine> ■ (Q -∗ <pers> Q) -∗ <affine> ■ (P -∗ Q) -∗ Q.
@@ -14,7 +14,7 @@ Global Instance: Params (@coreP) 1 := {}.
 Global Typeclasses Opaque coreP.
 
 Section core.
-  Context {PROP : bi} `{!BiPlainly PROP}.
+  Context `{!Sbi PROP}.
   Implicit Types P Q : PROP.
 
   Lemma coreP_intro P : P -∗ coreP P.
@@ -27,7 +27,7 @@ Section core.
   Qed.
 
   Global Instance coreP_persistent
-      `{!BiPersistentlyForall PROP, !BiPersistentlyImplPlainly PROP} P :
+      `{!BiPersistentlyForall PROP, !BiPersistentlyImplSiPure PROP} P :
     Persistent (coreP P).
   Proof.
     rewrite /coreP /Persistent. iIntros "HC" (Q).
@@ -65,7 +65,7 @@ Section core.
     [<affine>] modality makes it stronger since it appears in the LHS of the
     [⊢] in the premise. As a user, you have to prove [<affine> coreP P ⊢ Q],
     which is weaker than [coreP P ⊢ Q]. *)
-  Lemma coreP_entails `{!BiPersistentlyForall PROP, !BiPersistentlyImplPlainly PROP} P Q :
+  Lemma coreP_entails `{!BiPersistentlyForall PROP, !BiPersistentlyImplSiPure PROP} P Q :
     (<affine> coreP P ⊢ Q) ↔ (P ⊢ <pers> Q).
   Proof.
     split.
@@ -74,7 +74,7 @@ Section core.
     - iIntros (->) "HcQ". by iDestruct (coreP_elim with "HcQ") as "#HQ".
   Qed.
   (** A more convenient variant of the above lemma for affine [P]. *)
-  Lemma coreP_entails' `{!BiPersistentlyForall PROP, !BiPersistentlyImplPlainly PROP}
+  Lemma coreP_entails' `{!BiPersistentlyForall PROP, !BiPersistentlyImplSiPure PROP}
       P Q `{!Affine P} :
     (coreP P ⊢ Q) ↔ (P ⊢ □ Q).
   Proof.

iris/bi/lib/relations.v

@@ -9,7 +9,7 @@ Set Default Proof Using "Type*".
 
 (** * Definitions *)
 Section definitions.
-  Context {PROP : bi} `{!BiInternalEq PROP}.
+  Context `{!Sbi PROP}.
   Context {A : ofe}.
 
   Local Definition bi_rtc_pre (R : A → A → PROP)
@@ -42,7 +42,7 @@ Section definitions.
   Global Instance: Params (@bi_nsteps) 5 := {}.
 End definitions.
 
-Local Instance bi_rtc_pre_mono {PROP : bi} `{!BiInternalEq PROP}
+Local Instance bi_rtc_pre_mono {PROP : bi} `{!Sbi PROP}
     {A : ofe} (R : A → A → PROP) `{!NonExpansive2 R} (x : A) :
   BiMonoPred (bi_rtc_pre R x).
 Proof.
@@ -54,18 +54,18 @@ Proof.
   iDestruct ("H" with "Hrec") as "Hrec". eauto with iFrame.
 Qed.
 
-Global Instance bi_rtc_ne {PROP : bi} `{!BiInternalEq PROP} {A : ofe} (R : A → A → PROP) :
+Global Instance bi_rtc_ne {PROP : bi} `{!Sbi PROP} {A : ofe} (R : A → A → PROP) :
   NonExpansive2 (bi_rtc R).
 Proof.
   intros n x1 x2 Hx y1 y2 Hy. rewrite /bi_rtc Hx. f_equiv=> rec z.
   solve_proper.
 Qed.
 
-Global Instance bi_rtc_proper {PROP : bi} `{!BiInternalEq PROP} {A : ofe} (R : A → A → PROP)
+Global Instance bi_rtc_proper {PROP : bi} `{!Sbi PROP} {A : ofe} (R : A → A → PROP)
   : Proper ((≡) ==> (≡) ==> (⊣⊢)) (bi_rtc R).
 Proof. apply ne_proper_2. apply _. Qed.
 
-Local Instance bi_tc_pre_mono `{!BiInternalEq PROP}
+Local Instance bi_tc_pre_mono `{!Sbi PROP}
     {A : ofe} (R : A → A → PROP) `{NonExpansive2 R} (x : A) :
   BiMonoPred (bi_tc_pre R x).
 Proof.
@@ -77,7 +77,7 @@ Proof.
   iRight. iExists x'. iFrame "HR". by iApply "H".
 Qed.
 
-Global Instance bi_tc_ne `{!BiInternalEq PROP} {A : ofe}
+Global Instance bi_tc_ne `{!Sbi PROP} {A : ofe}
     (R : A → A → PROP) `{NonExpansive2 R} :
   NonExpansive2 (bi_tc R).
 Proof.
@@ -85,24 +85,24 @@ Proof.
   solve_proper.
 Qed.
 
-Global Instance bi_tc_proper `{!BiInternalEq PROP} {A : ofe}
+Global Instance bi_tc_proper `{!Sbi PROP} {A : ofe}
     (R : A → A → PROP) `{NonExpansive2 R}
   : Proper ((≡) ==> (≡) ==> (⊣⊢)) (bi_tc R).
 Proof. apply ne_proper_2. apply _. Qed.
 
-Global Instance bi_nsteps_ne {PROP : bi} `{!BiInternalEq PROP}
+Global Instance bi_nsteps_ne {PROP : bi} `{!Sbi PROP}
     {A : ofe} (R : A → A → PROP) `{NonExpansive2 R} (n : nat) :
   NonExpansive2 (bi_nsteps R n).
 Proof. induction n; solve_proper. Qed.
 
-Global Instance bi_nsteps_proper {PROP : bi} `{!BiInternalEq PROP}
+Global Instance bi_nsteps_proper {PROP : bi} `{!Sbi PROP}
     {A : ofe} (R : A → A → PROP) `{NonExpansive2 R} (n : nat)
   : Proper ((≡) ==> (≡) ==> (⊣⊢)) (bi_nsteps R n).
 Proof. apply ne_proper_2. apply _. Qed.
 
 (** * General theorems *)
 Section general.
-  Context {PROP : bi} `{!BiInternalEq PROP}.
+  Context `{!Sbi PROP}.
   Context {A : ofe}.
   Context (R : A → A → PROP) `{!NonExpansive2 R}.
 
@@ -396,7 +396,7 @@ Section general.
 End general.
 
 Section timeless.
-  Context {PROP : bi} `{!BiInternalEq PROP, !BiAffine PROP}.
+  Context `{!Sbi PROP, !Timeless (emp%I : PROP)}.
   Context `{!OfeDiscrete A}.
   Context (R : A → A → PROP) `{!NonExpansive2 R}.