diff --git a/theories/bi/lib/fixpoint.v b/theories/bi/lib/fixpoint.v index 27dd09a3fd3a70de93b3ae4e2c7e55680356078f..975266f3f835835f35d8e8eaf9d9b5ce9288cdc8 100644 --- a/theories/bi/lib/fixpoint.v +++ b/theories/bi/lib/fixpoint.v @@ -26,6 +26,10 @@ Global Instance least_fixpoint_ne {PROP : bi} {A : ofeT} n : Proper (pointwise_relation (A → PROP) (pointwise_relation A (dist n)) ==> dist n ==> dist n) bi_least_fixpoint. Proof. solve_proper. Qed. +Global Instance least_fixpoint_proper {PROP : bi} {A : ofeT} : + Proper (pointwise_relation (A → PROP) (pointwise_relation A (≡)) ==> + (≡) ==> (≡)) bi_least_fixpoint. +Proof. solve_proper. Qed. Section least. Context {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}. @@ -85,6 +89,10 @@ Global Instance greatest_fixpoint_ne {PROP : bi} {A : ofeT} n : Proper (pointwise_relation (A → PROP) (pointwise_relation A (dist n)) ==> dist n ==> dist n) bi_greatest_fixpoint. Proof. solve_proper. Qed. +Global Instance greatest_fixpoint_proper {PROP : bi} {A : ofeT} : + Proper (pointwise_relation (A → PROP) (pointwise_relation A (≡)) ==> + (≡) ==> (≡)) bi_greatest_fixpoint. +Proof. solve_proper. Qed. Section greatest. Context {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.