split derived_laws into BI and SBI laws

_CoqProject

@@ -27,7 +27,8 @@ theories/algebra/deprecated.v
 theories/algebra/proofmode_classes.v
 theories/bi/interface.v
 theories/bi/derived_connectives.v
-theories/bi/derived_laws.v
+theories/bi/derived_laws_bi.v
+theories/bi/derived_laws_sbi.v
 theories/bi/plainly.v
 theories/bi/big_op.v
 theories/bi/updates.v

theories/base_logic/derived.v

 From iris.base_logic Require Export upred.
-From iris.bi Require Export derived_laws.
+From iris.bi Require Export bi.
 Set Default Proof Using "Type".
-Import upred.uPred.
-Import interface.bi derived_laws.bi.
+Import upred.uPred bi.
 
 Module uPred.
 Section derived.

theories/base_logic/lib/boxes.v

@@ -100,8 +100,7 @@ Qed.
 
 Lemma box_alloc : box N ∅ True%I.
 Proof.
-  iIntros; iExists (λ _, True)%I; iSplit; last by auto.
-  iNext. by rewrite big_opM_empty.
+  iIntros. iExists (λ _, True)%I. iSplit; by auto.
 Qed.
 
 Lemma slice_insert_empty E q f Q P :

theories/bi/bi.v

-From iris.bi Require Export derived_laws big_op updates plainly embedding.
+From iris.bi Require Export derived_laws_bi derived_laws_sbi
+     big_op updates plainly embedding.
 Set Default Proof Using "Type".
 
 Module Import bi.
   Export bi.interface.bi.
-  Export bi.derived_laws.bi.
+  Export bi.derived_laws_bi.bi.
+  Export bi.derived_laws_sbi.bi.
   Export bi.big_op.bi.
 End bi.
 

theories/bi/big_op.v

 From iris.algebra Require Export big_op.
-From iris.bi Require Export derived_laws.
-From iris.bi Require Import plainly.
+From iris.bi Require Import derived_laws_sbi plainly.
 From stdpp Require Import countable fin_collections functions.
 Set Default Proof Using "Type".
 
@@ -42,7 +41,7 @@ Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P) X)
 
 (** * Properties *)
 Module bi.
-Import interface.bi derived_laws.bi.
+Import interface.bi derived_laws_bi.bi.
 Section bi_big_op.
 Context {PROP : bi}.
 Implicit Types Ps Qs : list PROP.

theories/bi/embedding.v

 From iris.algebra Require Import monoid.
-From iris.bi Require Import interface derived_laws big_op plainly updates.
+From iris.bi Require Import interface derived_laws_sbi big_op plainly updates.
 From stdpp Require Import hlist.
 
 Class Embed (A B : Type) := embed : A → B.

theories/bi/plainly.v

-From iris.bi Require Import derived_laws.
+From iris.bi Require Import derived_laws_sbi.
 From iris.algebra Require Import monoid.
-Import interface.bi derived_laws.bi.
+Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
 
 Class Plainly (A : Type) := plainly : A → A.
 Hint Mode Plainly ! : typeclass_instances.

theories/bi/updates.v

 From stdpp Require Import coPset.
-From iris.bi Require Import interface derived_laws big_op plainly.
+From iris.bi Require Import interface derived_laws_sbi big_op plainly.
 
 (* We first define operational type classes for the notations, and then later
 bundle these operational type classes with the laws. *)

theories/proofmode/class_instances.v

@@ -1089,7 +1089,7 @@ Proof.
 Qed.
 
 (* We add a useless hypothesis [BiEmbed PROP PROP'] in order to make
-   sure this iinstance is not used when there is no embedding between
+   sure this instance is not used when there is no embedding between
    PROP and PROP'.
    The first [`{BiEmbed PROP PROP'}] is not considered as a premise by
    Coq TC search mechanism because the rest of the hypothesis is dependent

theories/proofmode/tactics.v

 From iris.proofmode Require Import coq_tactics.
 From iris.proofmode Require Import base intro_patterns spec_patterns sel_patterns.
-From iris.bi Require Export bi big_op.
+From iris.bi Require Export bi.
 From stdpp Require Import namespaces.
 From iris.proofmode Require Export classes notation.
 From iris.proofmode Require Import class_instances.