Merge branch 'fractional-embed' into 'master'

Add Fractional and AsFractional instance for embed

See merge request iris/iris!868

CHANGELOG.md

@@ -134,6 +134,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`:**
 

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.

tests/proofmode_monpred.v

+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.