From 12e75edb7491767dada24e432b8514ab4e063a5d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 28 Aug 2023 13:15:32 +0200
Subject: [PATCH] Internal fractional tweaks.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- Add `Params` instance and `Proper` instances
- Use `tc_opaque` to prevent `iFrame`/`iNext` from unfolding
- Use `∗-∗` in `iff` lemma to remove `BiAffine`.
---
 iris/bi/lib/fractional.v          | 30 ++++++++++++++++++++++--------
 iris_heap_lang/lib/rw_lock.v      |  3 +--
 iris_heap_lang/lib/rw_spin_lock.v |  4 ++--
 3 files changed, 25 insertions(+), 12 deletions(-)

diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index 0f8973217..c8add9a28 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -197,26 +197,40 @@ Section fractional.
   Qed.
 End fractional.
 
+(** Marked [tc_opaque] instead [Typeclasses Opaque] so that you can use
+[iDestruct] to eliminate and [iModIntro] to introduce [internal_fractional],
+while still preventing [iFrame] and [iNext] from unfolding. *)
+Definition internal_fractional {PROP : bi} (Φ : Qp → PROP) : PROP :=
+  tc_opaque (□ ∀ p q, Φ (p + q)%Qp ∗-∗ Φ p ∗ Φ q)%I.
+Global Instance: Params (@internal_fractional) 1 := {}.
+
 Section internal_fractional.
   Context {PROP : bi}.
   Implicit Types Φ Ψ : Qp → PROP.
   Implicit Types q : Qp.
 
-  Definition internal_fractional Φ
-    := (□ (∀ p q, Φ (p + q)%Qp ∗-∗ Φ p ∗ Φ q))%I.
+  Global Instance internal_fractional_ne n :
+    Proper (pointwise_relation _ (dist n) ==> dist n) (@internal_fractional PROP).
+  Proof. solve_proper. Qed.
+  Global Instance internal_fractional_proper :
+    Proper (pointwise_relation _ (≡) ==> (≡)) (@internal_fractional PROP).
+  Proof. solve_proper. Qed.
+
+  Global Instance internal_fractional_affine Φ : Affine (internal_fractional Φ).
+  Proof. rewrite /internal_fractional /=. apply _. Qed.
   Global Instance internal_fractional_persistent Φ :
-    Persistent (internal_fractional Φ) := _.
+    Persistent (internal_fractional Φ).
+  Proof. rewrite /internal_fractional /=. apply _. Qed.
 
   Lemma fractional_internal_fractional Φ :
     Fractional Φ → ⊢ internal_fractional Φ.
   Proof.
-    intros frac.
-    iIntros "!>" (q1 q2).
-    rewrite [Φ (q1 + q2)%Qp]frac //=;  auto.
+    intros. iIntros "!>" (q1 q2).
+    rewrite [Φ (q1 + q2)%Qp]fractional //=; auto.
   Qed.
 
-  Lemma internal_fractional_iff `{!BiAffine PROP} Φ Ψ:
-    □ (∀ q, Φ q ↔ Ψ q) ⊢ internal_fractional Φ -∗ internal_fractional Ψ.
+  Lemma internal_fractional_iff Φ Ψ:
+    □ (∀ q, Φ q ∗-∗ Ψ q) ⊢ internal_fractional Φ -∗ internal_fractional Ψ.
   Proof.
     iIntros "#Hiff #HΦdup !>" (p q).
     iSplit.
diff --git a/iris_heap_lang/lib/rw_lock.v b/iris_heap_lang/lib/rw_lock.v
index 9e2196eac..2350e14a6 100644
--- a/iris_heap_lang/lib/rw_lock.v
+++ b/iris_heap_lang/lib/rw_lock.v
@@ -35,7 +35,7 @@ Class rwlock `{!heapGS_gen hlc Σ} := RwLock {
   (** * General properties of the predicates *)
   is_rw_lock_persistent γ lk Φ :> Persistent (is_rw_lock γ lk Φ);
   is_rw_lock_iff γ lk Φ Ψ :
-    is_rw_lock γ lk Φ -∗ ▷ □ (∀ q,  Φ q ↔ Ψ q) -∗ is_rw_lock γ lk Ψ;
+    is_rw_lock γ lk Φ -∗ ▷ □ (∀ q,  Φ q ∗-∗ Ψ q) -∗ is_rw_lock γ lk Ψ;
   reader_locked_timeless γ q :> Timeless (reader_locked γ q);
   writer_locked_timeless γ :> Timeless (writer_locked γ);
   writer_locked_exclusive γ : writer_locked γ -∗ writer_locked γ -∗ False;
@@ -63,4 +63,3 @@ Class rwlock `{!heapGS_gen hlc Σ} := RwLock {
     {{{ RET #(); True }}};
 }.
 Global Hint Mode rwlock + + + : typeclass_instances.
-
diff --git a/iris_heap_lang/lib/rw_spin_lock.v b/iris_heap_lang/lib/rw_spin_lock.v
index 5e984bbc3..f15555acb 100644
--- a/iris_heap_lang/lib/rw_spin_lock.v
+++ b/iris_heap_lang/lib/rw_spin_lock.v
@@ -96,7 +96,7 @@ Section proof.
   Qed.
 
   Lemma is_rw_lock_iff γ lk Φ Ψ :
-    is_rw_lock γ lk Φ -∗ ▷ □ (∀ q, Φ q ↔ Ψ q) -∗ is_rw_lock γ lk Ψ.
+    is_rw_lock γ lk Φ -∗ ▷ □ (∀ q, Φ q ∗-∗ Ψ q) -∗ is_rw_lock γ lk Ψ.
   Proof.
     iIntros "[#HΦdup [%l [-> #Hlockinv]]] #Hiff".
     unfold is_rw_lock.
@@ -393,7 +393,7 @@ Section proof.
   Qed.
 End proof.
 
-Program Definition rw_spin_lock `{!heapGS_gen hlc Σ, !rwlockG Σ} : rwlock :=
+Definition rw_spin_lock `{!heapGS_gen hlc Σ, !rwlockG Σ} : rwlock :=
   {| rw_lock.writer_locked_exclusive := writer_locked_exclusive;
      rw_lock.writer_locked_not_reader_locked := writer_locked_not_reader_locked;
      rw_lock.is_rw_lock_iff := is_rw_lock_iff;
-- 
GitLab