Internal fractional tweaks.

- 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

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

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

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;