diff --git a/CHANGELOG.md b/CHANGELOG.md index a1dd5effebfba19d070a9803f1297c648208fe1c..e5f92b825ee0812e2ee988bf159c47bfb8c5dfed 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -74,6 +74,7 @@ Coq 8.11 is no longer supported in this version of Iris. only printed, not parsed): added a `,` before `ABORT`, for consistency with `COMM`. * Add the lemmas `big_sepM_impl_strong` and `big_sepM_impl_dom_subseteq` that generalize the existing `big_sepM_impl` lemma. (by Simon Friis Vindum) +* Add new instance `fractional_big_sepL2`. (by Paolo G. Giarrusso, BedRock Systems) **Changes in `proofmode`:** diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v index ac13b5f7966f79de2b6495d15dc1a7259fd7b701..c310657d84a9d4c4266d2286e8f70b09257d1a2d 100644 --- a/iris/bi/lib/fractional.v +++ b/iris/bi/lib/fractional.v @@ -77,13 +77,18 @@ Section fractional. rewrite !assoc. f_equiv. by rewrite comm. Qed. - Global Instance fractional_big_sepL {A} l Ψ : - (∀ k (x : A), Fractional (Ψ k x)) → + Global Instance fractional_big_sepL {A} (l : list A) Ψ : + (∀ k x, Fractional (Ψ k x)) → Fractional (PROP:=PROP) (λ q, [∗ list] k↦x ∈ l, Ψ k x q)%I. Proof. intros ? q q'. rewrite -big_sepL_sep. by setoid_rewrite fractional. Qed. + Global Instance fractional_big_sepL2 {A B} (l1 : list A) (l2 : list B) Ψ : + (∀ k x1 x2, Fractional (Ψ k x1 x2)) → + Fractional (PROP:=PROP) (λ q, [∗ list] k↦x1; x2 ∈ l1; l2, Ψ k x1 x2 q)%I. + Proof. intros ? q q'. rewrite -big_sepL2_sep. by setoid_rewrite fractional. Qed. + Global Instance fractional_big_sepM `{Countable K} {A} (m : gmap K A) Ψ : - (∀ k (x : A), Fractional (Ψ k x)) → + (∀ k x, Fractional (Ψ k x)) → Fractional (PROP:=PROP) (λ q, [∗ map] k↦x ∈ m, Ψ k x q)%I. Proof. intros ? q q'. rewrite -big_sepM_sep. by setoid_rewrite fractional. Qed.