From a52b29fcded59894a0f1b3d0bf319db7d9eb805d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 6 Jul 2022 16:35:10 -0400
Subject: [PATCH] general lemma that a fixpoint is Persistent

---
 iris/bi/lib/fixpoint.v | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/iris/bi/lib/fixpoint.v b/iris/bi/lib/fixpoint.v
index 7fc0a394a..604f0afc7 100644
--- a/iris/bi/lib/fixpoint.v
+++ b/iris/bi/lib/fixpoint.v
@@ -277,3 +277,25 @@ Section greatest_coind.
     - iApply (greatest_fixpoint_strong_mono with "[] Hgfp"); eauto.
   Qed.
 End greatest_coind.
+
+(** Establishing persistence of fixpoints. *)
+Section persistent.
+  Context {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
+  Context `{!BiAffine PROP}.
+
+  (** If [F] preserves persistence, then its fixpoint is persistent. *)
+  Lemma least_fixpoint_persistent :
+    (∀ Φ : A → PROP, (∀ a, Persistent (Φ a)) → (∀ a, Persistent (F Φ a))) →
+    ∀ a, Persistent (bi_least_fixpoint F a).
+  Proof using Type*.
+    intros Hpreserve. rewrite /Persistent.
+    iApply least_fixpoint_iter; first solve_proper.
+    iIntros "!# %y".
+    assert (Persistent (F (λ x : A, <pers> bi_least_fixpoint F x) y)%I).
+    { apply Hpreserve. apply _. }
+    iIntros "#HF !>".
+    iApply least_fixpoint_unfold.
+    iApply (bi_mono_pred with "[] HF"); first solve_proper.
+    iClear "#". iIntros "!# %x #HF". done.
+  Qed.
+End persistent.
-- 
GitLab