diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v index 62dda575a86a55b4a7cc7834643a2505e14b21b7..e74c5775832c4e0882af61d8f17a1c1263c89ad2 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,13 +301,25 @@ 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. 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_impl' (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).