From 269dbd25c894c781b267eea53673ed2a5fdf94e4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 28 Apr 2023 16:04:28 +0200
Subject: [PATCH] And group more `monpred` BI instances.

---
 iris/bi/monpred.v | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index 5421efc91..f6a80ead4 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -553,6 +553,13 @@ Section instances.
     @monPred_defs.monPred_in_unseal).
   Ltac unseal := rewrite !monPred_unseal /=.
 
+  Global Instance monPred_bi_löb : BiLöb PROP → BiLöb monPredI.
+  Proof. rewrite {2}/BiLöb; unseal=> ? P HP; split=> i /=. apply löb_weak, HP. Qed.
+  Global Instance monPred_bi_positive : BiPositive PROP → BiPositive monPredI.
+  Proof. split => ?. rewrite /bi_affinely. unseal. apply bi_positive. Qed.
+  Global Instance monPred_bi_affine : BiAffine PROP → BiAffine monPredI.
+  Proof. split => ?. unseal. by apply affine. Qed.
+
   Global Instance monPred_bi_persistently_forall :
     BiPersistentlyForall PROP → BiPersistentlyForall monPredI.
   Proof. intros ? A φ. split=> /= i. unseal. by apply persistently_forall_2. Qed.
@@ -731,13 +738,6 @@ Section bi_facts.
   Global Instance monPred_in_flip_mono : Proper ((⊑) ==> flip (⊢)) (@monPred_in I PROP).
   Proof. solve_proper. Qed.
 
-  Global Instance monPred_bi_löb : BiLöb PROP → BiLöb monPredI.
-  Proof. rewrite {2}/BiLöb; unseal=> ? P HP; split=> i /=. apply löb_weak, HP. Qed.
-  Global Instance monPred_bi_positive : BiPositive PROP → BiPositive monPredI.
-  Proof. split => ?. rewrite /bi_affinely. unseal. apply bi_positive. Qed.
-  Global Instance monPred_bi_affine : BiAffine PROP → BiAffine monPredI.
-  Proof. split => ?. unseal. by apply affine. Qed.
-
   Lemma monPred_persistent P : (∀ i, Persistent (P i)) → Persistent P.
   Proof. intros HP. constructor=> i. unseal. apply HP. Qed.
   Lemma monPred_absorbing P : (∀ i, Absorbing (P i)) → Absorbing P.
-- 
GitLab