diff --git a/CHANGELOG.md b/CHANGELOG.md index df598d46245d05a7a68b13e0221fe6f3d97c12b5..019bda96a1435f90b31dd10e848b2649af7e6cfb 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 e7c88ae538f23d89312a2cfef9200173211a8893..5c33516a98db11e4b8d90888688e5fe7a953460e 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 Φ Ψ :