From 3f66477c9efa4ea733ed30d82c1f587c39fdbbc7 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Thu, 7 Mar 2019 20:07:50 +0100 Subject: [PATCH] Propers for fixpoints. --- theories/bi/lib/fixpoint.v | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/theories/bi/lib/fixpoint.v b/theories/bi/lib/fixpoint.v index 27dd09a3..975266f3 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}. -- GitLab