From e72da74cc1b9c442f0873df0b90481d58b9abd68 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 28 Sep 2020 09:07:44 +0200
Subject: [PATCH] apply review and fix and improve proof

---
 theories/base_logic/lib/ghost_var.v | 8 +++++---
 theories/bi/lib/fractional.v        | 5 +++++
 2 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/theories/base_logic/lib/ghost_var.v b/theories/base_logic/lib/ghost_var.v
index 32b9d2af6..b4f6bc80e 100644
--- a/theories/base_logic/lib/ghost_var.v
+++ b/theories/base_logic/lib/ghost_var.v
@@ -73,14 +73,16 @@ Section lemmas.
     (q1 + q2 = 1)%Qp →
     ghost_var γ q1 a1 -∗ ghost_var γ q2 a2 ==∗ ghost_var γ q1 b ∗ ghost_var γ q2 b.
   Proof.
-    iIntros (Hq) "[H1 H2]".
+    iIntros (Hq) "H1 H2".
     iDestruct (ghost_var_valid_2 with "H1 H2") as %[_ ->].
-    iCombine "H1 H2" as "H". rewrite -frac_agree_op Hq.
+    iDestruct (fractional_merge with "H1 H2") as "H". simpl. rewrite Hq.
     iMod (ghost_var_update with "H") as "H".
     rewrite -Hq. iApply ghost_var_split. done.
   Qed.
   Lemma ghost_var_update_halves b γ a1 a2 :
-    ghost_var γ (1/2) a1 -∗ ghost_var γ (1/2) a2 ==∗ ghost_var γ (1/2) b ∗ ghost_var γ (1/2) b.
+    ghost_var γ (1/2) a1 -∗
+    ghost_var γ (1/2) a2 ==∗
+    ghost_var γ (1/2) b ∗ ghost_var γ (1/2) b.
   Proof. iApply ghost_var_update_2. apply Qp_half_half. Qed.
 
 End lemmas.
diff --git a/theories/bi/lib/fractional.v b/theories/bi/lib/fractional.v
index 1721e6840..f5e18141b 100644
--- a/theories/bi/lib/fractional.v
+++ b/theories/bi/lib/fractional.v
@@ -38,6 +38,11 @@ Section fractional.
     P1 -∗ P2 -∗ P.
   Proof. intros. apply bi.wand_intro_r. by rewrite -(fractional_split P). Qed.
 
+  Lemma fractional_merge P1 P2 Φ q1 q2 `{!Fractional Φ} :
+    AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
+    P1 -∗ P2 -∗ Φ (q1 + q2)%Qp.
+  Proof. move=>-[-> _] [-> _]. rewrite fractional. apply bi.wand_intro_r. done. Qed.
+
   Lemma fractional_half P P12 Φ q :
     AsFractional P Φ q → AsFractional P12 Φ (q/2) →
     P ⊣⊢ P12 ∗ P12.
-- 
GitLab