From 8389920e79e2f7317af857849a8f1a9bd104dcb2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 12 Mar 2018 20:09:04 +0100
Subject: [PATCH] show that persistently and affinely-persistently are
 fixpoints of something

---
 theories/bi/derived_laws.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index b770e29ba..8da81d331 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -842,6 +842,14 @@ Proof.
   - by rewrite (affinely_elim_emp P) left_id affinely_elim.
 Qed.
 
+Lemma persistently_alt_fixpoint P :
+  <pers> P ⊣⊢ P ∗ <pers> P.
+Proof.
+  apply (anti_symm _).
+  - rewrite -persistently_and_sep_elim. apply and_intro; done.
+  - rewrite comm persistently_absorbing. done.
+Qed.
+
 Lemma persistently_wand P Q : <pers> (P -∗ Q) ⊢ <pers> P -∗ <pers> Q.
 Proof. apply wand_intro_r. by rewrite persistently_sep_2 wand_elim_l. Qed.
 
@@ -962,6 +970,17 @@ Proof.
   - apply impl_intro_l. by rewrite persistently_and_affinely_sep_l wand_elim_r.
 Qed.
 
+Lemma affinely_persistently_alt_fixpoint P :
+  □ P ⊣⊢ emp ∧ (P ∗ □ P).
+Proof.
+  apply (anti_symm (⊢)).
+  - apply and_intro; first exact: affinely_elim_emp.
+    rewrite {1}affinely_persistently_sep_dup. apply sep_mono; last done.
+    apply affinely_persistently_elim.
+  - apply and_mono; first done. rewrite {2}persistently_alt_fixpoint.
+    apply sep_mono; first done. apply and_elim_r.
+Qed.
+
 (* Conditional affinely modality *)
 Global Instance affinely_if_ne p : NonExpansive (@bi_affinely_if PROP p).
 Proof. solve_proper. Qed.
-- 
GitLab