From d9498942f1fda09d863f600cb10e334d2ed68fea Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 21 Dec 2016 15:35:34 +0100
Subject: [PATCH] uPred entailment commutes over limits

---
 theories/algebra/ofe.v      | 2 +-
 theories/base_logic/upred.v | 8 ++++++++
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index cf0dff498..2d4d87dde 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -68,7 +68,7 @@ End ofe_mixin.
 
 Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption.
 
-(** Discrete COFEs and Timeless elements *)
+(** Discrete OFEs and Timeless elements *)
 (* TODO: On paper, We called these "discrete elements". I think that makes
    more sense. *)
 Class Timeless `{Equiv A, Dist A} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index cb12bf33d..5266c9ca1 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -172,5 +172,13 @@ Lemma entails_equiv_l (P Q R : uPred M) : (P ⊣⊢ Q) → (Q ⊢ R) → (P ⊢
 Proof. by intros ->. Qed.
 Lemma entails_equiv_r (P Q R : uPred M) : (P ⊢ Q) → (Q ⊣⊢ R) → (P ⊢ R).
 Proof. by intros ? <-. Qed.
+
+Lemma entails_lim (P Q : chain (uPredC M)) :
+  (∀ n, P n ⊢ Q n) → compl P ⊢ compl Q.
+Proof.
+  intros Hlim. split. intros n m Hval HP.
+  eapply uPred_holds_ne, Hlim, HP; eauto using conv_compl.
+Qed.
+
 End entails.
 End uPred.
-- 
GitLab