From 5eb4474aaef2888f77df1ddd41308a13cc18f31d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 8 Aug 2023 14:16:00 +0200
Subject: [PATCH] make iApply greatest_fixpoint_paco work in more cases

---
 iris/bi/lib/fixpoint.v |  2 +-
 tests/fixpoint.ref     |  0
 tests/fixpoint.v       | 27 +++++++++++++++++++++++++++
 3 files changed, 28 insertions(+), 1 deletion(-)
 create mode 100644 tests/fixpoint.ref
 create mode 100644 tests/fixpoint.v

diff --git a/iris/bi/lib/fixpoint.v b/iris/bi/lib/fixpoint.v
index 300a46074..e4bae919c 100644
--- a/iris/bi/lib/fixpoint.v
+++ b/iris/bi/lib/fixpoint.v
@@ -312,7 +312,7 @@ Section greatest_coind.
   Qed.
   Local Existing Instance paco_mono.
 
-  Lemma greatest_fixpoint_paco `{!NonExpansive Φ} :
+  Lemma greatest_fixpoint_paco (Φ : A → PROP) `{!NonExpansive Φ} :
     □ (∀ y, Φ y -∗ F (bi_greatest_fixpoint (λ Ψ a, Φ a ∨ F Ψ a)) y) -∗
     ∀ x, Φ x -∗ bi_greatest_fixpoint F x.
   Proof using Type*.
diff --git a/tests/fixpoint.ref b/tests/fixpoint.ref
new file mode 100644
index 000000000..e69de29bb
diff --git a/tests/fixpoint.v b/tests/fixpoint.v
new file mode 100644
index 000000000..d29352023
--- /dev/null
+++ b/tests/fixpoint.v
@@ -0,0 +1,27 @@
+From iris.bi Require Import lib.fixpoint.
+From iris.proofmode Require Import proofmode.
+From iris.prelude Require Import options.
+
+Section fixpoint.
+  Context {PROP : bi} `{!BiInternalEq PROP}
+    {A : ofe} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
+
+  Definition L := bi_least_fixpoint F.
+  Definition G := bi_greatest_fixpoint F.
+
+  (* Make sure the lemmas apply without having to repeat the induction predicate [Φ]. *)
+  Lemma ind_test (a : A) :
+    ∀ x, L x -∗ x ≡ a.
+  Proof.
+    iApply (least_fixpoint_ind F); first by solve_proper. Undo.
+    iApply (least_fixpoint_ind_wf F); first by solve_proper. Undo.
+  Abort.
+
+  Lemma coind_test (a : A) :
+    ∀ x, x ≡ a -∗ G x.
+  Proof.
+    iApply (greatest_fixpoint_coind F); first by solve_proper. Undo.
+    iApply (greatest_fixpoint_paco F); first by solve_proper. Undo.
+  Abort.
+
+End fixpoint.
-- 
GitLab