From ca0996a8cd47530bdf3d0609abfc8f63283006d3 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 4 Dec 2017 20:10:44 +0100
Subject: [PATCH] Split bi/derived.v intro bi/derived_connectives.v and
 bi/derived_laws.v

---
 _CoqProject                               |   3 +-
 theories/base_logic/derived.v             |   4 +-
 theories/base_logic/upred.v               |   2 +-
 theories/bi/bi.v                          |   4 +-
 theories/bi/big_op.v                      |   4 +-
 theories/bi/derived_connectives.v         | 111 ++++++++++++++++++++++
 theories/bi/{derived.v => derived_laws.v} | 110 +--------------------
 7 files changed, 121 insertions(+), 117 deletions(-)
 create mode 100644 theories/bi/derived_connectives.v
 rename theories/bi/{derived.v => derived_laws.v} (95%)

diff --git a/_CoqProject b/_CoqProject
index 8b92bf43d..1211cbed0 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -26,7 +26,8 @@ theories/algebra/coPset.v
 theories/algebra/deprecated.v
 theories/algebra/proofmode_classes.v
 theories/bi/interface.v
-theories/bi/derived.v
+theories/bi/derived_connectives.v
+theories/bi/derived_laws.v
 theories/bi/big_op.v
 theories/bi/bi.v
 theories/bi/tactics.v
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index f3da2382d..b193b9474 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -1,8 +1,8 @@
 From iris.base_logic Require Export upred.
-From iris.bi Require Export interface derived.
+From iris.bi Require Export derived_laws.
 Set Default Proof Using "Type".
 Import upred.uPred.
-Import interface.bi derived.bi.
+Import interface.bi derived_laws.bi.
 
 Module uPred.
 Section derived.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index dce0d1ca3..d65acf875 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export cmra updates.
-From iris.bi Require Export interface.
+From iris.bi Require Export derived_connectives.
 From stdpp Require Import finite.
 Set Default Proof Using "Type".
 Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|].
diff --git a/theories/bi/bi.v b/theories/bi/bi.v
index f4c5f8fc6..8e90d845f 100644
--- a/theories/bi/bi.v
+++ b/theories/bi/bi.v
@@ -1,9 +1,9 @@
-From iris.bi Require Export interface derived big_op.
+From iris.bi Require Export derived_laws big_op.
 Set Default Proof Using "Type".
 
 Module Import bi.
   Export bi.interface.bi.
-  Export bi.derived.bi.
+  Export bi.derived_laws.bi.
   Export bi.big_op.bi.
 End bi.
 
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 2ae8c66a5..3472d004e 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export big_op.
-From iris.bi Require Export derived.
+From iris.bi Require Export derived_laws.
 From stdpp Require Import countable fin_collections functions.
 Set Default Proof Using "Type".
 
@@ -41,7 +41,7 @@ Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P) X)
 
 (** * Properties *)
 Module bi.
-Import interface.bi derived.bi.
+Import interface.bi derived_laws.bi.
 Section bi_big_op.
 Context {PROP : bi}.
 Implicit Types Ps Qs : list PROP.
diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
new file mode 100644
index 000000000..942c2f1de
--- /dev/null
+++ b/theories/bi/derived_connectives.v
@@ -0,0 +1,111 @@
+From iris.bi Require Export interface.
+From iris.algebra Require Import monoid.
+From stdpp Require Import hlist.
+
+Definition bi_iff {PROP : bi} (P Q : PROP) : PROP := ((P → Q) ∧ (Q → P))%I.
+Arguments bi_iff {_} _%I _%I : simpl never.
+Instance: Params (@bi_iff) 1.
+Infix "↔" := bi_iff : bi_scope.
+
+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.
+
+Class Plain {PROP : bi} (P : PROP) := plain : P ⊢ bi_plainly P.
+Arguments Plain {_} _%I : simpl never.
+Arguments plain {_} _%I {_}.
+Hint Mode Plain + ! : typeclass_instances.
+Instance: Params (@Plain) 1.
+
+Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ bi_persistently P.
+Arguments Persistent {_} _%I : simpl never.
+Arguments persistent {_} _%I {_}.
+Hint Mode Persistent + ! : typeclass_instances.
+Instance: Params (@Persistent) 1.
+
+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 "â–¡ P" := (bi_affinely (bi_persistently P))%I
+  (at level 20, right associativity) : bi_scope.
+Notation "â–  P" := (bi_affinely (bi_plainly P))%I
+  (at level 20, right associativity) : bi_scope.
+
+Class Affine {PROP : bi} (Q : PROP) := affine : Q ⊢ emp.
+Arguments Affine {_} _%I : simpl never.
+Arguments affine {_} _%I {_}.
+Hint Mode Affine + ! : typeclass_instances.
+
+Class BiAffine (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
+Existing Instance absorbing_bi | 0.
+
+Class BiPositive (PROP : bi) :=
+  bi_positive (P Q : PROP) : bi_affinely (P ∗ Q) ⊢ bi_affinely P ∗ Q.
+
+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.
+
+Class Absorbing {PROP : bi} (P : PROP) := absorbing : bi_absorbingly P ⊢ P.
+Arguments Absorbing {_} _%I : simpl never.
+Arguments absorbing {_} _%I.
+
+Definition bi_plainly_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
+  (if p then bi_plainly P else P)%I.
+Arguments bi_plainly_if {_} !_ _%I /.
+Instance: Params (@bi_plainly_if) 2.
+Typeclasses Opaque bi_plainly_if.
+
+Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
+  (if p then bi_persistently P else P)%I.
+Arguments bi_persistently_if {_} !_ _%I /.
+Instance: Params (@bi_persistently_if) 2.
+Typeclasses Opaque bi_persistently_if.
+
+Definition bi_affinely_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
+  (if p then bi_affinely P else P)%I.
+Arguments bi_affinely_if {_} !_ _%I /.
+Instance: Params (@bi_affinely_if) 2.
+Typeclasses Opaque bi_affinely_if.
+Notation "â–¡? p P" := (bi_affinely_if p (bi_persistently_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" := (bi_affinely_if p (bi_plainly_if p P))%I
+  (at level 20, p at level 9, P at level 20,
+   right associativity, format "â– ? p  P") : bi_scope.
+
+Fixpoint bi_hexist {PROP : bi} {As} : himpl As PROP → PROP :=
+  match As return himpl As PROP → PROP with
+  | tnil => id
+  | tcons A As => λ Φ, ∃ x, bi_hexist (Φ x)
+  end%I.
+Fixpoint bi_hforall {PROP : bi} {As} : himpl As PROP → PROP :=
+  match As return himpl As PROP → PROP with
+  | tnil => id
+  | tcons A As => λ Φ, ∀ x, bi_hforall (Φ x)
+  end%I.
+
+Definition bi_laterN {PROP : sbi} (n : nat) (P : PROP) : PROP :=
+  Nat.iter n bi_later P.
+Arguments bi_laterN {_} !_%nat_scope _%I.
+Instance: Params (@bi_laterN) 2.
+Notation "â–·^ n P" := (bi_laterN n P)
+  (at level 20, n at level 9, P at level 20, format "â–·^ n  P") : bi_scope.
+Notation "â–·? p P" := (bi_laterN (Nat.b2n p) P)
+  (at level 20, p at level 9, P at level 20, format "â–·? p  P") : bi_scope.
+
+Definition bi_except_0 {PROP : sbi} (P : PROP) : PROP := (▷ False ∨ P)%I.
+Arguments bi_except_0 {_} _%I : simpl never.
+Notation "â—‡ P" := (bi_except_0 P) (at level 20, right associativity) : bi_scope.
+Instance: Params (@bi_except_0) 1.
+Typeclasses Opaque bi_except_0.
+
+Class Timeless {PROP : sbi} (P : PROP) := timeless : ▷ P ⊢ ◇ P.
+Arguments Timeless {_} _%I : simpl never.
+Arguments timeless {_} _%I {_}.
+Hint Mode Timeless + ! : typeclass_instances.
+Instance: Params (@Timeless) 1.
diff --git a/theories/bi/derived.v b/theories/bi/derived_laws.v
similarity index 95%
rename from theories/bi/derived.v
rename to theories/bi/derived_laws.v
index 33d351edc..6b64871b8 100644
--- a/theories/bi/derived.v
+++ b/theories/bi/derived_laws.v
@@ -1,115 +1,7 @@
-From iris.bi Require Export interface.
+From iris.bi Require Export derived_connectives.
 From iris.algebra Require Import monoid.
 From stdpp Require Import hlist.
 
-Definition bi_iff {PROP : bi} (P Q : PROP) : PROP := ((P → Q) ∧ (Q → P))%I.
-Arguments bi_iff {_} _%I _%I : simpl never.
-Instance: Params (@bi_iff) 1.
-Infix "↔" := bi_iff : bi_scope.
-
-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.
-
-Class Plain {PROP : bi} (P : PROP) := plain : P ⊢ bi_plainly P.
-Arguments Plain {_} _%I : simpl never.
-Arguments plain {_} _%I {_}.
-Hint Mode Plain + ! : typeclass_instances.
-Instance: Params (@Plain) 1.
-
-Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ bi_persistently P.
-Arguments Persistent {_} _%I : simpl never.
-Arguments persistent {_} _%I {_}.
-Hint Mode Persistent + ! : typeclass_instances.
-Instance: Params (@Persistent) 1.
-
-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 "â–¡ P" := (bi_affinely (bi_persistently P))%I
-  (at level 20, right associativity) : bi_scope.
-Notation "â–  P" := (bi_affinely (bi_plainly P))%I
-  (at level 20, right associativity) : bi_scope.
-
-Class Affine {PROP : bi} (Q : PROP) := affine : Q ⊢ emp.
-Arguments Affine {_} _%I : simpl never.
-Arguments affine {_} _%I {_}.
-Hint Mode Affine + ! : typeclass_instances.
-
-Class BiAffine (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
-Existing Instance absorbing_bi | 0.
-
-Class BiPositive (PROP : bi) :=
-  bi_positive (P Q : PROP) : bi_affinely (P ∗ Q) ⊢ bi_affinely P ∗ Q.
-
-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.
-
-Class Absorbing {PROP : bi} (P : PROP) := absorbing : bi_absorbingly P ⊢ P.
-Arguments Absorbing {_} _%I : simpl never.
-Arguments absorbing {_} _%I.
-
-Definition bi_plainly_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
-  (if p then bi_plainly P else P)%I.
-Arguments bi_plainly_if {_} !_ _%I /.
-Instance: Params (@bi_plainly_if) 2.
-Typeclasses Opaque bi_plainly_if.
-
-Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
-  (if p then bi_persistently P else P)%I.
-Arguments bi_persistently_if {_} !_ _%I /.
-Instance: Params (@bi_persistently_if) 2.
-Typeclasses Opaque bi_persistently_if.
-
-Definition bi_affinely_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
-  (if p then bi_affinely P else P)%I.
-Arguments bi_affinely_if {_} !_ _%I /.
-Instance: Params (@bi_affinely_if) 2.
-Typeclasses Opaque bi_affinely_if.
-Notation "â–¡? p P" := (bi_affinely_if p (bi_persistently_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" := (bi_affinely_if p (bi_plainly_if p P))%I
-  (at level 20, p at level 9, P at level 20,
-   right associativity, format "â– ? p  P") : bi_scope.
-
-Fixpoint bi_hexist {PROP : bi} {As} : himpl As PROP → PROP :=
-  match As return himpl As PROP → PROP with
-  | tnil => id
-  | tcons A As => λ Φ, ∃ x, bi_hexist (Φ x)
-  end%I.
-Fixpoint bi_hforall {PROP : bi} {As} : himpl As PROP → PROP :=
-  match As return himpl As PROP → PROP with
-  | tnil => id
-  | tcons A As => λ Φ, ∀ x, bi_hforall (Φ x)
-  end%I.
-
-Definition bi_laterN {PROP : sbi} (n : nat) (P : PROP) : PROP :=
-  Nat.iter n bi_later P.
-Arguments bi_laterN {_} !_%nat_scope _%I.
-Instance: Params (@bi_laterN) 2.
-Notation "â–·^ n P" := (bi_laterN n P)
-  (at level 20, n at level 9, P at level 20, format "â–·^ n  P") : bi_scope.
-Notation "â–·? p P" := (bi_laterN (Nat.b2n p) P)
-  (at level 20, p at level 9, P at level 20, format "â–·? p  P") : bi_scope.
-
-Definition bi_except_0 {PROP : sbi} (P : PROP) : PROP := (▷ False ∨ P)%I.
-Arguments bi_except_0 {_} _%I : simpl never.
-Notation "â—‡ P" := (bi_except_0 P) (at level 20, right associativity) : bi_scope.
-Instance: Params (@bi_except_0) 1.
-Typeclasses Opaque bi_except_0.
-
-Class Timeless {PROP : sbi} (P : PROP) := timeless : ▷ P ⊢ ◇ P.
-Arguments Timeless {_} _%I : simpl never.
-Arguments timeless {_} _%I {_}.
-Hint Mode Timeless + ! : typeclass_instances.
-Instance: Params (@Timeless) 1.
-
 Module bi.
 Import interface.bi.
 Section bi_derived.
-- 
GitLab