From 4df29af74ea6164e54e6e21dcc2d9600b87d47b5 Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Mon, 21 Nov 2022 14:49:33 +0100
Subject: [PATCH] Add Fractional and AsFractional instance for embed

---
 CHANGELOG.md              | 2 ++
 iris/bi/lib/fractional.v  | 8 ++++++++
 tests/proofmode_monpred.v | 9 ++++++++-
 3 files changed, 18 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 54670738d..50b92c502 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -103,6 +103,8 @@ and Tej Chajed. Thanks a lot to everyone involved!
 * Rename `laterN_plus` into `laterN_add`.
 * Remove `make_laterable` from atomic updates. This relies on Iris now having
   support for later credits (see below).
+* Add `Fractional` and `AsFractional` instances for `embed` such that the
+  embedding of something fractional is also fractional. (by Simon Friis Vindum).
 
 **Changes in `proofmode`:**
 
diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index 2303c1c31..05917ee57 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -87,6 +87,14 @@ Section fractional.
     rewrite !assoc. f_equiv. by rewrite comm.
   Qed.
 
+  Global Instance fractional_embed `{!BiEmbed PROP PROP'} Φ :
+    Fractional Φ → Fractional (λ q, ⎡ Φ q ⎤ : PROP')%I.
+  Proof. intros ???. by rewrite fractional embed_sep. Qed.
+
+  Global Instance as_fractional_embed `{!BiEmbed PROP PROP'} P Φ q :
+    AsFractional P Φ q → AsFractional (⎡ P ⎤) (λ q, ⎡ Φ q ⎤)%I q.
+  Proof. split; [by rewrite ->!as_fractional | apply _]. Qed.
+
   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.
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 638add08e..d7d70dce9 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -1,5 +1,6 @@
+From iris.bi.lib Require Import fractional.
 From iris.proofmode Require Import tactics monpred.
-From iris.base_logic.lib Require Import invariants.
+From iris.base_logic.lib Require Import invariants ghost_var.
 From iris.prelude Require Import options.
 
 Unset Mangle Names.
@@ -183,6 +184,7 @@ Section tests_iprop.
   Context {I : biIndex} `{!invGS_gen hlc Σ}.
 
   Local Notation monPred := (monPred I (iPropI Σ)).
+  Local Notation monPredI := (monPredI I (iPropI Σ)).
   Implicit Types P Q R : monPred.
   Implicit Types 𝓟 𝓠 𝓡 : iProp Σ.
 
@@ -210,4 +212,9 @@ Section tests_iprop.
     iPoseProof (own_update with "Hγ") as "H"; first done.
     by iMod "H".
   Qed.
+
+  Lemma test_embed_fractional `{!ghost_varG Σ A} γ q (a : A) :
+    ⎡ghost_var γ q a⎤ ⊢@{monPredI} ⎡ghost_var γ (q/2) a⎤ ∗ ⎡ghost_var γ (q/2) a⎤.
+  Proof. iIntros "[$ $]". Qed.
+
 End tests_iprop.
-- 
GitLab