Merge branch 'ralf/upred' into 'gen_proofmode'

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

See merge request FP/iris-coq!148

_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,9 +45,10 @@ 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/proofmode.v
 theories/base_logic/base_logic.v
-theories/base_logic/soundness.v
 theories/base_logic/double_negation.v
 theories/base_logic/lib/iprop.v
 theories/base_logic/lib/own.v

theories/base_logic/base_logic.v

-From iris.base_logic Require Export derived.
+From iris.base_logic Require Export derived proofmode.
 From iris.bi Require Export bi.
-From iris.algebra Require Import proofmode_classes.
 Set Default Proof Using "Type".
 
 (* The trick of having multiple [uPred] modules, which are all exported in
 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 base_logic.bi.uPred.
   Export derived.uPred.
-  Export bi.
+  Export bi.bi.
 End uPred.
-
-(* Setup of the proof mode *)
-Section class_instances.
-Context {M : ucmraT}.
-Implicit Types P Q R : uPred M.
-
-Global Instance into_pure_cmra_valid `{CmraDiscrete A} (a : A) :
-  @IntoPure (uPredI M) (✓ a) (✓ a).
-Proof. by rewrite /IntoPure discrete_valid. Qed.
-
-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.
-Qed.
-
-Global Instance from_sep_ownM (a b1 b2 : M) :
-  IsOp a b1 b2 →
-  FromSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof. intros. by rewrite /FromSep -ownM_op -is_op. Qed.
-Global Instance from_sep_ownM_core_id (a b1 b2 : M) :
-  IsOp a b1 b2 → TCOr (CoreId b1) (CoreId b2) →
-  FromAnd (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof.
-  intros ? H. rewrite /FromAnd (is_op a) ownM_op.
-  destruct H; by rewrite persistent_and_sep.
-Qed.
-
-Global Instance into_and_ownM p (a b1 b2 : M) :
-  IsOp a b1 b2 → IntoAnd p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof.
-  intros. apply intuitionistically_if_mono. by rewrite (is_op a) ownM_op sep_and.
-Qed.
-
-Global Instance into_sep_ownM (a b1 b2 : M) :
-  IsOp a b1 b2 → IntoSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof. intros. by rewrite /IntoSep (is_op a) ownM_op. Qed.
-End class_instances.

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 instances for uPred, and re-stating the remaining primitive laws in terms
+of the BI interface.  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) (λ _ : 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) (λ _ : 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.
+Global 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.
+Global Instance uPred_bi_bupd M : BiBUpd (uPredI M) := {| bi_bupd_mixin := uPred_bupd_mixin M |}.
+
+Global 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.
+(* Also add this to the global hint database, otherwise [eauto] won't work for
+many lemmas that have [BiAffine] as a premise. *)
+Hint Immediate uPred_affine.
+
+Global Instance uPred_plainly_exist_1 : BiPlainlyExist (uPredSI M).
+Proof. exact: @plainly_exist_1. Qed.
+
+(** Re-state/export lemmas about Iris-specific primitive connectives (own, valid) *)
+
+Module uPred.
+
+Section restate.
+Context {M : ucmraT}.
+Implicit Types φ : Prop.
+Implicit Types P Q : uPred M.
+Implicit Types A : Type.
+
+(* Force implicit argument M *)
+Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
+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 : cmraT} : NonExpansive (@uPred_cmra_valid M A)
+  := uPred_primitive.cmra_valid_ne.
+
+(** 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.
+
+(** Consistency/soundness statement *)
+Lemma soundness φ n : (▷^n ⌜ φ ⌝ : uPred M)%I → φ.
+Proof. exact: uPred_primitive.soundness. Qed.
+
+End restate.
+
+(** New unseal tactic that also unfolds the BI layer.
+    This is used by [base_logic.double_negation].
+    TODO: Can we get rid of this? *)
+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.
+
+End uPred.

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 base_logic.bi.uPred.
+
+(** Derived laws for Iris-specific primitive connectives (own, valid).
+    This file does NOT unseal! *)
 
 Module uPred.
 Section derived.
@@ -14,7 +17,20 @@ 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 Instance ownM_proper: Proper ((≡) ==> (⊣⊢)) (@uPred_ownM M) := ne_proper _.
+Global Instance cmra_valid_proper {A : cmraT} :
+  Proper ((≡) ==> (⊣⊢)) (@uPred_cmra_valid M A) := ne_proper _.
+
+(** 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.
@@ -43,7 +59,7 @@ Proof.
   by apply bupd_mono, exist_elim=> y'; apply pure_elim_l=> ->.
 Qed.
 
-(* Timeless instances *)
+(** Timeless instances *)
 Global Instance valid_timeless {A : cmraT} `{CmraDiscrete A} (a : A) :
   Timeless (✓ a : uPred M)%I.
 Proof. rewrite /Timeless !discrete_valid. apply (timeless _). Qed.
@@ -56,12 +72,12 @@ Proof.
     auto using and_elim_l, and_elim_r.
 Qed.
 
-(* Plainness *)
+(** Plainness *)
 Global Instance cmra_valid_plain {A : cmraT} (a : A) :
   Plain (✓ a : uPred M)%I.
 Proof. rewrite /Persistent. apply plainly_cmra_valid_1. Qed.
 
-(* Persistence *)
+(** Persistence *)
 Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
   Persistent (✓ a : uPred M)%I.
 Proof. rewrite /Persistent. apply persistently_cmra_valid_1. Qed.
@@ -70,13 +86,19 @@ Proof.
   intros. rewrite /Persistent -{2}(core_id_core a). apply persistently_ownM_core.
 Qed.
 
-(* For big ops *)
+(** For big ops *)
 Global Instance uPred_ownM_sep_homomorphism :
   MonoidHomomorphism op uPred_sep (≡) (@uPred_ownM M).
 Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
+
+
+(** Consistency/soundness statement *)
+Corollary consistency_modal n : ¬ (▷^n False : uPred M)%I.
+Proof. exact (soundness False n). Qed.
+
+Corollary consistency : ¬(False : uPred M)%I.
+Proof. exact (consistency_modal 0). Qed.
+
 End derived.
 
-(* Also add this to the global hint database, otherwise [eauto] won't work for
-many lemmas that have [BiAffine] as a premise. *)
-Hint Immediate uPred_affine.
 End uPred.

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/base_logic/proofmode.v

+From iris.base_logic Require Export derived.
+From iris.algebra Require Import proofmode_classes.
+
+Import base_logic.bi.uPred.
+
+(* Setup of the proof mode *)
+Section class_instances.
+Context {M : ucmraT}.
+Implicit Types P Q R : uPred M.
+
+Global Instance into_pure_cmra_valid `{CmraDiscrete A} (a : A) :
+  @IntoPure (uPredI M) (✓ a) (✓ a).
+Proof. by rewrite /IntoPure discrete_valid. Qed.
+
+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 bi.affinely_if_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).
+Proof. intros. by rewrite /FromSep -ownM_op -is_op. Qed.
+Global Instance from_sep_ownM_core_id (a b1 b2 : M) :
+  IsOp a b1 b2 → TCOr (CoreId b1) (CoreId b2) →
+  FromAnd (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Proof.
+  intros ? H. rewrite /FromAnd (is_op a) ownM_op.
+  destruct H; by rewrite bi.persistent_and_sep.
+Qed.
+
+Global Instance into_and_ownM p (a b1 b2 : M) :
+  IsOp a b1 b2 → IntoAnd p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Proof.
+  intros. apply bi.intuitionistically_if_mono. by rewrite (is_op a) ownM_op bi.sep_and.
+Qed.
+
+Global Instance into_sep_ownM (a b1 b2 : M) :
+  IsOp a b1 b2 → IntoSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Proof. intros. by rewrite /IntoSep (is_op a) ownM_op. Qed.
+End class_instances.

theories/base_logic/soundness.v

-From iris.base_logic Require Export base_logic.
-Set Default Proof Using "Type".
-Import uPred.
-
-Section adequacy.
-Context {M : ucmraT}.
-
-(** Consistency and adequancy statements *)
-Lemma soundness φ n : (▷^n ⌜ φ ⌝ : uPred M)%I → φ.
-Proof.
-  cut ((▷^n ⌜ φ ⌝ : uPred M)%I n ε → φ).
-  { intros help H. eapply help, H; eauto using ucmra_unit_validN. by unseal. }
-  rewrite /sbi_laterN; unseal. induction n as [|n IH]=> H; auto.
-Qed.
-
-Corollary consistency_modal n : ¬ (▷^n False : uPred M)%I.
-Proof. exact (soundness False n). Qed.
-
-Corollary consistency : ¬(False : uPred M)%I.
-Proof. exact (consistency_modal 0). Qed.
-End adequacy.

theories/bi/big_op.v

@@ -5,40 +5,26 @@ Set Default Proof Using "Type".
 Import interface.bi derived_laws_bi.bi.
 
 (* Notations *)
-Notation "'[∗' 'list]' k ↦ x ∈ l , P" := (big_opL bi_sep (λ k x, P) l)
-  (at level 200, l at level 10, k, x at level 1, right associativity,
-   format "[∗  list]  k ↦ x  ∈  l ,  P") : bi_scope.
-Notation "'[∗' 'list]' x ∈ l , P" := (big_opL bi_sep (λ _ x, P) l)
-  (at level 200, l at level 10, x at level 1, right associativity,
-   format "[∗  list]  x  ∈  l ,  P") : bi_scope.
-
-Notation "'[∗]' Ps" :=
-  (big_opL bi_sep (λ _ x, x) Ps) (at level 20) : bi_scope.
-
-Notation "'[∧' 'list]' k ↦ x ∈ l , P" := (big_opL bi_and (λ k x, P) l)
-  (at level 200, l at level 10, k, x at level 1, right associativity,
-   format "[∧  list]  k ↦ x  ∈  l ,  P") : bi_scope.
-Notation "'[∧' 'list]' x ∈ l , P" := (big_opL bi_and (λ _ x, P) l)
-  (at level 200, l at level 10, x at level 1, right associativity,
-   format "[∧  list]  x  ∈  l ,  P") : bi_scope.
-
-Notation "'[∧]' Ps" :=
-  (big_opL bi_and (λ _ x, x) Ps) (at level 20) : bi_scope.
-
-Notation "'[∗' 'map]' k ↦ x ∈ m , P" := (big_opM bi_sep (λ k x, P) m)
-  (at level 200, m at level 10, k, x at level 1, right associativity,
-   format "[∗  map]  k ↦ x  ∈  m ,  P") : bi_scope.
-Notation "'[∗' 'map]' x ∈ m , P" := (big_opM bi_sep (λ _ x, P) m)
-  (at level 200, m at level 10, x at level 1, right associativity,
-   format "[∗  map]  x  ∈  m ,  P") : bi_scope.
-
-Notation "'[∗' 'set]' x ∈ X , P" := (big_opS bi_sep (λ x, P) X)
-  (at level 200, X at level 10, x at level 1, right associativity,
-   format "[∗  set]  x  ∈  X ,  P") : bi_scope.
-
-Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P) X)
-  (at level 200, X at level 10, x at level 1, right associativity,
-   format "[∗  mset]  x  ∈  X ,  P") : bi_scope.
+Notation "'[∗' 'list]' k ↦ x ∈ l , P" :=
+  (big_opL bi_sep (λ k x, P) l) : bi_scope.
+Notation "'[∗' 'list]' x ∈ l , P" :=
+  (big_opL bi_sep (λ _ x, P) l) : bi_scope.
+
+Notation "'[∗]' Ps" := (big_opL bi_sep (λ _ x, x) Ps) : bi_scope.
+
+Notation "'[∧' 'list]' k ↦ x ∈ l , P" :=
+  (big_opL bi_and (λ k x, P) l) : bi_scope.
+Notation "'[∧' 'list]' x ∈ l , P" :=
+  (big_opL bi_and (λ _ x, P) l) : bi_scope.
+
+Notation "'[∧]' Ps" := (big_opL bi_and (λ _ x, x) Ps) : bi_scope.
+
+Notation "'[∗' 'map]' k ↦ x ∈ m , P" := (big_opM bi_sep (λ k x, P) m) : bi_scope.
+Notation "'[∗' 'map]' x ∈ m , P" := (big_opM bi_sep (λ _ x, P) m) : bi_scope.
+
+Notation "'[∗' 'set]' x ∈ X , P" := (big_opS bi_sep (λ x, P) X) : bi_scope.
+
+Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P) X) : bi_scope.
 
 (** * Properties *)
 Section bi_big_op.

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.