From f1d7773731c7db6a91ae9cbf466eb5264f30aa63 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 1 Mar 2017 20:14:54 +0100
Subject: [PATCH] add tactic for showing Iris assertions involving limits of
 chains

---
 theories/base_logic/upred.v | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 0ac232c72..45fdacf7e 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -186,5 +186,21 @@ Proof.
   eapply uPred_holds_ne, Hlim, HP; eauto using conv_compl.
 Qed.
 
+Lemma entails_lim' {T : ofeT} `{Cofe T} (P Q : T → uPredC M)
+      `{!NonExpansive P} `{!NonExpansive Q} (c : chain T) :
+  (∀ n, P (c n) ⊢ Q (c n)) → P (compl c) ⊢ Q (compl c).
+Proof.
+  set (cP := chain_map P c). set (cQ := chain_map Q c).
+  rewrite -!compl_chain_map=>HPQ. exact: entails_lim.
+Qed.
+
 End entails.
+
+Ltac entails_lim c :=
+  pattern (compl c);
+  match goal with
+  | |- (λ o, ?P ⊢ ?Q) ?x => change (((λ o, P) x) ⊢ (λ o, Q) x)
+  end;
+  apply entails_lim'.
+
 End uPred.
-- 
GitLab