feat: InternalFractional and rw lock examples

Iris/Iris/Algebra/Frac.lean

@@ -59,6 +59,12 @@ def Qp.div (x y : Qp) : Qp := ⟨x.val / y.val, Rat.div_pos x.2 y.2⟩
 instance instHDivQpQpQp : HDiv Qp Qp Qp where
   hDiv := Qp.div
 
+/-- The fraction `1/4`. -/
+def Qp.quarter : Qp := ⟨1 / 4, by grind⟩
+
+/-- The fraction `3/4`. -/
+def Qp.threeQuarters : Qp := ⟨3 / 4, by grind⟩
+
 def Qp.divide_even (q : Qp) (n : Nat) (hn : 0 < n) : Qp :=
   ⟨q.val / n, Rat.div_pos q.2 (by exact_mod_cast hn)⟩
 
@@ -86,14 +92,15 @@ instance instCMRAQp : CMRA Qp where
   extend {_ x y z} := by
     rintro H He; exact ⟨y, z, He, .rfl, .rfl⟩
 
-
 -- TODO: A different solution to having these bridge lemmas might be to internalize
 -- positivity into the CMRA's validity predicate, removing the sybtype, and having Qp
 -- become just a Leibniz CMRA over Rat. This admits two-way coercions to Rat for the automation.
 
 @[simp, grind =] theorem Qp.val_add (x y : Qp) : (x + y).val = x.val + y.val := rfl
 @[simp, grind =] theorem Qp.val_one : (1 : Qp).val = 1 := rfl
 @[simp, grind =] theorem Qp.val_half (q : Qp) : q.half.val = q.val / 2 := rfl
+@[simp, grind =] theorem Qp.val_quarter : Qp.quarter.val = 1 / 4 := rfl
+@[simp, grind =] theorem Qp.val_threeQuarters : Qp.threeQuarters.val = 3 / 4 := rfl
 @[simp, grind =] theorem Qp.val_div (x y : Qp) : (x / y).val = x.val / y.val := rfl
 @[simp, grind =] theorem Qp.val_divide_even (q : Qp) (n : Nat) (hn : 0 < n) :
     (q.divide_even n hn).val = q.val / n := rfl
@@ -106,6 +113,9 @@ instance instCMRAQp : CMRA Qp where
 @[simp] theorem Qp.dist_iff {n} {x y : Qp} : x ≡{n}≡ y ↔ x.val = y.val := Subtype.ext_iff
 @[simp, rocq_alias frac_valid_1] theorem Qp.valid_one : ✓ (1 : Qp) := by grind
 @[simp, grind =] theorem Qp.half_add_half (q : Qp) : q.half + q.half = q := Subtype.ext (by grind)
+@[grind =] theorem Qp.add_left_comm (x y z : Qp) : x + (y + z) = y + (x + z) := by grind
+@[simp, grind =] theorem Qp.quarter_add_threeQuarters : Qp.quarter + Qp.threeQuarters = 1 := by
+  grind
 
 theorem Qp.lt_iff_exists_add {a b : Qp} : a < b ↔ ∃ c : Qp, a + c = b := by
   refine ⟨fun h => ⟨⟨b.val - a.val, by have := Qp.lt_iff.mp h; grind⟩, Subtype.ext (by grind)⟩, ?_⟩

Iris/Iris/Algebra/Lib.lean

@@ -4,5 +4,6 @@ public import Iris.Algebra.Lib.DFracAgree
 public import Iris.Algebra.Lib.ExclAuth
 public import Iris.Algebra.Lib.FracAuth
 public import Iris.Algebra.Lib.MonoNat
+public import Iris.Algebra.Lib.MultiSetAuth
 public import Iris.Algebra.Lib.MonoZ
 public import Iris.Algebra.Lib.UFracAuth

Iris/Iris/Algebra/Lib/MultiSetAuth.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2026. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus de Medeiros
+-/
+module
+
+public import Iris.Algebra.Auth
+public import Iris.Algebra.LeibnizMultiSet
+meta import Iris.Std.RocqPorting
+
+@[expose] public section
+
+/-!
+# Authoritative multisets
+
+The authority owns a multiset and each fragment owns some of its elements: adding an element to
+the authority hands out the matching singleton fragment, and returning it removes the element.
+-/
+
+open Iris Std CMRA
+
+namespace LeibnizMultiSet
+
+variable {MS : Type _} [LawfulMultiSet MS A]
+
+@[rocq_alias heap_lang.auth_valid_gmultiset_singleton]
+theorem auth_valid_singleton {dq : DFrac} {v : A} {g : MS}
+    (h : ✓ ((●{dq} .ofSet g : Auth (LeibnizMultiSet MS)) • ◯ LeibnizMultiSet.ofSet {v})) : v ∈ g :=
+  singleton_subset_iff.mp (included_iff_subset.mp (Auth.both_dfrac_valid_discrete.mp h).2.1)
+
+theorem auth_alloc_singleton {v : A} {g : MS} :
+    (● .ofSet g : Auth (LeibnizMultiSet MS)) ~~>
+      (● LeibnizMultiSet.ofSet (g ⊎ {v})) • ◯ LeibnizMultiSet.ofSet {v} := by
+  refine Auth.auth_update_alloc ?_
+  have h := localUpdate_alloc (X := g) (Y := (∅ : MS)) (X' := {v})
+  rwa [disjUnion_empty_left] at h
+
+theorem auth_dealloc_singleton {v : A} {g : MS} :
+    ((● .ofSet g : Auth (LeibnizMultiSet MS)) • ◯ LeibnizMultiSet.ofSet {v}) ~~>
+      ● LeibnizMultiSet.ofSet (g \ {v}) := by
+  refine Auth.auth_update_dealloc ?_
+  have h := localUpdate_dealloc (X := g) (Y := ({v} : MS)) (X' := {v}) subset_refl
+  rwa [difference_self] at h
+
+end LeibnizMultiSet

Iris/Iris/BI/Lib/Fractional.lean

@@ -134,3 +134,55 @@ theorem fractional_divide_equal {Φ : Qp → PROP} [Fractional Φ] (q : Qp) (n :
   grind
 
 end Divide
+
+/-! ## Internal fractional
+
+`internalFractional Φ` internalises `Fractional Φ` into the logic, so that it can be kept in an
+invariant and transported along an internal `∗-∗`. -/
+
+section InternalFractional
+variable {PROP : Type _} [BI PROP] {Φ Ψ : Qp → PROP}
+
+@[rocq_alias internal_fractional]
+def internalFractional (Φ : Qp → PROP) : PROP := iprop(□ ∀ p q, Φ (p + q) ∗-∗ Φ p ∗ Φ q)
+
+@[rocq_alias internal_fractional_ne]
+instance internalFractional_ne : NonExpansive (internalFractional (PROP := PROP)) where
+  ne _ _ _ h := intuitionistically_ne.ne <|
+    forall_ne fun p => forall_ne fun q => wandIff_ne.ne (h _) (sep_ne.ne (h p) (h q))
+
+#rocq_ignore internal_fractional_proper "OFE equivalence is Lean equality; use `congrArg`."
+
+@[rocq_alias internal_fractional_affine]
+instance internalFractional_affine : Affine (internalFractional Φ) := by
+  unfold internalFractional; infer_instance
+
+@[rocq_alias internal_fractional_persistent]
+instance internalFractional_persistent : Persistent (internalFractional Φ) := by
+  unfold internalFractional; infer_instance
+
+@[rocq_alias fractional_internal_fractional]
+theorem fractional_internalFractional (h : Fractional Φ) : ⊢ internalFractional Φ := by
+  unfold internalFractional
+  iintro !> %p %q
+  iapply equiv_wandIff (h.fractional p q)
+
+@[rocq_alias internal_fractional_iff]
+theorem internalFractional_iff :
+    □ (∀ q, Φ q ∗-∗ Ψ q) ⊢ internalFractional Φ -∗ internalFractional Ψ := by
+  unfold internalFractional
+  iintro #Hiff #Hdup !> %p %q
+  isplit
+  · iintro HΨ
+    icases Hdup $$ %p %q (Hiff $$ %(p + q) HΨ) with ⟨H1, H2⟩
+    isplitl [H1]
+    · iapply Hiff $$ H1
+    · iapply Hiff $$ H2
+  · iintro ⟨H1, H2⟩
+    iapply Hiff
+    iapply Hdup
+    isplitl [H1]
+    · iapply Hiff $$ H1
+    · iapply Hiff $$ H2
+
+end InternalFractional

Iris/Iris/HeapLang/Lib.lean

@@ -9,6 +9,8 @@ public import Iris.HeapLang.Lib.Lock
 public import Iris.HeapLang.Lib.NondetBool
 public import Iris.HeapLang.Lib.Par
 public import Iris.HeapLang.Lib.Quicksort
+public import Iris.HeapLang.Lib.RwLock
+public import Iris.HeapLang.Lib.RwSpinLock
 public import Iris.HeapLang.Lib.Spawn
 public import Iris.HeapLang.Lib.SpinLock
 public import Iris.HeapLang.Lib.Unwrap

Iris/Iris/HeapLang/Lib/RwLock.lean

@@ -0,0 +1,98 @@
+/-
+Copyright (c) 2026. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus de Medeiros
+-/
+module
+
+public import Iris.BI.Lib.Fractional
+public import Iris.ProgramLogic.WeakestPre
+public import Iris.HeapLang.Notation
+public import Iris.HeapLang.Instances
+
+namespace Iris.HeapLang
+
+open BI OFE
+
+@[expose] public section
+
+/-- A general interface for a reader-writer lock. -/
+@[rocq_alias heap_lang.rwlock]
+structure RwLock (GF : BundledGFunctors) [IrisGS_gen hlc Exp GF] where
+  -- Operations
+  newlock : Val
+  acquireReader : Val
+  releaseReader : Val
+  acquireWriter : Val
+  releaseWriter : Val
+  -- Ghost state
+  rwlockG : BundledGFunctors → Type
+  name : Type
+  -- Predicates
+  isRwLock : rwlockG GF → name → Val → (Qp → IProp GF) → IProp GF
+  readerLocked : rwlockG GF → name → Qp → IProp GF
+  writerLocked : rwlockG GF → name → IProp GF
+  -- General properties of the predicates
+  isRwLock_persistent {L} γ lk Φ : Persistent (isRwLock L γ lk Φ)
+  isRwLock_iff {L} γ lk Φ Ψ : isRwLock L γ lk Φ ⊢ (▷ □ ∀ q, Φ q ∗-∗ Ψ q) -∗ isRwLock L γ lk Ψ
+  readerLocked_timeless {L} γ q : Timeless (readerLocked L γ q)
+  writerLocked_timeless {L} γ : Timeless (writerLocked L γ)
+  writerLocked_exclusive {L} γ : writerLocked L γ ∗ writerLocked L γ ⊢@{IProp GF} False
+  writerLocked_not_readerLocked {L} γ q :
+    writerLocked L γ ∗ readerLocked L γ q ⊢@{IProp GF} False
+  -- Program specs
+  newlock_spec {L} (Φ : Qp → IProp GF) {P ioΦ ioq} [AsFractional P ioΦ Φ ioq 1] :
+    {{ P }} hl(&newlock #()) {{ lk γ, RET lk; isRwLock L γ lk Φ }}
+  acquireReader_spec {L} γ lk Φ :
+    {{ isRwLock L γ lk Φ }} hl(&acquireReader &lk)
+    {{ q, RET hl_val(#()); readerLocked L γ q ∗ Φ q }}
+  releaseReader_spec {L} γ lk Φ q :
+    {{ isRwLock L γ lk Φ ∗ readerLocked L γ q ∗ Φ q }} hl(&releaseReader &lk)
+    {{ RET hl_val(#()); True }}
+  acquireWriter_spec {L} γ lk Φ :
+    {{ isRwLock L γ lk Φ }} hl(&acquireWriter &lk)
+    {{ RET hl_val(#()); writerLocked L γ ∗ Φ 1 }}
+  releaseWriter_spec {L} γ lk Φ :
+    {{ isRwLock L γ lk Φ ∗ writerLocked L γ ∗ Φ 1 }} hl(&releaseWriter &lk)
+    {{ RET hl_val(#()); True }}
+
+section lemmas
+
+variable [IrisGS_gen hlc Exp GF] (rw : RwLock GF) (L : rw.rwlockG GF)
+
+instance instPersistentIsRwLock γ lk Φ : Persistent (rw.isRwLock L γ lk Φ) :=
+  rw.isRwLock_persistent γ lk Φ
+
+instance instTimelessReaderLocked γ q : Timeless (rw.readerLocked L γ q) :=
+  rw.readerLocked_timeless γ q
+
+instance instTimelessWriterLocked γ : Timeless (rw.writerLocked L γ) :=
+  rw.writerLocked_timeless γ
+
+@[rocq_alias heap_lang.is_rw_lock_contractive]
+instance isRwLock_contractive γ lk : Contractive (rw.isRwLock L γ lk) := by
+  rw [contractive_internalEq (PROP := IProp GF)]
+  iintro %Φ₁ %Φ₂ #HEQ
+  ihave #HΦ : iprop(▷ ∀ q, Φ₁ q ≡ Φ₂ q) $$ [HEQ]
+  · iapply later_mono (discreteFun_equivI Φ₁ Φ₂).mp $$ [$]
+  iapply prop_ext
+  imodintro
+  isplit
+  · iintro #H
+    iapply rw.isRwLock_iff $$ H
+    iintro !> !> %q
+    irewrite [HΦ $$ %q]
+    · exact ⟨fun _ _ _ h => wandIff_ne.ne h .rfl⟩
+    · iapply equiv_wandIff; exact .rfl
+  · iintro #H
+    iapply rw.isRwLock_iff $$ H
+    iintro !> !> %q
+    irewrite [HΦ $$ %q]
+    · exact ⟨fun _ _ _ h => wandIff_ne.ne .rfl h⟩
+    · iapply equiv_wandIff; exact .rfl
+
+#rocq_ignore heap_lang.is_rw_lock_proper "OFE is Leibniz; use equality"
+
+end lemmas
+
+end