From 5f2e82228f3d870ee018d340800d42489262fe46 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 6 Jun 2021 10:51:22 +0200
Subject: [PATCH] move BI interface extensions to their own file
---
CHANGELOG.md | 2 ++
_CoqProject | 1 +
iris/base_logic/bi.v | 2 +-
iris/bi/derived_connectives.v | 33 ------------------------------
iris/bi/derived_laws.v | 2 +-
iris/bi/extensions.v | 38 +++++++++++++++++++++++++++++++++++
6 files changed, 43 insertions(+), 35 deletions(-)
create mode 100644 iris/bi/extensions.v
diff --git a/CHANGELOG.md b/CHANGELOG.md
index f93680cbf..3e6881be0 100644
--- a/CHANGELOG.md
+++ b/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`:**
diff --git a/_CoqProject b/_CoqProject
index 21b032e94..1ec070191 100644
--- a/_CoqProject
+++ b/_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
diff --git a/iris/base_logic/bi.v b/iris/base_logic/bi.v
index 77be327e6..f555ec335 100644
--- a/iris/base_logic/bi.v
+++ b/iris/base_logic/bi.v
@@ -1,4 +1,4 @@
-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.
diff --git a/iris/bi/derived_connectives.v b/iris/bi/derived_connectives.v
index 7f965854e..a5071e78a 100644
--- a/iris/bi/derived_connectives.v
+++ b/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 âŒ.
diff --git a/iris/bi/derived_laws.v b/iris/bi/derived_laws.v
index d5713f5cf..fc8d8955d 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -1,5 +1,5 @@
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*]. *)
diff --git a/iris/bi/extensions.v b/iris/bi/extensions.v
new file mode 100644
index 000000000..6764ebe25
--- /dev/null
+++ b/iris/bi/extensions.v
@@ -0,0 +1,38 @@
+(** 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 âŒ.
--
GitLab