From 7991ed5495098f09e5b9526f88f7e38ac452cbd3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 8 Jun 2023 21:03:18 +0200
Subject: [PATCH] make fractional_split truly forwards lemmas

---
 iris/bi/lib/fractional.v | 23 +++++++++++++----------
 1 file changed, 13 insertions(+), 10 deletions(-)

diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index e297ea398..5c2f306cd 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -66,17 +66,20 @@ Section fractional.
     Fractional Φ → AsFractional (Φ q) Φ q.
   Proof. done. Qed.
 
-  Lemma fractional_split P P1 P2 Φ q1 q2 :
-    AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
-    P ⊣⊢ P1 ∗ P2.
-  Proof. by move=>-[-> ->] [-> _] [-> _]. Qed.
-  Lemma fractional_split_1 P P1 P2 Φ q1 q2 :
-    AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
-    P -∗ P1 ∗ P2.
+  (** These lemmas are meant to be used when [P] is known but the split-up
+      pieces ([Φ], [q1], [q2]) are not.
+      See [fractional_merge] below for the dual situation. *)
+  Lemma fractional_split P Φ q1 q2 :
+    AsFractional P Φ (q1 + q2) →
+    P ⊣⊢ Φ q1 ∗ Φ q2.
+  Proof. by move=>-[-> ->]. Qed.
+  Lemma fractional_split_1 P Φ q1 q2 :
+    AsFractional P Φ (q1 + q2) →
+    P -∗ Φ q1 ∗ Φ q2.
   Proof. intros. apply bi.entails_wand. by rewrite -(fractional_split P). Qed.
-  Lemma fractional_split_2 P P1 P2 Φ q1 q2 :
-    AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
-    P1 -∗ P2 -∗ P.
+  Lemma fractional_split_2 P Φ q1 q2 :
+    AsFractional P Φ (q1 + q2) →
+    Φ q1 -∗ Φ q2 -∗ P.
   Proof. intros. apply bi.entails_wand, bi.wand_intro_r. by rewrite -(fractional_split P). Qed.
 
   Lemma fractional_merge P1 P2 Φ q1 q2 `{!Fractional Φ} :
-- 
GitLab