Make uPred itself independent of BI interface and just prove primitive laws (like in master branch)

The BI interface is then instantiated using these laws.  In particular, this
shows that the rules we claim to be admissible actually are.

_CoqProject

@@ -26,6 +26,7 @@ theories/algebra/gmultiset.v
 theories/algebra/coPset.v
 theories/algebra/deprecated.v
 theories/algebra/proofmode_classes.v
+theories/bi/notation.v
 theories/bi/interface.v
 theories/bi/derived_connectives.v
 theories/bi/derived_laws_bi.v
@@ -44,6 +45,7 @@ theories/bi/lib/laterable.v
 theories/bi/lib/atomic.v
 theories/bi/lib/core.v
 theories/base_logic/upred.v
+theories/base_logic/bi.v
 theories/base_logic/derived.v
 theories/base_logic/base_logic.v
 theories/base_logic/soundness.v

theories/base_logic/base_logic.v

@@ -7,7 +7,6 @@ Set Default Proof Using "Type".
 another [uPred] module is by Jason Gross and described in:
 https://sympa.inria.fr/sympa/arc/coq-club/2016-12/msg00069.html *)
 Module Import uPred.
-  Export upred.uPred.
   Export derived.uPred.
   Export bi.
 End uPred.
@@ -25,7 +24,7 @@ Global Instance from_pure_cmra_valid {A : cmraT} af (a : A) :
   @FromPure (uPredI M) af (✓ a) (✓ a).
 Proof.
   rewrite /FromPure. eapply bi.pure_elim; [by apply affinely_if_elim|]=> ?.
-  rewrite -cmra_valid_intro //. by apply pure_intro.
+  rewrite -cmra_valid_intro //.
 Qed.
 
 Global Instance from_sep_ownM (a b1 b2 : M) :

theories/base_logic/bi.v

+From iris.bi Require Export derived_connectives updates plainly.
+From iris.base_logic Require Export upred.
+Import uPred_primitive.
+
+(** BI and other MoSeL instances for uPred.  This file does *not* unseal. *)
+
+Definition uPred_emp {M} : uPred M := uPred_pure True.
+
+Local Existing Instance entails_po.
+
+Lemma uPred_bi_mixin (M : ucmraT) :
+  BiMixin
+    uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
+    (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand
+    uPred_persistently.
+Proof.
+  split.
+  - exact: entails_po.
+  - exact: equiv_spec.
+  - exact: pure_ne.
+  - exact: and_ne.
+  - exact: or_ne.
+  - exact: impl_ne.
+  - exact: forall_ne.
+  - exact: exist_ne.
+  - exact: sep_ne.
+  - exact: wand_ne.
+  - exact: persistently_ne.
+  - exact: pure_intro.
+  - exact: pure_elim'.
+  - exact: @pure_forall_2.
+  - exact: and_elim_l.
+  - exact: and_elim_r.
+  - exact: and_intro.
+  - exact: or_intro_l.
+  - exact: or_intro_r.
+  - exact: or_elim.
+  - exact: impl_intro_r.
+  - exact: impl_elim_l'.
+  - exact: @forall_intro.
+  - exact: @forall_elim.
+  - exact: @exist_intro.
+  - exact: @exist_elim.
+  - exact: sep_mono.
+  - exact: True_sep_1. 
+  - exact: True_sep_2.
+  - exact: sep_comm'.
+  - exact: sep_assoc'.
+  - exact: wand_intro_r.
+  - exact: wand_elim_l'.
+  - exact: persistently_mono.
+  - exact: persistently_idemp_2.
+  - (* emp ⊢ <pers> emp (ADMISSIBLE) *)
+    trans (uPred_forall (M:=M) (fun _ : False => uPred_persistently uPred_emp)).
+    + apply forall_intro=>[[]].
+    + etrans; first exact: persistently_forall_2.
+      apply persistently_mono. exact: pure_intro.
+  - exact: @persistently_forall_2.
+  - exact: @persistently_exist_1.
+  - (* <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.
+  - exact: persistently_and_sep_l_1.
+Qed.
+
+Lemma uPred_sbi_mixin (M : ucmraT) : SbiMixin
+  uPred_entails uPred_pure uPred_or uPred_impl
+  (@uPred_forall M) (@uPred_exist M) uPred_sep
+  uPred_persistently (@uPred_internal_eq M) uPred_later.
+Proof.
+  split.
+  - exact: later_contractive.
+  - 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: later_mono.
+  - exact: later_intro.
+  - exact: @later_forall_2.
+  - exact: @later_exist_false.
+  - exact: later_sep_1.
+  - exact: later_sep_2.
+  - exact: later_persistently_1.
+  - exact: later_persistently_2.
+  - exact: later_false_em.
+Qed.
+
+Canonical Structure uPredI (M : ucmraT) : bi :=
+  {| bi_ofe_mixin := ofe_mixin_of (uPred M); bi_bi_mixin := uPred_bi_mixin M |}.
+Canonical Structure uPredSI (M : ucmraT) : sbi :=
+  {| sbi_ofe_mixin := ofe_mixin_of (uPred M);
+     sbi_bi_mixin := uPred_bi_mixin M; sbi_sbi_mixin := uPred_sbi_mixin M |}.
+
+Coercion uPred_valid {M} : uPred M → Prop := bi_emp_valid.
+
+Lemma uPred_plainly_mixin M : BiPlainlyMixin (uPredSI M) uPred_plainly.
+Proof.
+  split.
+  - exact: plainly_ne.
+  - exact: plainly_mono.
+  - exact: plainly_elim_persistently.
+  - exact: plainly_idemp_2.
+  - exact: @plainly_forall_2.
+  - exact: persistently_impl_plainly.
+  - exact: plainly_impl_plainly.
+  - (* P ⊢ ■ emp (ADMISSIBLE) *)
+    intros P.
+    trans (uPred_forall (M:=M) (fun _ : 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: prop_ext.
+  - exact: later_plainly_1.
+  - exact: later_plainly_2.
+Qed.
+Instance uPred_plainlyC M : BiPlainly (uPredSI M) :=
+  {| bi_plainly_mixin := uPred_plainly_mixin M |}.
+
+Lemma uPred_bupd_mixin M : BiBUpdMixin (uPredI M) uPred_bupd.
+Proof.
+  split.
+  - exact: bupd_ne.
+  - exact: bupd_intro.
+  - exact: bupd_mono.
+  - exact: bupd_trans.
+  - exact: bupd_frame_r.
+Qed.
+Instance uPred_bi_bupd M : BiBUpd (uPredI M) := {| bi_bupd_mixin := uPred_bupd_mixin M |}.
+
+Instance uPred_bi_bupd_plainly M : BiBUpdPlainly (uPredSI M).
+Proof. exact: bupd_plainly. Qed.
+
+(** extra BI instances *)
+
+Global Instance uPred_affine : BiAffine (uPredI M) | 0.
+Proof. intros P Q. exact: pure_intro. Qed.
+
+Global Instance uPred_plainly_exist_1 : BiPlainlyExist (uPredSI M).
+Proof. exact: @plainly_exist_1. Qed.

theories/base_logic/derived.v

-From iris.base_logic Require Export upred.
+From iris.base_logic Require Export bi.
 From iris.bi Require Export bi.
 Set Default Proof Using "Type".
-Import upred.uPred bi.
+Import bi.
 
 Module uPred.
+
+(* New unseal tactic that also unfolds the BI layer *)
+Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
+  unfold bi_emp; simpl; unfold sbi_emp; simpl;
+  unfold uPred_emp, bupd, bi_bupd_bupd, bi_pure,
+  bi_and, bi_or, bi_impl, bi_forall, bi_exist,
+  bi_sep, bi_wand, bi_persistently, sbi_internal_eq, sbi_later; simpl;
+  unfold sbi_emp, sbi_pure, sbi_and, sbi_or, sbi_impl, sbi_forall, sbi_exist,
+  sbi_internal_eq, sbi_sep, sbi_wand, sbi_persistently; simpl;
+  unfold plainly, bi_plainly_plainly; simpl;
+  uPred_primitive.unseal.
+
 Section derived.
 Context {M : ucmraT}.
 Implicit Types φ : Prop.
@@ -14,7 +26,57 @@ Implicit Types A : Type.
 Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
 Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
 
-(* Own and valid derived *)
+(** Propers *)
+Global Instance uPred_valid_proper : Proper ((⊣⊢) ==> iff) (@uPred_valid M).
+Proof. solve_proper. Qed.
+Global Instance uPred_valid_mono : Proper ((⊢) ==> impl) (@uPred_valid M).
+Proof. solve_proper. Qed.
+Global Instance uPred_valid_flip_mono :
+  Proper (flip (⊢) ==> flip impl) (@uPred_valid M).
+Proof. solve_proper. Qed.
+
+Global Existing Instance uPred_primitive.ownM_ne.
+Global Instance ownM_proper: Proper ((≡) ==> (⊣⊢)) (@uPred_ownM M) := ne_proper _.
+
+Global Existing Instance uPred_primitive.cmra_valid_ne.
+Global Instance cmra_valid_proper {A : cmraT} :
+  Proper ((≡) ==> (⊣⊢)) (@uPred_cmra_valid M A) := ne_proper _.
+
+(** Re-exporting primitive Own and valid lemmas *)
+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 ε).
+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.
+Lemma bupd_ownM_updateP x (Φ : M → Prop) :
+  x ~~>: Φ → uPred_ownM x ⊢ |==> ∃ y, ⌜Φ y⌝ ∧ uPred_ownM y.
+Proof. exact: uPred_primitive.bupd_ownM_updateP. Qed.
+
+Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
+Proof. exact: uPred_primitive.ownM_valid. Qed.
+Lemma cmra_valid_intro {A : cmraT} P (a : A) : ✓ a → P ⊢ (✓ a).
+Proof. exact: uPred_primitive.cmra_valid_intro. Qed.
+Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
+Proof. exact: uPred_primitive.cmra_valid_elim. Qed.
+Lemma plainly_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ ■ ✓ a.
+Proof. exact: uPred_primitive.plainly_cmra_valid_1. Qed.
+Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
+Proof. exact: uPred_primitive.cmra_valid_weaken. Qed.
+Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
+Proof. exact: uPred_primitive.prod_validI. Qed.
+Lemma option_validI {A : cmraT} (mx : option A) :
+  ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True : uPred M end.
+Proof. exact: uPred_primitive.option_validI. Qed.
+Lemma discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
+Proof. exact: uPred_primitive.discrete_valid. Qed.
+Lemma ofe_fun_validI `{B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
+Proof. exact: uPred_primitive.ofe_fun_validI. Qed.
+
+(** Own and valid derived *)
 Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ <pers> (✓ a : uPred M).
 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.

theories/base_logic/lib/own.v

@@ -118,7 +118,7 @@ Lemma own_alloc_strong a (G : gset gname) :
 Proof.
   intros Ha.
   rewrite -(bupd_mono (∃ m, ⌜∃ γ, γ ∉ G ∧ m = iRes_singleton γ a⌝ ∧ uPred_ownM m)%I).
-  - rewrite /uPred_valid /bi_emp_valid ownM_unit.
+  - rewrite /uPred_valid /bi_emp_valid (ownM_unit emp).
     eapply bupd_ownM_updateP, (ofe_fun_singleton_updateP_empty (inG_id _));
       first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
       naive_solver.
@@ -168,7 +168,7 @@ Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
 
 Lemma own_unit A `{inG Σ (A:ucmraT)} γ : (|==> own γ ε)%I.
 Proof.
-  rewrite /uPred_valid /bi_emp_valid ownM_unit !own_eq /own_def.
+  rewrite /uPred_valid /bi_emp_valid (ownM_unit emp) !own_eq /own_def.
   apply bupd_ownM_update, ofe_fun_singleton_update_empty.
   apply (alloc_unit_singleton_update (cmra_transport inG_prf ε)); last done.
   - apply cmra_transport_valid, ucmra_unit_valid.

theories/bi/derived_connectives.v

@@ -11,7 +11,7 @@ Definition bi_wand_iff {PROP : bi} (P Q : PROP) : PROP :=
   ((P -∗ Q) ∧ (Q -∗ P))%I.
 Arguments bi_wand_iff {_} _%I _%I : simpl never.
 Instance: Params (@bi_wand_iff) 1.
-Infix "∗-∗" := bi_wand_iff (at level 95, no associativity) : bi_scope.
+Infix "∗-∗" := bi_wand_iff : bi_scope.
 
 Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ <pers> P.
 Arguments Persistent {_} _%I : simpl never.
@@ -23,8 +23,7 @@ Definition bi_affinely {PROP : bi} (P : PROP) : PROP := (emp ∧ P)%I.
 Arguments bi_affinely {_} _%I : simpl never.
 Instance: Params (@bi_affinely) 1.
 Typeclasses Opaque bi_affinely.
-Notation "'<affine>' P" := (bi_affinely P)
-  (at level 20, right associativity) : bi_scope.
+Notation "'<affine>' P" := (bi_affinely P) : bi_scope.
 
 Class Affine {PROP : bi} (Q : PROP) := affine : Q ⊢ emp.
 Arguments Affine {_} _%I : simpl never.
@@ -43,8 +42,7 @@ Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True ∗ P)%I.
 Arguments bi_absorbingly {_} _%I : simpl never.
 Instance: Params (@bi_absorbingly) 1.
 Typeclasses Opaque bi_absorbingly.
-Notation "'<absorb>' P" := (bi_absorbingly P)
-  (at level 20, right associativity) : bi_scope.
+Notation "'<absorb>' P" := (bi_absorbingly P) : bi_scope.
 
 Class Absorbing {PROP : bi} (P : PROP) := absorbing : <absorb> P ⊢ P.
 Arguments Absorbing {_} _%I : simpl never.
@@ -56,35 +54,28 @@ Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
 Arguments bi_persistently_if {_} !_ _%I /.
 Instance: Params (@bi_persistently_if) 2.
 Typeclasses Opaque bi_persistently_if.
-Notation "'<pers>?' p P" := (bi_persistently_if p P)
-  (at level 20, p at level 9, P at level 20,
-   right associativity, format "'<pers>?' p  P") : bi_scope.
+Notation "'<pers>?' p P" := (bi_persistently_if p P) : bi_scope.
 
 Definition bi_affinely_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
   (if p then <affine> P else P)%I.
 Arguments bi_affinely_if {_} !_ _%I /.
 Instance: Params (@bi_affinely_if) 2.
 Typeclasses Opaque bi_affinely_if.
-Notation "'<affine>?' p P" := (bi_affinely_if p P)
-  (at level 20, p at level 9, P at level 20,
-   right associativity, format "'<affine>?' p  P") : bi_scope.
+Notation "'<affine>?' p P" := (bi_affinely_if p P) : bi_scope.
 
 Definition bi_intuitionistically {PROP : bi} (P : PROP) : PROP :=
   (<affine> <pers> P)%I.
 Arguments bi_intuitionistically {_} _%I : simpl never.
 Instance: Params (@bi_intuitionistically) 1.
 Typeclasses Opaque bi_intuitionistically.
-Notation "□ P" := (bi_intuitionistically P)%I
-  (at level 20, right associativity) : bi_scope.
+Notation "□ P" := (bi_intuitionistically P) : bi_scope.
 
 Definition bi_intuitionistically_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
   (if p then □ P else P)%I.
 Arguments bi_intuitionistically_if {_} !_ _%I /.
 Instance: Params (@bi_intuitionistically_if) 2.
 Typeclasses Opaque bi_intuitionistically_if.
-Notation "'□?' p P" := (bi_intuitionistically_if p P)
-  (at level 20, p at level 9, P at level 20,
-   right associativity, format "'□?' p  P") : bi_scope.
+Notation "'□?' p P" := (bi_intuitionistically_if p P) : bi_scope.
 
 Fixpoint bi_hexist {PROP : bi} {As} : himpl As PROP → PROP :=
   match As return himpl As PROP → PROP with
@@ -101,14 +92,12 @@ Definition sbi_laterN {PROP : sbi} (n : nat) (P : PROP) : PROP :=
   Nat.iter n sbi_later P.
 Arguments sbi_laterN {_} !_%nat_scope _%I.
 Instance: Params (@sbi_laterN) 2.
-Notation "▷^ n P" := (sbi_laterN n P)
-  (at level 20, n at level 9, P at level 20, format "▷^ n  P") : bi_scope.
-Notation "▷? p P" := (sbi_laterN (Nat.b2n p) P)
-  (at level 20, p at level 9, P at level 20, format "▷? p  P") : bi_scope.
+Notation "▷^ n P" := (sbi_laterN n P) : bi_scope.
+Notation "▷? p P" := (sbi_laterN (Nat.b2n p) P) : bi_scope.
 
 Definition sbi_except_0 {PROP : sbi} (P : PROP) : PROP := (▷ False ∨ P)%I.
 Arguments sbi_except_0 {_} _%I : simpl never.
-Notation "◇ P" := (sbi_except_0 P) (at level 20, right associativity) : bi_scope.
+Notation "◇ P" := (sbi_except_0 P) : bi_scope.
 Instance: Params (@sbi_except_0) 1.
 Typeclasses Opaque sbi_except_0.
 

theories/bi/derived_laws_bi.v

@@ -531,7 +531,7 @@ Lemma pure_wand_forall φ P `{!Absorbing P} : (⌜φ⌝ -∗ P) ⊣⊢ (∀ _ :
 Proof.
   apply (anti_symm _).
   - apply forall_intro=> Hφ.
-    by rewrite -(left_id emp%I _ (_ -∗ _)%I) (pure_intro emp%I φ) // wand_elim_r.
+    by rewrite -(left_id emp%I _ (_ -∗ _)%I) (pure_intro φ emp%I) // wand_elim_r.
   - apply wand_intro_l, wand_elim_l', pure_elim'=> Hφ.
     apply wand_intro_l. rewrite (forall_elim Hφ) comm. by apply absorbing.
 Qed.

theories/bi/interface.v

 From iris.algebra Require Export ofe.
+From iris.bi Require Export notation.
 Set Primitive Projections.
 
-Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity).
-Reserved Notation "P '⊢@{' PROP } Q" (at level 99, Q at level 200, right associativity).
-Reserved Notation "('⊢@{' PROP } )" (at level 99).
-Reserved Notation "P ⊣⊢ Q" (at level 95, no associativity).
-Reserved Notation "P '⊣⊢@{' PROP } Q" (at level 95, no associativity).
-Reserved Notation "('⊣⊢@{' PROP } )" (at level 95).
-Reserved Notation "'emp'".
-Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ ⌝").
-Reserved Notation "P ∗ Q" (at level 80, right associativity).
-Reserved Notation "P -∗ Q" (at level 99, Q at level 200, right associativity).
-Reserved Notation "'<pers>' P" (at level 20, right associativity).
-Reserved Notation "▷ P" (at level 20, right associativity).
-
 Section bi_mixin.
   Context {PROP : Type} `{Dist PROP, Equiv PROP}.
   Context (bi_entails : PROP → PROP → Prop).
@@ -77,7 +65,7 @@ Section bi_mixin.
     bi_mixin_persistently_ne : NonExpansive bi_persistently;
 
     (** Higher-order logic *)
-    bi_mixin_pure_intro P (φ : Prop) : φ → P ⊢ ⌜ φ ⌝;
+    bi_mixin_pure_intro (φ : Prop) P : φ → P ⊢ ⌜ φ ⌝;
     bi_mixin_pure_elim' (φ : Prop) P : (φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P;
     (* This is actually derivable if we assume excluded middle in Coq,
        via [(∀ a, φ a) ∨ (∃ a, ¬φ a)]. *)
@@ -195,7 +183,6 @@ Instance: Params (@bi_sep) 1.
 Instance: Params (@bi_wand) 1.
 Instance: Params (@bi_persistently) 1.
 
-Delimit Scope bi_scope with I.
 Arguments bi_car : simpl never.
 Arguments bi_dist : simpl never.
 Arguments bi_equiv : simpl never.
@@ -347,7 +334,7 @@ Global Instance persistently_ne : NonExpansive (@bi_persistently PROP).
 Proof. eapply bi_mixin_persistently_ne, bi_bi_mixin. Qed.
 
 (* Higher-order logic *)
-Lemma pure_intro P (φ : Prop) : φ → P ⊢ ⌜ φ ⌝.
+Lemma pure_intro (φ : Prop) P : φ → P ⊢ ⌜ φ ⌝.
 Proof. eapply bi_mixin_pure_intro, bi_bi_mixin. Qed.
 Lemma pure_elim' (φ : Prop) P : (φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P.
 Proof. eapply bi_mixin_pure_elim', bi_bi_mixin. Qed.

theories/bi/notation.v

+(** Just reserve the notation. *)
+Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity).
+Reserved Notation "P '⊢@{' PROP } Q" (at level 99, Q at level 200, right associativity).
+Reserved Notation "('⊢@{' PROP } )" (at level 99).
+Reserved Notation "P ⊣⊢ Q" (at level 95, no associativity).
+Reserved Notation "P '⊣⊢@{' PROP } Q" (at level 95, no associativity).
+Reserved Notation "('⊣⊢@{' PROP } )" (at level 95).
+Reserved Notation "'emp'".
+Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ ⌝").
+Reserved Notation "P ∗ Q" (at level 80, right associativity).
+Reserved Notation "P -∗ Q" (at level 99, Q at level 200, right associativity).
+
+Reserved Notation "'<pers>' P" (at level 20, right associativity).
+Reserved Notation "'<pers>?' p P" (at level 20, p at level 9, P at level 20,
+   right associativity, format "'<pers>?' p  P").
+
+Reserved Notation "▷ P" (at level 20, right associativity).
+Reserved Notation "▷? p P" (at level 20, p at level 9, P at level 20,
+   format "▷? p  P").
+Reserved Notation "▷^ n P" (at level 20, n at level 9, P at level 20,
+   format "▷^ n  P").
+
+Reserved Infix "∗-∗" (at level 95, no associativity).
+
+Reserved Notation "'<affine>' P" (at level 20, right associativity).
+Reserved Notation "'<affine>?' p P" (at level 20, p at level 9, P at level 20,
+   right associativity, format "'<affine>?' p  P").
+
+Reserved Notation "'<absorb>' P" (at level 20, right associativity).
+
+Reserved Notation "□ P" (at level 20, right associativity).
+Reserved Notation "'□?' p P" (at level 20, p at level 9, P at level 20,
+   right associativity, format "'□?' p  P").
+
+Reserved Notation "◇ P" (at level 20, right associativity).
+
+Reserved Notation "■ P" (at level 20, right associativity).
+Reserved Notation "■? p P" (at level 20, p at level 9, P at level 20,
+   right associativity, format "■? p  P").
+
+Reserved Notation "|==> Q" (at level 99, Q at level 200, format "|==>  Q").
+Reserved Notation "P ==∗ Q" (at level 99, Q at level 200, format "P  ==∗  Q").
+
+(** Define the scope *)
+Delimit Scope bi_scope with I.

theories/bi/plainly.v

@@ -5,8 +5,7 @@ Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
 Class Plainly (A : Type) := plainly : A → A.
 Hint Mode Plainly ! : typeclass_instances.
 Instance: Params (@plainly) 2.
-Notation "■ P" := (plainly P)%I
-  (at level 20, right associativity) : bi_scope.
+Notation "■ P" := (plainly P) : bi_scope.
 
 (* Mixins allow us to create instances easily without having to use Program *)
 Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := {
@@ -96,9 +95,7 @@ Arguments plainly_if {_ _} !_ _%I /.
 Instance: Params (@plainly_if) 2.
 Typeclasses Opaque plainly_if.
 
-Notation "■? p P" := (plainly_if p P)%I
-  (at level 20, p at level 9, P at level 20,
-   right associativity, format "■? p  P") : bi_scope.
+Notation "■? p P" := (plainly_if p P) : bi_scope.
 
 (* Derived laws *)
 Section plainly_derived.
@@ -167,7 +164,7 @@ Proof.
   - by rewrite plainly_elim_persistently persistently_pure.
   - apply pure_elim'=> Hφ.
     trans (∀ x : False, ■ True : PROP)%I; [by apply forall_intro|].
-    rewrite plainly_forall_2. by rewrite -(pure_intro _ φ).
+    rewrite plainly_forall_2. by rewrite -(pure_intro φ).
 Qed.
 Lemma plainly_forall {A} (Ψ : A → PROP) : ■ (∀ a, Ψ a) ⊣⊢ ∀ a, ■ (Ψ a).
 Proof.

theories/bi/updates.v

@@ -7,12 +7,9 @@ Class BUpd (PROP : Type) : Type := bupd : PROP → PROP.
 Instance : Params (@bupd) 2.
 Hint Mode BUpd ! : typeclass_instances.
 
-Notation "|==> Q" := (bupd Q)
-  (at level 99, Q at level 200, format "|==>  Q") : bi_scope.
-Notation "P ==∗ Q" := (P ⊢ |==> Q)
-  (at level 99, Q at level 200, only parsing) : stdpp_scope.
-Notation "P ==∗ Q" := (P -∗ |==> Q)%I
-  (at level 99, Q at level 200, format "P  ==∗  Q") : bi_scope.
+Notation "|==> Q" := (bupd Q) : bi_scope.
+Notation "P ==∗ Q" := (P ⊢ |==> Q) (only parsing) : stdpp_scope.
+Notation "P ==∗ Q" := (P -∗ |==> Q)%I : bi_scope.
 
 Class FUpd (PROP : Type) : Type := fupd : coPset → coPset → PROP → PROP.
 Instance: Params (@fupd) 4.

theories/proofmode/class_instances_sbi.v

@@ -354,7 +354,7 @@ Global Instance into_forall_wand_pure φ P Q :
 Proof.
   rewrite /FromPureT /FromPure /IntoForall=> -[φ' [-> <-]] /=.
   apply forall_intro=>? /=.
-  by rewrite -(pure_intro True%I) // /bi_affinely right_id emp_wand.
+  by rewrite -(pure_intro _ True%I) // /bi_affinely right_id emp_wand.
 Qed.
 
 Global Instance into_forall_plainly `{BiPlainly PROP} {A} P (Φ : A → PROP) :