From 448ece34cf724d2501cc30b9e688165edb3d258d Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sun, 18 Jul 2021 15:57:28 +0200
Subject: [PATCH] persistent_fractional: strengthen like bi.persistent_sep_dup

In 13c5c1adf9f69a94849d89bf26d56f45290f0f25 I strengthened bi.persistent_sep_dup
to support propositions that are persistent and either affine or absorbing; do
the same for `persistent_fractional`.
---
 CHANGELOG.md             | 2 ++
 iris/bi/lib/fractional.v | 4 ++--
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index df598d462..8c93d365e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -77,6 +77,8 @@ Coq 8.11 is no longer supported in this version of Iris.
 * 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`.
+* Strengthen `persistent_fractional` to support propositions that are persistent
+  and either affine or absorbing (by Paolo G. Giarrusso, BedRock Systems).
 
 **Changes in `base_logic`:**
 
diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index e7c88ae53..5c33516a9 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -65,8 +65,8 @@ Section fractional.
   Proof. intros. apply bi.wand_intro_r. by rewrite -(fractional_half P). Qed.
 
   (** Fractional and logical connectives *)
-  Global Instance persistent_fractional P :
-    Persistent P → Absorbing P → Fractional (λ _, P).
+  Global Instance persistent_fractional (P : PROP) :
+    Persistent P → TCOr (Affine P) (Absorbing P) → Fractional (λ _, P).
   Proof. intros ?? q q'. apply: bi.persistent_sep_dup. Qed.
 
   Global Instance fractional_sep Φ Ψ :
-- 
GitLab