From 830e81489a37d3caee259cd306364c673808e04b Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Fri, 1 Oct 2021 20:25:35 +0200
Subject: [PATCH] Prove missing fractional_big_sepL2

---
 CHANGELOG.md             | 1 +
 iris/bi/lib/fractional.v | 5 +++++
 2 files changed, 6 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a1dd5effe..e5f92b825 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 ac13b5f79..997910f90 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -82,6 +82,11 @@ Section fractional.
     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)) →
     Fractional (PROP:=PROP) (λ q, [∗ map] k↦x ∈ m, Ψ k x q)%I.
-- 
GitLab