From 26de02a9a351f1d7a9652096632628566c59f252 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 11 Aug 2022 13:37:14 -0400
Subject: [PATCH 1/3] add limit_preserving_iff

---
 iris/algebra/ofe.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 62dda575a..1fc18c69f 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -307,6 +307,16 @@ Section limit_preserving.
     eapply Hlim1, HP1. apply dist_le with n; last lia. apply (conv_compl n).
   Qed.
 
+  (** This is strictly weaker than the [_impl] variant, but sometimes automation
+      is better at proving [Proper] for [iff] than for [impl]. *)
+  Lemma limit_preserving_iff (P1 P2 : A → Prop) :
+    Proper (dist 0 ==> iff) P1 → LimitPreserving P2 →
+    LimitPreserving (λ x, P1 x → P2 x).
+  Proof.
+    intros HP1. apply limit_preserving_impl. intros ???.
+    apply iff_impl_subrelation. eapply HP1. done.
+  Qed.
+
   Lemma limit_preserving_forall {B} (P : B → A → Prop) :
     (∀ y, LimitPreserving (P y)) →
     LimitPreserving (λ x, ∀ y, P y x).
-- 
GitLab


From dbfcb32fb2baa940eb50593af2d3a3ed85515391 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 11 Aug 2022 14:09:09 -0400
Subject: [PATCH 2/3] less confusing line breaks

---
 iris/algebra/ofe.v | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 1fc18c69f..1b61b0be8 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -290,7 +290,8 @@ Section limit_preserving.
   Proof. intros PH c Hc. by rewrite (conv_compl 0). Qed.
 
   Lemma limit_preserving_and (P1 P2 : A → Prop) :
-    LimitPreserving P1 → LimitPreserving P2 →
+    LimitPreserving P1 →
+    LimitPreserving P2 →
     LimitPreserving (λ x, P1 x ∧ P2 x).
   Proof.
     intros Hlim1 Hlim2 c Hc.
@@ -300,7 +301,8 @@ Section limit_preserving.
   Qed.
 
   Lemma limit_preserving_impl (P1 P2 : A → Prop) :
-    Proper (dist 0 ==> impl) P1 → LimitPreserving P2 →
+    Proper (dist 0 ==> impl) P1 →
+    LimitPreserving P2 →
     LimitPreserving (λ x, P1 x → P2 x).
   Proof.
     intros Hlim1 Hlim2 c Hc HP1. apply Hlim2=> n; apply Hc.
@@ -310,7 +312,8 @@ Section limit_preserving.
   (** This is strictly weaker than the [_impl] variant, but sometimes automation
       is better at proving [Proper] for [iff] than for [impl]. *)
   Lemma limit_preserving_iff (P1 P2 : A → Prop) :
-    Proper (dist 0 ==> iff) P1 → LimitPreserving P2 →
+    Proper (dist 0 ==> iff) P1 →
+    LimitPreserving P2 →
     LimitPreserving (λ x, P1 x → P2 x).
   Proof.
     intros HP1. apply limit_preserving_impl. intros ???.
-- 
GitLab


From 8d4ba814bd97a865c5722563846b312eb447ff4c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 12 Aug 2022 08:29:15 -0400
Subject: [PATCH 3/3] better naming

---
 iris/algebra/ofe.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 1b61b0be8..e74c57758 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -311,7 +311,7 @@ Section limit_preserving.
 
   (** This is strictly weaker than the [_impl] variant, but sometimes automation
       is better at proving [Proper] for [iff] than for [impl]. *)
-  Lemma limit_preserving_iff (P1 P2 : A → Prop) :
+  Lemma limit_preserving_impl' (P1 P2 : A → Prop) :
     Proper (dist 0 ==> iff) P1 →
     LimitPreserving P2 →
     LimitPreserving (λ x, P1 x → P2 x).
-- 
GitLab