From 1650c2a048c0e0ee8338c9cffa45e93487978bfb Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 11 Dec 2017 17:10:28 +0100
Subject: [PATCH] Move FUpd and BUpd classes to bi/interface.v

---
 theories/base_logic/lib/fancy_updates.v | 21 ----------------
 theories/base_logic/upred.v             |  9 -------
 theories/bi/interface.v                 | 33 +++++++++++++++++++++++++
 3 files changed, 33 insertions(+), 30 deletions(-)

diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 9037e518f..7960c20a4 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -7,33 +7,12 @@ Set Default Proof Using "Type".
 Export invG.
 Import uPred.
 
-Class FUpd (A : Type) : Type := fupd : coPset → coPset → A → A.
-Instance: Params (@fupd) 4.
-
 Definition uPred_fupd_def `{invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
   (wsat ∗ ownE E1 ==∗ ◇ (wsat ∗ ownE E2 ∗ P))%I.
 Definition uPred_fupd_aux `{invG Σ} : seal uPred_fupd_def. by eexists. Qed.
 Instance uPred_fupd `{invG Σ} : FUpd (iProp Σ):= unseal uPred_fupd_aux.
 Definition uPred_fupd_eq `{invG Σ} : fupd = uPred_fupd_def := seal_eq uPred_fupd_aux.
 
-Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
-  (at level 99, E1, E2 at level 50, Q at level 200,
-   format "|={ E1 , E2 }=>  Q") : bi_scope.
-Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)%I
-  (at level 99, E1,E2 at level 50, Q at level 200,
-   format "P  ={ E1 , E2 }=∗  Q") : bi_scope.
-Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)
-  (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
-
-Notation "|={ E }=> Q" := (fupd E E Q)
-  (at level 99, E at level 50, Q at level 200,
-   format "|={ E }=>  Q") : bi_scope.
-Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)%I
-  (at level 99, E at level 50, Q at level 200,
-   format "P  ={ E }=∗  Q") : bi_scope.
-Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)
-  (at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope.
-
 Section fupd.
 Context `{invG Σ}.
 Implicit Types P Q : iProp Σ.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 195a6040b..4f016b1ec 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -317,9 +317,6 @@ Definition uPred_cmra_valid {M A} := unseal uPred_cmra_valid_aux M A.
 Definition uPred_cmra_valid_eq :
   @uPred_cmra_valid = @uPred_cmra_valid_def := seal_eq uPred_cmra_valid_aux.
 
-Class BUpd (A : Type) : Type := bupd : A → A.
-Instance : Params (@bupd) 2.
-
 Program Definition uPred_bupd_def {M} (Q : uPred M) : uPred M :=
   {| uPred_holds n x := ∀ k yf,
       k ≤ n → ✓{k} (x ⋅ yf) → ∃ x', ✓{k} (x' ⋅ yf) ∧ Q k x' |}.
@@ -570,12 +567,6 @@ Coercion uPred_valid {M} : uPred M → Prop := bi_valid.
 
 (* Latest notation *)
 Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : bi_scope.
-Notation "|==> Q" := (bupd Q)
-  (at level 99, Q at level 200, format "|==>  Q") : bi_scope.
-Notation "P ==∗ Q" := (P ⊢ |==> Q)
-  (at level 99, Q at level 200, only parsing) : stdpp_scope.
-Notation "P ==∗ Q" := (P -∗ |==> Q)%I
-  (at level 99, Q at level 200, format "P  ==∗  Q") : bi_scope.
 
 Module uPred.
 Include uPred_unseal.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index b47515630..c14f5d56d 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -1,3 +1,4 @@
+From stdpp Require Import coPset.
 From iris.algebra Require Export ofe.
 Set Primitive Projections.
 
@@ -522,4 +523,36 @@ Proof. eapply (sbi_mixin_later_persistently_2 bi_entails), sbi_sbi_mixin. Qed.
 Lemma later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P).
 Proof. eapply sbi_mixin_later_false_em, sbi_sbi_mixin. Qed.
 End sbi_laws.
+
 End bi.
+
+Class BUpd (A : Type) : Type := bupd : A → A.
+Instance : Params (@bupd) 2.
+
+Notation "|==> Q" := (bupd Q)
+  (at level 99, Q at level 200, format "|==>  Q") : bi_scope.
+Notation "P ==∗ Q" := (P ⊢ |==> Q)
+  (at level 99, Q at level 200, only parsing) : stdpp_scope.
+Notation "P ==∗ Q" := (P -∗ |==> Q)%I
+  (at level 99, Q at level 200, format "P  ==∗  Q") : bi_scope.
+
+Class FUpd (A : Type) : Type := fupd : coPset → coPset → A → A.
+Instance: Params (@fupd) 4.
+
+Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
+  (at level 99, E1, E2 at level 50, Q at level 200,
+   format "|={ E1 , E2 }=>  Q") : bi_scope.
+Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)%I
+  (at level 99, E1,E2 at level 50, Q at level 200,
+   format "P  ={ E1 , E2 }=∗  Q") : bi_scope.
+Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)
+  (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
+
+Notation "|={ E }=> Q" := (fupd E E Q)
+  (at level 99, E at level 50, Q at level 200,
+   format "|={ E }=>  Q") : bi_scope.
+Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)%I
+  (at level 99, E at level 50, Q at level 200,
+   format "P  ={ E }=∗  Q") : bi_scope.
+Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)
+  (at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope.
-- 
GitLab