From 3bc2d2a3d13bf2a6ad5b346901a4e525a3871ef1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 11 Aug 2023 15:35:01 +0200
Subject: [PATCH] fix a lemma being accidentally about the wrong fixpoint...

---
 CHANGELOG.md           | 1 +
 iris/bi/lib/fixpoint.v | 6 +++---
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9dfd0a3f2..af9fec978 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -112,6 +112,7 @@ Coq 8.13 is no longer supported.
 * Provide smart constructor `bi_persistently_mixin_discrete` for
   `BiPersistentlyMixin`: Given a discrete BI that enjoys the existential
   property, a trivial definition of the persistence modality can be given.
+* Fix `greatest_fixpoint_ne'` accidentally being about the least fixpoint.
 
 **Changes in `proofmode`:**
 
diff --git a/iris/bi/lib/fixpoint.v b/iris/bi/lib/fixpoint.v
index 300a46074..f474c5ffb 100644
--- a/iris/bi/lib/fixpoint.v
+++ b/iris/bi/lib/fixpoint.v
@@ -27,7 +27,7 @@ Global Arguments bi_greatest_fixpoint : simpl never.
 
 (* Both non-expansiveness lemmas do not seem to be interderivable.
   FIXME: is there some lemma that subsumes both? *)
-Lemma least_fixpoint_ne' {PROP : bi} {A : ofe} (F: (A → PROP) → (A → PROP)):
+Lemma least_fixpoint_ne' {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP)):
   (∀ Φ, NonExpansive Φ → NonExpansive (F Φ)) → NonExpansive (bi_least_fixpoint F).
 Proof. solve_proper. Qed.
 Global Instance least_fixpoint_ne {PROP : bi} {A : ofe} n :
@@ -193,8 +193,8 @@ Qed.
 
 (* Both non-expansiveness lemmas do not seem to be interderivable.
   FIXME: is there some lemma that subsumes both? *)
-Lemma greatest_fixpoint_ne' {PROP : bi} {A : ofe} (F: (A → PROP) → (A → PROP)):
-  (∀ Φ, NonExpansive Φ → NonExpansive (F Φ)) → NonExpansive (bi_least_fixpoint F).
+Lemma greatest_fixpoint_ne' {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP)):
+  (∀ Φ, NonExpansive Φ → NonExpansive (F Φ)) → NonExpansive (bi_greatest_fixpoint F).
 Proof. solve_proper. Qed.
 Global Instance greatest_fixpoint_ne {PROP : bi} {A : ofe} n :
   Proper (pointwise_relation (A → PROP) (pointwise_relation A (dist n)) ==>
-- 
GitLab