From 5a95398c8e79ca1a8bbbc76fe8fa8e2bc0fdcd4e Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 6 Dec 2016 00:01:12 +0100
Subject: [PATCH] Fractional instances for persistent and bigop.

---
 base_logic/lib/fractional.v | 47 +++++++++++++++++++++++++++++++++++--
 1 file changed, 45 insertions(+), 2 deletions(-)

diff --git a/base_logic/lib/fractional.v b/base_logic/lib/fractional.v
index a2247bf43..d00d1af1a 100644
--- a/base_logic/lib/fractional.v
+++ b/base_logic/lib/fractional.v
@@ -1,4 +1,6 @@
+From iris.prelude Require Import gmap gmultiset.
 From iris.base_logic Require Export derived.
+From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import classes class_instances.
 
 Class Fractional {M} (Φ : Qp → uPred M) :=
@@ -17,10 +19,10 @@ Section fractional.
   Implicit Types Φ : Qp → uPred M.
   Implicit Types p q : Qp.
 
-  Lemma fractional_sep `{Fractional _ Φ} p q :
+  Lemma fractional_split `{Fractional _ Φ} p q :
     Φ (p + q)%Qp ⊢ Φ p ∗ Φ q.
   Proof. by rewrite fractional. Qed.
-  Lemma sep_fractional `{Fractional _ Φ} p q :
+  Lemma fractional_combine `{Fractional _ Φ} p q :
     Φ p ∗ Φ q ⊢ Φ (p + q)%Qp.
   Proof. by rewrite fractional. Qed.
   Lemma fractional_half_equiv `{Fractional _ Φ} p :
@@ -33,6 +35,47 @@ Section fractional.
     Φ (p/2)%Qp ∗ Φ (p/2)%Qp ⊢ Φ p.
   Proof. by rewrite -fractional_half_equiv. Qed.
 
+  (** Fractional and logical connectives *)
+
+  Global Instance persistent_fractional P :
+    PersistentP P → Fractional (λ _, P).
+  Proof. intros HP q q'. by apply uPred_derived.always_sep_dup. Qed.
+
+  Global Instance fractional_sep Φ Ψ :
+    Fractional Φ → Fractional Ψ → Fractional (λ q, Φ q ∗ Ψ q)%I.
+  Proof.
+    intros ?? q q'. rewrite !fractional -!assoc. f_equiv.
+    rewrite !assoc. f_equiv; last done. by rewrite comm.
+  Qed.
+
+  Global Instance fractional_big_sepL {A} l Ψ :
+    (∀ k (x : A), Fractional (Ψ k x)) →
+    Fractional (M:=M) (λ q, [∗ list] k↦x ∈ l, Ψ k x q)%I.
+  Proof.
+    intros ? q q'. rewrite -big_sepL_sepL. by setoid_rewrite fractional.
+  Qed.
+
+  Global Instance fractional_big_sepM `{Countable K} {A} (m : gmap K A) Ψ :
+    (∀ k (x : A), Fractional (Ψ k x)) →
+    Fractional (M:=M) (λ q, [∗ map] k↦x ∈ m, Ψ k x q)%I.
+  Proof.
+    intros ? q q'. rewrite -big_sepM_sepM. by setoid_rewrite fractional.
+  Qed.
+
+  Global Instance fractional_big_sepS `{Countable A} (X : gset A) Ψ :
+    (∀ x, Fractional (Ψ x)) →
+    Fractional (M:=M) (λ q, [∗ set] x ∈ X, Ψ x q)%I.
+  Proof.
+    intros ? q q'. rewrite -big_sepS_sepS. by setoid_rewrite fractional.
+  Qed.
+
+  Global Instance fractional_big_sepMS `{Countable A} (X : gmultiset A) Ψ :
+    (∀ x, Fractional (Ψ x)) →
+    Fractional (M:=M) (λ q, [∗ mset] x ∈ X, Ψ x q)%I.
+  Proof.
+    intros ? q q'. rewrite -big_sepMS_sepMS. by setoid_rewrite fractional.
+  Qed.
+
   (** Mult instances *)
 
   Global Instance mult_fractional_l Φ Ψ p :
-- 
GitLab