From 599c70e12d0a570b8fb93955f1dae0c17c877d3a Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Thu, 5 Jan 2017 15:08:49 +0100 Subject: [PATCH] a little theory about limit preservation --- theories/algebra/ofe.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v index 33bd7151..d2dc52b7 100644 --- a/theories/algebra/ofe.v +++ b/theories/algebra/ofe.v @@ -959,6 +959,21 @@ Qed. Class LimitPreserving `{!Cofe A} (P : A → Prop) : Prop := limit_preserving : ∀ c : chain A, (∀ n, P (c n)) → P (compl c). +Section limit_preserving. + Context {A : ofeT} `{!Cofe A}. + (* These are not instances as they will never fire automatically... + but they can still be helpful in proving things to be limit preserving. *) + + Lemma limit_preserving_and (P1 P2 : A → Prop) : + LimitPreserving P1 → LimitPreserving P2 → + LimitPreserving (λ x, P1 x ∧ P2 x). + Proof. + intros Hlim1 Hlim2 c Hc. split. + - apply Hlim1, Hc. + - apply Hlim2, Hc. + Qed. +End limit_preserving. + Section sigma. Context {A : ofeT} {P : A → Prop}. -- 2.26.2