move BI interface extensions to their own file

CHANGELOG.md

@@ -56,6 +56,8 @@ Coq 8.11 is no longer supported in this version of Iris.
 **Changes in `bi`:**
 
 * Add lemmas characterizing big-ops over pure predicates (`big_sep*_pure*`).
+* Move `BiAffine`, `BiPositive`, `BiLöb`, and `BiPureForall` from
+  `bi.derived_connectives` to `bi.extensions`.
 
 **Changes in `base_logic`:**
 

_CoqProject

@@ -58,6 +58,7 @@ iris/si_logic/bi.v
 iris/bi/notation.v
 iris/bi/interface.v
 iris/bi/derived_connectives.v
+iris/bi/extensions.v
 iris/bi/derived_laws.v
 iris/bi/derived_laws_later.v
 iris/bi/plainly.v

iris/base_logic/bi.v

-From iris.bi Require Export derived_connectives updates internal_eq plainly.
+From iris.bi Require Export derived_connectives extensions updates internal_eq plainly.
 From iris.base_logic Require Export upred.
 From iris.prelude Require Import options.
 Import uPred_primitive.

iris/bi/derived_connectives.v

@@ -30,14 +30,6 @@ Global Arguments Affine {_} _%I : simpl never.
 Global Arguments affine {_} _%I {_}.
 Global Hint Mode Affine + ! : typeclass_instances.
 
-Class BiAffine (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
-Global Hint Mode BiAffine ! : typeclass_instances.
-Global Existing Instance absorbing_bi | 0.
-
-Class BiPositive (PROP : bi) :=
-  bi_positive (P Q : PROP) : <affine> (P ∗ Q) ⊢ <affine> P ∗ Q.
-Global Hint Mode BiPositive ! : typeclass_instances.
-
 Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := True ∗ P.
 Global Arguments bi_absorbingly {_} _%I : simpl never.
 Global Instance: Params (@bi_absorbingly) 1 := {}.
@@ -117,28 +109,3 @@ Definition bi_wandM {PROP : bi} (mP : option PROP) (Q : PROP) : PROP :=
 Global Arguments bi_wandM {_} !_%I _%I /.
 Notation "mP -∗? Q" := (bi_wandM mP Q)
   (at level 99, Q at level 200, right associativity) : bi_scope.
-
-(** The class [BiLöb] is required for the [iLöb] tactic. However, for most BI
-logics [BiLaterContractive] should be used, which gives an instance of [BiLöb]
-automatically (see [derived_laws_later]). A direct instance of [BiLöb] is useful
-when considering a BI logic with a discrete OFE, instead of an OFE that takes
-step-indexing of the logic in account.
-
-The internal/"strong" version of Löb [(▷ P → P) ⊢ P] is derivable from [BiLöb].
-It is provided by the lemma [löb] in [derived_laws_later]. *)
-Class BiLöb (PROP : bi) :=
-  löb_weak (P : PROP) : (▷ P ⊢ P) → (True ⊢ P).
-Global Hint Mode BiLöb ! : typeclass_instances.
-Global Arguments löb_weak {_ _} _ _.
-
-Notation BiLaterContractive PROP :=
-  (Contractive (bi_later (PROP:=PROP))) (only parsing).
-
-(** The class [BiPureForall] states that universal quantification commutes with
-the embedding of pure propositions. The reverse direction of the entailment
-described by this type class is derivable, so it is not included.
-
-An instance of [BiPureForall] itself is derivable if we assume excluded middle
-in Coq, see the lemma [bi_pure_forall_em] in [derived_laws]. *)
-Class BiPureForall (PROP : bi) :=
-  pure_forall_2 : ∀ {A} (φ : A → Prop), (∀ a, ⌜ φ a ⌝) ⊢@{PROP} ⌜ ∀ a, φ a ⌝.

iris/bi/derived_laws.v

 From iris.algebra Require Import monoid.
-From iris.bi Require Export derived_connectives.
+From iris.bi Require Export extensions.
 From iris.prelude Require Import options.
 
 (* The sections add [BiAffine] and the like, which is only picked up with [Type*]. *)

iris/bi/extensions.v

+(** This file defines various extensions to the base BI interface, via
+typeclasses that BIs can optionally implement. *)
+
+From iris.bi Require Export derived_connectives.
+From iris.prelude Require Import options.
+
+Class BiAffine (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
+Global Hint Mode BiAffine ! : typeclass_instances.
+Global Existing Instance absorbing_bi | 0.
+
+Class BiPositive (PROP : bi) :=
+  bi_positive (P Q : PROP) : <affine> (P ∗ Q) ⊢ <affine> P ∗ Q.
+Global Hint Mode BiPositive ! : typeclass_instances.
+
+(** The class [BiLöb] is required for the [iLöb] tactic. However, for most BI
+logics [BiLaterContractive] should be used, which gives an instance of [BiLöb]
+automatically (see [derived_laws_later]). A direct instance of [BiLöb] is useful
+when considering a BI logic with a discrete OFE, instead of an OFE that takes
+step-indexing of the logic in account.
+
+The internal/"strong" version of Löb [(▷ P → P) ⊢ P] is derivable from [BiLöb].
+It is provided by the lemma [löb] in [derived_laws_later]. *)
+Class BiLöb (PROP : bi) :=
+  löb_weak (P : PROP) : (▷ P ⊢ P) → (True ⊢ P).
+Global Hint Mode BiLöb ! : typeclass_instances.
+Global Arguments löb_weak {_ _} _ _.
+
+Notation BiLaterContractive PROP :=
+  (Contractive (bi_later (PROP:=PROP))) (only parsing).
+
+(** The class [BiPureForall] states that universal quantification commutes with
+the embedding of pure propositions. The reverse direction of the entailment
+described by this type class is derivable, so it is not included.
+
+An instance of [BiPureForall] itself is derivable if we assume excluded middle
+in Coq, see the lemma [bi_pure_forall_em] in [derived_laws]. *)
+Class BiPureForall (PROP : bi) :=
+  pure_forall_2 : ∀ {A} (φ : A → Prop), (∀ a, ⌜ φ a ⌝) ⊢@{PROP} ⌜ ∀ a, φ a ⌝.